Changes between Version 6 and Version 7 of Records/OverloadedRecordFields/Design


Ignore:
Timestamp:
Apr 22, 2014 10:13:02 AM (16 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Records/OverloadedRecordFields/Design

    v6 v7  
    207207The third parameter of the `Upd` class represents the new type being assigned to the field. Thus it is not functionally dependent on the first two. Consequently, we must use a bare type variable `b` in the instance declaration, with an equality constraint `b ~ [c]` postponed until after the instance matches.
    208208
    209 If a type variable is shared by multiple fields, it cannot be changed using `setField`. Moreover, the use of the `UpdTy` type family means that phantom type variables cannot be changed. For example, in
    210 
    211 {{{
    212 data V a b c = MkV { foo :: (a, b), bar :: a }
    213 }}}
    214 
    215 an update to `foo` must keep `a` and `c` the same, since `a` occurs in the
    216 type of `bar`, and `c` does not occur in the type of `foo`, but the update may change `b`.  Thus we generate:
    217 
    218 {{{
    219 type instance UpdTy (V a b c) "foo" (a, b') = V a b' c
    220 
    221 instance t ~ (a, b') => Upd (V a b c) "foo" t where
     209=== Type-changing update: phantom arguments ===
     210
     211Consider the datatype
     212
     213{{{
     214data T a = MkT { foo :: Int }
     215}}}
     216
     217where `a` is a phantom type argument (it does not occur in the type of `foo`). The traditional update syntax can change the phantom argument, for example if `r :: T Int` then `r { foo = 3 } :: T Bool` typechecks. However, `setField` cannot do so, because this is illegal:
     218
     219{{{
     220type instance UpdTy (T a) "foo" Int = T b
     221}}}
     222
     223Note that the result of the type family involves an unbound variable `b`.
     224
     225In general, a use of `setField` can change only type variables that occur in the field type being updated, and do not occur in any of the other fields' types.
     226
     227=== Type-changing update: multiple fields ===
     228
     229Because `setField` changes a single field, you cannot use to change the type
     230of a type variable that appears in more than one field. For example:
     231{{{
     232data V a b = MkV { foo :: (a, b), bar :: a }
     233}}}
     234We can change the type of `b` but not `a`, because the latter occurs in
     235two different fields.  So we generate these instances:
     236{{{
     237instance t ~ (a, b') => Upd (V a b) "foo" t where
    222238  setField _ (MkV _ bar) e = MkV e bar
    223 }}}
    224 
    225 
     239
     240instance t ~ a => Upd (V a b) "bar" t where
     241  setField _ (MkV foo _) e = MkV foo e
     242}}}
     243In the first we can change `b`'s type to `b'`, but in the second `a`'s type remains unchanged.
     244
     245=== Type-changing update: type families ===
     246
     247Consider the following definitions:
     248
     249{{{
     250type family Goo a
     251data T a = MkT { foo :: Goo a }
     252}}}
     253
     254In order to change the type of the field `foo`, we would need to define something like this:
     255
     256{{{
     257type instance UpdTy (T a) "foo" (Goo b) = T b
     258}}}
     259
     260But pattern-matching on a type family (like `Goo`) doesn't work, because type families are not injective. Thus we cannot change type variables that appear only underneath type family applications. We generate an instance like this instead:
     261
     262{{{
     263type instance UpdTy (T a) "foo" x = T b
     264}}}
     265
     266On the other hand, in the datatype
     267
     268{{{
     269data U a = MkU { bar :: a -> Goo a }
     270}}}
     271
     272it is fine to change `a` when updating `bar`, because it occurs rigidly as well as under a type family, so we can generate this:
     273
     274{{{
     275type instance UpdTy (U a) "bar" (b -> x) = U b
     276}}}
     277
     278This is all a bit subtle. We could make updates entirely non-type-changing if the field type contains a type family, which would be simpler but somewhat unnecessarily restrictive.
     279
     280---------------------------
    226281=== Lens integration ===
    227282
     
    281336
    282337
    283 === Type-changing update: phantom arguments ===
    284 
    285 Consider the datatype
    286 
    287 {{{
    288 data T a = MkT { foo :: Int }
    289 }}}
    290 
    291 where `a` is a phantom type argument (it does not occur in the type of `foo`). The traditional update syntax can change the phantom argument, for example if `r :: T Int` then `r { foo = 3 } :: T Bool` typechecks. However, `setField` cannot do so, because this is illegal:
    292 
    293 {{{
    294 type instance UpdTy (T a) "foo" Int = T b
    295 }}}
    296 
    297 Note that the result of the type family involves an unbound variable `b`.
    298 
    299 In general, a use of `setField` can change only type variables that occur in the field type being updated, and do not occur in any of the other fields' types.
    300 
    301 
    302 === Type-changing update: type families ===
    303 
    304 Consider the following definitions:
    305 
    306 {{{
    307 type family Goo a
    308 data T a = MkT { foo :: Goo a }
    309 }}}
    310 
    311 In order to change the type of the field `foo`, we would need to define something like this:
    312 
    313 {{{
    314 type instance UpdTy (T a) "foo" (Goo b) = T b
    315 }}}
    316 
    317 But pattern-matching on a type family (like `Goo`) doesn't work, because type families are not injective. Thus we cannot change type variables that appear only underneath type family applications. We generate an instance like this instead:
    318 
    319 {{{
    320 type instance UpdTy (T a) "foo" x = T b
    321 }}}
    322 
    323 On the other hand, in the datatype
    324 
    325 {{{
    326 data U a = MkU { bar :: a -> Goo a }
    327 }}}
    328 
    329 it is fine to change `a` when updating `bar`, because it occurs rigidly as well as under a type family, so we can generate this:
    330 
    331 {{{
    332 type instance UpdTy (U a) "bar" (b -> x) = U b
    333 }}}
    334 
    335 This is all a bit subtle. We could make updates entirely non-type-changing if the field type contains a type family, which would be simpler but somewhat unnecessarily restrictive.
    336338
    337339