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

[Iavor Diatchki]

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