Hindley–Milner
Encyclopedia
In type theory
, Hindley–Milner (HM) (also known as Damas–Milner or Damas–Hindley–Milner) is a classical type inference
method with parametric polymorphism
for the lambda calculus
, 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 the properties making HM so outstanding is completeness and its ability to deduce the most general type of a given source without the need of any type annotations or other hints. HM is a fast algorithm, computing a type almost in linear time with respect to the size of the source, making it practically usable to type large programs. HM is preferably used for functional 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 by constrained types as used in Haskell
.
How expressions and types fit to each other is described by means of a deductive system
. Like any proof system, it allows different ways to come to a conclusion and since one and the same expression arguably might have different types, dissimilar conclusions about an expressions are possible. Contrary to this, the type inference method itself (Algorithm W) is defined as a step-by-step procedure, leaving no choice what to do next. Thus clearly, decisions not present in the logic might have been made constructing the algorithm, which demand a closer look and justifications but would perhaps remain non-obvious without the above differentiation.
Logic and algorithm share the notions of "expression" and "type", whose form is made precise by the syntax
.
The expressions to be typed are exactly those of the lambda calculus
, enhanced by a let-expression.
Readers unfamiliar with the lambda calculus might not only be puzzled by the syntax, which can
quickly be straightened out translating, that the application
represents
the function application, often written
and that the abstraction means
anonymous function
or function literal, common in most contemporary programming languages,
there perhaps spelled only more verbosely
.
Types as a whole are split into two groups, called mono- and polytypes.Polytypes are called "type schemes" in the original article.
Monotypes
, syntactically terms
, always designate a particular type in the sense, that it is equal only to itself and different from all others. The most typical representatives of monotypes are type constants like
or 
. Types can be parametric
like
. All these types are examples of applications of type functions 
,
i.e.
in the before mentioned examples, where the superscript indicates the number of type parameters. While the choice of 
is completely arbitrary, in context of HM it must contain at least 
, the type of
functions, which is written infix for convenience, e.g. a function mapping integers to strings has type
.
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 hold 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 the 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 have been presented here as only a special case.
Perhaps a bit irritating, type variables are monotypes, either. Standing alone, a type variable
is meant
to be as concrete like
or 
and clearly different from both. Type variables occurring as monotypes behave as if they were type constants, of which one only does not have any further information. Correspondingly, a function typed 
only maps values of the particular type 
on itself. Such a function can only be applied
to values having type
and to no others.
A function with polytype
by contrast 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. The count of members is a value for this type. Note that qualifiers can only appear top level, i.e. a
type
for instance, is excluded by syntax of types and that monotypes
are included in the polytypes, thus a type has the general form
.
In a type
, the symbol 
is the qualifier binding the type variables 
in the monotype 
. The variables 
are called qualified and any occurrence of a qualified type variable in 
is called bound and all unbound type variables in 
are call free. Like in the lambda calculus, the notion of free and bound variables
are essential for the understanding of the meaning of types.
This is certainly the hardest part of HM, perhaps because polytypes containing free variables are not represented in programming languages like Haskell
. Likely, one does not have clauses with free variables in Prolog
clauses. In particular developers experienced with both languages and actually knowing all the prerequisites of HM, are likely to slip this point. In Haskell
for example, all type variables implicitly occur qualified, i.e. a Haskell type
means 
here. Because a type like 
, though it may practically occur in a Haskell program, cannot be expressed there, it is easily be confused with its qualified version.
So what function can have a type like e.g.
, i.e. a mixture of both bound and unbound type variables and what could the free type variable 
therein mean?
Consider
in Example 1, with type annotations in brackets.
Its parameter
is not used in the body, but the variable 
bound in the outer context of 
sure is.
As a consequence,
accepts every value as argument, while returning a value bound outside and with it its type. 
to the contrary has type 
, in which all occurring type variables are bound
Evaluating, for instance
, results in a function of type 
, perfectly reflecting that foo's monotype 
in 
has been refined by this call.
In this example, the free monotype variable
in foo's type becomes meaningful by being qualified in the outer scope, namely in bar's type.
I.e. in context of the example, the same type variable
appears both bound and free in different types. As a consequence, a free type variable cannot be interpreted better than stating it is a monotype without knowing the context. Turning the statement around, in general, a typing is not meaningful without a context.
Consequently, to get the yet disjoint the parts of the syntax, expressions and types together meaningfully, a third
part, the context is needed. Syntactically, it is a list of pairs
, called
assignments or assumptions
, stating for each value variable
therein a type
. All three parts combined gives a typing of the form 
,
stating, that under assumptions
, the expression 
has type 
.
Now having the complete syntax at hand, one can finally make a senseful statement about the type of
in example 1, above,
namely
. Contrary to the above formulations, the monotype
variable
does not longer appear unbound, i.e. meaningless, but bound in the context as the type of the value variable
. The circumstance whether a type variable is bound or free in the context apparently plays a significant
role for a type as part of a typing, so
it is made precise in the side box.
Since the expression syntax might appear far too inexpressive to readers unfamiliar with the lambda calculus
, and because the examples given below will likely support this misconception, some notes that the HM is not dealing with toy languages might be helpful. As a central result in research on computability, the expression syntax defined above (without the let-variant) is able to express any computable function. Moreover all other programming language constructions can be relatively directly transformed syntactically into expressions of the lambda calculus. Therefore, this simple expression is used as a model for programming languages in research. A method known to work well for the lambda calculus can easily be extended to all or at least many other syntactical construction of a particular programming language using the before mentioned syntactical transformations.
As an example, the additional expression variant
can be transformed to 
.
It is added to expression syntax in HM only to support generalization during the type inference and not because syntax lacks computational strength.
Thus HM deals with inference of types in programs in general and the various functional languages using this method demonstrate, how well a result formulated only for the syntax of the lambda calculus can be extend to syntactically complex languages.
Contrary to the impression, that the expressions might be too inexpressive for practical application, they are actually far too expressive to be meaningfully typed at all. This is a consequence of the decision problem
being undecidable
for anything as expressive as the expression of the lambda calculus. Consequently, computing typings is a hopeless venture in general. Depending on the nature of the type system, it will either never terminate or otherwise refuse to work.
HM belongs to the later group of type systems. A collapse of the type system presents itself then as more subtle situation in that suddenly only one and the same type is yielded for the expressions of interest. This is not a fault in HM, but inherent in the problem of typing itself and can easily be created within any strongly typed programming language e.g. by coding an evaluator (the universal function) for the "too simple" expression. One then has a single concrete type that represents the universal data type as usual in untyped languages. The type system of the host programming language is then collapsed and cannot longer differentiate between the various types of values handed to or produced by the evaluator. In this context, it still delivers or checks types, but always the same, just as if the type system were not longer present at all.
expressing that 
is more special than 
.
When being applied to a value a polymorphic functions has to change its shape specializing to deal with this particular type of values. During this process, it also changes its type to match that of the parameter. If for instance the identity function having type
is to be applied on a number having type 
, both simply cannot work together, because all the types are different and nothing fits. What is needed is a function of type 
. Thus, during application, the polymorphic identity is specialized to a monomorphic version of itself. In terms of the specialization relation, one writes 
Now the shape shifting of polymorphic values is not fully arbitrary but rather limited by their pristine polytype. Following what has happened in the example one could paraphrase the rule of specialization, saying, a polymorphic type
is specialized by consistently replacing each occurrence of 
in 
and dropping the qualifier. While this rule works well for any monotype uses as replacement, it fails when a polytype, say 
is tried as a replacement, resulting in the non-syntactical type 
.
But not only that. Even if a type with nested qualified types would be allowed in the syntax, the result of the substitution would not longer preserve the property of the pristine type, in which both the parameter and the result of the function have the same type, which are now only seemingly equal because both subtypes became independent from each other allowing to specialize the parameter and the result with different types resulting in, e.g.
, hardly the right task for an identity function.
The syntactic restriction to allow qualification only top-level is imposed to prevent generalization while specializing. Instead
the more special type 
must be produces in this case.
One could undo the former specialization by specializing on some value of type
again. In terms of the relation
one gains
as a summary, meaning that syntactically different polytypes are equal w.r.t. to renaming their qualified variables.
Now focusing only on the question whether a type is more special than another and not longer what the specialized type is used for, one could summarize the specialization as in the box above. Paraphrasing it clockwise, a type
is specialized by consistently replacing any of the qualified variables 
by arbitrary monotypes 
gaining a monotype 
. Finally, type variables in 
not occurring free in the pristine type can optionally be qualified.
Thus the specialization rules makes sure that no free variable, i.e. monotype in the pristine type becomes unintentionally bound by a qualifier, but originally qualified variable can be replaced with whatever, even with types introducing new qualified or unqualified type variables.
Starting with a polytype
, the specialization could either replace the body by another qualified variable, actually a rename or by some type constant (including the function type) which may or may not have parameters filled either with monotypes or qualified type variables. Once a qualified variable is replaced by a type application, this specialization cannot be undone through another substitution as it was possible for qualified variables. Thus the type application is there to stay. Only if it contains another qualified type variable, the specialization could continue further replacing for it.
So the specialization introduces no further equivalence on polytype beside the already known renaming. Polytypes are syntactically equal up to renaming their qualified variables. The equality of types is a reflexive, antisymmetric and transitive relation and the remaining specializations of polytypes are transitive and with this the relation
an order.
The syntax of HM is carried forward to the syntax of the inference rules
that form the body of the formal system
, by using the typings as judgments
. Each of the rules define what conclusion could be drawn from what premises. Additionally to the judgments, some extra conditions introduced above might be used as premises, too.
A proof using the rules is a sequence of judgments such that all premises are listed before a conclusion. Please see the Examples 2, 3 below for a possible format of proofs. From left to right, each line shows the conclusion, the
of the rule applied and the premises, either by referring to an earlier line (number) if the premise is a judgment or by making the predicate explicit.
The side box shows the deduction rules of the HM type system. On can roughly divide them into two groups:
The first four rules
, 
, 
and 
are centered around the syntax, presenting one rule for each of the expression forms. Their meaning is pretty obvious at the first glance, as they decompose each expression, prove their sub-expressions and finally combine the individual types found in the premises to the type in the conclusion.
The second group is formed by the remaining two rules
and 
.
They handle specialization and generalization of types. While the rule
should be clear from the section on specialization above, 
complements the former, working in the opposite direction. It allow generalization, i.e. to qualify monotype variables that are not bound in the context. The necessity of this restriction 
is introduced the section on free type variables.
The following two examples exercise the rule system in action
Example 2: A proof for
where 
,
could be written
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, Hindley–Milner (HM) (also known as Damas–Milner or Damas–Hindley–Milner) is a classical type inference
Type inference
Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
method with parametric polymorphism
Parametric polymorphism
In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...
for the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
, first described by J. Roger Hindley
J. Roger Hindley
J. Roger Hindley is a prominent British logician best known for the Hindley–Milner type inference algorithm. Since 1998, he has been an Honorary Research Fellow at Swansea University.-Education:...
and later rediscovered by Robin Milner
Robin Milner
Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
.
Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis. Among the properties making HM so outstanding is completeness and its ability to deduce the most general type of a given source without the need of any type annotations or other hints. HM is a fast algorithm, computing a type almost in linear time with respect to the size of the source, making it practically usable to type large programs. HM is preferably used for functional 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 by constrained types as used in Haskell
Haskell
Haskell may refer to:*Haskell , a standardized pure functional programming language with non-strict semantics* Haskell Indian Nations University, a four year degree granting university in Lawrence, Kansas which offers free tuition to members of registered Native American tribes in the United...
.
Introduction
Organizing their original paper, Damas and Milner clearly separated two very different tasks. One is to describe what types an expression can have and another to present an algorithm actually computing a type. Keeping both aspects apart from each other allows to focus separately on the logic (i.e. meaning) behind the algorithm as well as to established a benchmark for the algorithm's properties.How expressions and types fit to each other is described by means of a deductive system
Deductive system
A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
. Like any proof system, it allows different ways to come to a conclusion and since one and the same expression arguably might have different types, dissimilar conclusions about an expressions are possible. Contrary to this, the type inference method itself (Algorithm W) is defined as a step-by-step procedure, leaving no choice what to do next. Thus clearly, decisions not present in the logic might have been made constructing the algorithm, which demand a closer look and justifications but would perhaps remain non-obvious without the above differentiation.
Syntax
| Expressions |
 |
