FDs and confluence

[Ross Paterson]

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.