Changes between Version 40 and Version 41 of Records/OverloadedRecordFields/Plan


Ignore:
Timestamp:
Feb 15, 2014 2:08:13 PM (19 months ago)
Author:
adamgundry
Comment:

Back to three parameters

Legend:

Unmodified
Added
Removed
Modified
  • Records/OverloadedRecordFields/Plan

    v40 v41  
    33This 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.google-melange.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.
    44
    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/packages-base packages-base], [https://github.com/adamgundry/haddock haddock] and [https://github.com/adamgundry/testsuite testsuite] repositories (on branch 'overloaded-record-fields'). A [https://github.com/adamgundry/records-prototype prototype implementation] is also available.
     5This 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/packages-base packages-base] and [https://github.com/adamgundry/haddock haddock] repositories (on branch 'overloaded-record-fields'). A [https://github.com/adamgundry/records-prototype prototype implementation] is also available.
    66
    77=== Motivation ===
     
    3939A 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.
    4040
    41 A record field constraint `r { x :: t }` is syntactic sugar for the pair of constraints `(Has r "x", FldTy r "x" ~ t)`, where
     41A record field constraint `r { x :: t }` is syntactic sugar for the constraint `Has r "x" t`, where
    4242
    4343{{{
    4444type family FldTy (r :: *) (n :: Symbol) :: *
    4545
    46 class Has r (n :: Symbol) where
    47   getField :: Proxy# n -> r -> FldTy r n
     46class t ~ FldTy r n => Has r (n :: Symbol) t where
     47  getField :: Proxy# n -> r -> t
    4848}}}
    4949
    5050Recall 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].) The type `Proxy#` is zero-width, so it will be erased at runtime, and is used to pass in the type-level string argument, since we don't have explicit type application (yet).
    5151
    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])`.
     52The 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`.
    5353
    5454Instances 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
     
    6363type instance FldTy (T a) "x" = [a]
    6464
    65 instance Has (T a) "x" where
     65instance b ~ [a] => Has (T a) "x" b where
    6666  getField _ (MkT x) = x
    6767}}}
    6868
    69 We have considered using a three-parameter 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).
     69The 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
     71The reason for using a three-parameter class, rather than just two parameters and a type family, is to support the syntactic sugar and improve type inference error messags. With a two-parameter class we could easily end up inferring types like the following, and it would be hard to reapply the sugar:
     72
     73{{{
     74f :: (Has r "x", Has r "y", FldTy r "x" ~ Int, FldTy r "y" ~ Int) => r -> Int
     75f r = x r + y r :: Int
     76}}}
     77
     78Moreover, error messages would tend to be reported in terms of unification failures for `FldTy` rather than unsolved `Has` class constraints.
    7079
    7180
     
    8392}}}
    8493
    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.
     94Any 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.
    8695
    8796
     
    166175type family UpdTy (r :: *) (n:: Symbol) (a :: *) :: *
    167176
    168 class (Has r n, r ~ UpdTy r n (FldTy r n)) =>
    169           Upd (r :: *) (n :: Symbol) (a :: *) where
    170   setField :: Proxy# n -> r -> a -> UpdTy r n a
     177class (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
    171180}}}
    172181
     
    203212=== Lens integration ===
    204213
    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, using
    206 
    207 {{{
    208 field :: Accessor p r n => Proxy# n -> p r (FldTy r n)
     214It 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/data-accessor data-accessor] or [http://hackage.haskell.org/package/data-lens data-lens]). This requires a slightly more general translation, using
     215
     216{{{
     217field :: Accessor p r n t => Proxy# n -> p r t
    209218field z = accessField z (getField z) (setField z)
    210219}}}
    211220
    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) where
     221to translate `foo` to `field (proxy# :: Proxy# "foo") :: Accessor p r "foo" t => p r t`. The `Accessor` class is defined thus:
     222
     223{{{
     224class Accessor (p :: * -> * -> *) (r :: *) (n :: Symbol) (t :: *) where
    216225  accessField :: Proxy# n ->
    217                  (Has r n => r -> FldTy r n) ->
     226                 (Has r n t => r -> t) ->
    218227                 (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` and the setter completely:
    223 
    224 {{{
    225 instance Has r n => Accessor (->) r n where
     228                 p r t
     229}}}
     230
     231An 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{{{
     234instance Has r n t => Accessor (->) r n t where
    226235  accessor _ getter setter = getter
    227236}}}
     
    233242{{{
    234243newtype WrapLens n r a
    235   = MkWrapLens (forall b . Upd r n b => Lens r (SetResult r n b) a b)
     244  = MkWrapLens (forall b . Upd r n b => Lens r (UpdTy r n b) a b)
    236245
    237246instance m ~ n => Accessor (WrapLens m) r n where
    238247  accessor _ getter setter = MkWrapLens (\ w s -> setter s <$> w (getter s))
    239248
    240 fieldLens :: Upd r n b => WrapLens n r a -> Lens r (SetResult r n b) a b
     249fieldLens :: Upd r n b => WrapLens n r a -> Lens r (UpdTy r n b) a b
    241250fieldLens (MkWrapLens l) = l
    242251}}}
     
    251260   , setDL :: r -> a -> r }
    252261
    253 instance Upd r n (FldTy r n) => Accessor DataLens r n where
     262instance Upd r n t => Accessor DataLens r n t where
    254263  accessField _ g s = DataLens g s
    255264}}}
     
    413422=== Syntactic sugar for `Upd` constraints ===
    414423
    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 }`?
     424Should 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 }`?
    416425
    417426
     
    421430=== Trouble in paradise ===
    422431
    423 [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 `Has` class took three parameters and the third 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
     432[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 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
    424433
    425434{{{
     
    445454
    446455type instance FldTy Person "fullName" = String
    447 instance Has Person "fullName" where
     456instance t ~ String => Has Person "fullName" t where
    448457  getField _ p = firstName p ++ " " ++ lastName p
    449458}}}