Using Polymorphic Higher-order Functions

02 Sep 2013

core.typed has some special rules for annotating functions.

The two basic rules are:

  • all function parameters should be annotated
  • 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 common pattern is to map a keyword over a list of maps.

First, let's demonstrate how a keyword can be used as a function.

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

map is polymorphic and often is passed a polymorphic function as the first argument.

We can use an unparameterised function without instantiation with map.

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

(See AnyInteger).

A polymorphic higher order function passed to map should be manually instantiated, otherwise core.typed might lose accuracy or throw a type error.

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

inst takes a value of polymorphic type and a number of types, and returns the value instantiated with the types. At runtime, a call to inst merely returns the first argument.

(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.

(cf
  (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