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 from

null : ∀α (α list → bool)
nil  : ∀α (α list)
cons : ∀α (α → (α list → α list))
hd   : ∀α (α list → α)
tl   : ∀α (α list → α list)

will be deduced

map  : ∀α ∀β ((α → β) → (α list → β 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 α 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 : ∀α (α list → 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  : ∀α (α 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 : ∀α (α → (α list → α 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  : ∀α ∀β ((α → β) → (α list → β 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.

Advertisements

6 thoughts on “Excessive explanation, part five

    • Yeah, I’ve made that mistake since I was a child. I know the mnemonics: that you would never say hi’s instead of his to indicate a possessive, and so you would not for “its” or “hers” or “ones” either. Knowing the mnemonics does not help when the keystrokes happen with no connection between brain and fingertips. 🙂

      • I’ve historically always gotten caught up with its and it’s myself too until a few years ago when I had one helpful person claim it was easy since we _already_ had the apostrophe rule for contractions, we couldn’t also use the apostrophe with possessive pronouns. I found the idea that we already had one rule but not the other ridiculous, but it stuck with me all the same.

  1. “∀α” serves pretty much the purpose of “template” in C++: it binds the type parameter, so it’s taken to be a fresh one and not related to any type parameter in the context.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s