[Haskell-cafe] "Least common supertype"?

[sterl]

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