[Haskell-cafe] looking for examples of non-full Functional
Dependencies
Martin Sulzmann
martin.sulzmann at gmail.com
Mon Apr 21 06:44:09 EDT 2008
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
>> <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