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

[Martin Sulzmann]

Iavor Diatchki writes:
 > Hello,
 > 
 > On 10/19/07, Martin Sulzmann <sulzmann at comp.nus.edu.sg> 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