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 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. 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, 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