FDs and confluence

Martin Sulzmann sulzmann at comp.nus.edu.sg
Mon Apr 10 05:49:15 EDT 2006

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

```