(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@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
