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


Ignore:
Timestamp:
Feb 15, 2014 2:08:13 PM (17 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}}}