| Types |
 |
Logic and algorithm share the notions of "expression" and "type", whose form is made precise by the syntax
Syntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
.
The expressions to be typed are exactly those of the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
, enhanced by a let-expression.
Readers unfamiliar with the lambda calculus might not only be puzzled by the syntax, which can
quickly be straightened out translating, that the application
representsthe function application, often written
and that the abstraction meansanonymous function
Anonymous function
In programming language theory, an anonymous function is a function defined, and possibly called, without being bound to an identifier. Anonymous functions are convenient to pass as an argument to a higher-order function and are ubiquitous in languages with first-class functions such as Haskell...
or function literal, common in most contemporary programming languages,
there perhaps spelled only more verbosely
.Types as a whole are split into two groups, called mono- and polytypes.Polytypes are called "type schemes" in the original article.
Monotypes
, syntactically termsTerm (logic)
In mathematical logic, universal algebra, and rewriting systems, terms are expressions which can be obtained from constant symbols, variables and function symbols...
, always designate a particular type in the sense, that it is equal only to itself and different from all others. The most typical representatives of monotypes are type constants like
or . Types can be parametriclike
. All these types are examples of applications of type functions ,i.e.
in the before mentioned examples, where the superscript indicates the number of type parameters. While the choice of is completely arbitrary, in context of HM it must contain at least , the type offunctions, which is written infix for convenience, e.g. a function mapping integers to strings has type
.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 hold 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 the 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 have been presented here as only a special case.Perhaps a bit irritating, type variables are monotypes, either. Standing alone, a type variable
is meantto be as concrete like
or and clearly different from both. Type variables occurring as monotypes behave as if they were type constants, of which one only does not have any further information. Correspondingly, a function typed only maps values of the particular type on itself. Such a function can only be appliedto values having type
and to no others.A function with polytype
by contrast can map any value of the same type to itself,and the identity function
Identity function
In mathematics, an identity function, also called identity map or identity transformation, is a function that always returns the same value that was used as its argument...
is a value for this type. As another example
is the type ofa function mapping all finite sets to integers. The count of members is a value for this type. Note that qualifiers can only appear top level, i.e. a
type
for instance, is excluded by syntax of types and that monotypesare included in the polytypes, thus a type has the general form
.Free type variables
| Free Type Variables |
 |
