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 === |
133 | | An alternative view of the confluence problem discussed under ''GHC and Hugs'' is that the improvement rules should be modified. |
| 79 | === Properties === |
| 80 | |
| 81 | With FlexibleInstances and no OverlappingInstances, this system is coherent and decidable (CHR paper, corr. 1). |
| 82 | |
| 83 | Unfortunately the "coverage" condition rules out instances like the following, from the monad transformer library: |
| 84 | {{{ |
| 85 | class (Monoid w, Monad m) => MonadWriter w m | m -> w |
| 86 | instance MonadWriter w m => MonadWriter w (ReaderT r m) |
| 87 | }}} |
| 88 | |
| 89 | == GHC and Hugs == |
| 90 | |
| 91 | GHC and Hugs implement the following relaxed version of the above "coverage" condition: |
| 92 | |
| 93 | 1. '''Dependency.''' |
| 94 | For any instance |
| 95 | {{{ |
| 96 | instance 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 | |
| 100 | They thus accept instances like the above `MonadWriter` example. |
| 101 | Unfortunately, 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 | {{{ |
| 106 | class Mul a b c | a b -> c where |
| 107 | (.*.) :: a -> b -> c |
| 108 | |
| 109 | instance Mul Int Int Int where (.*.) = (*) |
| 110 | instance Mul Int Float Float where x .*. y = fromIntegral x * y |
| 111 | instance 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 | {{{ |
| 115 | f = \ 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 | {{{ |
| 121 | class B a b | a -> b |
| 122 | class C a b c | a -> b where f :: a -> b -> c -> Bool |
| 123 | |
| 124 | instance 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 | |
| 133 | The following are alternatives. |
| 134 | |
| 135 | === Modified coverage condition === |
| 136 | |
| 137 | The 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 | {{{ |
| 141 | instance ... => 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 | |
| 147 | The fullness condition restores confluence, while the variable argument condition restores termination. |
| 148 | |
| 149 | Note that functional dependencies corresponding to [wiki:AssociatedTypes associated type synonyms] are always full. |
| 150 | |
| 151 | === Modified instance improvement === |
| 152 | |
| 153 | Assume the dependency condition in place of coverage. |
| 154 | For an instance |
| 155 | {{{ |
| 156 | instance ... => C t |
| 157 | }}} |
| 158 | if 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). |
| 159 | Hence we can unify s with S t. |
| 160 | Local 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 | |
| 163 | A restriction on instances to guarantee termination would also be needed. |