Core.typed adds an optional type system to dynamically typed Clojure. It aims to combine the best of both worlds: the brevity and flexibility of Clojure and the safety guarantees that a type-checker provides. Because the type system is optional, it can be used gradually where it provides the highest value. From the core.typed user guide:
Types, when coupled with an appropriate doc-string, are excellent machine checkable documentation. They never go out of date, and are often invaluable as a quick reminder of what a function does.
Types are useful when a program grows, especially when there are multiple contributors. If a contribution passes the type system, we know that it is type correct (type errors are amongst the most common user errors in programming).
Core.typed automatically figures out many of the types for you using type-inference, explicit type annotations are needed for vars, function parameters and some macros, and you can also annotate protocols and datatypes. For example, an annotation for a function that adds two numbers looks like this:
(ann add [Number Number -> Number]) (defn add [a b] (+ a b))
Because the type declarations are separate from the implementations, it's easy to add type annotations to third party code, like it's done here with clojure.core.
The author of core.typed, Ambrose Bonnaire-Sergeant, says that the current version 0.2 is production ready, meaning that it "can find bugs in real code and will not slow down your existing code". The API should also be stable now.
InfoQ talked to Ambrose to learn how he started with core.typed:
The project started as my Undergraduate Honours project for my Bachelor of Computer Science at the University of Western Australia. I was inspired Sam Tobin-Hochstadt's Typed Racket, which is the source of most of the theory and implementation behind Typed Clojure [editor's note: Typed Clojure is the former name of core.typed].
InfoQ: Regarding verification, there are a lot of unit tests in core.typed. Did you also formally verify your type checker? (I assume core.typed uses core.typed?)
I believe any project will benefit from a combination of verification techniques. core.typed is mainly verified using unit tests, but I have also started type checking the implementation.
The type checker has a broad applicability, it can even statically verify properties about the usage of other verification techniques. For example, if core.typed and Prismatic's Schema learn about each other, core.typed can check if your runtime tests with Schema are sufficient to avoid a type error.
Some of the more interesting properties Typed Clojure can check at compile time include the absence of Null Pointer Exceptions, the correctness of Java interop and the correct usage of immutable bindings.
Type checking a body of code with good test coverage isn't necessarily going to find bugs, but I find the process of converting untyped code to typed to be similar to a code review. The type system is a good gauge of how complex your code: if your types are large and messy, perhaps there's an opportunity for refactoring. Messy types often mean messy logic.
InfoQ: To a Scala programmer, some type names might look familiar. Scala has local type inference too, did Scala have any influence on core.typed?
Sure, there was some influence. Typed Clojure interfaces well with Java code and it was useful to compare how Scala deals with some of the quirks of Java's type system like array covariance and null pointers.
There's also a little jealousy of Scala: Odersky's Colored Local Type Inference is a nice extension of Local Type Inference that allows Scala programmer to omit certain annotations. Typed Clojure and Typed Racket extend Local Type Inference in other ways, but we have always had our eye on extensions like Colored Local Type Inference to make certain annotations unnecessary.
InfoQ: How was the feedback from the Clojure community?
I've been very pleased by the response. I think it shows that Clojure programmers have been eagerly wait for a powerful, completely optional type system at their disposal when building Clojure programs.
InfoQ: What are your plans for the next version?
I have enumerated my immediate plans as part of the crowdfunding campaign for full time Typed Clojure development.
My favourite upcoming changes include supporting Clojurescript as a type checking target, generating runtime contracts based on static types, targetting a self-hosted Clojure compiler and pushing the boundaries of what Typed Clojure is capable of.
For further information on core.typed, visit the project website, or take a look at this workshop recording. If you like core.typed, don't forget to support Ambrose's crowd funding campaing.