Hi Mark,
Declaration Formula ----------- ------- class Eq a => Ord a forall a. Ord a => Eq a instance Eq a => Eq [a] forall a. Eq a => Eq [a] class C a b | a -> b forall a, b. C a b /\ C a c => b = c
This correspondence between declarations and formulas seems to be very similar to what you did in the paper using CHRs. I haven't read the paper carefully enough to know what extra mileage and/or problems you get by using CHRs. To me, predicate logic seems more natural, but I don't think that matters here---I just wanted to acknowledge that essentially the same idea is in your paper.
i wondered about that "extra mileage" question when i first encountered chrs and the fd-to-chr translations - here's my take on it: while chr started out with a predicate logic semantics, it helps to think of them as representing a subset of linear logic instead (which is where recent chr semantics are headed). other relevant aspects are: committed choice language (no reliance on backtracking), no implicit unification (left-hand sides of rules are matched, unification has to be called explicitly in right-hand sides, *after* committing to a rule). what is helpful about using chr, then, is that they are closer to implementations of functional dependencies, making it easier to expose/discuss some general issues relevant to implementations but not to abstract semantics (such as incomplete and changing knowledge due to separate compilation, or some implementations risking to lose information), without having to wade through all other implementation-level details. in other words, chr expose a few more details, so more things can go wrong; which is useful, because one can discuss how to avoid these wrongs, providing more concrete guidelines for implementations. they also avoid exposing details not (currently) relevant to the application, as a mapping to prolog would.
I don't dispute your claim that fullness is necessary to establish confluence with CHRs. But that is a consequence of the formal proof/rewrite system that you're using, and not of the underlying semantics.
i tried to argue that case (the confluence issues are due to the translation, not inherent in functional dependencies) last year, even suggested an alternate translation of fd to chr. something like this (the 'TC a b' should be 'TC a1..an', i think, and the notation is meant to correspond to figure 2 in the jfp paper): http://www.haskell.org//pipermail/haskell-prime/2006-March/000893.html simplifying slightly, the alternate translation uses an embedding of classical into linear logic, so knowledge about fds never decreases as long as it remains consistent, whereas the jfp paper translation works directly in a linear logic (<==> is like linear implication -o, consuming its pre-conditions), so applying inference steps in the "wrong" order can lose knowledge about fds, leading to loss of confluence (unless additional restrictions are introduced). if i recall correctly, the paper also relied on confluence as one possible means to ensure termination, meaning that results about termination or results relying on termination were to some extent tied up with the extra conditions used to ensure confluence. i believe that fixing the translation to chr would get rid of the confluence issues discussed in the paper alltogether, so it could have focussed on the remaining issues, like termination, without distraction. frustratingly, while the paper was still a draft at the time, the discussion came too late to have an impact on the version published in jfp. hope this helps, claus