In a type
, the symbol is the qualifier binding the type variables in the monotype . The variables are called qualified and any occurrence of a qualified type variable in is called bound and all unbound type variables in are call free. Like in the lambda calculus, the notion of free and bound variablesFree variables and bound variables
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation that specifies places in an expression where substitution may take place...
are essential for the understanding of the meaning of types.
This is certainly the hardest part of HM, perhaps because polytypes containing free variables are not represented in programming languages like Haskell
Haskell
Haskell may refer to:*Haskell , a standardized pure functional programming language with non-strict semantics* Haskell Indian Nations University, a four year degree granting university in Lawrence, Kansas which offers free tuition to members of registered Native American tribes in the United...
. Likely, one does not have clauses with free variables in Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
clauses. In particular developers experienced with both languages and actually knowing all the prerequisites of HM, are likely to slip this point. In Haskell
Haskell
Haskell may refer to:*Haskell , a standardized pure functional programming language with non-strict semantics* Haskell Indian Nations University, a four year degree granting university in Lawrence, Kansas which offers free tuition to members of registered Native American tribes in the United...
for example, all type variables implicitly occur qualified, i.e. a Haskell type
means here. Because a type like , though it may practically occur in a Haskell program, cannot be expressed there, it is easily be confused with its qualified version.So what function can have a type like e.g.
, i.e. a mixture of both bound and unbound type variables and what could the free type variable therein mean?| Example 1 |
 |
