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. E.g.: cons : forall a . a -> List a -> List a nil : forall a . List a id : forall a . a -> a Polymorphic types can become monomorphic by consistent substitution of their variables. Examples of monomorphic instances are: id' : String -> String nil' : List Number 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 define when deriving an instance of a value is admissible. Ideally, this would be allowed with any use of a bound variable, as in: (λ id . ... (id 3) ... (id "text") ... ) (λ x . x) Unfortunately, type inference in polymorphic lambda calculus is not decidable. Instead, HM provides a let-polymorphism of the form let id = λ x . x in ... (id 3) ... (id "text") ... restricting the binding mechanism in an extension of the expression syntax. Only values bound in a let construct are subject to instantiation, i.e. are polymorphic, while the parameters in lambda-abstractions are treated as being monomorphic. 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