FDs and confluence
Claus Reinke
claus.reinke at talk21.com
Mon Apr 10 09:39:18 EDT 2006
> (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
More information about the Haskell-prime
mailing list