[Haskell-cafe] RE: [Haskell] [Fwd: undecidable & overlapping
instances: a bug?]
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Fri Oct 19 06:35:13 EDT 2007
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
More information about the Haskell-Cafe
mailing list