Changes between Version 31 and Version 32 of Records/OverloadedRecordFields/Plan


Ignore:
Timestamp:
Aug 29, 2013 8:14:37 AM (8 months ago)
Author:
adamgundry
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Records/OverloadedRecordFields/Plan

    v31 v32  
    3737=== Record field constraints ===  
    3838 
    39 A record field constraint is introduced when a field is used in an expression. If every `x` in scope is a record fields, then an occurrence of `x` has type `a { x :: b } => a -> b` instead of generating an ambiguity error. The overloaded `x` is translated using a typeclass, described below. If there are any normal identifiers `x` in scope (as well as fields) then a use of `x` leads to an ambiguity error.  
     39A record field constraint is introduced when a field is used in an expression. If every `x` in scope is a record field, then an occurrence of `x` has type `a { x :: b } => a -> b` instead of generating an ambiguity error. The overloaded `x` is translated using a typeclass, described below. If there are any normal identifiers `x` in scope (as well as fields) then a use of `x` leads to an ambiguity error.  
    4040 
    4141Record field constraints `r { x :: t }` are syntactic sugar for typeclass constraints `Has r "x" t`, where 
     
    6363type instance GetResult (T a) "x" = [a] 
    6464 
    65 instance (b ~ [a]) => Has (T a) "x" b where 
     65instance Has (T a) "x" [a] where 
    6666  getField _ (MkT x) = x 
    6767}}} 
    6868 
    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]. 
     69The equality superclass on the `Has` class is important for type inference. For example, if the constraint `Has (T c) "x" d` is encountered, the instance will not match initially (because `d` is not of the form `[c]`), but a derived equality constraint `d ~ GetResult (T c) "x"` will be generated. This computes to `d ~ [c]`, so the original constraint becomes `Has (T c) "x" [c]`, which means the instance will match. 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]. 
    7070 
    7171The reason for using a three-parameter class, rather than just two parameters and a type family, is to support the syntactic sugar. With a two-parameter class we could easily end up inferring types like the following, and it would be hard to reapply the sugar: 
     
    7979=== Representation hiding === 
    8080 
    81 At present, a datatype in one module can declare a field, but if the selector function is not exported, then the field is hidden from clients of the module. It is important to support this. Typeclasses in general have no controls over their scope, but for implicitly generated `Has` instances, the instance is available for a module if `-XOverloadedRecordFields` is enabled for that module and the record field selector function is in scope. Instances are generated on the client side, rather than being exported from the defining module. 
     81At present, a datatype in one module can declare a field, but if the selector function is not exported, then the field is hidden from clients of the module. It is important to support this. Typeclasses in general have no controls over their scope, but for implicitly generated `Has` instances, the instance is available for a module if `-XOverloadedRecordFields` is enabled for that module and the record field selector function is in scope. Instances are not exported from the module that defines the datatype, but are created implicitly when needed by the typechecker. 
    8282 
    8383This enables representation hiding: just like at present, exporting the field selector permits access to the field. For example, consider the following module: 
     
    120120 
    121121 
    122 === Record update === 
     122=== Qualified names === 
     123 
     124A qualified name must refer to a unique field; it cannot be overloaded. Consider the following example: 
     125 
     126{{{ 
     127module M where 
     128  data S = MkS { foo :: Int } 
     129 
     130module N where 
     131  data T = MkT { foo :: Int } 
     132  data U = MkU { foo :: Int } 
     133 
     134module O where 
     135  import M 
     136  import N 
     137 
     138  f x = M.foo x 
     139  g x = N.foo x 
     140  h x = foo x 
     141}}} 
     142 
     143Here `f` is okay, because `M.foo` is unambiguous, but `g` is forbidden. This is because we have no way to support polymorphism over fields only from one module. The user must write `h` instead, making it explicit that the field is not qualified. 
     144 
     145 
     146== Record update == 
    123147 
    124148Supporting polymorphic record update is rather more complex than polymorphic lookup. In particular: 
     
    149173type family SetResult (r :: *) (f :: Symbol) (a :: *) :: * 
    150174 
    151 class Has r f (GetResult r f) => 
     175class (Has r f (GetResult r f), r ~ SetResult r f (GetResult r f)) => 
    152176          Upd (r :: *) (f :: Symbol) (a :: *) where 
    153177  setField :: proxy f -> r -> a -> SetResult r f a 
     
    164188  setField _ r e = r { x = e } 
    165189}}} 
     190 
     191The third parameter of the `Upd` class represents the new type being assigned to the field, unlike the `Has` class, where it represents the current type. 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. 
    166192 
    167193If 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, in 
     
    227253 
    228254 
     255=== Type-changing update: phantom arguments === 
     256 
     257Consider the datatype 
     258 
     259{{{ 
     260data T a = MkT { foo :: Int } 
     261}}} 
     262 
     263where `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: 
     264 
     265{{{ 
     266type instance SetResult (T a) "foo" Int = T b 
     267}}} 
     268 
     269Note that the result of the type family involves an unbound variable `b`.  
     270 
     271In 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. 
     272 
     273 
     274 
    229275== Design choices == 
     276 
     277== Unambiguous fields == 
     278 
     279What if `foo` occurs in an expression, and there is only one datatype `T` with a field `foo` in scope? There are three obvious choices: 
     280 
     2811. Generate a polymorphic use of `field` as normal. 
     2822. Generate a use of `field`, specialised to the type `T`, but still polymorphic in the choice of `Accessor`. 
     2833. Use the record selector for `foo`, without any polymorphism. 
     284 
     285The first and second options are likely to be preferred by users who wish to write polymorphic code, while the third is better if the desire is only to overload field names but not write code that is polymorphic in the choice of datatype. The third option severely hampers the integration with lenses, because a field will only be a lens if it is ambiguous. However, the third would allow higher-rank fields to be used when unambiguous. This suggests a fourth option: 
     286 
     2874. Use the record selector for `foo` if it is applied to one or more arguments, and generate a use of `field` specialised to the type `T` otherwise.  
     288 
     289This makes higher-rank fields usable (though possibly requiring eta-expansion), and it allows lens integration. On the other hand, it is still an impediment to users wishing to write polymorphic code. 
    230290 
    231291