Excessive explanation, part six

Continuing with the question of how to deduce the “type scheme” of

letrec map f s = if null s then nil
                 else cons(f(hd s)) (map f (tl s))

Knowing the type schemes of null, nil, and so on.

Let’s reason informally, just using ordinary logic rather than not some formal system. You’d probably reason something like this:

  • I know that map takes two arguments, f and s, from its declaration.
  • Functions of two arguments in ML are actually functions that take one argument and return another function. Therefore I know that map has to take something of f’s type, and return a function.
  • The returned function must take something of s’s type
  • The returned function must return something of a list type, because there’s a “nil” on one half of the “if” and a “cons” with two arguments on the other. (Obviously “if” in ML is ?: in C#.)
  • I know that s must be some kind of list, because it is passed to null.
  • and so on; can you fill in the rest?

Of course, the whole point of this paper is to develop a formal algorithm for making these sorts of deductions. Which we’ll get to at some point, I’m sure!

Moving on; we’ve been using the phrase “type” and “type scheme” without defining either!

Types are built from type constants (bool, ...) and type variables 
(α, β, ...) using type operators (such as infixed → for functions and
postfixed list for lists); a type-scheme is a type with (possibly)
quantification of type variables at the outermost.

Here we’re just making a bit more formal what we mean by a type.

  • We have a bunch of “built in” types like bool and int and string; they are types by fiat.
  • We have generic type parameters (called here “type variables” though of course they are not variables in the sense of “storage of a value”).
  • And we have operators that act on types; “list” can be thought of as a postfix operator on a type that produces a new type, and the arrow can be thought of as an infix operator that takes two types and produces a function type.
  • “Quantification” is a use of the “for all” operator that introduces a type variable.
  • “Outermost” means that the type variables are introduced as far to the left as possible.

Thus, the main result of this paper is that the type-scheme deduced for
such a declaration (and more generally, for any ML expression) is a 
principal type-scheme, i.e. that any other type-scheme for the 
declaration is a generic instance of it. This is a generalisation of 
Hindley’s result for Combinatory Logic [3].

We’re re-stating the goal of the paper: that the algorithm presented here should find not just a correct type scheme, but the most general possible type scheme. By “generic instance” we mean of course that “string list” is a more specific instance of a scheme like “for any alpha, alpha list”.

Combinatory logic is the study of “combinators” — functions that take functions and return functions. You’re probably heard that this kind of type inference is called “Hindley-Milner” inference, and now you know why.

ML may be contrasted with Algol 68, in which there is no polymorphism, 
and with Russell [2], in which parametric types appear explicitly as 
arguments to polymorphic functions. The generic types of Ada may be 
compared with type-schemes. 

Nothing particularly interesting here; we’re just calling out that ML’s polymorphic type system is just one approach and that you might want to compare it to languages that try other approaches.

For simplicity, our definitions and results here are formulated for a 
skeletal language, since their extension to ML is a routine matter. 
For example recursion is omitted since it can be introduced by simply
adding the polymorphic fixed-point operator

fix  : ∀α ((α → α) → α)

What we’re saying here is that we can present an algorithm for a very simple language, show that it is correct, and then easily extend that algorithm to a more complex language.

Now, you might think that surely it must be difficult to write an algorithm that produces a type for recursive methods like map; there seems to be a regression problem here, where we cannot infer types of a method that calls itself, because we’d need to know the type of the called method in order to work out the calling method, but they are the same method, so, hmm, how do to that?

Fortunately it turns out that you can always transform a recursive method into a non-recursive method, and then apply the type inference to the non-recursive version to deduce the type of the recursive version. We do this by using a fixed-point operator. Therefore the algorithm that will be presented does not have to worry about recursion.

Next time: what the heck is a fixed-point operator?

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.

Excessive explanation, part four

Continuing with my excessively detailed explanation of type inference in ML…

After several years of successful use of the language, both in 
LCF and other research, and in teaching to undergraduates, it has 
become important to answer these questions — particularly because
the combination of flexibility (due to polymorphism), robustness (due
to semantic soundness) and detection of errors at compile time has 
proved to be one of the strongest aspects of ML.

ML and its descendants are indeed very pleasant languages. Parametric polymorphism, a sound type system, and good error detection mean that if your program type checks, odds are pretty good it is correct. That said, thirty years later the case is a bit overstated. I’m using OCaml every day and I’m pretty frustrated by the quality of the error messages. In a large complex program it can be hard to determine where the error really is when the type system tells you you’ve made a mistake.

But my purpose here is not to editorialize on the considerable merits of ML, but rather to explicate this paper. So onwards!

The discipline can be well illustrated by a small example. Let
us define in ML the function map, which maps a given function over
a given list — that is

map f [x1; ...; xn] = [f(x1),...,f(xn)]

The map function is familiar to C# programmers by another name. In C# parlance it is:

static IEnumerable<R> Select<A, R>(
  IEnumerable<A> items, 
  Func<A, R> projection)

That is, it takes a sequence of items and a projection function, and it returns a sequence of the items with the projection applied to them. We seek to deduce the same thing about the map function that we will define below: that it takes a sequence of this and a function from this to that, and returns a sequence of that.

The notation used in the paper could use some explanation.

First of all, function application is denoted in ML by stating the function (map) and then the arguments separated by spaces. So f is the first argument, and it is the projection function. The second argument is a list of items x1 through xn. Lists are denoted a couple of different ways in ML; here we are using the syntax “surround the whole thing with square brackets and separate the items with semicolons”.

Plainly the thing on the right hand side is intended to be the list of items after the function has been applied to them, but I must confess that I am mystified as to why the authors of the paper have changed notations here! I would have expected this to say

map f [x1; ...; xn] = [f x1; ...; f xn]

in keeping with the standard ML syntax. Anyone care to hazard a guess? Is this a typo or is there some subtlety here?

The required declaration is

letrec map f s = if null s then nil
                 else cons(f(hd s)) (map f (tl s))

We are defining (“let”) the recursive (“rec”) function map, which takes two arguments, f, a function, and s, a linked list. This is the standard recursive definition; first we consider the base case. null is a function that takes a list and returns true if it is the empty list or false otherwise. If the list is empty then the result of mapping is an empty list, written here as nil. If the list is not empty then it must have a head item, hd s and a tail list tl s. We apply the function to the head item, and recursively solve the problem on the tail, and then append the new head to the new tail using cons.

Now remember, the problem that we’re trying to solve here is “what is the signature of map?” Notice that we have no type information whatsoever in the parameter list. But if we already know the type signatures of the functions used here then we should be able to deduce the type signature.

Next time: given the types of all the parts of map, can we deduce the type of map?

Excessive explanation, part three

Continuing with my excessive explanation of type inference in ML…

Here we answer the question in the affirmative, for the purely 
applicative part of ML. It follows immediately that it is decidable 
whether a program is well-typed, in contrast with the elegant and 
slightly more permissive type discipline of Coppo. [1]

The “applicative” part of a language is the part of a language concerned with the question “what happens when we call a function with some bunch of arguments?” That is, the function is said to be “applied” to its arguments. (Or is the argument applied to the function? It’s a mystery.)

What we’re getting at here is: there’s a lot of stuff in real-world ML that we’re not going to worry about here: data structures and integer literals and pattern matching and all that stuff. The applicative part of the language is its core, and if we can make a sound, general type assignment algorithm for this core of the language, then that’s the interesting part; the rest is just filling in the corners, in some sense.

By “in the affirmative”, we mean that the paper will show two things. First, that the type assignment algorithm really does always find a type assignment if one exists, and produces an error if it does not. It never goes into infinite loops or returns the wrong answer. And second, that if an answer is produced, it is the most general type possible.

By “decidable” we mean that it is possible to write a computer program that takes as its input a syntactically well-formed ML program and always produces as its output either true: the program does not violate the type system, or false, the program does violate the type system. It never hangs, and it never produces the wrong answer. A program that takes some string and produces a Boolean like this is called a “decision algorithm”, and a problem for which a decision algorithm exists is a “decidable problem”.

Not all problems are decidable! The canonical example is the Halting Problem, which is “given a well-formed program, can this program go into an infinite loop?” We know that it is impossible to write a computer program that always answers this question correctly; either such a program is sometimes incorrect, or it sometimes goes into an infinite loop itself.

Note that not all type systems are decidable, and in fact, it was recently proven that the C# type system is not decidable! It is possible to write a C# program where the type checker will either get it wrong or run forever, though it is a pretty weird program. I’ll talk about that in a later blog series. (I had a very, very, VERY small part in this recent proof which is quite hilarious.)

The paper of Coppo mentioned notes that the ML type system does not allow you to represent some functions. For example, the function “take a function as the argument, pass the function to itself, and return the result” does not have a type in the ML type system.

Now, you might think, hey, we can represent that in C#:

delegate D D(D d);
D weird = d => d(d);

Though that is a function that takes a function as the argument, passes it to itself, and returns the result, notice that this is not general! There’s nothing generic here. Coppo points out that there are lots of different types of functions that match the pattern of “it’s legal to pass the function to itself”, and that there is no way to express that pattern in the ML type system.

In the paper, Coppo presents an extension to the ML type system that allows that, but the authors here point out that Coppo’s type system has the down side that it is not actually decidable.

This happens a lot in type systems; you often trade ability to represent a particular kind of odd function in the system for undecidability in extremely weird cases.

Next time, a not-weird case: how can we analyze the type of “map”?