[Haskell-cafe] looking for examples of non-full Functional
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.
- 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.
Iavor Diatchki wrote:
> 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 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
> 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.
>> 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
>> The motivation for this condition is to avoid inconsistencies when
>> deriving improvement rules from instances.
>> 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.
More information about the Haskell-Cafe