Changes between Version 1 and Version 2 of FunDeps


Ignore:
Timestamp:
Jan 5, 2013 8:42:55 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • FunDeps

    v1 v2  
    1 Consistency of Functional Dependencies
    2 --------------------------------------
     1= Consistency of Functional Dependencies =
    32
    43The functional dependencies on a class restrict the instances that may
    54be declared for a given class.  The instances of a class:
    6 
     5{{{
    76    class C a b c | b -> c where f :: ...
    8 
     7}}}
    98are consistent with its functional dependency if the following invariant holds:
    10 
     9{{{
    1110    byFD(C,1): forall a1 a2 b c1 c2. (C a1 b c1, C a2 b c2) => (c1 ~ c2)
    12 
     11}}}
    1312Please note that the question of FD-consistency is orthogonal to
    1413instance coherence (i.e, uniqueness of evidence, overlapping instances,
     
    2221
    2322For example, if we have an instance:
    24 
     23{{{
    2524  I: instance F Int Int Char
    26 
     25}}}
    2726and we have a constraint `C: F Int Int a`, then we can use the
    2827FD-invariant to prove that `a` must be `Char`:
     28{{{
     29    byFD(C,1) (C,I) :: a ~ Char
     30}}}
    2931
    30     byFD(C,1) (C,I) :: a ~ Char
    31 
    32 
    33 Checking FD-Consistency
    34 -----------------------
     32== Checking FD-Consistency ==
    3533
    3634To ensure FD-consistency, before accepting an instance we need to check
     
    3937imported instances.  Consider adding a new instance to an FD-consistent
    4038set of instances:
    41 
     39{{{
    4240    I: instance P(as,bs) => C t1(as,bs) t2(as) t3(as,bs)
    43 
     41}}}
    4442The notation `t(as)` states the variables in `t` are a subset of `as`.
    4543
     
    4745     instantiations of `I` to violate FD-consistency).  Self consistency
    4846     follows if we can prove the following theorem:
    49 
     47{{{
    5048         forall as bs cs. (P, P[cs/bs]) => t3[cs/bs] ~ t3[cs/bs]
    51 
     49}}}
    5250  2. Check that `I` is FD-consistent with all existing instances of the class.
    5351     So, for each existing instance, `J`:
    54 
     52{{{
    5553         J: instance Q(xs) => C s1(xs) s2(xs) s3(xs)
    56 
     54}}}
    5755     we need to show that:
    58 
     56{{{
    5957         forall as bs xs. (P,Q,s2 ~ t2) => (s3 ~ t3)
    60 
     58}}}
    6159     Assuming no type-functions in instance heads, the equality
    6260     assumption is equivalent to stating that `s2` and `t2` may be
    6361     unified, so another way to state our goal is:
    64 
     62{{{
    6563         forall as bs xs. (P[su], Q[su]) => (s3[su] ~ t3[su])
    66 
     64}}}
    6765     where `su` is the most general unifier of `s2` and `t2`.
    6866
     
    7472the FD-consistency follows trivially.
    7573
    76 Examples
    77 --------
     74== Examples ==
     75
    7876
    7977  * FD-consistency is orthogonal to instance coherence.
    8078
    8179     FD-consistent but not coherent:
    82 
     80{{{
    8381         instance C Int Int Int where f = definition_1
    8482         instance C Int Int Int where f = definition_2
    85 
     83}}}
    8684     Coherent but not FD-consistent:
    87 
     85{{{
    8886         instance C Int  Int Char where ...
    8987         instance C Char Int Bool where ...
    90 
     88}}}
    9189   * FD-consistency is orthogonal to termination of instances.
    9290
    9391     FD-consistent but "non-terminating":
    94 
     92{{{
    9593         instance C a b c => C a b c
    96 
     94}}}
    9795     Terminating but not FD-consistent:
    98 
     96{{{
    9997         instance C Int  Int Char where ...
    10098         instance C Char Int Bool where ...
    101 
    102 
     99}}}