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

I now recall the reason for NOT using D a b, D [a] c ==> c = [b] The reason is that the above rule creates a new critical pair with instance D a b => D [a] [b] To resolve the critical pair we need yet another rule D a b, D [[a]] c ==> c =[[b]] You can already see where this leads to. In general, we need an infinite rules of the form D a b, D [a]^k c ==> c = [b]^k where [a]^k stands for the k nested list [ ... [a] ... ] The FD-CHR approach therefore proposes to use D [a] c ==> c = [b] which is a "stronger" rule (that is, is not a logical consequence). Martin Martin Sulzmann wrote:

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 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