# Understanding least common generalization (or anti-unification) of types

I am learning how to extend a basic Hindley-Milner type system to support overloaded variables by following Geoffrey Seward Smith's dissertation.

The proposed type inference algorithm makes use of the "least common generalization" (or LCG) of an overloaded variables types and cites this Reynolds paper as providing an algorithm for computing the LCG. I understand the logical concept of "least common generalization" but I am struggling to understand the mechanics of Reynolds algorithm for computing it.

My understanding is that Reynolds shows that a "least common generalization" can be found via "anti-unification". Below is a screenshot of the anti-unification algorithm described in the Reynolds paper.

I will describe my understanding of this algorithm in the context of types and highlight a few places where I have questions.

• The sequence $$Z_1, Z_2, ...$$ can be thought of as a infinite generator of "fresh" type vars.

• When Reynolds says "Set the variables $$\overline{A}$$ to $$A$$" and then later "let $$k$$ be te first symbol position at which $$\overline{A}$$..." does this suggest (in the context of types) that $$\overline{A}$$ is the sequence of free type vars in the type $$A$$? Or perhaps the entire type $$A$$ represented as an AST?

• I don't understand step (d).

• I understand that that step (e) can be thought of as replacing the parts of the types that differ with a type variable, however I don't fully understand what "beginning in the kth position" means. Does it mean some kind of sub-tree replacement in the AST that defines the type?

Is there a more appropriate resource for understanding LCG and/or anti-unification with respect to types?