[Haskell-cafe] looking for examples of non-full Functional
Dependencies
Martin Sulzmann
martin.sulzmann at gmail.com
Fri Apr 18 14:04:30 EDT 2008
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
>>
>>
>>
More information about the Haskell-Cafe
mailing list