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/
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