Consider
in Example 1, with type annotations in brackets.Its parameter
is not used in the body, but the variable bound in the outer context of sure is.As a consequence,
accepts every value as argument, while returning a value bound outside and with it its type. to the contrary has type , in which all occurring type variables are boundEvaluating, for instance
, results in a function of type , perfectly reflecting that foo's monotype in has been refined by this call.In this example, the free monotype variable
in foo's type becomes meaningful by being qualified in the outer scope, namely in bar's type.I.e. in context of the example, the same type variable
appears both bound and free in different types. As a consequence, a free type variable cannot be interpreted better than stating it is a monotype without knowing the context. Turning the statement around, in general, a typing is not meaningful without a context.Context and typing
| Syntax |
 |
| Free Type Variables |
 |
Consequently, to get the yet disjoint the parts of the syntax, expressions and types together meaningfully, a third
part, the context is needed. Syntactically, it is a list of pairs
, calledassignments or assumptions
Assumption
In logic an assumption is a proposition that is taken for granted, as if it were true based upon presupposition without preponderance of the facts...
, stating for each value variable
therein a type
. All three parts combined gives a typing of the form ,stating, that under assumptions
, the expression has type .Now having the complete syntax at hand, one can finally make a senseful statement about the type of
in example 1, above,namely
. Contrary to the above formulations, the monotypevariable
does not longer appear unbound, i.e. meaningless, but bound in the context as the type of the value variable. The circumstance whether a type variable is bound or free in the context apparently plays a significantrole for a type as part of a typing, so
it is made precise in the side box.Note on expressivness
Since the expression syntax might appear far too inexpressive to readers unfamiliar with the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
, and because the examples given below will likely support this misconception, some notes that the HM is not dealing with toy languages might be helpful. As a central result in research on computability, the expression syntax defined above (without the let-variant) is able to express any computable function. Moreover all other programming language constructions can be relatively directly transformed syntactically into expressions of the lambda calculus. Therefore, this simple expression is used as a model for programming languages in research. A method known to work well for the lambda calculus can easily be extended to all or at least many other syntactical construction of a particular programming language using the before mentioned syntactical transformations.
As an example, the additional expression variant
can be transformed to .It is added to expression syntax in HM only to support generalization during the type inference and not because syntax lacks computational strength.
Thus HM deals with inference of types in programs in general and the various functional languages using this method demonstrate, how well a result formulated only for the syntax of the lambda calculus can be extend to syntactically complex languages.
Contrary to the impression, that the expressions might be too inexpressive for practical application, they are actually far too expressive to be meaningfully typed at all. This is a consequence of the decision problem
Decision problem
In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...
being undecidable
Undecidable
Undecidable may refer to:In mathematics and logic* Undecidable problem - a decision problem which no algorithm can decide* "Undecidable" is sometimes used as a synonym of "independent", where a formula in mathematical logic is independent of a logical theory if neither that formula nor its negation...
for anything as expressive as the expression of the lambda calculus. Consequently, computing typings is a hopeless venture in general. Depending on the nature of the type system, it will either never terminate or otherwise refuse to work.
HM belongs to the later group of type systems. A collapse of the type system presents itself then as more subtle situation in that suddenly only one and the same type is yielded for the expressions of interest. This is not a fault in HM, but inherent in the problem of typing itself and can easily be created within any strongly typed programming language e.g. by coding an evaluator (the universal function) for the "too simple" expression. One then has a single concrete type that represents the universal data type as usual in untyped languages. The type system of the host programming language is then collapsed and cannot longer differentiate between the various types of values handed to or produced by the evaluator. In this context, it still delivers or checks types, but always the same, just as if the type system were not longer present at all.
Polymorphic type order
While the equality of monotypes is purely syntactical, polytypes offer a richer structure by being related to other types through a specialization relation expressing that is more special than .When being applied to a value a polymorphic functions has to change its shape specializing to deal with this particular type of values. During this process, it also changes its type to match that of the parameter. If for instance the identity function having type
is to be applied on a number having type , both simply cannot work together, because all the types are different and nothing fits. What is needed is a function of type . Thus, during application, the polymorphic identity is specialized to a monomorphic version of itself. In terms of the specialization relation, one writes Now the shape shifting of polymorphic values is not fully arbitrary but rather limited by their pristine polytype. Following what has happened in the example one could paraphrase the rule of specialization, saying, a polymorphic type
is specialized by consistently replacing each occurrence of in and dropping the qualifier. While this rule works well for any monotype uses as replacement, it fails when a polytype, say is tried as a replacement, resulting in the non-syntactical type .But not only that. Even if a type with nested qualified types would be allowed in the syntax, the result of the substitution would not longer preserve the property of the pristine type, in which both the parameter and the result of the function have the same type, which are now only seemingly equal because both subtypes became independent from each other allowing to specialize the parameter and the result with different types resulting in, e.g.
, hardly the right task for an identity function.The syntactic restriction to allow qualification only top-level is imposed to prevent generalization while specializing. Instead
the more special type must be produces in this case.One could undo the former specialization by specializing on some value of type
again. In terms of the relationone gains
as a summary, meaning that syntactically different polytypes are equal w.r.t. to renaming their qualified variables.| Specialization Rule |
 |
