46 | | class t ~ GetResult r f => Get r (f :: Symbol) t where |
47 | | getFld :: proxy f -> r -> t |
48 | | }}} |
49 | | |
50 | | Recall that `Symbol` is the kind of type-level strings. Roughly speaking, an occurrence of a field name `x` is translated into `getFld (Proxy :: Proxy "x")`. (Actually a slightly more general translation may be used, as [#Lensintegration discussed below].) |
51 | | |
52 | | The syntactic sugar extends to conjunctions: `r {x :: tx, y :: ty}` means `(Get r "x" tx, Get r "y" ty)`. Note also that `r` and `t` might be arbitrary types, not just type variables or type constructors. For example, `T (Maybe v) { x :: [Maybe v] }` means `(Get (T (Maybe b)) "x" [Maybe v])`. |
53 | | |
54 | | Instances for the `Get` typeclass and `GetResult` type family are automatically generated (for modules with `-XOverloadedRecordFields` enabled) using the record fields that are in scope. For example, the data type |
| 46 | class t ~ GetResult r f => Has r (f :: Symbol) t where |
| 47 | getField :: proxy f -> r -> t |
| 48 | }}} |
| 49 | |
| 50 | Recall that `Symbol` is the kind of type-level strings. Roughly speaking, an occurrence of a field name `x` is translated into `getField (Proxy :: Proxy "x")`. (Actually a slightly more general translation is used, as [#Lensintegration discussed below].) |
| 51 | |
| 52 | The syntactic sugar extends to conjunctions: `r {x :: tx, y :: ty}` means `(Has r "x" tx, Has r "y" ty)`. Note also that `r` and `t` might be arbitrary types, not just type variables or type constructors. For example, `T (Maybe v) { x :: [Maybe v] }` means `(Has (T (Maybe b)) "x" [Maybe v])`. |
| 53 | |
| 54 | Instances for the `Has` typeclass and `GetResult` type family are automatically generated (for modules with `-XOverloadedRecordFields` enabled) using the record fields that are in scope. For example, the data type |
65 | | instance (b ~ [a]) => Get (T a) "x" b where |
66 | | getFld _ (MkT x) = x |
67 | | }}} |
68 | | |
69 | | The bare type variable `b` in the instance head is important, so that we get an instance match from the first two parameters only, then the equality constraint `(b ~ [a])` improves `b`. For example, if the constraint `Get (T c) "x" d` is encountered during type inference, the instance will match and generate the constraints `(a ~ c, b ~ d, b ~ [a])`. Moreover, the `GetResult` type family ensures that the third parameter is functionally dependent on the first two, which is needed to [#Troubleinparadise avoid ambiguity errors when composing overloaded fields]. |
| 65 | instance (b ~ [a]) => Has (T a) "x" b where |
| 66 | getField _ (MkT x) = x |
| 67 | }}} |
| 68 | |
| 69 | The bare type variable `b` in the instance head is important, so that we get an instance match from the first two parameters only, then the equality constraint `(b ~ [a])` improves `b`. For example, if the constraint `Has (T c) "x" d` is encountered during type inference, the instance will match and generate the constraints `(a ~ c, b ~ d, b ~ [a])`. Moreover, the `GetResult` type family ensures that the third parameter is functionally dependent on the first two, which is needed to [#Troubleinparadise avoid ambiguity errors when composing overloaded fields]. |
| 144 | === Limited type-changing update === |
| 145 | |
| 146 | As noted above, supporting a polymorphic version of the existing record update syntax (in its full generality) is difficult. However, we can generate instances of the following class, which permits type-changing update of single fields: |
| 147 | |
| 148 | {{{ |
| 149 | type family SetResult (r :: *) (f :: Symbol) (a :: *) :: * |
| 150 | |
| 151 | class Has r f (GetResult r f) => |
| 152 | Upd (r :: *) (f :: Symbol) (a :: *) where |
| 153 | setField :: proxy f -> r -> a -> SetResult r f a |
| 154 | }}} |
| 155 | |
| 156 | For example, the datatype `T` above would give rise to these instances: |
| 157 | |
| 158 | {{{ |
| 159 | type instance SetResult (T a) "x" [c] = T c |
| 160 | |
| 161 | instance (b ~ [c]) => Upd (T a) "x" b where |
| 162 | setField _ r e = r { x = e } |
| 163 | }}} |
| 164 | |
| 165 | If a type variable is shared by multiple fields, it cannot be changed using `setField`. Moreover, the use of the `SetResult` type family means that phantom type variables cannot be changed. For example, |
| 166 | |
| 167 | {{{ |
| 168 | data U a b c = MkU { foo :: (a, b), bar :: a } |
| 169 | }}} |
| 170 | |
| 171 | an update to `foo` must keep `a` and `c` the same, since `a` occurs in the |
| 172 | type of `bar`, and `c` does not occur in the type of `foo`, but the update may change `b`. Thus we generate: |
| 173 | |
| 174 | {{{ |
| 175 | type instance SetResult (T a b c) "foo" (a, b') = T a b' c |
| 176 | |
| 177 | instance t ~ (a, b') => Upd (T a b c) "foo" t where |
| 178 | setField _ r e = r { foo = e } |
| 179 | }}} |
| 180 | |
| 181 | |
| 182 | === Lens integration === |
| 183 | |
| 184 | It was implied above that a field like `foo` translates into `getField (Proxy :: Proxy "foo") :: Has r "foo" t => r -> t`, but this is not quite the whole story. We would like fields to be usable as lenses (e.g. using the [http://hackage.haskell.org/package/lens lens] package). This requires a slightly more general translation, using |
| 185 | |
| 186 | {{{ |
| 187 | field :: (Has r f t, Accessor p f) => proxy f -> p r t |
| 188 | field z = accessor z (getField z) (setField z) |
| 189 | }}} |
| 190 | |
| 191 | to translate `foo` to `field (Proxy :: Proxy "foo") :: (Has r "foo" t, Accessor p "foo") => p r t`. The `Accessor` class is defined thus: |
| 192 | |
| 193 | {{{ |
| 194 | class Accessor (p :: * -> * -> *) (f :: Symbol) where |
| 195 | accessor :: proxy f -> (r -> GetResult r f) -> |
| 196 | (forall a . Upd r f a => r -> a -> SetResult r f a) -> |
| 197 | p r (GetResult r f) |
| 198 | }}} |
| 199 | |
| 200 | An instance of `Accessor p f` means that `p` may contain a getter and setter for the field `f`. In particular, we can give an instance for functions that ignores `f` and the setter completely: |
| 201 | |
| 202 | {{{ |
| 203 | instance Accessor (->) f where |
| 204 | accessor _ getter setter = getter |
| 205 | }}} |
| 206 | |
| 207 | Thus, whenever a field `foo` is used at a function type (by applying it or composing it, for example), this instance will be selected. If `z` is a proxy of type `Proxy "foo"`, then `foo` translates to `field z`, which computes to `accessor z (getField z) (setField z)`, and hence to `getField z` by the `Accessor` instance for functions. |
| 208 | |
| 209 | However, `p` does not have to be the function arrow. Suppose the `lens` library defined the following newtype wrapper: |
| 210 | |
| 211 | {{{ |
| 212 | newtype WrapLens f r a |
| 213 | = MkWrapLens (forall b . Upd r f b => Lens r (SetResult r f b) a b) |
| 214 | |
| 215 | instance f ~ g => Accessor (WrapLens f) g where |
| 216 | accessor _ getter setter = MkWrapLens (\ w s -> setter s <$> w (getter s)) |
| 217 | |
| 218 | fieldLens :: Upd r f b => WrapLens f r a -> Lens r (SetResult r f b) a b |
| 219 | fieldLens (MkWrapLens l) = l |
| 220 | }}} |
| 221 | |
| 222 | Now `fieldLens foo` is a lens whenever `foo` is an overloaded record field. |
| 223 | |
| 224 | Other lens libraries can define their own instances of `Accessor`, even if they do not support type-changing update, and the same machinery enables fields to be used with them. |
| 225 | |
| 226 | |
167 | | === Lens integration === |
168 | | |
169 | | As noted above, supporting a polymorphic version of the existing record update syntax (in its full generality) is difficult. However, we can generate instances of the following class, which permits type-changing update of single fields: |
170 | | |
171 | | {{{ |
172 | | type family SetResult (r :: *) (f :: Symbol) (a :: *) :: * |
173 | | |
174 | | class Set (r :: *) (f :: Symbol) (a :: *) where |
175 | | setFld :: proxy f -> r -> a -> SetResult r f a |
176 | | }}} |
177 | | |
178 | | For example, the datatype `T` above would give rise to these instances: |
179 | | |
180 | | {{{ |
181 | | type instance SetResult (T a) "x" [c] = T c |
182 | | |
183 | | instance (b ~ [c]) => Set (T a) "x" b where |
184 | | setFld _ (MkT _) y = MkT y |
185 | | }}} |
186 | | |
187 | | It was implied above that a field like `foo` translates into `getFld (Proxy :: Proxy "foo") :: Get r "foo" t => r -> t`, but this is not quite the whole story. We would like fields to be usable as lenses (e.g. using the [http://hackage.haskell.org/package/lens lens] package). This requires a slightly more general translation, using |
188 | | |
189 | | {{{ |
190 | | field :: (Get r f t, Accessor p f) => proxy f -> p r t |
191 | | field z = accessor z (getFld z) (setFld z) |
192 | | }}} |
193 | | |
194 | | to translate `foo` to `field (Proxy :: Proxy "foo") :: (Get r "foo" t, Accessor p "foo") => p r t`. The `Accessor` class is defined thus: |
195 | | |
196 | | {{{ |
197 | | class Accessor (p :: * -> * -> *) (f :: Symbol) where |
198 | | accessor :: proxy f -> (r -> GetResult r f) -> |
199 | | (forall a . Set r f a => r -> a -> SetResult r f a) -> |
200 | | p r (GetResult r f) |
201 | | }}} |
202 | | |
203 | | An instance of `Accessor p f` means that `p` may contain a getter and setter for the field `f`. In particular, we can give an instance for functions that ignores `f` and the setter completely: |
204 | | |
205 | | {{{ |
206 | | instance Accessor (->) f where |
207 | | accessor _ getter setter = getter |
208 | | }}} |
209 | | |
210 | | Thus, whenever a field `foo` is used at a function type (by applying it or composing it, for example), this instance will be selected. If `z` is a proxy of type `Proxy "foo"`, then `foo` translates to `field z`, which computes to `accessor z (getFld z) (setFld z)`, and hence to `getFld z` by the `Accessor` instance for functions. |
211 | | |
212 | | However, `p` does not have to be the function arrow. Suppose the `lens` library defined the following newtype wrapper: |
213 | | |
214 | | {{{ |
215 | | newtype WrapLens f r a |
216 | | = MkWrapLens (forall b . Set r f b => Lens r (SetResult r f b) a b) |
217 | | |
218 | | instance f ~ g => Accessor (WrapLens f) g where |
219 | | accessor _ getter setter = MkWrapLens (\ w s -> setter s <$> w (getter s)) |
220 | | |
221 | | fieldLens :: Set r f b => WrapLens f r a -> Lens r (SetResult r f b) a b |
222 | | fieldLens (MkWrapLens l) = l |
223 | | }}} |
224 | | |
225 | | Now `fieldLens foo` is a lens whenever `foo` is an overloaded record field. |
226 | | |
227 | | |
228 | | === Trouble in paradise === |
229 | | |
230 | | [http://www.haskell.org/pipermail/glasgow-haskell-users/2013-July/022584.html Edward Kmett points out] that a previous version of this proposal, where the third parameter of `Get` was not functionally dependent on the first two, fell short in an important respect: composition of polymorphic record fields would lead to ambiguity errors, as the intermediate type cannot be determined. For example, suppose |
231 | | |
232 | | {{{ |
233 | | foo :: Get b "foo" c => b -> c |
234 | | bar :: Get a "bar" b => a -> b |
235 | | }}} |
236 | | |
237 | | then |
238 | | |
239 | | {{{ |
240 | | foo . bar :: (Get a "bar" b, Get b "foo" c) => a -> c |
241 | | }}} |
242 | | |
243 | | and `b` is an ambiguous type variable. This shows the need for the `GetResult` type family. |
244 | | |
245 | | |
246 | | === User-defined `Get` instances === |
247 | | |
248 | | Should the user be allowed to write explicit `Get` instances? For example: |
249 | | |
250 | | {{{ |
251 | | instance ctx => Get r "x" t where |
252 | | getFld = blah :: r -> t |
253 | | }}} |
254 | | |
255 | | Even with an explicit `Get` instance as above, the name `x` will not be in scope unless a datatype has a field with name `x`. Thus it is not really useful. The previous proposal, where `(.x)` always meant "project out the `x` field", used explicit `Has` instances for virtual fields. |
256 | | |
257 | | |
| 269 | |
| 270 | |
| 271 | === Syntactic sugar for `Upd` constraints === |
| 272 | |
| 273 | Should we have a special syntax for `Upd` constraints, just as `r { x :: t }` sugars `Has r "x" t`? What should it look like? Perhaps something like `r { x ::= t }`? |
| 274 | |
| 275 | |
| 276 | == Remarks == |
| 277 | |
| 278 | |
| 279 | === Trouble in paradise === |
| 280 | |
| 281 | [http://www.haskell.org/pipermail/glasgow-haskell-users/2013-July/022584.html Edward Kmett points out] that a previous version of this proposal, where the third parameter of `Get` was not functionally dependent on the first two, fell short in an important respect: composition of polymorphic record fields would lead to ambiguity errors, as the intermediate type cannot be determined. For example, suppose |
| 282 | |
| 283 | {{{ |
| 284 | foo :: Has b "foo" c => b -> c |
| 285 | bar :: Has a "bar" b => a -> b |
| 286 | }}} |
| 287 | |
| 288 | then |
| 289 | |
| 290 | {{{ |
| 291 | foo . bar :: (Has a "bar" b, Has b "foo" c) => a -> c |
| 292 | }}} |
| 293 | |
| 294 | and `b` is an ambiguous type variable. This shows the need for the `GetResult` type family. |
| 295 | |
| 296 | |
| 297 | === User-defined `Has` instances === |
| 298 | |
| 299 | The user can write explicit `Has` instances, and they are scoped normally. For example: |
| 300 | |
| 301 | {{{ |
| 302 | instance ctx => Has r "x" t where |
| 303 | getField = blah :: proxy "x" -> r -> t |
| 304 | }}} |
| 305 | |
| 306 | Even with an explicit `Has` instance as above, the name `x` will not be in scope unless a datatype has a field with name `x`. This is likely to make it less useful. However, it does allow virtual fields to be declared. |