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 others are more specific and can be derived from the general one by consistently replacing another type for the type parameter, i.e. the quantified variable . The counter-example fails because the replacement is not consistent. The consistent replacement can be made formal by applying a substitution to the term of a type , written . As the example suggests, substitution is not only strongly related to an order, that expresses that a type is more or less special, but also with the all-quantification which allows the substitution to be applied. Formally, in HM, a type is more general than , formally , if some quantified variable in is consistently substituted such that one gains as shown in the side bar. This order is part of the type definition of the type system. In our previous example, applying the substitution would result in . While substituting a monomorphic (ground) type for a quantified variable is straight forward, substituting a polytype has some pitfalls caused by the presence of free variables. Most particularly, unbound variables must not be replaced. They are treated as constants here. Additionally, quantifications can only occur top-level. Substituting a parametric type, one has to lift its quantifiers. The table on the right makes the rule precise. Alternatively, consider an equivalent notation for the polytypes without quantifiers in which quantified variables are represented by a different set of symbols. In such a notation, the specialization reduces to plain consistent replacement of such variables. The relation is a partial order and is its smallest element. Principal type While specialization of a type scheme is one use of the order, it plays a crucial second role in the type system. Type inference with polymorphism faces the challenge of summarizing all possible types an expression may have. The order guarantees that such a summary exists as the most general type of