Changes between Version 15 and Version 16 of FunctionalDependencies


Ignore:
Timestamp:
Apr 7, 2006 9:40:33 AM (9 years ago)
Author:
ross@…
Comment:

rearrange, add modified instance improvement rule

Legend:

Unmodified
Added
Removed
Modified
  • FunctionalDependencies

    v15 v16  
    3535 * AssociatedTypes seem to be more promising. 
    3636 
    37 == Restrictions on instances == 
     37== Original Proposal == 
    3838 
    39 There are several versions. 
     39This is the system proposed in the original paper, with names according to the FD-CHR paper. 
     40Suppose a class ''C'' has a functional dependency ''X'' `->` ''Y''. 
    4041 
    41 === Original version === 
     42=== Restrictions on instances === 
    4243 
    43 These are the restrictions from the original paper, named according to the FD-CHR paper. 
    44 Suppose a class ''C'' has a functional dependency ''X'' `->` ''Y''. 
    4544The original paper imposed two restrictions on instances of the class ''C'' (sect. 6.1): 
    4645 
     
    5150}}} 
    5251    any variable occurring free in t,,Y,, must also occur free in t,,X,,. 
     52 
    5353 2. '''Consistency.''' 
    5454    If there is a second instance 
     
    6161It 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. 16). 
    6262 
    63 With FlexibleInstances and no OverlappingInstances, these restrictions yield a coherent and decidable system (CHR paper, corr. 1). 
    64  
    65 === GHC and Hugs === 
    66  
    67 GHC and Hugs implement a relaxed version of the above "coverage" condition: 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,,. 
    68 They thus accept instances like the following from the monad transformer library, which is invalid according to the original rules: 
    69 {{{ 
    70 class (Monoid w, Monad m) => MonadWriter w m | m -> w 
    71 instance MonadWriter w m => MonadWriter w (ReaderT r m) 
    72 }}} 
    73 Unfortunately, this relaxation breaks the guarantees of termination and coherence: 
    74  
    75  * The following instances (CHR paper, ex. 6) seem reasonable: 
    76    {{{ 
    77 class Mul a b c | a b -> c where 
    78         (.*.) :: a -> b -> c 
    79  
    80 instance Mul Int Int Int where (.*.) = (*) 
    81 instance Mul Int Float Float where x .*. y = fromIntegral x * y 
    82 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v 
    83 }}} 
    84    and yet instance inference fails to terminate for the following (erroneous) definition: 
    85    {{{ 
    86 f = \ b x y -> if b then x .*. [y] else y 
    87 }}} 
    88  
    89  * The following instances (adapted from CHR paper, ex. 18) are sensitive to the order in which rules are applied: 
    90    {{{ 
    91 class B a b | a -> b 
    92 class C a b | a -> b 
    93 class D a b c | a -> b where f :: a -> b -> c -> Bool 
    94  
    95 instance B a b => D [a] [b] Bool 
    96 instance C a b => D [a] [b] Char 
    97 }}} 
    98    Given the constraint ``D [a] [b] Bool, D [a] [c] Char``, 
    99     * if we apply the dependency first, and then reduce using the instances, we obtain ``b = c, B a b, C a b``. 
    100     * if we first reduce using the instances, we obtain ``B a b, C a c``. 
    101   (GHC and Hugs yield the former, because they defer context reduction: see FlexibleContexts). 
    102  
    103 === New version === 
    104  
    105 The following complex relaxation of the "coverage" condition is safe (CHR paper, sect. 6), and allows the instances in the monad transformer library: 
    106  
    107  1. For any instance 
    108     {{{ 
    109 instance ... => C t 
    110 }}} 
    111     either 
    112     * any variable occurring free in t,,Y,, must also occur free in t,,X,,, or 
    113     * 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,,. 
    114  
    115 Note that functional dependencies corresponding to [wiki:AssociatedTypes associated type synonyms] are always full. 
    116  
    117 == Improvement of inferred types == 
     63=== Improvement of inferred types === 
    11864 
    11965"Improvement", as used by Mark Jones, means using information about what instances could match a predicate to instantiate its type variables, or to fail. 
     
    13177    (This rule is justified by the above "consistency" condition.) 
    13278 
    133 An alternative view of the confluence problem discussed under ''GHC and Hugs'' is that the improvement rules should be modified. 
     79=== Properties === 
     80 
     81With FlexibleInstances and no OverlappingInstances, this system is coherent and decidable (CHR paper, corr. 1). 
     82 
     83Unfortunately the "coverage" condition rules out instances like the following, from the monad transformer library: 
     84{{{ 
     85class (Monoid w, Monad m) => MonadWriter w m | m -> w 
     86instance MonadWriter w m => MonadWriter w (ReaderT r m) 
     87}}} 
     88 
     89== GHC and Hugs == 
     90 
     91GHC and Hugs implement the following relaxed version of the above "coverage" condition: 
     92 
     93 1. '''Dependency.''' 
     94    For any instance 
     95    {{{ 
     96instance ctxt => C t 
     97}}} 
     98    any variable occurring free in t,,Y,, must be dependent (using dependencies of classes in the context) on variables that occur free in t,,X,,. 
     99 
     100They thus accept instances like the above `MonadWriter` example. 
     101Unfortunately, this relaxation breaks the guarantees of termination and coherence: 
     102 
     103 '''Loss of termination''':: 
     104   The following instances (CHR paper, ex. 6) seem reasonable: 
     105   {{{ 
     106class Mul a b c | a b -> c where 
     107        (.*.) :: a -> b -> c 
     108 
     109instance Mul Int Int Int where (.*.) = (*) 
     110instance Mul Int Float Float where x .*. y = fromIntegral x * y 
     111instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v 
     112}}} 
     113   and yet instance inference fails to terminate for the following (erroneous) definition: 
     114   {{{ 
     115f = \ b x y -> if b then x .*. [y] else y 
     116}}} 
     117 
     118 '''Loss of confluence''':: 
     119   The following instances (adapted from CHR paper, ex. 18) are sensitive to the order in which rules are applied: 
     120   {{{ 
     121class B a b | a -> b 
     122class C a b c | a -> b where f :: a -> b -> c -> Bool 
     123 
     124instance B a b => C [a] [b] Bool 
     125}}} 
     126   Given the constraint ``C [a] [b] Bool, C [a] [c] d``, 
     127    * if we apply the dependency first, and then reduce using the instances, we obtain ``b = c, B a b, C [a] [b] d``. 
     128    * if we first reduce using the instances, we obtain ``B a b, C [a] [c] d``. 
     129  (GHC and Hugs yield the former, because they defer context reduction: see FlexibleContexts). 
     130 
     131== Fixes == 
     132 
     133The following are alternatives. 
     134 
     135=== Modified coverage condition === 
     136 
     137The following complex relaxation of the "coverage" condition is safe (CHR paper, sect. 6), and allows the instances in the monad transformer library: 
     138 
     139 1. For any instance 
     140    {{{ 
     141instance ... => C t 
     142}}} 
     143    either 
     144    * any variable occurring free in t,,Y,, must also occur free in t,,X,,, or 
     145    * 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,,. 
     146 
     147The fullness condition restores confluence, while the variable argument condition restores termination. 
     148 
     149Note that functional dependencies corresponding to [wiki:AssociatedTypes associated type synonyms] are always full. 
     150 
     151=== Modified instance improvement === 
     152 
     153Assume the dependency condition in place of coverage. 
     154For an instance 
     155{{{ 
     156instance ... => C t 
     157}}} 
     158if t,,Y,, is not covered by t,,X,,, then for any constraint `C s` with s,,X,, = S t,,X,,, there cannot be another matching instance (as it would violate the consistency condition). 
     159Hence we can unify s with S t. 
     160Local confluence is straight-forward. 
     161(In the above confluence example, `d` is instantiated to `Bool` and both alternatives reduce to {{{b = c, d = Bool, B a b}}}). 
     162 
     163A restriction on instances to guarantee termination would also be needed.