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 (I, I^2, ...) using type operators (such as infixed a' for functions andpostfixed 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 forsuch 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 simplyadding the polymorphic fixed-point operatorfix : aI ((I a' I) a' I)

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?