[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]

Iavor Diatchki writes:

Hello,

On 10/19/07, Martin Sulzmann wrote:

...

Simon Peyton-Jones writes:

...

... Like you, Iavor, I find it very hard to internalise just why (B) and (C) are important. But I believe the paper gives examples of why they are, and Martin is getting good at explaining it. Martin: can you give an example, once more, of the importance of (B) (=fullness)?

Fullness (B) is a necessary condition to guarantee that the constraint solver (aka CHR solver) derived from the type class program is confluent.

Here's an example (taken from the paper).

class F a b c | a->b instance F Int Bool Char instance F a b Bool => F [a] [b] Bool

The FD is not full because the class parameter c is not involved in the FD. We will show now that the CHR solver is not confluent.

Here is the translation to CHRs (see the paper for details)

rule F a b1 c, F a b2 d ==> b1=b2 -- (FD) rule F Int Bool Char <==> True -- (Inst1) rule F Int a b ==> a=Bool -- (Imp1) rule F [a] [b] Bool <==> F a b Bool -- (Inst2) rule F [a] c d ==> c=[b] -- (Imp2)

The above CHRs are not confluent. For example, there are two possible CHR derivations for the initial constraint store F [a] [b] Bool, F [a] b2 d

F [a] [b] Bool, F [a] b2 d -->_FD (means apply the FD rule) F [a] [b] Bool, F [a] [b] d , b2=[b] --> Inst2 F a b Bool, F [a] [b] d , b_2=[b] (*)

Here's the second CHR derivation

F [a] [b] Bool, F [a] b2 d -->_Inst2 F a b Bool, F [a] b2 d -->_Imp2 F a b Bool, F [a] [c] d, b2=[c] (**)

(*) and (**) are final stores (ie no further CHR are applicable). Unfortunately, they are not logically equivalent (one store says b2=[b] whereas the other store says b2=[c]).

But what is wrong with applying the following logical reasoning:

Well, you apply the above CHRs from left to right *and* right to left. In contrast, I apply the CHRs only from left to right.

Starting with (**): F a b Bool, F [a] [c] d, b2=[c] (by inst2) F a b Bool, F [a] [c] d, b2=[c], F [a] [b] Bool (by FD) F a b Bool, F [a] [c] d, b2=[c], F [a] [b] Bool, [c] = [b] (applying equalities and omitting unnecessary predicates) F [a] [b] Bool, F [a] b2 d (...and then follow your argument to reach (*)...)

Alternatively, if we start at (*): F a b Bool, F [a] [b] d , b_2=[b] (by inst2) F a b Bool, F [a] [b] d , b_2=[b], F [a] [b] Bool (applying equalities, rearranging, and omitting unnecessary predicates) F [a] [b] Bool, F [a] b_2 d (... and then follow you reasoning to reach (**) ...)

So it would appear that the two sets of predicates are logically equivalent.

I agree that the two sets F a b Bool, F [a] [b] d , b_2=[b] (*) and F a b Bool, F [a] [c] d, b2=[c] (**) are logically equivalent wrt the above CHRs (see your proof). The problem/challenge we are facing is to come up with a confluent and terminating CHR solver. Why is this useful? (1) We get a deterministic solver (2) We can decide whether two constraints C1 and C2 are equal by solving (a) C1 -->* D1 and (b) C2 -->* D2 and then checking that D1 and D2 are equivalent. The equivalence is a simple syntactic check here. The CHR solving strategy applies rules in a fixed order (from left to right). My example shows that under such a strategy the CHR solver becomes non-confluent for type class programs with non-full FDs. We can show non-confluence by having two derivations starting with the same initial store leading to different final stores. Recall: F [a] [b] Bool, F [a] b2 d -->* F a b Bool, F [a] [b] d , b_2=[b] (*) F [a] [b] Bool, F [a] b2 d -->* F a b Bool, F [a] [c] d, b2=[c] (**) I said

...

(*) and (**) are final stores (ie no further CHR are applicable). Unfortunately, they are not logically equivalent (one store says b2=[b] whereas the other store says b2=[c]).

More precisely, I meant here that (*) and (**) are not logically equivalent *not* taking into account the above CHRs. This means that (*) and (**) are different (syntactically).

...

To conclude, fullness is a necessary condition to establish confluence of the CHR solver. Confluence is vital to guarantee completeness of type inference.

I don't think that fullness is an onerous condition.

I agree with you that, in practice, many classes probably use "full" FDs. However, these extra conditions make the system more complicated, and we should make clear what exactly are we getting in return for the added complexity.

You can get rid of non-full FDs (see the paper). BTW, type functions are full by construction. Martin