[Haskell-cafe] "Least common supertype"?

[wren ng thornton]

wren ng thornton wrote:
> sterl wrote:
>> 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.

And part of the reason I say "only in a particular sense" is that it 
depends what graph we're talking about. There are many different 
varieties of relations we could draw among types. One is a parametric 
polymorphism relationship where some types are more polymorphic than and 
subsume other types. But we could also be discussing languages with a 
class hierarchy, or refinement types, or some other sense in which one 
type is "bigger" or "contains" another.

Ideas like most general unifier and least specific generalization are 
just another relation on types. But they're particularly quirky because 
they take some subset of other type relations into account. Which is 
also to say that they may choose not to take certain other relations 
into account. A classic example here is the way Java generics ignore 
super-/subclass relations in the parameters. So the graph we draw of the 
MGU/LSG relation may not be coextensive with other graphs of "super" and 
"sub" types. Also, because of the properties of the function arrow there 
can be issues of contravariance to muddy the picture as well.

Your intuition is on the right track, but it can be problematic to pin 
down in a way that adds meaningfully to the understanding of MGU/LSG.

-- 
Live well,
~wren