Iavor Diatchki writes: > Hello, > > On 10/19/07, Martin Sulzmann <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe