Changes between Version 12 and Version 13 of FunctionalDependencies


Ignore:
Timestamp:
Feb 12, 2006 12:33:45 AM (8 years ago)
Author:
ross@…
Comment:

spell out versions

Legend:

Unmodified
Added
Removed
Modified
  • FunctionalDependencies

    v12 v13  
    3232 * AssociatedTypes seem to be more promising. 
    3333 
    34 == Details == 
     34== Variations == 
    3535 
    36 === Restrictions on instances === 
     36=== Original version === 
    3737 
    38 The original paper imposed two restrictions on instances (sect. 6.1), stated here for the class `C` declared above: 
     38Suppose a class ''C'' has a functional dependency ''X'' `->` ''Y''. 
     39The original paper imposed two restrictions on instances of the class ''C'' (sect. 6.1): 
    3940 
    4041 1. For any instance 
    4142    {{{ 
    42 instance ... => C Ta Tb Tc 
     43instance ... => C t 
    4344}}} 
    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,,. 
    4546 2. If there is a second instance 
    4647    {{{ 
    47 instance ... => C Sa Sb Sc 
     48instance ... => C s 
    4849}}} 
    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,,. 
    5051 
    5152Haskell 98 requires that the context of an instance declaration use only type variables that appear in the head. 
    5253It 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 non-termination (CHR paper, ex. 15). 
     54 
    5355With FlexibleInstances and no OverlappingInstances, these restrictions yield a coherent and decidable system (CHR paper, corr. 1). 
    5456 
    55 However the first restriction forbids instances like the following from the monad transformer library: 
     57=== GHC and Hugs === 
     58 
     59GHC 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,,. 
     60They thus accept instances like the following from the monad transformer library, which is invalid according to the original rules: 
    5661{{{ 
    5762class (Monoid w, Monad m) => MonadWriter w m | m -> w 
    5863instance MonadWriter w m => MonadWriter w (ReaderT r m) 
    5964}}} 
    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. 
     65Unfortunately, this relaxation breaks the guarantees of termination and coherence: 
    6366 
    64 === Type inference === 
     67 * The following instances (CHR paper, ex. 6) seem reasonable: 
     68   {{{ 
     69class Mul a b c | a b -> c where 
     70        (.*.) :: a -> b -> c 
    6571 
    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. 
     72instance Mul Int Int Int where (.*.) = (*) 
     73instance Mul Int Float Float where x .*. y = fromIntegral x * y 
     74instance 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   {{{ 
     78f = \ 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   {{{ 
     83class B a b | a -> b 
     84class C a b | a -> b 
     85class D a b c | a -> b where f :: a -> b -> c -> Bool 
     86 
     87instance B a b => D [a] [b] Bool 
     88instance 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 
     97The 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    {{{ 
     101instance ... => 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 
     107Note that functional dependencies corresponding to [wiki:AssociatedTypes associated type synonyms] are always full.