[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlappinginstances: a bug?]

[Claus Reinke]

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