[Haskell-cafe] looking for examples of non-full Functional Dependencies

[Martin Sulzmann]

Thanks Iavor! Things become now clear.

Let's consider our running example

class D a b | a -> b
instance D a b => D [a] [b]

which we can write in CHR notation

D a b, D a c ==> b=c    (FD)

D [a] [b] <=> D a b       (Inst)

These rules overlap.

Let's consider the critical pair

D [a] [b], D [a] c

The following two derivations are possible

                D [a] [b], D [a] c
   -->FD   D [a] [b], c = [b]
   -->Inst   D a b, c = [b]


               D [a] [b], D [a] c
   -->Inst D a b, D [a] c

The two final stores differ which means that the
CHR system is non-confluent. Hence, the
proof theory is (potentially) incomplete.
What does this mean?
Logically true statement may not be derivable
using our CHR/typeclass-FD solver.

Iavor suggests to add the rule

D [a] c, D a b ==> c = [b]    (Imp1)

Makes perfect sense!

This rule is indeed a theorem and makes the system confluent.

But that's not what the FD-CHR paper does.

The FD-CHR paper generates the "stronger" rule

D [a] c ==> c = [b]     (Imp2)

This rule is NOT a theorem (ie logical consequence from the
FD and Inst rule).
But this rule also makes the system confluent.

Why does the FD-CHR paper suggest this rule.
Some reasons:

 - the (Imp2) matches the GHC and I believe also Hugs implementation
 - the (Imp2) is "easier" to implement, we only need to look for
   a single constraint when firing the rule
- (Arguable) The (Imp2) matches better the programmer's intuition.
   We only consider the instance head when generating improvement
   but ignore the instance context.
- (Historical note: The rule suggested by Iavor were discussed
   when writing the FD-CHR paper but somehow we never
   pursued this alternative design space.
   I have to dig out some old notes, maybe there some other reasons,
   infinite completion, why this design space wasn't pursued).

To summarize, I see now where the confusion lies.
The FD-CHR studies a "stronger" form of FDs where the CHR
improvement rules generated guarantee confluence but the
rules are not necessarily logical consequence.
Therefore, the previously discussed property

  a -> b and a -> c iff a -> b c

does of course NOT hold. That is,
the combination of improvement rules derived from a -> b and a -> c
is NOT equivalent to the improvement rules derived from a -> b c.
Logically, the equivalence obviously holds.

Martin


Iavor Diatchki wrote:
> Hello,
>
> On Thu, Apr 17, 2008 at 12:05 PM, Martin Sulzmann
> <martin.sulzmann at gmail.com> wrote:
>   
>>  Can you pl specify the improvement rules for your interpretation of FDs.
>> That would help!
>>     
>
> Each functional dependency on a class adds one extra axiom to the
> system (aka CHR rule, improvement rule).  For the example in question
> we have:
>
> class D a b | a -> b where ...
>
> the extra axiom is:
>
> forall a b c. (D a b, D a c) => (b = c)
>
> This is the definition of "functional dependency"---it specifies that
> the relation 'D' is functional.  An improvement rule follows from a
> functional dependency if it can be derived from this rule.  For
> example, if we have an instance (i.e., another axiom):
>
> instance D Char Bool
>
> Then we can derive the following theorem:
>
> (D Char a) => (a = Bool)
>
> I think that in the CHR paper this was called "instance" improvement.
> Note that this is not an extra axiom but rather a theorem---adding it
> to the system as an axiom does not make the system any more
> expressive.  Now consider what happens when we have a qualified
> instance:
>
> instance D a a => D [a] [a]
>
> We can combine this with the FD axiom to get:
>
> (D a a, D [a] b) => b = [a]
>
> This is all that follows from the functional dependency.  Of course,
> in the presence of other instances, we could obtain more improvement
> rules.
>
> As for the "consistency rule", it is intended to ensure that instances
> are consistent with the FD axiom.  As we saw from the previous
> examples, it is a bit conservative in that it rejects some instances
> that do not violate the functional dependency.   Now, we could choose
> to exploit this fact to compute stronger improvement rules---nothing
> wrong with that.  However, this goes beyond FDs.
>
> -Iavor
>
>
>
>
>
>
>
>
>   
>>  I'm simply following Mark Jones' style FDs.
>>
>>  Mark's ESOP'00 paper has a consistency condition:
>>  If two instances match on the FD domain then the must also match on their
>> range.
>>  The motivation for this condition is to avoid inconsistencies when
>>  deriving improvement rules from instances.
>>
>>  For
>>     
>
>
>   
>>  class D a b | a -> b
>>
>>  instance D a a => D [a] [a]
>>  instance D [Int] Char
>>
>>
>>  we get
>>
>>  D [a] b ==> b =[a]
>>  D [Int] b ==> b=Char
>>
>>  In case of
>>
>>  D [Int] b we therefore get b=Char *and* b =[a] which leads to a
>> (unification) error.
>>  The consistency condition avoids such situations.
>>
>>
>>  The beauty of formalism FDs with CHRs (or type functions/families) is that
>>  the whole improvement process becomes explicit. Of course, it has to match
>>  the programmer's intuition. See the discussion regarding multi-range FDs.
>>
>>  Martin
>>
>>
>>