[still talking to myself..?]
all confluence problems in the FD-CHR paper, as far as they were
not due to instances inconsistent with the FDs, seem to be due to
conflicts between improvement and inference rules. we restore
confluence by splitting these two constraint roles, letting inference
and improvements work on constraints in separate roles, thus
removing the conflicts.
I should have mentioned that the improved confluence obtained by
separating the dimensions of FD-based improvement and instance
inference buys us a lot more than just permitting more valid programs
(compared to the original, incomplete CHR):
- separating the two dimensions of inference and improvement leads
to better confluence (implementations are no longer forced to
iterate improvement before continuing inference; fewer conservative
restrictions are needed in the static semantics of TC; more valid
code can be accepted)
- better confluence guarantees that all improvement rules that apply will
be run eventually, which means that the new CHR is self-checking
wrt FD consistency!
[if consistency is violated, there are at least two instances with
different FD range types for the same FD domain types; that
means there will be two instance improvement rules with the
same lhs, but different equations on their rhs; if any constraint
arises that would run into the FD inconsistency by using one
of those improvement rules, the other will cause the derivation
to fail]
we can see this in action by looking at the relevant example of the
FD-CHR paper (last revised Feb2006), section 5.1 Confluence,
example 5:
class Mul a b c | a b -> c
instance Mul Int Float Float
instance Mul Int Float Int
the old CHR for this example (which violates FD consistency) is
not confluent, allowing derivation of both c=Float and c=Int for
the constraint Mul Int Float c. the revised paper still claims that
consistency is "inuitively necessary" to guarantee confluence (it
also still claims that it isn't sufficient, referring to the example we
dealt with in the previous email).
but if we apply the new Tc2CHR translation, we obtain a
confluent CHR for the same example (there doesn't appear
to be a way to switch off the consistency check in GHC, so
I had to translate the two instances separately..):
mul(A,B,C) <=> infer_mul(A,B,C), memo_mul(A,B,C).
/* functional dependencies */
memo_mul(A,B,C1), memo_mul(A,B,C2) ==> C1=C2.
/* instance inference: */
infer_mul(int,float,float) <=> true.
infer_mul(int,float,int) <=> true.
/* instance improvements: */
memo_mul(int,float,C) ==> C=float.
memo_mul(int,float,C) ==> C=int.
now, if we consider the problematic constraint again, and its two
initially diverging derivations, we see that the derivations can be
rejoined, exposing the inconsistency:
mul(int,float,C)
<=> infer_mul(int,float,C), memo_mul(int,float,C)
[
==> infer_mul(int,float,C), memo_mul(int,float,C), C=float
<=> true, memo_mul(int,float,float), C=float
==> memo_mul(int,float,float), C=float, float=int
|
==> infer_mul(int,float,C), memo_mul(int,float,C), C=int
<=> true, memo_mul(int,float,int), C=int
==> memo_mul(int,float,int), C=int, int=float
]
<=> fail
this dynamic safety does not mean that we should drop the
consistency check in the static semantics completely! but whereas
the old CHR translation _depends_ on the consistency check for
safety, and is therefore stuck with it, the new translation gives us
some manouvering space when we try to relax that check to
account for the combination of overlap resolution and FDs.
cheers,
claus
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
