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

[Iavor Diatchki]

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:

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.

> 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.

-Iavor