Using polymorphic higher-order functions

When it comes to annotating functions in core.typed, there are some special rules to keep in mind. Here are two.

  1. all function parameters should be annotated
  2. polymorphic functions should be instantiated when used as a parameters to polymorphic higher-order functions.

Annotating function parameters

There are several ways for function argument annotations to propagate downwards.

To annotate a full function type, use ann-form.

(cf (ann-form (fn [a] (inc a)) [Number -> Number]))
;=> [Number -> Number]

cf takes a second argument which expands into ann-form.

(cf (fn [a] (inc a)) [Number -> Number])
;=> [Number -> Number]

fn supports partial and full annotations.

(cf (fn [a :- Number] (inc a)))
;=> [Number -> Number]

Polymorphic higher-order functions

A keyword can be used as a function.

(cf (:foo {:foo 1}))
;=> (Value 1)

The first argument to the polymorphic function map is often, itself, polymorphic. This thwarts the local type inference algorithm. Passing monomorphic arguments works fine.

(cf (map + [1 2 3]))
;=> (clojure.lang.LazySeq AnyInteger)

(See AnyInteger).

However if we map over a polymorphic function — say, a keyword — we must provide a more specific type via instantiation.

(cf (map (inst :foo Number) [{:foo 1} {:foo 2}]))
;=> (clojure.lang.LazySeq Number)

inst takes a polymorphic expression and a number of types, and has a return type that replaces the bound type variables in the polymorphic type with the types provided. A call to inst returns the first argument at runtime.

(cf (inst :foo Number))
;=> [(HMap :mandatory {:foo Number}) -> Number]

(See Heterogeneous Maps for further discussion on heterogeneous map types)

I often introduce a local binding, or even a top-level definition that is just an instantiated type. This can get your type annotations out of the way and get back some of the readability of just using a plain keyword.

  (let [get-foo (inst :foo Number)]
    (map get-foo [{:foo 1} {:foo 2}])))
;=> (clojure.lang.LazySeq Number)

Why is this necessary?

core.typed and Typed Racket use Local Type Inference (PDF) (Pierce and Turner) to infer applications of polymorphic arguments.

It turns out we can infer direct applications of polymorphic types fairly easily, but higher-order polymorphic types are more difficult to infer when passed other polymorphic types. Hosoya and Pierce describe exactly what “plain” local type inference is capable of.

The developers of core.typed and Typed Racket are both keen to develop more powerful local inference, but it probably will require a non-trivial amount of effort. Scala’s Colored Local Type Inference (Odersky, Zenger, Zenger and Lausanne) is the kind of extension to local type inference type we’re jealous of.

Furthermore, Typed Clojure and Typed Racket already include extensions of its own to support Practical Variable-arity Polymorphism (PDF) (Strickland, Tobin-Hochstadt and Felleisen), which helps us type check polymorphic functions with non-trivial variable-parameters like map.

See also

03 Sep 2013