Simon Peyton-Jones writes:
| I believe that this "weak coverage condition" (which is also called | "the dependency condition" somewhere on the wiki) is exactly what GHC | 6.4 used to implement but than in 6.6 this changed. According to | Simon's comments on the trac ticket, this rule requires FDs to be | "full" to preserve the confluence of the system that is described in | the "Understanding Fds via CHRs" paper. I have looked at the paper | many times, and I am very unclear on this point, any enlightenment | would be most appreciated.
Right. In the language of http://hackage.haskell.org/trac/ghc/ticket/1241, last comment (date 10/17/07), it would be *great* to
replace the Coverage Condition (CC) with the Weak Coverage Condition (WCC)
as Mark suggests. BUT to retain soundness we can only replace CC with WCC + B WCC alone without (B) threatens soundness. To retain termination as well (surely desirable) we must have WCC + B + C
(You'll have to look at the ticket to see what B,C are.)
And since A+B+C are somewhat onerous, we probably want to have CC or (WCC + B + C)
At least we know of nothing else weaker that will do (apart from CC of course).
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]). 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. Martin