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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
