Least Common Generalization. Cheers, Thu 2009/11/11 Eugene Kirpichov :

Is the name of the concept.... "Most general unifier" (MGU) ? (See: Hindley-Milner type inference)

2009/11/11 Sean Leather :

...

Is there a name for the following concept? Can you point me to any references on it?

Suppose I have the following two functions ...

...

swap1 :: (Int, Char) -> (Char, Int) swap2 :: (Char, Int) -> (Int, Char)

... and, for some reason, I think I can unify these into a single function. I think, hmm, given that the structure is that same, let's do a first pass:

...

swap? :: (a, b) -> (c, d)

But then I go back to the input types to confirm that this will work, and, alas, it will not, because there are similarities that I missed. This is way too general. I need to ensure that what's an Int stays an Int and likewise for Char.

...

swap! :: (a, b) -> (b, a)

And now I have found a type that is more general than swap1 and swap2 and yet not so general that the shared constraints are left out. This seems somewhat analogous to the least common multiple.

Another example is the following:

...

showFloat :: Float -> String showBool :: Bool -> String

We could say the more general type is ...

...

show? :: a -> String

... but then we lose the implied constraint that we must know something about 'a' to produce a string. So, we add back such some such constraint:

...

show! :: (Show a) => a -> String

Of course, with all of this, it may not be clear what to do about the definitions of the functions, but I'm curious if there's a name for the concept from a type perspective.

Thanks, Sean

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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". I.e. if there is a function that is used in both the first and second context provided, then one can infer that its constraints must satisfy both signatures. To then unify the signatures, construct a supertype which by definition both must satisfy. Eventually (when you know the constraints are fully saturated), you can then unify the supertype constraints by taking the least upper bound -- which, by contravariance, is the greatest lower bound of the input and the least upper bound of the output. The greatest lower bound of the inputs will enforce parametricity because the only common subtype of Int and Char is bottom. The least upper bound of the output is then trivial. --S

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