Changes between Version 40 and Version 41 of Records/OverloadedRecordFields/Plan
 Timestamp:
 Feb 15, 2014 2:08:13 PM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Records/OverloadedRecordFields/Plan
v40 v41 3 3 This is a plan to implement overloaded record fields, along the lines of SPJ's [wiki:Records/OverloadedRecordFields Simple Overloaded Record Fields] proposal, as a Google Summer of Code project. (See the [http://www.googlemelange.com/gsoc/project/google/gsoc2013/adamgundry/23001 GSoC project details], for reference.) The page on [wiki:Records Records] gives the motivation and many options. In particular, the proposal for [wiki:Records/DeclaredOverloadedRecordFields Declared Overloaded Record Fields] is closely related but makes some different design decisions. 4 4 5 This page describes the design. Separate [wiki:Records/OverloadedRecordFields/Implementation notes on the implementation] are available, but not necessarily comprehensible. Development of the extension is taking place on forks of the [https://github.com/adamgundry/ghc ghc], [https://github.com/adamgundry/packagesbase packagesbase] , [https://github.com/adamgundry/haddock haddock] and [https://github.com/adamgundry/testsuite testsuite] repositories (on branch 'overloadedrecordfields'). A [https://github.com/adamgundry/recordsprototype prototype implementation] is also available.5 This page describes the design. Separate [wiki:Records/OverloadedRecordFields/Implementation notes on the implementation] are available, but not necessarily comprehensible. Development of the extension is taking place on forks of the [https://github.com/adamgundry/ghc ghc], [https://github.com/adamgundry/packagesbase packagesbase] and [https://github.com/adamgundry/haddock haddock] repositories (on branch 'overloadedrecordfields'). A [https://github.com/adamgundry/recordsprototype prototype implementation] is also available. 6 6 7 7 === Motivation === … … 39 39 A 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` (roughly) 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. 40 40 41 A record field constraint `r { x :: t }` is syntactic sugar for the pair of constraints `(Has r "x", FldTy r "x" ~ t)`, where41 A record field constraint `r { x :: t }` is syntactic sugar for the constraint `Has r "x" t`, where 42 42 43 43 {{{ 44 44 type family FldTy (r :: *) (n :: Symbol) :: * 45 45 46 class Has r (n :: Symbol)where47 getField :: Proxy# n > r > FldTy r n46 class t ~ FldTy r n => Has r (n :: Symbol) t where 47 getField :: Proxy# n > r > t 48 48 }}} 49 49 50 50 Recall that `Symbol` is the kind of typelevel 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].) The type `Proxy#` is zerowidth, so it will be erased at runtime, and is used to pass in the typelevel string argument, since we don't have explicit type application (yet). 51 51 52 The syntactic sugar extends to conjunctions: `r {x :: tx, y :: ty}` means `(Has r "x" , FldTy r "x" ~ tx, Has r "y", FldTy 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", FldTy (T (Maybe b)) "x" ~ [Maybe v])`.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]`. To make these desugarings accepted, `XOverloadedRecordFields` implies `XFlexibleContexts` and `XConstraintKinds`. 53 53 54 54 Instances for the `Has` typeclass and `FldTy` type family are automatically generated (for modules with `XOverloadedRecordFields` enabled) using the record fields that are in scope. For example, the data type … … 63 63 type instance FldTy (T a) "x" = [a] 64 64 65 instance Has (T a) "x"where65 instance b ~ [a] => Has (T a) "x" b where 66 66 getField _ (MkT x) = x 67 67 }}} 68 68 69 We have considered using a threeparameter version of the `Has` class, with the third parameter (the field type) being functionally dependent on the first two, but this version seems more straightforward (at the cost of exposing the encoding underlying the syntactic sugar more often). 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 `FldTy` 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]. 70 71 The reason for using a threeparameter class, rather than just two parameters and a type family, is to support the syntactic sugar and improve type inference error messags. With a twoparameter class we could easily end up inferring types like the following, and it would be hard to reapply the sugar: 72 73 {{{ 74 f :: (Has r "x", Has r "y", FldTy r "x" ~ Int, FldTy r "y" ~ Int) => r > Int 75 f r = x r + y r :: Int 76 }}} 77 78 Moreover, error messages would tend to be reported in terms of unification failures for `FldTy` rather than unsolved `Has` class constraints. 70 79 71 80 … … 83 92 }}} 84 93 85 Any module that imports `M` will have access to the `x` field from `R` but not from `S`, because the instance `Has R "x" ` will be available but the instance `Has S "x"` will not be. Thus `R { x :: Int }` will be solved but `S { x :: Bool }` will not.94 Any module that imports `M` will have access to the `x` field from `R` but not from `S`, because the instance `Has R "x" Int` will be available but the instance `Has S "x" Bool` will not be. Thus `R { x :: Int }` will be solved but `S { x :: Bool }` will not. 86 95 87 96 … … 166 175 type family UpdTy (r :: *) (n:: Symbol) (a :: *) :: * 167 176 168 class (Has r n , r ~ UpdTy r n (FldTy r n)) =>169 Upd (r :: *) (n :: Symbol) ( a:: *) where170 setField :: Proxy# n > r > a > UpdTy r n a177 class (Has r n (FldTy r n), r ~ UpdTy r n (FldTy r n)) => 178 Upd (r :: *) (n :: Symbol) (t :: *) where 179 setField :: Proxy# n > r > t > UpdTy r n t 171 180 }}} 172 181 … … 203 212 === Lens integration === 204 213 205 It was implied above that a field like `foo` translates into `getField (proxy# :: Proxy# "foo") :: Has r "foo" => r > FldTy r "foo"`, 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, using206 207 {{{ 208 field :: Accessor p r n => Proxy# n > p r (FldTy r n)214 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 packages such as [http://hackage.haskell.org/package/lens lens], [http://hackage.haskell.org/package/dataaccessor dataaccessor] or [http://hackage.haskell.org/package/datalens datalens]). This requires a slightly more general translation, using 215 216 {{{ 217 field :: Accessor p r n t => Proxy# n > p r t 209 218 field z = accessField z (getField z) (setField z) 210 219 }}} 211 220 212 to translate `foo` to `field (proxy# :: Proxy# "foo") :: Accessor p r "foo" => p r (FldTy r "foo")`. The `Accessor` class is defined thus:213 214 {{{ 215 class Accessor (p :: * > * > *) (r :: *) (n :: Symbol) where221 to translate `foo` to `field (proxy# :: Proxy# "foo") :: Accessor p r "foo" t => p r t`. The `Accessor` class is defined thus: 222 223 {{{ 224 class Accessor (p :: * > * > *) (r :: *) (n :: Symbol) (t :: *) where 216 225 accessField :: Proxy# n > 217 (Has r n => r > FldTy r n) >226 (Has r n t => r > t) > 218 227 (forall a . Upd r n a => r > a > UpdTy r n a) > 219 p r (FldTy r n)220 }}} 221 222 An instance of `Accessor p r n ` means that `p` may contain a getter and setter for the field `n` in record type `r`. In particular, we can give an instance for functions that ignores `r`, `n` andthe setter completely:223 224 {{{ 225 instance Has r n => Accessor (>) r nwhere228 p r t 229 }}} 230 231 An instance of `Accessor p r n t` means that `p` may contain a getter and setter for the field `n` of type `t` in record type `r`. In particular, we can give an instance for functions that ignores the setter completely: 232 233 {{{ 234 instance Has r n t => Accessor (>) r n t where 226 235 accessor _ getter setter = getter 227 236 }}} … … 233 242 {{{ 234 243 newtype WrapLens n r a 235 = MkWrapLens (forall b . Upd r n b => Lens r ( SetResultr n b) a b)244 = MkWrapLens (forall b . Upd r n b => Lens r (UpdTy r n b) a b) 236 245 237 246 instance m ~ n => Accessor (WrapLens m) r n where 238 247 accessor _ getter setter = MkWrapLens (\ w s > setter s <$> w (getter s)) 239 248 240 fieldLens :: Upd r n b => WrapLens n r a > Lens r ( SetResultr n b) a b249 fieldLens :: Upd r n b => WrapLens n r a > Lens r (UpdTy r n b) a b 241 250 fieldLens (MkWrapLens l) = l 242 251 }}} … … 251 260 , setDL :: r > a > r } 252 261 253 instance Upd r n (FldTy r n) => Accessor DataLens r nwhere262 instance Upd r n t => Accessor DataLens r n t where 254 263 accessField _ g s = DataLens g s 255 264 }}} … … 413 422 === Syntactic sugar for `Upd` constraints === 414 423 415 Should we have a special syntax for `Upd` constraints, just as `r { x :: t }` sugars ` (Has r "x", FldTy r "x" ~ t)`? What should it look like? Perhaps something like `r { x ::= t }`?424 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 }`? 416 425 417 426 … … 421 430 === Trouble in paradise === 422 431 423 [http://www.haskell.org/pipermail/glasgowhaskellusers/2013July/022584.html Edward Kmett points out] that a previous version of this proposal, where the `Has` class took three parameters and the thirdwas 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, suppose432 [http://www.haskell.org/pipermail/glasgowhaskellusers/2013July/022584.html Edward Kmett points out] that a previous version of this proposal, where the third parameter of the `Has` class 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 424 433 425 434 {{{ … … 445 454 446 455 type instance FldTy Person "fullName" = String 447 instance Has Person "fullName"where456 instance t ~ String => Has Person "fullName" t where 448 457 getField _ p = firstName p ++ " " ++ lastName p 449 458 }}}