FDs and confluence
Simon PeytonJones
simonpj at microsoft.com
Mon Apr 10 12:58:04 EDT 2006
Interesting! It'd be great if you've found a simpler more uniform rule.
(Which you seem to be getting rather good at.) Let's see if you can
convince Martin, first, and then articulate the proposed rules. I'll
look fwd to that.
Simon
 Original Message
 From: haskellprimebounces at haskell.org
[mailto:haskellprimebounces at haskell.org] On Behalf Of
 Ross Paterson
 Sent: 10 April 2006 09:53
 To: haskellprime at haskell.org
 Subject: FDs and confluence

 (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 cutdown
 version of Ex. 18 from the FDCHR 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)

 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.

 _______________________________________________
 Haskellprime mailing list
 Haskellprime at haskell.org
 http://haskell.org/mailman/listinfo/haskellprime
More information about the Haskellprime
mailing list