FDs and confluence

[Claus Reinke]

> (see the FunctionalDependencies page for background omitted here)

which seems to ignore much of the discussion of confluence we had 
here some weeks ago? I thought this list was for communication with 
the committee, and since the ticket exists, I had been hoping that the
type class subcommittee would ensure that the wiki would be updated.
but it seems I have been talking to myself..
 
> One of the problems with the relaxed coverage condition implemented
> by GHC and Hugs is a loss of confluence.  Here is a slightly cut-down
> version of Ex. 18 from the FD-CHR paper:
> 
> class B a b | a -> b
> class C a b c | a -> b
> 
> instance B a b => C [a] b Bool
> 
> Starting from a constraint set C [a] b Bool, C [a] c d, we have two
> possible reductions:
> 
> 1) C [a] b Bool, C [a] c d
> => c = b, C [a] b Bool, C [a] b d (use FD on C)
> => c = b, B a b, C [a] b d (reduce instance)
> 
> 2) C [a] b Bool, C [a] c d
> => C a b, C [a] c d (reduce instance)

CHR-alt:

B a b <=> infer_B a b, memo_B a b.
memo_B a b1, memo_B a b2 ==>b1=b2.

C a b c <=> infer_C a b c, memo_C a b c.
memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2.
infer_C [a] b Bool <=> B a b.
memo_C [a] b' c' ==> b'=b.

reduction:

3)  C [a] b Bool, C [a] c d
<=> infer_C [a] b Bool, memo_C [a] b Bool, infer_C [a] c d, memo_C [a] c d
{reducing instances cannot disable use of FDs!}
<=> B a b, memo_C [a] b Bool, infer_C [a] c d, memo_C [a] c d
{use FD now or earlier..}
==> B a b, infer_C [a] c d, memo_C [a] b Bool, memo_C [a] c d, b=c

there is no loss of confluence. there is no implication that d=Bool
(you could add: 'instance B a b => C [a] b Char' without violating
FD consistency). just a useless instance improvement rule for C.
just blindly applying the alternative translation..

what am I missing here?

claus

> The proposed solution was to tighten the restrictions on instances to
> forbid those like the above one for C.  However there may be another
> way out.
> 
> The consistency condition implies that there cannot be another
> instance C [t1] t2 t3: a substitution unifying a and t1 need not
> unify b and t2.  Thus we could either
> 
> 1) consider the two constraint sets equivalent, since they describe
>   the same set of ground instances, or
> 
> 2) enhance the instance improvement rule: in the above example, we
>   must have d = Bool in both cases, so both reduce to
> 
> c = b, d = Bool, B a b
> 
>   More precisely, given a dependency X -> Y and an instance C t, if
>   tY is not covered by tX, then for any constraint C s with sX = S tX
>   for some substitution S, we can unify s with S t.
> 
>   We would need a restriction on instances to guarantee termination:
>   each argument of the instance must either be covered by tX or be
>   a single variable.  That is less restrictive (and simpler) than
>   the previous proposal, however.
> 
> Underlying this is an imbalance between the two restrictions on instances.
> In the original version, neither took any account of the context of the
> instance declaration.  The implementations change this for the coverage
> condition but not the consistency condition.  Indeed the original form of
> the consistency condition is necessary for the instance improvement rule.
> 
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://haskell.org/mailman/listinfo/haskell-prime