Now focusing only on the question whether a type is more special than another and not longer what the specialized type is used for, one could summarize the specialization as in the box above. Paraphrasing it clockwise, a type
is specialized by consistently replacing any of the qualified variables by arbitrary monotypes gaining a monotype . Finally, type variables in not occurring free in the pristine type can optionally be qualified.Thus the specialization rules makes sure that no free variable, i.e. monotype in the pristine type becomes unintentionally bound by a qualifier, but originally qualified variable can be replaced with whatever, even with types introducing new qualified or unqualified type variables.
Starting with a polytype
, the specialization could either replace the body by another qualified variable, actually a rename or by some type constant (including the function type) which may or may not have parameters filled either with monotypes or qualified type variables. Once a qualified variable is replaced by a type application, this specialization cannot be undone through another substitution as it was possible for qualified variables. Thus the type application is there to stay. Only if it contains another qualified type variable, the specialization could continue further replacing for it.So the specialization introduces no further equivalence on polytype beside the already known renaming. Polytypes are syntactically equal up to renaming their qualified variables. The equality of types is a reflexive, antisymmetric and transitive relation and the remaining specializations of polytypes are transitive and with this the relation
an order.Deductive system
| The Syntax of Rules |
 |
The syntax of HM is carried forward to the syntax of the inference rules
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
that form the body of the formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
, by using the typings as judgments
Judgment (mathematical logic)
In mathematical logic, a judgment can be for example an assertion about occurrence of a free variable in an expression of the object language, or about provability of a proposition ; but judgments can be also other inductively definable assertions in the metatheory...
. Each of the rules define what conclusion could be drawn from what premises. Additionally to the judgments, some extra conditions introduced above might be used as premises, too.
A proof using the rules is a sequence of judgments such that all premises are listed before a conclusion. Please see the Examples 2, 3 below for a possible format of proofs. From left to right, each line shows the conclusion, the
of the rule applied and the premises, either by referring to an earlier line (number) if the premise is a judgment or by making the predicate explicit.Typing rules
| Declarative Rule System |
 |
