Typed Clojure is a gradual type system for Clojure and ClojureScript. In practice, type checking resembles “linting”: it is separate from compilation and must be called explicitly.
This has some interesting implications.
Instead of porting your old code to a “typed” variant of your language, you can gradually add type annotations and run the type checking function when needed; the checker will never stop your code from compiling normally.
However, we lose some of the more useful features most type systems enjoy, including the ability to transform code. This forces simpler optimisations that can be applied to any code.
By separating the type checker from the compiler, we also avoid infecting the rest of the language with the massive complexities of a static type system. Our compiler is simple and robust, our language design is unrestricted by an arbitrary type system, and our users are free to choose the right type system for the job.
We explore this idea further and demonstrate what such a type system is like to use.