Type inference

Standard ML supports a form of polymorphism. Before going further, we should clarify the precise nature of the polymorphism which is permitted. It is sometimes referred to as ``let-polymorphism''. This name derives from the fact that in this system the term

let  val Id = fn x => x   in  (Id 3, Id true)  end

is a well-typed term whereas the very similar

(fn Id => (Id 3, Id true)) (fn x => x)

is not. The let .. in .. end construct is not just syntactic sugar for function application, it is essential to provide the polymorphism without compromising the type security of the language. This polymorphic type system has a long history; the early work was done by Roger Hindley [Hin69] but his work did not become well-known nor was its importance realised until the type system was re-discovered and extended by Robin Milner [Mil78].

We can distinguish between two kinds of bound variables: those which are bound by the keyword fn and those which are bound by the keyword let. The distinction is this:

• all occurrences of a fn-bound identifier must have the same type; but
• each occurrence of a let-bound identifier may have a different type provided it is a instance of the principal--or most general--type inferred for that identifier.

We need to make clearer what we mean by ``instance'' and what we mean by ``principal type''. That will be done in the next chapter. For the moment we will proceed by informally introducing the notation and main concepts.