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

[Claus Reinke]

a second oversight, in variation B: CHR rules are selected by matching, 
not by unification (which is quite essential to modelling the way type 
class inference works). this means that the idea of generating memo_
constraints for the instance fdis and relying on the clas fdi rules to
use that information is not going to work directly. 

however, we can look at the intended composition of those fdi instance
rules with the fdi class rules, and specialize the latter when applied to 
the rhs of the former (assuming unification while doing so).

!!
the nice thing about this is that variation B now looks very much like
the original translation, differing only in the splitting of roles, without
any other tricks merged in. that means it should now be more obvious
why variation B is a modification of the original translation with better
confluence properties. 

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.

============= Tc2CHR alternative, with separated roles

    class C => TC a1..an | fd1,..,fdm

    where fdi is of the form: ai1..aik -> ai0

    ->  TC a b <=> infer_TC a b, memo_TC a b, C. (two roles +superclasses)

    ->  memo_TC  a1..an, memo_TC th(b1)..th(bn) => ai0=bi0. (fdi)

         where th(bij) | j>0 = aij
               th(bl)  | not (exists j>0. l==ij) = bl 

============= Variation B (separate instance inference/FD improvement):

    instance C => TC t1..tn

    -> infer_TC t1..tn <=> C.   (instance inference)

    -> memo_TC th(b1)..th(bn) => ti0=bi0. (fdi instance improvement)

         where th(bij) | j>0 = tij
               th(bl)  | not (exists j>0. l==ij) = bl 

=============================================

in particular, the new CHRs for examples 14 and 18 (coverage violations,
hence not variable-restricted, hence confluence proof doesn't apply)
should now be confluent, because even after simplification, we can still use 
the class FDs for improvement.

here are the relevant rules for example 14:

    /* one constraint, two roles + superclasses */
    eval(Env,Exp,T) <=> infer_eval(Env,Exp,T), memo_eval(Env,Exp,T), true.

    /* functional dependencies */
    memo_eval(Env,Exp,T1), memo_eval(Env,Exp,T2) ==> T1=T2.

    /* instance inference: */
    infer_eval(Env,expAbs(X, Exp),to(V1, V2)) <=> eval(cons((X, V1), Env), Exp, V2).

    /* instance improvements: */
    memo_eval(Env_,Exp_,T_) ==> T_=to(V1, V2).

and the troublesome example constraints:

    eval(Env,expAbs(X,Exp),T1), eval(Env,expAbs(X,Exp),T2).
->
    infer_eval(Env,expAbs(X,Exp),T1), infer_eval(Env,expAbs(X,Exp),T2), 
    memo_eval(Env,expAbs(X,Exp),T1), memo_eval(Env,expAbs(X,Exp),T2).

[
-> [class FD first]
    infer_eval(Env,expAbs(X,Exp),T2), memo_eval(Env,expAbs(X,Exp),T2),
    T1=T2.
|
-> [instance improvement and simplification first]
    eval(cons((X,V11),Env),Exp,V12), eval(cons((X,V21),Env),Exp,V22), 
    memo_eval(Env,expAbs(X,Exp),T1), memo_eval(Env,expAbs(X,Exp),T2),
    T1=to(V11,V12), T2=to(V21,V22).
]

-> [rejoin inferences]
    eval(cons((X,V21),Env),Exp,V22), 
    memo_eval(Env,expAbs(X,Exp),T2),
    T1=T2, T2=to(V21,V22).
-> ..

cheers,
claus

ps I've only listed the updated variation B here, to limit confusion. if you 
    want the updated code and full text, you should be able to use

    darcs get http://www.cs.kent.ac.uk/~cr3/chr/