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

[Claus Reinke]

[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