Hello, On Thu, Apr 17, 2008 at 12:05 PM, Martin Sulzmann <[EMAIL PROTECTED]> 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 > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe