Changes between Version 1 and Version 2 of FunDeps


Ignore:
Timestamp:
Jan 5, 2013 8:42:55 PM (18 months 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}}}