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

[Martin Sulzmann]

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