The main focus of the FD paper is how to restore confluence which is important for complete inference.
That is indeed my second major problem with the paper!-) There are examples in the paper that show how some conditions are sufficient to ensure confluence, but they hardly ever seem to be necessary for the original program, only for the current mapping. 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. As I mentioned before, capturing this is the one point where I can imagine an advantage of using CHRs, by putting the "memo-table" for the type function implied by an FD into the global constraint store. So I was rather surprised to see the way FDs are currently mapped into CHRs. And indeed, as far as I noticed, *nearly all* the confluence problems are due to that mapping, not due to FDs. In a way, it is nice that loosing confluence shows up cases where information about an FD may be thrown away while there are still opportunities to use it, but since confluence is hard to check without termination, that doesn't really help in practice unless we take it as an additional reason to want guaranteed termination.. So, why not get rid of that problem and clearly model the memo effect of FDs as an aspect separable from the instance constraint? class C a b | a -> b instance Ctxt => C t1 t2 in the current mapping, the class FD CHR needs two constraints for C to generate an equation for the two b parameters, but the instance simplification rules may take constraints away before that class FD CHR was applied, resulting in the danger of non-confluence. the instance FD CHRs, instead, need only a single constraint to generate an equation, because they compare that constraint to one of the instances. still, the constraint might be simplified away before its instance FD CHR was applied. this is slightly less risky, because any new constraint that might profit from the information we threw away is itself subject to the instance FD CHR. but it still results in the danger of non-confluence, corresponding to ignoring some information about the class' FD contributed by independent constraints "communicating" via the same instance FD CHR! the paper suggests not generating the class FD CHR in the first place, or restricting the order in which rules may be applied. but why not encode the memo aspect of FDs directly in the constraint store? we'd have to represent _separately_ the constraints that need to be proven, and the memo aspect of those constraints we _have used_ at any point in the deduction. for the class C above, something roughly like this (tweak as needed;): (instance FD) rule C t1 t2 <==> Ctxt, MEMO-C t1 t2 (class FD) rule C t1 t2, MEMO-C t1 t3 ==> t2==t3 note that the (instance FD) CHR could also be called the (constraint FD) CHR, because it triggers whenever any constraint is simplified using a specific instance declaration in the inference. unlike the current instance improvement CHR, which hard-codes the part of the information gathered from the instance declaration, this mapping separates the generation and use of FD information, but ties the generation to simplification. unlike ordinary constraints, MEMO constraints no longer imply proof obligations in terms of instance inference, they just record a type dependency that has been used in a simplification step. if my understanding of propagation rules in CHR is correct, applications of the class FD CHR will preserve that recorded information, so there will always be a second constraint to compare with when we want to use FDs to generate equations. I'm not entirely sure how consistency of constraints is checked in CHR - we may need to add a rule that exposes inconsistent MEMO constraints: (inconsistent FD) rule MEMO-C t1 t2, MEMO t1 t3 ==> t2/=t3 | YELL!-) am I on the right track here? cheers, claus