On Mon, Apr 10, 2006 at 02:39:18PM +0100, Claus Reinke wrote:
class B a b | a -> b class C a b c | a -> b
instance B a b => C [a] b Bool
Starting from a constraint set C [a] b Bool, C [a] c d, [...]
CHR-alt:
B a b <=> infer_B a b, memo_B a b. memo_B a b1, memo_B a b2 ==>b1=b2.
C a b c <=> infer_C a b c, memo_C a b c. memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2. infer_C [a] b Bool <=> B a b. memo_C [a] b' c' ==> b'=b.
OK, so you want to modify the usual instance reduction rule by recording functional dependencies from the head. That is, you get confluence by remembering all the choices you had along the way, so you can still take them later. My problem with this scheme is that it makes FDs an essential part of the semantics, rather than just a shortcut, as they are in the original system. With the old system, one can understand instances using a Herbrand model, determined by the instance declarations alone. If the instances respect FDs, types can be made more specific using improvement rules justified by that semantics. With your system, there's only the operational semantics. To understand types, programmers must operate the rewriting system. And the constraint store they must work with will be quite cluttered with all these memoized FDs.