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