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 becausethe combination of flexibility (due to polymorphism), robustness (dueto 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. Letus define in ML the function map, which maps a given function overa given list - that ismap 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 isletrec 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?
