Changes between Version 12 and Version 13 of FunctionalDependencies
 Timestamp:
 Feb 12, 2006 12:33:45 AM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

FunctionalDependencies
v12 v13 32 32 * AssociatedTypes seem to be more promising. 33 33 34 == Details ==34 == Variations == 35 35 36 === Restrictions on instances===36 === Original version === 37 37 38 The original paper imposed two restrictions on instances (sect. 6.1), stated here for the class `C` declared above: 38 Suppose a class ''C'' has a functional dependency ''X'' `>` ''Y''. 39 The original paper imposed two restrictions on instances of the class ''C'' (sect. 6.1): 39 40 40 41 1. For any instance 41 42 {{{ 42 instance ... => C Ta Tb Tc43 instance ... => C t 43 44 }}} 44 any variable occurring free in Tb must also occur free in Ta.45 any variable occurring free in t,,Y,, must also occur free in t,,X,,. 45 46 2. If there is a second instance 46 47 {{{ 47 instance ... => C Sa Sb Sc48 instance ... => C s 48 49 }}} 49 then any substitution unifying Ta and Sa must also unify Tb and Sb.50 then any substitution unifying t,,X,, with s,,X,, must also unify t,,Y,, with s,,Y,,. 50 51 51 52 Haskell 98 requires that the context of an instance declaration use only type variables that appear in the head. 52 53 It was originally thought that this could be relaxed (original paper, sect. 6.3), to variables determined by those in the head, but this can lead to nontermination (CHR paper, ex. 15). 54 53 55 With FlexibleInstances and no OverlappingInstances, these restrictions yield a coherent and decidable system (CHR paper, corr. 1). 54 56 55 However the first restriction forbids instances like the following from the monad transformer library: 57 === GHC and Hugs === 58 59 GHC and Hugs implement a relaxed version of the first restriction above: they require only that any variable occurring free in t,,Y,, be dependent (using dependencies of classes in the context) on variables that occur free in t,,X,,. 60 They thus accept instances like the following from the monad transformer library, which is invalid according to the original rules: 56 61 {{{ 57 62 class (Monoid w, Monad m) => MonadWriter w m  m > w 58 63 instance MonadWriter w m => MonadWriter w (ReaderT r m) 59 64 }}} 60 GHC and Hugs accept this, because they relax the restriction by using dependency information from the context of the instance declaration. 61 Unfortunately, this relaxation breaks the guarantees of termination (CHR paper, ex. 6) and coherence (CHR paper, ex. 18). 62 This restriction and others may be safely relaxed in some circumstances, but no simple general rule is known. 65 Unfortunately, this relaxation breaks the guarantees of termination and coherence: 63 66 64 === Type inference === 67 * The following instances (CHR paper, ex. 6) seem reasonable: 68 {{{ 69 class Mul a b c  a b > c where 70 (.*.) :: a > b > c 65 71 66 Again the implemented system is more powerful (and useful) than the specified one, e.g. the example in sect. 7 of the original paper. 67 The CHR version is closer. 72 instance Mul Int Int Int where (.*.) = (*) 73 instance Mul Int Float Float where x .*. y = fromIntegral x * y 74 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v 75 }}} 76 and yet instance inference fails to terminate for the following (erroneous) definition: 77 {{{ 78 f = \ b x y > if b then x .*. [y] else y 79 }}} 80 81 * The following instances (adapted from CHR paper, ex. 18) are sensitive to the order in which rules are applied: 82 {{{ 83 class B a b  a > b 84 class C a b  a > b 85 class D a b c  a > b where f :: a > b > c > Bool 86 87 instance B a b => D [a] [b] Bool 88 instance C a b => D [a] [b] Char 89 }}} 90 Given the constraint ``D [a] [b] Bool, D [a] [c] Char``, 91 * if we apply the dependency first, and then reduce using the instances, we obtain ``b = c, B a b, C a b``. 92 * if we first reduce using the instances, we obtain ``B a b, C a c``. 93 (GHC and Hugs yield the former, because they defer context reduction: see FlexibleContexts). 94 95 === New version === 96 97 The following complex relaxation of the first rule is safe (CHR paper, sect. 6), and allows the instances in the monad transformer library: 98 99 1. For any instance 100 {{{ 101 instance ... => C t 102 }}} 103 either 104 * any variable occurring free in t,,Y,, must also occur free in t,,X,,, or 105 * the functional dependency is ''full'' (involves all the arguments of the class), and the arguments t,,Y,, are type variables determined by the free variables of t,,X,,. 106 107 Note that functional dependencies corresponding to [wiki:AssociatedTypes associated type synonyms] are always full.