Typed Clojure

A digression

I’m going to go off on a tangent for a bit and look at core.typed. This is more of a brain dump, so that I can refer to this material later. Before reading this post, you should read the rationale and the introduction/motivation for the core.typed project. I’ve barely begun looking at core.typed but I can already see that Ambrose has done some incredible things. I’m looking forward to where this project is going to go.

Taking it from the top

Static typing is all about having the compiler check your code for correctness at compile time rather than waiting until runtime. It’s a complement to unit testing, not a replacement. Amanda Laucher and Paul Snively gave a great talk at Strangeloop about this. I recommend you watch it.

In the end, types are all about telling the compiler what kind of values each symbol in your program can be set to. core.typed is really a language that gives you the tools to do this. To get up to speed with core.typed, you need to understand the principles of types, the syntax of core.typed and the infrastructure surrounding type checking.

First off, you type check a namespace with the check-ns function. check-ns reads the namespace from the file, so to start experimenting with core.typed, first create one like this:

(ns typed
  (:require [clojure.core.typed :as t]))

save that and start a repl, then call check-ns.

(require '[clojure.core.typed :as t])
=> nil

(t/check-ns 'typed)
=> nil

Since check-ns loads the namespace, you can now switch to that namespace which makes it more convenient to work with from the repl.

(in-ns 'typed)
=> #<Namespace typed>

To tell core.typed what the type of a var is, you write an annotation using ann, so add the following to the file and save it

(t/ann x Long)
(def x 10)

Running check-ns gives the following:

(t/check-ns)
=> "Checking line:" 4
=> "Checking line:" 5

This tells you that the expressions on those lines have been properly type checked.

Now add the following and check it:

(t/ann y Integer)
(def y 10)

You should see the following error:

Type Error, typed:8

Actual type
        java.lang.Long
is not a subtype of Expected type
        java.lang.Integer

Clojure defaults all integers to Long, not Integer. But the type annotation says y must be an Integer, so the checking blows up. Changing the annotation to:

(t/ann y Number)

This works because Long is a subtype of Number, so anywhere a Number should appear, a Long will work just fine and correctly type check. Now add the following:

(t/ann z Long)
(def z 10)
(def z "10")

This will blow up because z must be a Long and you try to set it to a String value. But if you change it to:

(t/ann z String)

It will also blow up because z must be a String and you try to set it to a Long value. If you instead say:

(t/ann z Any)

Everything checks because Any is the supertype for all other types. But suppose you wanted z to only be a String or a Long but no other types. Then you can declare it to be a union type of Long or String like this:

(t/ann z (t/U Long String))

and you’ve just entered the world of type expressions. You can think of U as a type function that takes an optional number of types and generates a new type which can be any of the given types. So now, if you add:

(def z :z)

you get another error saying that “(Value :z)” is not a subtype of the expected type. Changing the annotation to read:

(t/ann z (t/U Long String (Value :z))

adds a new type to the union. Value is another type function that takes any Clojure value and creates a new type that has that value as the only one for that type. So if you now add

(def z :a)

it fails to check. I hope by now that you’re starting to get a hint of the possibilities and power of core.typed. The basic types are just the various boxed java types. String is shorthand for java.lang.String, etc. There are also a couple of shorthand types for nil, true and false. Also, java primitive types are subtypes of their respective boxed types, so int is a subtype of java.lang.Integer.

More power (and complexity)

So those are the basics of specifying types for simple values. The next logical step is to specify types for functions. Before we define types for our own fn’s, it would be helpful to look at some function types that are already in clojure.core. Not every fn in core has been typed, but many have. It’s possible find out the type of a var at the REPL using the cf macro in core.typed like so:

(t/cf inc)
=> (Fn [clojure.core.typed/AnyInteger -> clojure.core.typed/AnyInteger]
       [java.lang.Number -> java.lang.Number])

This tells us that inc is a fn that either takes AnyInteger and returns AnyInteger or takes a Number and returns a Number. From that we can see that fn’s can be typed using a type function named Fn which takes multiple type expressions. The [parameters -> result] form tells us that a fn takes a number of parameters and transforms them into a value of a result type. In the simplest, and most common, cases we can leave off the Fn and enclosing parenthesis and just use a vector expression.

(t/ann f [Integer -> Integer])
(defn f [x] (int (inc x)))

The interesting thing here, is that we have to cast the result of (inc x) to an int because inc is typed as returning AnyInteger, which is not compatible with Integer. (I’m not sure why, yet.) You can specify the types of multiple parameters on the left side of the ->:

(t/ann g [Integer Integer -> Integer])
(defn g [x y] (int (+ x y)))

If the function can take variable number of args, you can add a * right before the ->, which means the type just before the * is used for all the remaining parameters. Which leads to something interesting. If you do this:

(t/ann h [Integer Integer * -> Integer])
(defn h [x & [y]] (int (inc + x y)))

It won’t type check because it’s possible for y to be nil which would violate the type for +. This is one of the great things about static types. No more NPE’s! (Or at least greatly reduced.) For that alone, core.typed is worth the effort to learn and use.

Stay tuned

And with that, I’ll end day one of my exploration of core.typed. Stay tuned for more.

Jim Duey 14 March 2013
blog comments powered by Disqus