On Thu, Mar 02, 2006 at 12:03:59PM -0000, Claus Reinke wrote:
The way I interpret FDs implies that they introduce a systematic space
leak into the inference process: if any stage in the inference uses *any*
constraint with a class which is subject to an FD, that results in an
additional bit of information about that class' FD. and we *cannot*
throw that bit of information away unless we know that we will
never need to refer to it in the remainder of the inference chain.
But with the current system you can throw it away, because it's implied
by the FDs on the classes in the context. A system where that was
not the case would be significantly more complex than the current FDs,
which I think disqualifies it for Haskell'.
I'm not sure what FD system you are referring to here? in the CHR
representation of FDs (which seems to be the only candidate for
Haskell'), you _cannot_ throw this information away, and the
potential of doing so accounts for the majority of confluence
violations in the paper "understanding FDs via CHRs": if you simplify
a constraint before using it for propagation, you end up missing
some improvements and you may not be able to rejoin the diverging
deductions.
that's what I was referring to: there shouldn't be any confluence
problems with the original code (type classes w FDs), but there are
confluence problems with the CHRs used to represent that code!
the worst example of that is example 14 (fragment of a type-directed
evaluator), for which the paper's CHR translation is _not_ confluent,
and for which the paper suggests that adding coverage would be
sufficient to guarantee confluence, but coverage is violated.. (cf also
the end of section 6, where a variant of example 14 without the
class-FD-CHR is considered to avoid non-confluence, but the
result doesn't support improvement as well as expected).
the two diverging deductions given on p21 correspond to doing
both simplifications first, thus disabling propagation (throwing
away the FD-related information), or first doing propagation
(accounting for the FD-related info), then doing simplifications.
in the system I suggested, confluence would not depend on
coverage, because the two roles of constraints (inference and
FDs) would be treated separately, and the FD-related info
would always be available for propagation (implied by the class
FDs), even after doing the simplification steps first. so the
translation I'd like to see would be _simpler_ (having fewer
problems) than the current candidate.
the translation into CHRs would be something like:
class C a b | a -> b
instance ctxt => C t1 t2
-->
C a b <=> infer_C a b, memo_C a b. (two roles)
infer_C a b <=> ctxt. (instance inference)
memo_C a b1, memo_C a b2 => b1=b2. (class FD)
so there'd be one preparatory inference rule to split all constraints
occurring in the process into their two roles, one inference rule for
each instance declaration, and one propagation rule for each FD.
the CHR succeeds if there are no non-memo constraints left.
the Chameleon implementation appears to be in a transitory state,
but if we forgoe Haskell syntax, there are lots of other free CHR
implementations around, especially with Prolog systems:
http://www.cs.kuleuven.ac.be/~dtai/projects/CHR/chr-impl.html
I append a translation of example 14 into CHR that works, eg,
with SWI Prolog. it quite can't succeed for the example call from
the paper
eval(Env,expabs(X,Exp),T1),eval(Env,expabs(X,Exp),T2).
because the code fragment doesn't contain all instances; so one
infer-constraint remains in the final store, but it should still be
confluent, no matter whether you treat inference or FDs first.
cheers,
claus
:- module(tc,[eval/3]).
:- use_module(library(chr)).
:- chr_constraint eval/3,infer_eval/3,memo_eval/3.
/* accounting for the FD */
memo_eval(Env,Exp,T1), memo_eval(Env,Exp,T2) ==> T1=T2.
/* separating proof and FD aspects */
eval(Env,Exp,T) <=> infer_eval(Env,Exp,T), memo_eval(Env,Exp,T).
/* accounting for the instance */
infer_eval(Env,expabs(X,Exp),V) <=>
V=to(V1,V2), eval(cons((X,V1),Env),Exp,V2).
/* removing duplicate constraints */
infer_eval(Env,Exp,T) \ infer_eval(Env,Exp,T) <=> true.
memo_eval(Env,Exp,T) \ memo_eval(Env,Exp,T) <=> true.
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
