Automatic Annotations: Inferring Function Types


Automatic annotations logo

Previously, we covered why automatic annotations are useful, and some basics underlying the infrastructure to perform automatic annotations.

In this post we’ll see how function types are inferred, as well as simple map types.

This work is part of a crowdfunding effort, please support the campaign here!

Inferring Functions

Automatic annotations for Typed Clojure only work if you provide tests. Let’s suppose we have the following point function with two unit tests.

Definition of point with tests

As in the previous post, to track the value of a def you track its initial value.

Tracking a function definition

Now we have an interesting problem: how do we track functions? We need to learn two things about functions, namely its inputs and output. By wrapping the original function, we can track each of these subcomponents.

Tracking a function invocation

Since this waits for the function to be called, we need tests to exercise the function. This is the intuition behind Write Tests, Get Types!.

Let’s track point.

Further tracking of function

Notice we have added two new path elements corresponding to the input and output of functions. We can combine these to make arbitrarily deep paths, and encode statements like the first parameter’s second parameter of var foo-bar is of type Long.

Let’s step through the evaluation of (point 1 2). First, the wrapped function is called and we are left with a call to the original function.

Further tracking of function

We then evaluate the first argument to point, which tracks 1.

Further tracking of function

After this reduction, we infer the first argument to be of type Long. We then do the same for the second argument.

Further tracking of function

Now we have evaluated the arguments, we invoke the actual point function.

Further tracking of function

It returns a map; to track a map, we need a new kind of path element, key path elements, to track map entries. We push the track inside the map’s values, using key path elements.

Further tracking of function

Notice the richness of the paths here: 1 is point’s range’s :x entry. Reducing the first argument fills in part of the return type.

Further tracking of function

The final reduction completes the type of point.

Further tracking of function

Great, we have a type, but there is a mystery step we have skipped: how we get from inference results like [point (:dom 0)] : Long and [point (:dom 1)] : Long to final var types like point : [Long Long -> '{:x Long :y :Long}].

This is handled by converting inference results to types, then combining then with join. For example, the type for point after inferring its arguments is

join([Long ? -> ?], [? Long -> ?]) = [Long Long -> ?]

Each new inference result is joined in this way, so inferring the function return type is similar.

Inferring Functions via Tests

The basic approach of inferring types for functions is to wrap them and inspect their behaviour when invoked. The parameters and return types are incrementally inferred, and combined with the join metafunction.

In the next post, we talk about inferring types for possibly-infinite sequences and vectors.

This work is part of a crowdfunding effort, please support the campaign here!

15 Aug 2016