[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping
instances: a bug?]
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Sun Oct 21 23:52:47 EDT 2007
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
More information about the Haskell-Cafe
mailing list