Ross Paterson writes:
> (see the FunctionalDependencies page for background omitted here)
>
> 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)
^^^^^
should be B a b
> 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
>
That's troublesome for (complete) type inference.
Two constraint stores are equivalent if they are equivalent
for any satisfying ground instance? How to check that?
> 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.
>
I'm not following you here, you're saying?
rule C [a] b d ==> d=Bool
Are you sure that you're not introducing further "critical pairs"?
> 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.
>
Maybe, you found a "simple" solution (that would be great)
but I'not 100% convinced yet.
The problem you're addressing only arises for non-full FDs.
Aren't such cases very rare in practice?
Martin
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
