[Haskell-cafe] "Least common supertype"?
wren ng thornton
wren at freegeek.org
Thu Nov 12 02:36:01 EST 2009
> 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.)
More information about the Haskell-Cafe