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


Ignore:
Timestamp:
Apr 22, 2014 10:13:02 AM (13 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