Changes between Version 25 and Version 26 of Records/OverloadedRecordFields/Implementation


Ignore:
Timestamp:
Aug 6, 2013 7:24:57 AM (9 months ago)
Author:
adamgundry
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Records/OverloadedRecordFields/Implementation

    v25 v26  
    11= Overloaded record fields: implementation notes = 
    22 
    3 Here be dragons. This page describes implementation details and progress on the implementation of [wiki:Records/OverloadedRecordFields/Plan the overloaded record fields plan]. Development of the extension is taking place on forks of the [https://github.com/adamgundry/ghc ghc] and [https://github.com/adamgundry/packages-base packages-base] repositories (on branch 'overloaded-record-fields'). 
     3Here be dragons. This page describes implementation details and progress on the implementation of [wiki:Records/OverloadedRecordFields/Plan the overloaded record fields plan]. Development of the extension is taking place on forks of the [https://github.com/adamgundry/ghc ghc] and [https://github.com/adamgundry/packages-base packages-base] repositories (on branch 'overloaded-record-fields'). A [https://github.com/adamgundry/records-prototype/blob/master/RecordsPrototype.hs prototype implementation] is also available. 
    44 
    55== The basic idea == 
    66 
    7 Typechecking a record datatype still generates record selectors, but their names have a `$sel` prefix and end with the name of their type. Thus 
     7The `Has` and `Upd` classes, and `GetResult` and `SetResult` type families, are defined in the module [https://github.com/adamgundry/packages-base/blob/overloaded-record-fields/GHC/Records.hs GHC.Records] in the `base` package. 
     8 
     9Typechecking a record datatype still generates record selectors, but their names have a `$sel` prefix and end with the name of their type. Moreover, instances for the classes and type families are generated. For example, 
    810 
    911{{{ 
     
    1416 
    1517{{{ 
    16 $sel_x_T :: T -> Int       -- record selector (used to be called `x`) 
     18$sel_x_T :: T -> Int -- record selector (used to be called `x`) 
    1719$sel_x_T (MkT x) = x 
    1820 
    19 $dfHasTx :: Has T "x"      -- corresponds to the Has instance decl 
    20 $dfHasTx = Has { getField _     = $sel_x_T 
    21                , setField _ s e = s { x = e } } 
     21$dfHasTx :: forall a . a ~ Int => Has T "x" a -- corresponds to the Has instance decl 
     22$dfHasTx = Has { getField _ = $sel_x_T } 
    2223 
    23 axiom TFCo:R:GetResult : GetResult T "x" = Int  -- corresponds to the GetResult type family instance 
     24$dfUpdTx :: forall a . a ~ Int => Upd T "x" a -- corresponds to the Upd instance decl 
     25$dfUpdTx = Upd { setField _ s e = s { x = e } } 
     26 
     27axiom TFCo:R:GetResult : GetResult T "x" = Int   -- corresponds to the GetResult type family instance 
     28axiom TFCo:R:SetResult : SetResult T "x" Int = T -- corresponds to the SetResult type family instance 
    2429}}} 
    2530 
     
    3439}}} 
    3540 
    36 '''SLPJ''' moreover I think we should store the ''dictionary'' `$dfHasTfoo` in the GRE for `foo`, not the selector.  That way we get both getter and setter (via the dictionary) in one go.  '''AMG''' Now I'm not sure about this. We can't build the dictionary for higher-rank fields, but they have a perfectly good selector. Moreover, if we want type-changing update there will be two dictionaries (one for the getter and one for the setter). 
     41'''SLPJ''' moreover I think we should store the ''dictionary'' `$dfHasTfoo` in the GRE for `foo`, not the selector.  That way we get both getter and setter (via the dictionary) in one go.  '''AMG''' Now I'm not sure about this. We can't build the dictionary for higher-rank fields, but they have a perfectly good selector. Moreover, with type-changing update there are two dictionaries (one for the getter and one for the setter) and two coercion axioms. 
    3742 
    3843Note that the `OccName` used when adding a GRE to the environment (`greOccName`) now depends on the parent field: for `FldParent` it is the field label rather than the selector name.