Excessive explanation, part five

Today, what's the type of map given the types of its parts?

 The type checker will deduce a type-scheme for map from existing type-schemes for null, nil, cons, hd and tl; the term type-scheme is appropriate since all these objects are polymorphic. In fact fromnull : aI (I list a' bool)nil : aI (I list)cons : aI (I a' (I list a' I list))hd : aI (I list a' I)tl : aI (I list a' I list)will be deducedmap : aI aI^2 ((I a' I^2) a' (I list a' I^2 list)).

One of the difficulties in reading papers like this for people who don't already have an academic background is that so much notation is used before it is defined, or simply assumed. So let's unpack this.

First off, polymorphic types ("generics" in C# parlance) are notated as I list. That is, the type argument comes first, followed by the type being parameterized. This has always struck me as weird! You can think of a generic type as a kind of function that takes in type arguments and produces types. In ML we notate a function that takes in an argument and produces a value by putting the argument to the right of the function. But a generic type has its argument to the left. I've asked a number of ML experts why this is, and they usually say something about how it is "more natural" to say "string list", but this is question-begging; it is only "more natural" because that's what you're used to seeing! VB solves the problem with "List of String", which seems far more "natural" to me than "string list".

Anyways, long story short, for polymorphic types in ML, the type argument comes to the left of the polymorphic type.

So what is this?

null : aI (I list a' bool)

This is saying that null is a generic function; its type scheme is to the right of the colon. The upside-down A is the universal quantifier, and is read "for all" or "for any". The arrow means that this is a function that takes a thing of the left type and produces a thing of the right type.

So: null has the type scheme: for any type alpha, there is a function called null that takes a list of alpha and produces a bool. In C# we'd say something like

static bool IsEmpty<T>(List<T> items)

What about

nil : aI (I list)

This thing has no arrow so it isn't even a function. ML allows polymorphic values; this is saying that there exists an empty list of any element type, and it is called nil.

The head and tail functions should be straightforward; they take a list of alphas and produce either an alpha, (the head) or a list of alphas (the tail).

But what is up with cons? It should take two arguments; an item of type alpha and a list of alphas. And it should produce a list of alphas. Its scheme is:

cons : aI (I a' (I list a' I list))

What is up with this? It looks like it is saying that cons takes an alpha and produces a function. That function in turn takes a list of alphas and produces a list of alphas.

And indeed that is what it does. When you say

let append_hello = cons "hello"

then append_hello is a function that takes a list of strings and returns a list with "hello" appended to it. So

let x = cons "hello" mylist

is the same as

let append_hello = cons "hello"let x = append_hello mylist

Functions always take one argument; a function of two arguments actually is a function of one argument that returns another function.

So what do we want to deduce as the type scheme for map?

map : aI aI^2 ((I a' I^2) a' (I list a' I^2 list))

The first argument to map must be a function from any type alpha to any type beta. That gives us back a function that takes a list of alphas and returns the list of betas which is the result of applying the given function to each alpha in the list. Somehow the type assignment algorithm needs to deduce this type scheme, given the schemes for all the functions called by the implementation.

Next time: we'll go through the deductive steps needed to figure out the type of map.