[Haskell-cafe] "Least common supertype"?

[wren ng thornton]

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