the first patch I found myself:-) I forgot to account for superclasses: diff -rN old-chr/tc2chr.txt new-chr/tc2chr.txt 24c24 < -> TC a b <=> infer_TC a b, memo_TC a b. (two roles) ---
-> TC a b <=> infer_TC a b, memo_TC a b, C. (two roles +superclasses)
186c186 < B = bool <-- determined by superclass fd ---
B = bool <-- determined by instance context fd
--------------------------------------------------- this was not entirely accidental, though. I'd been thinking about that old reverse-the-superclass-arrow issue, and I now find to my surprise that the authors of the FD-CHR papers agree with me on this issue, even though they claim not to!-) recall the ancient folklore that a superclass constraint class C => TC ought to be interpreted as the reverse implication between the type predicates (and so the superclass arrow ought to be reversed): TC |- C we rehashed that argument only last month on this very list ("The worst piece of syntax in Haskell" and "superclass implications"), and, once again, I felt fairly lonely when I said that the implication could indeed be interpreted as an implication (either by considering two phases of checks, as in Haskell at the moment, or by accepting more programs as valid). now, the FD-CHR authors appear to be firmly in the reverse-the-arrow camp: 1) For each class C => TC t we generate a propagation CHR rule TC t ==> C Ex: class Eq a => Ord a translates to rule Ord a ==> Eq a ... BTW, 1) shows that the superclass arrow should indeed be the other way around .. http://www.haskell.org//pipermail/haskell-prime/2006-February/000798.html however, while fixing the superclass omission in my alternative translation, I finally remembered that arrows are not arrows! in qualified types, we're talking about predicate entailment, ie, when we have the class predicate, we can infer the superclass predicate. in CHR, we're talking about adding and removing _proof obligations_ to/from the constraint store, ie, that propagation rule says: when we need to prove the class constraint, we also need to prove the superclass constraint. in other words, the CHR translations treat the superclass constraints as a pre-condition of the class constraints, just as the superclass arrow in the Haskell syntax suggests, not as a consequence! how can that be right, you might ask? the way the class CHR works, (a) it can never be used to infer the validity of the superclass constraints from the validity of the class constraint (b) it generates a proof obligation for the superclass constraints whenever the class constraint is considered the point to note here are the conditions that Haskell places the validity of instance declarations. these imply that (a) is never needed, because the system has already checked that the superclass constraints can be inferred without adding that extra implication, which also means that (b) is always going to succeed if the the class constraint can be discharged. that alone is surprising enough - it seems to indicate that the reverse-the-arrow campaign was a red herring!-) why then, is that class CHR needed in the original translation to CHR, and why do I have to add something similar to my alternative translation? we know that the proof obligaton has already been discharged by the validity check, but we need to connect the class constraint to the superclass constraints in order to inherit any FD information. in fact, it is noted in the earlier "theory of overloading" paper that without those validity checks, the original translation into CHR would not give a confluent rule system, as class CHR and instance CHR form a critical pair (using the instance CHR before the class CHR disables the latter, preventing use of superclass FD info). cheers, claus