alternative translation of type classes to CHR (was: relaxedinstance rules spec)

[Claus Reinke]

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