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.