there is no implication that d=Bool (you could add:
'instance B a b => C [a] b Char' without violating
FD consistency).
These instances (alpha-renamed):
instance B a1 b1 => C [a1] b1 Bool
instance B a2 b2 => C [a2] b2 Char
violate the consistency condition: a substitution that unifies a1 and
a2 need not unify b1 and b2, because the consistency condition makes
no mention of the contexts. (If it did, the instance improvement rule
would be invalid.)
??
the consistency condition does mention b1 and b2 as t_b and s_b, so
any substitution that unifies a1 and a2 (t_a and s_a) needs to unify b1
and b2, independent of context.
note also that we are talking about different things here: I am talking about
FD consistency, you are talking about the FD consistency condition.
let's be concrete:
class B a b | a -> b
class C a b c | a -> b
instance B a1 b1 => C [a1] b1 Bool
instance B a2 b2 => C [a2] b2 Char
with these declarations, you are concerned about constraints
C [a] b Bool,C [a] c Char, which you claim are substitution instances
of these declaration heads even if b and c differ. but the class instances
of class C are constrained by an FD, and if b and c differ, these two
constraints are _not_ substitution instances under that FD. they would
be substitution instances if that FD wasn't there (*).
the FD consistency condition is an approximation of FD consistency,
and it is a strange approximation at that, because it is neither sufficient
nor necessary (with the alternative CHR translation) for consistency:
- if all instance declarations fulfill the FD consistency condition, the
constraint store may still be inconsistent, because it may represent
an inconsistent query; so the condition is not sufficient
- one of the bonuses of a confluent CHR is that deductions on
inconsistent stores will not terminate successfully (if they terminate,
they are certain to fail), so the condition is not necessary, either
[it was with the old translation, though]
as this example shows once again, there are instance declarations
for which the FD consistency condition, as currently interpreted by
Hugs, fails, even though no inconsistent constraints are implied. so I
fail to see the point of continuing to require the FD consistency
condition in unrevised form.
but my point was that there is no confluence problem. everything
else, with the exception of termination, follows from there.
cheers,
claus
(*) this is similar to patterns and guards in the expression language,
for instance:
f a = .. -- some function
c [a1] b1 Bool | b1 == f [a1] = b a1 b1
c [a2] b2 Char | b2 == f [a2] = b a2 b2
now, c [a] b1 Bool and c [a] b2 Char are defined if (b1==f [a])
and (b2==f [a]) and if b a b1 and b a b2 are defined as well.
c [a] d Bool with (d/=f[a]) matches the pattern, but fails the
guard, so it is not a substitution instance of c's left hand sides
under the guard.
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
