Changes between Version 1 and Version 2 of FunDeps
 Timestamp:
 Jan 5, 2013 8:42:55 PM (3 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

FunDeps
v1 v2 1 Consistency of Functional Dependencies 2  1 = Consistency of Functional Dependencies = 3 2 4 3 The functional dependencies on a class restrict the instances that may 5 4 be declared for a given class. The instances of a class: 6 5 {{{ 7 6 class C a b c  b > c where f :: ... 8 7 }}} 9 8 are consistent with its functional dependency if the following invariant holds: 10 9 {{{ 11 10 byFD(C,1): forall a1 a2 b c1 c2. (C a1 b c1, C a2 b c2) => (c1 ~ c2) 12 11 }}} 13 12 Please note that the question of FDconsistency is orthogonal to 14 13 instance coherence (i.e, uniqueness of evidence, overlapping instances, … … 22 21 23 22 For example, if we have an instance: 24 23 {{{ 25 24 I: instance F Int Int Char 26 25 }}} 27 26 and we have a constraint `C: F Int Int a`, then we can use the 28 27 FDinvariant to prove that `a` must be `Char`: 28 {{{ 29 byFD(C,1) (C,I) :: a ~ Char 30 }}} 29 31 30 byFD(C,1) (C,I) :: a ~ Char 31 32 33 Checking FDConsistency 34  32 == Checking FDConsistency == 35 33 36 34 To ensure FDconsistency, before accepting an instance we need to check … … 39 37 imported instances. Consider adding a new instance to an FDconsistent 40 38 set of instances: 41 39 {{{ 42 40 I: instance P(as,bs) => C t1(as,bs) t2(as) t3(as,bs) 43 41 }}} 44 42 The notation `t(as)` states the variables in `t` are a subset of `as`. 45 43 … … 47 45 instantiations of `I` to violate FDconsistency). Self consistency 48 46 follows if we can prove the following theorem: 49 47 {{{ 50 48 forall as bs cs. (P, P[cs/bs]) => t3[cs/bs] ~ t3[cs/bs] 51 49 }}} 52 50 2. Check that `I` is FDconsistent with all existing instances of the class. 53 51 So, for each existing instance, `J`: 54 52 {{{ 55 53 J: instance Q(xs) => C s1(xs) s2(xs) s3(xs) 56 54 }}} 57 55 we need to show that: 58 56 {{{ 59 57 forall as bs xs. (P,Q,s2 ~ t2) => (s3 ~ t3) 60 58 }}} 61 59 Assuming no typefunctions in instance heads, the equality 62 60 assumption is equivalent to stating that `s2` and `t2` may be 63 61 unified, so another way to state our goal is: 64 62 {{{ 65 63 forall as bs xs. (P[su], Q[su]) => (s3[su] ~ t3[su]) 66 64 }}} 67 65 where `su` is the most general unifier of `s2` and `t2`. 68 66 … … 74 72 the FDconsistency follows trivially. 75 73 76 Examples 77  74 == Examples == 75 78 76 79 77 * FDconsistency is orthogonal to instance coherence. 80 78 81 79 FDconsistent but not coherent: 82 80 {{{ 83 81 instance C Int Int Int where f = definition_1 84 82 instance C Int Int Int where f = definition_2 85 83 }}} 86 84 Coherent but not FDconsistent: 87 85 {{{ 88 86 instance C Int Int Char where ... 89 87 instance C Char Int Bool where ... 90 88 }}} 91 89 * FDconsistency is orthogonal to termination of instances. 92 90 93 91 FDconsistent but "nonterminating": 94 92 {{{ 95 93 instance C a b c => C a b c 96 94 }}} 97 95 Terminating but not FDconsistent: 98 96 {{{ 99 97 instance C Int Int Char where ... 100 98 instance C Char Int Bool where ... 101 102 99 }}}