relaxed instance rules spec (was: the MPTC Dilemma(pleasesolve))

[Claus Reinke]

> 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.