Home » forums » LtU Forum

Non-transitivity of type unification

We know type unification is not transitive in general

a ~ b /\ b ~ c does not imply a ~ c

And it's easy to find examples that don't unify

a |-> Int; b |-> b; c |-> Bool
a |-> (Int, a'); b |-> (Int, Bool); c |-> (c', Bool)

In all the examples I can make up, there's two outer types that don't unify, and a piggy in the middle that is either strictly more general than the outers (bare b) or strictly subsumed (Int, Bool).

For some (malicious) testing, I want an example where each three pairings of types unify, but the three types together do not. That is

a ~ b /\ b ~ c /\ a ~ c but not mgu(a, b) ~ c

Can anybody concoct such an example?
Or point me to something showing it's impossible.

By AntC at 2018-03-18 11:12 | LtU Forum | previous forum topic | next forum topic | other blogs | 3372 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

repeated type vars

OK cracked it

a |-> (Int, a'); b |-> (b', b'); c |-> (c', Bool)

a ~ b, mgu |-> (Int, Int)
b ~ c, mgu |-> (Bool, Bool)
a ~ c, mgu |-> (Int, Bool)

None of those mgus unify.

Are there any examples not relying on repeated type vars?

By AntC at Sun, 2018-03-18 13:02 | login or register to post comments

Probably need type vars?

Offhand, it seems like you'd need to have repeated type var. If you had a conflict between concrete type constructors in some part of the type, that conflict would exhibit with the pair that introduced those constructors.

By Matt M at Sun, 2018-03-18 15:28 | login or register to post comments