together into equivalence classes by means of a procedure and to pick a representative for each such class using a procedure. Emphasizing the word procedure in the sense of side effect, we're clearly leaving the realm of logic in order to prepare an effective algorithm. The representative of a is determined such that, if both and are type variables then the representative is arbitrarily one of them, but 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' Now having a sketch of an inference algorithm at hand, a more formal presentation is given in the next section. It is described in Milner P. 370 ff. as algorithm J. Algorithm J The presentation of Algorithm J is a misuse of the notation of logical rules, since it includes side effects but allows 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. 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 quantification 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 nearly O(1) cost, the overall cost of the algorithm is close to linear in 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-hard, if not undecidable with respect to termination. Thus the HM performs as well as the best