FDs and confluence
iavor.diatchki at gmail.com
Sat Apr 15 12:30:42 EDT 2006
On 4/13/06, Ross Paterson <ross at soi.city.ac.uk> wrote:
> They are equivalent, but C [a] b d, Num c and C [a] c d, Num c are not.
I agree that this is the case if you are thinking of
"forall a b c d. (C [a] b d, Num c) <=> (C [a] c d, Num c)"
Here is a counter example (assume we also add an instance B Char Int
to the example)
a = Char, b = Char, c = Int, d = Bool
LHS: (C [Char] Char Bool, Num Int) => B Char Char => False
RHS: (C [Char] Int Bool, Num Int) => B Char Int => True
However, I don't think this is the case if you are thinking of:
"forall a c d. exists b. (C [a] b d, Num c) <=> (C [a] c d, Num c)"
becuase I can pick 'b' to be 'c'.
In any case I think this thread is drifting in the wrong direction. I
was just looking for a concrete example of where we have a problem
with the non-conflence that people have found, e.g. somehitng like
'here is an expression for which we can infer these two schemas, and
they have different sets of monomorphic instances'. I think such an
example would be very useful for me (and perhaps others) to clarify
exactly what is the problem, so that we can try to correct it.
More information about the Haskell-prime