The side box shows the deduction rules of the HM type system. On can roughly divide them into two groups:
The first four rules
, , and are centered around the syntax, presenting one rule for each of the expression forms. Their meaning is pretty obvious at the first glance, as they decompose each expression, prove their sub-expressions and finally combine the individual types found in the premises to the type in the conclusion.The second group is formed by the remaining two rules
and .They handle specialization and generalization of types. While the rule
should be clear from the section on specialization above, complements the former, working in the opposite direction. It allow generalization, i.e. to qualify monotype variables that are not bound in the context. The necessity of this restriction is introduced the section on free type variables.The following two examples exercise the rule system in action
Example 2: A proof for
where ,could be written
-
Example 3: To demonstrate generalization,
is shown below:
-
Principal type
As mentioned in the introduction, the rules allow to deduce different types for one and the same expression. See for instance, Example 2, steps 1,2 and Example 3, steps 2,3 for three different typings of the same expression. Clearly, the different results are not fully unrelated, but connected by the type order. It is an important property of the rule system and this order that whenever more but one type can be deduced for an expression, among them is (modulo alpha-renaming of the type variableType variableIn type theory and programming languages, a type variable is a mathematical variable ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond to some memory locations.Programming languages that...
s) a unique most general type in the sense, that all others are specialization of it. Though the rule system must allow to derive specialized types, a type inference algorithm should deliver this most general or principal type as its result.
Let-polymorphism
Not visible immediately, the rule set encodes a regulation under which circumstances a type might be generalized or not by a slightly varying use of mono- and polytypes in the rules
and 
.
In rule
, the value variable of the parameter of the function 
is added to the context with a monomorphic type through the premise 
, while in the rule 
, the variable enters the environment in polymorphic form 
. Though in both cases the presence of x in the context prevents the use of the generalisation rule for any monotype variable in the assignment, this regulation forces the parameter x in a 
-expression to remain monomorphic, while in a let-expression, the variable could already be introduced polymorphic, making specializations possible.
As a consequence of this regulation, no type can be inferred for
since the parameter
is in a monomorphic position, while 
yields a type 
, because 
has been introduced in a let-expression and is treated polymorphic therefore.
Note that this behaviour is in strong contrast to the usual definition
and the reason why the let-expression appears in the syntax at all. This distinction is called let-polymorphism or let generalization and is a conception owned to HM.
Towards an algorithm
Now that the deduction system of HM is at hand, one could present an algorithm and validate it w.r.t. the rules.
Alternatively, it might be possible to derive it by taking a closer look on how the rules interact and proof are
formed. This is done in the remainder of this article focusing on the possible decisions one can make while proving a typing.
Degrees of freedom choosing the rules
Isolating the points in a proof, where no decision is possible at all,
the first group of rules centered around the syntax leaves no choice since
to each syntactical rule corresponds a unique typing rule, which determines
a part of the proof, while between the conclusion and the premises of these
fixed parts chains of
and 
could occur. Such a chain could also exist between the conclusion of the
proof and the rule for topmost expression. All proof must have
the so sketched shape.
Because the only choice in a proof with respect of rule selection are the
and 
chains, the
form of the proof suggests the question whether it can be made more precise,
where these chains might be needed. This is in fact possible and leads to a
variant of the rules system without both rules.
Syntax-directed rule system
Syntactical Rule System 
Generalization 
A contemporary treatment of HM uses a purely syntax-directed rule system due to
Clement
as an intermediate step. In this system, the specialization is located directly after the original
rule
and merged into it, while the generalization becomes part of the
rule. There the generalization is
also determined to always produce the most general type by introducing the function
, which qualifies
all monotype variables not bound in
.
Formally, to validate, that this new rule system
is equivalent to the original 
, one has
to show that
, which falls apart into two sub-proofs:
-
(ConsistenceConsistencyConsistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
) -
(Completeness)
While consistency can be seen by decomposing the rules
and 
of
into proofs in 
, it is likely visible that 
is incomplete, as
one cannot show
in 
, for instance, but only
. An only slightly weaker version of completeness is provable
though, namely
implying, one can derive the principal type for an expression in
allowing to generalize the proof in the end.
Comparing
and 
note that only monotypes appear in the judgments of all rules, now.
Degrees of freedom instanciating the rules
Within the rules themselves, assuming a given expression, one is free to pick
the instances for (rule) variables not occurring in this expression. These are
the instances for the type variable in the rules. Working towards finding the
most general type, this choice can be limited to picking suitable types for
in 
and 
.
The decision of a suitable choice cannot be made locally, but its quality becomes apparent
in the premises of
, the only rule, in which
two different types, namely the function's formal and actual parameter type have
to come together as one.
Therefor, the general strategy for finding a proof would be to make the most
general assumption (
) for 
in
and to refine this and the choice to be made in
until all side conditions imposed by the
rules are finally met. Fortunately, no trial and
error is needed, since an effective method is known to compute all the choices,
Robinson's Unification
in combination with the so-called Union-FindDisjoint-set data structureIn computing, a disjoint-set data structure is a data structure that keeps track of a set of elements partitioned into a number of disjoint subsets. A union-find algorithm is an algorithm that performs two useful operations on such a data structure:* Find: Determine which set a particular element...
algorithm.
To briefly summarize the union-find algorithm, given the set of all types in a proof, it allows to
to group them together into equivalence classes by means of a
procedure and to pick a representativeRepresentativeRepresentative may refer to:*Representation*Legislator, someone who is part of a legislature*House of Representatives*Representative sample in statistics...
for each such class using a
procedure. Emphasizing on the word procedure in the sense of side effectSide effect (computer science)In computer science, a function or expression is said to have a side effect if, in addition to returning a value, it also modifies some state or has an observable interaction with calling functions or the outside world...
,
we're clearly leaving the realm of logic to prepare an effective algorithm.
The representative of a
is determined such, that if both 
and 
are type variables
the representative is arbitrarily one of them, while uniting a variable and a term, the term becomes the representative. Assuming an implementation of union-find at hand, one can formulate the unification of two monotypes as follows:
unify(ta,tb):
ta = find(ta)
tb = find(tb)
if both ta,tb are terms of the form D p1..pn with identical D,n then
unify(ta[i],tb[i]) for each corresponding ith parameter
else
if at least one of ta,tb is a type variable then
union(ta,tb)
else
error 'types do not match'
Algorithm W
Algorithm W 
The presentation of Algorithm W as shown in the side box does not only deviate significantly from the original but is also a gross abuse of the notation of logical rules, since it includes side effects. It is legitimized here, for allowing a direct comparison with
while expressing an efficient implementation at the same time. The rules now specify a procedure with parameters 
yielding 
in the conclusion where the execution of the premises proceeds from left to right. Alternatively to a procedure, it could be viewed as an attributationAttribute grammarAn attribute grammar is a formal way to define attributes for the productions of a formal grammar, associating these attributes to values. The evaluation occurs in the nodes of the abstract syntax tree, when the language is processed by some parser or compiler....
of the expression.
The procedure '
' specializes the polytype 
by copying the term and replacing the bound type variables consistently by new monotype variables. '
' produces a new monotype variable. Likely, 
has to copy the type introducing new variables for the qualification to avoid unwanted captures. Overall, the algorithm now proceeds by always making the most general choice leaving the specialization to the unification, which by itself produces the most general result. As noted above, the final result 
has to be generalized to 
in the end, to gain the most general type for a given expression.
Because the procedures used in the algorithm have near O(1) cost, the overall cost of the algorithm is close linear to the size of the expression for which a type is to be inferred. This is in strong contrast to many other attempts to derive type inference algorithms, which often came out to be NP-hardNP-hardNP-hard , in computational complexity theory, is a class of problems that are, informally, "at least as hard as the hardest problems in NP". A problem H is NP-hard if and only if there is an NP-complete problem L that is polynomial time Turing-reducible to H...
, if not undecidableUndecidable problemIn computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
w.r.t. termination. Thus the HM performs as good as the best fully informed type-checking algorithms can. Type-checking here means, that an algorithm does not have to find a proof, but only to validate a given one.
The efficiency is slightly lowered for two reasons. First, the binding of type variables in the context has to be maintained to allow computation of
and an occurs checkOccurs checkIn computer science, the occurs check is a part of algorithms forsyntactic unification. It causes unification of a logic variable V and a structure S to fail if S contains V....
has to made to prevent recursive types to be build during
.
An example of such a case is
, for which no type can be derived using HM. Because practically types are only small terms and do not build up expanding structures, one can treat them in complexity analysis as being smaller as some constant, retaining O(1) costs.
Original presentation of Algorithm W
In the original paper, the algorithm is presented more formally using a substitution style instead of side effects in the method above. In the later form, the side effect invisibly takes care of all places where a type variable is used. Explicitly using substitutions does not only makes the algorithm hard to read, because the side effect occurs virtually everywhere, but also gives the false impression that the method might be costly. When implemented using purely functional means or for the purpose to prove the algorithm to be basically equivalent to the deduction system, full explicitness is of cause needed and the original formulation a necessary refinement.
Recursive definitions
A central property of the lambda calculus is, that recursive definitions are non-elemental, but can instead be expressed by a fixed point combinatorFixed point combinatorIn computer science, a fixed-point combinator is a higher-order function that computes a fixed point of other functions. A fixed point of a function f is a value x such that x = f. For example, 0 and 1 are fixed points of the function f = x2, because 0 = 02 and 1 = 12...
.
The original paper notes that recursion can realized by this combinator's type
. A possible recursive definitions could thus be formulated as
.
Alternatively an extension of the expression syntax and an extra typing rule is possible as:
-
where
basically merging
and 
while including the recursively defined
variables in monotype positions where they occur left to the
but as polytypes right to it. This
formulation perhaps best summarizes the essence of let-polymorphism. -
-
-
