sterl wrote:
Richard O'Keefe wrote:
On Nov 12, 2009, at 9:24 AM, Sean Leather wrote:
Is there a name for the following concept?
[Generalising from
    (Int, Char) -> (Char, Int)
    (Char, Int) -> (Int, Char)
 to    (x,    y  ) -> (y,   x   )]

It's the "least specific generalisation", also known as anti-unification.
(Because unification finds the most general specialisation.)
As far as I know, it originated in this paper:
Gordon D. Plotkin. A Note on Inductive Generalization. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 5, pages 153-163. Elsevier North-Holland, New York, 1970.

IANTT (I am not a type theorist) but...

If you're talking about supertypes and subtypes, then I think this can be classified as a "least upper bound".

It is a least upper bound, but only in a particular sense. The particular sense is (of course) anti-unification.

To strike to the core of why it's not unification, if we try to unify Int and Char the answer is "no, those do not unify" because the type Int&Char is overconstrained (i.e. empty). This is exactly the behavior we want for HM type inference: type variables are allowed to be specialized down to (possibly ungrounded) terms, but if they specialize down too far then there's a type error, and there's no way to un-specialize terms back up because that would let us lose track of constraints on permissible types.

Unification is a variety of intersection. Antiunification is the dual notion which is a variety of unioning. If we antiunify Int and Char, the answer will be Int|Char or whatever the closest analogue is (e.g. a free type variable) if the language doesn't allow indiscriminate unions. Depending on how we think of the sortal graph, we could also say unification returns the GLB whereas antiunification returns the LUB.

(Antiunification shouldn't be confused with disunification, which is the negative of unification rather than the dual. Disunification says "these things are not allowed to be equal" so it's a sort of symmetric difference.)

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to