Ambrose Bonnaire-Sergeant

There are also tentative plans to integrate core.typed with the Clojure compiler so type annotations can be used during compilation (e.g., type hints through inference). There was a post about it, but the best I could find is a recent paper: http://frenchy64.github.io/papers/typed-clojure-draft.pdf

Speaking speculatively, improving type inference is a great place for collaboration. Concretely, I've extended several minor ideas. Typed Clojure uses occurrence typing in sequential forms, as well as conditionals: http://frenchy64.github.io/2013/09/08/simple-reasoning-assertions-core… We can type check (filter identity coll) a little more accurately (which is actually quite hard to do): https://github.com/clojure/core.typed/blob/master/src/main/clojure/clo… The type system's interaction with Java's type system is interesting, which is something I've fleshed out. I have heterogeneous maps as well as heterogeneous vectors, and support complex operations like merge. Unsure if relevant to Racket. There are lots of other ideas which I need to implement to type check Clojure, but aren't necessarily crucial to type checking Racket, but would be nice to have.

Unsound things can be useful. https://frenchy64.github.io/2018/04/09/unsoundness-reply.html

I believe that's where core.typed is going: http://frenchy64.github.io/2015/06/19/gradual-typing.html Typed and untyped code must (and will soon) be able to cooperate in providing compile-time and run-time type checking in Clojure.

Clojure also takes this approach with core.typed as well https://frenchy64.github.io/2015/06/19/gradual-typing.html I personally haven't found a place where this is necessary yet, but who knows what might happen in the future. :)

Interestingly, if you read the article [0] linked in the reddit post referred to in this blog post, the author points out that the Haskell version of the bottom type has a problem - you can construct an inhabitant. Pulling out the relevant section of code: fix :: (a -> a) -> a -- defined in Data.Function fix f = let x = f x in x -- least fixed point of f false :: Void false = fix (id :: Void -> Void) Since you can find an inhabitant of Void, you can therefore create an inhabitant of any type, so you can prove any proposition: inhabitant :: a inhabitant = fix id I don't know if this is only really a problem if you were trying to use Haskell as a theorem prover. It might be the case that in practice, you're unlikely to run into this inconsistency. I think [1] provides a bit more discussion regarding this. [0]: https://gciruelos.com/propositions-as-types.html [1]: https://frenchy64.github.io/2018/04/07/unsoundness-in-untyped-types.ht… EDIT: Just found this [2] which describes the above problem in type theory language. [2]: https://en.wikipedia.org/wiki/System_U#Girard's_paradox