A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.
Among HM's more notable properties are its completeness and its ability to infer the most general type of a given program without programmer-supplied type annotations or other hints. Algorithm W is an efficient type inference method in practice and has been successfully applied on large code bases, although it has a high theoretical complexity.Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus, the complexity theoretic proofs by and came as a surprise to the research community. HM is preferably used for functional programming languages. It was first implemented as part of the type system of the programming language ML. Since then, HM has been extended in various ways, most notably with type class constraints like those in Haskell.
Introduction
As a type inference method, Hindley–Milner is able to deduce the types of variables, expressions and functions from programs written in an entirely untyped style. Being scope sensitive, it is not limited to deriving the types only from a small portion of source code, but rather from complete programs or modules. Being able to cope with parametric types, too, it is core to the type systems of many functional programming languages. It was first applied in this manner in the ML programming language.
The origin is the type inference algorithm for the simply typed lambda calculus that was devised by Haskell Curry and Robert Feys in 1958. In 1969, J. Roger Hindley extended this work and proved that their algorithm always inferred the most general type. In 1978, Robin Milner, independently of Hindley's work, provided an equivalent algorithm, Algorithm W. In 1982, Luis Damas finally proved that Milner's algorithm is complete and extended it to support systems with polymorphic references.
Monomorphism vs. polymorphism
In the simply typed lambda calculus, types are either atomic type constants or function types of form . Such types are monomorphic. Typical examples are the types used in arithmetic values:
Contrary to this, the untyped lambda calculus is neutral to typing at all, and many of its functions can be meaningfully applied to all type of arguments. The trivial example is the identity function
which simply returns whatever value it is applied to. Less trivial examples include parametric types like lists.
While polymorphism in general means that operations accept values of more than one type, the polymorphism used here is parametric. One finds the notation of type schemes in the literature, too, emphasizing the parametric nature of the polymorphism. Additionally, constants may be typed with (quantified) type variables. For example, the following type schemes quantify universally over , meaning that they are true for all possible :
Polymorphic types can become monomorphic by consistent substitution of their variables. Examples of monomorphic instances are:
More generally, types are polymorphic when they contain type variables, while types without them are monomorphic.
Contrary to the type systems used for example in Pascal (1970) or C (1972), which only support monomorphic types, HM is designed with emphasis on parametric polymorphism. The successors of the languages mentioned, like C++ (1985), focused on different types of polymorphism, namely subtyping in connection with object-oriented programming and overloading. While subtyping is incompatible with HM, a variant of systematic overloading is available in the HM-based type system of Haskell.
Let-polymorphism
When extending the type inference for the simply-typed lambda calculus towards polymorphism, one has to decide whether assigning a polymorphic type not only as type of an expression, but also as the type of a λ-bound variable is admissible. This would allow the generic identity type to be assigned to the variable 'id' in:
(λ id . ... (id 3) ... (id "text") ... ) (λ x . x)
Allowing this gives rise to the polymorphic lambda calculus; however, type inference in this system is not decidable. Instead, HM distinguishes variables that are immediately bound to an expression from more general λ-bound variables, calling the former let-bound variables, and allows polymorphic types to be assigned only to these. This leads to let-polymorphism where the above example takes the form
let id = λ x . x in ... (id 3) ... (id "text") ...
which can be typed with a polymorphic type for 'id'. As indicated, the expression syntax is extended to make the let-bound variables explicit, and by restricting the type system to allow only let-bound variable to have polymorphic types, while the parameters in lambda-abstractions must get a monomorphic type, type inference becomes decidable.
Overview
The remainder of this article proceeds as follows:
The HM type system is defined. This is done by describing a deduction system that makes precise what expressions have what type, if any. From there, it works towards an implementation of the type inference method. After introducing a syntax-driven variant of the above deductive system, it sketches an efficient implementation (algorithm J), appealing mostly to the reader's metalogical intuition. Because it remains open whether algorithm J indeed realises the initial deduction system, a less efficient implementation (algorithm W), is introduced and its use in a proof is hinted. Finally, further topics related to the algorithm are discussed.
The same description of the deduction system is used throughout, even for the two algorithms, to make the various forms in which the HM method is presented directly comparable.
The Hindley–Milner type system
The type system can be formally described by syntax rules that fix a language for the expressions, types, etc. The presentation here of such a syntax is not too formal, in that it is written down not to study the surface grammar, but rather the depth grammar, and leaves some syntactical details open. This form of presentation is usual. Building on this, typing rules are used to define how expressions and types are related. As before, the form used is a bit liberal.
Syntax Expressions TypesContext and Typing Free Type Variables The expressions to be typed are exactly those of the lambda calculus extended with a let-expression as shown in the adjacent table. Parentheses can be used to disambiguate an expression. The application is left-binding and binds stronger than abstraction or the let-in construct.
Types are syntactically split into two groups, monotypes and polytypes.Polytypes are called "type schemes" in the original article.
Monotypes Monotypes always designate a particular type. Monotypes are syntactically represented as terms.
Examples of monotypes include type constants like or , and parametric types like . The latter types are examples of applications of type functions, for example, from the set , where the superscript indicates the number of type parameters. The complete set of type functions is arbitrary in HM,The parametric types were not present in the original paper on HM and are not needed to present the method. None of the inference rules below will take care or even note them. The same holds for the non-parametric "primitive types" in said paper. All the machinery for polymorphic type inference can be defined without them. They have been included here for sake of examples but also because the nature of HM is all about parametric types. This comes from the function type , hard-wired in the inference rules, below, which already has two parameters and has been presented here as only a special case. except that it must contain at least , the type of functions. It is often written in infix notation for convenience. For example, a function mapping integers to strings has type . Again, parentheses can be used to disambiguate a type expression. The application binds stronger than the infix arrow, which is right-binding.
Type variables are admitted as monotypes. Monotypes are not to be confused with monomorphic types, which exclude variables and allow only ground terms.
Two monotypes are equal if they have identical terms.
Polytypes
Polytypes (or type schemes) are types containing variables bound by zero or more for-all quantifiers, e.g. .
A function with polytype can map any value of the same type to itself, and the identity function is a value for this type.
As another example, is the type of a function mapping all finite sets to integers. A function which returns the cardinality of a set would be a value of this type.
Quantifiers can only appear top level. For instance, a type is excluded by the syntax of types. Also monotypes are included in the polytypes, thus a type has the general form , where and is a monotype.
Equality of polytypes is up to reordering the quantification and renaming the quantified variables (-conversion). Further, quantified variables not occurring in the monotype can be dropped.
Context and typing
To meaningfully bring together the still disjoint parts (syntax expressions and types) a third part is needed: context. Syntactically, a context is a list of pairs , called assignments, assumptions or bindings, each pair stating that value variable has type All three parts combined give a typing judgment of the form , stating that under assumptions , the expression has type .
Free type variables
In a type , the symbol is the quantifier binding the type variables in the monotype . The variables are called quantified and any occurrence of a quantified type variable in is called bound and all unbound type variables in are called free. Additionally to the quantification in polytypes, type variables can also be bound by occurring in the context, but with the inverse effect on the right hand side of the . Such variables then behave like type constants there. Finally, a type variable may legally occur unbound in a typing, in which case they are implicitly all-quantified.
The presence of both bound and unbound type variables is a bit uncommon in programming languages. Often, all type variables are implicitly treated all-quantified. For instance, one does not have clauses with free variables in Prolog. Likewise in Haskell,Haskell provides the ScopedTypeVariables language extension allowing to bring all-quantified type variables into scope. where all type variables implicitly occur quantified, i.e. a Haskell type a -> a means here. Related and also very uncommon is the binding effect of the right hand side of the assignments.
Typically, the mixture of both bound and unbound type variables originate from the use of free variables in an expression. The constant function K = provides an example. It has the monotype . One can force polymorphism by . Herein, has the type . The free monotype variable originates from the type of the variable bound in the surrounding scope. has the type . One could imagine the free type variable in the type of be bound by the in the type of . But such a scoping cannot be expressed in HM. Rather, the binding is realized by the context.
Type order
Polymorphism means that one and the same expression can have (perhaps infinitely) many types. But in this type system, these types are not completely unrelated, but rather orchestrated by the parametric polymorphism.
As an example, the identity can have as its type as well as or and many others, but not . The most general type for this function is , while the