Changes between Version 8 and Version 9 of Records/OverloadedRecordFields/Plan


Ignore:
Timestamp:
Jun 19, 2013 8:37:33 AM (10 months ago)
Author:
adamgundry
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Records/OverloadedRecordFields/Plan

    v8 v9  
    8080 
    8181Any 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 in scope but the instance `Has S "x" Bool` will not be. Thus `R { x :: Int }` will be solved but `S { x :: Bool }` will not. 
    82  
    83  
    84 === Record selectors ===  
    85  
    86 Optionally, we could [wiki:Records/DeclaredOverloadedRecordFields/NoMonoRecordFields add a flag `-XNoMonoRecordFields`] to disable the generation of the usual monomorphic record field selector functions.  This is not essential, but would free up the namespace for other record systems (e.g. '''lens'''). Note that `-XOverloadedRecordFields` will generate monomorphic selectors by default for backwards compatibility reasons, but they will not be usable if multiple selectors with the same name are in scope. 
    87  
    88 When either flag is enabled, the same field label may be declared repeatedly in a single module (or a label may be declared when a function of that name is already in scope). 
    89  
    90 Even if the selector functions are suppressed, we still need to be able to mention the fields in import and export lists, to control access to them (as discussed in the previous section). 
    91  
    92 '''AMG''' perhaps we should also have a flag to automatically generate the polymorphic record selectors? These are slightly odd: if two independent imported modules declare fields with the same label, only a single polymorphic record selector should be brought into scope. 
    9382 
    9483 
     
    157146 
    158147 
     148=== Record selectors ===  
     149 
     150Optionally, we could [wiki:Records/DeclaredOverloadedRecordFields/NoMonoRecordFields add a flag `-XNoMonoRecordFields`] to disable the generation of the usual monomorphic record field selector functions.  This is not essential, but would free up the namespace for other record systems (e.g. '''lens'''). Note that `-XOverloadedRecordFields` will generate monomorphic selectors by default for backwards compatibility reasons, but they will not be usable if multiple selectors with the same name are in scope. 
     151 
     152When either flag is enabled, the same field label may be declared repeatedly in a single module (or a label may be declared when a function of that name is already in scope). 
     153 
     154Even if the selector functions are suppressed, we still need to be able to mention the fields in import and export lists, to control access to them (as discussed in the [wiki:Records/OverloadedRecordFields/Plan#Representationhiding representation hiding] section). 
     155 
     156'''AMG''' perhaps we should also have a flag to automatically generate the polymorphic record selectors? These are slightly odd: if two independent imported modules declare fields with the same label, only a single polymorphic record selector should be brought into scope. 
     157 
     158 
    159159=== Monomorphism restriction and defaulting === 
    160160 
     
    176176 
    177177 
    178  
    179 == Implementation details == 
    180  
    181  
    182 === Example of constraint solving === 
    183  
    184 '''AMG''' need to update these examples. 
    185  
    186 '''SLPJ''' Making the first example rely on the monomorphism restriction is not a good plan! 
     178=== Higher-rank fields === 
     179 
     180If a field has a rank-1 type, the `Has` encoding works fine: for example, 
     181{{{ 
     182data T = MkT { x :: forall a . a -> a } 
     183}}} 
     184gives rise to the instance 
     185{{{ 
     186instance b ~ a -> a => Has T "x" b 
     187}}} 
     188 
     189However, if a field has a rank-2 type or higher (so the selector function has rank at least 3), things are looking dangerously impredicative: 
     190{{{ 
     191data T b = MkT { x :: (forall a . a -> a) -> b } 
     192}}} 
     193would give 
     194{{{ 
     195instance c ~ (forall a . a -> a) -> b => Has (T b) "x" c 
     196}}} 
     197but this is currently forbidden by GHC, even with `-XImpredicativeTypes` enabled. Indeed, it would not be much use if it were possible, because bidirectional type inference relies on being able to immediately infer the type of neutral terms like `e.x`, but overloaded record fields prevent this. Traditional monomorphic selector functions are likely to be needed in this case. 
     198 
     199 
     200== Example of constraint solving == 
    187201 
    188202Consider the example 
     
    199213 
    200214  foo e = e.x 
    201  
    202   qux = (.y) 
    203215  
    204216  bar :: Bool 
     
    208220}}} 
    209221 
    210 When checking `foo`, `e` is a variable of unknown type `alpha`, and the projection generates the constraint `alpha { x :: beta }` where `beta` is fresh.  
    211 This constraint cannot be solved immediately, so generalisation yields the type `a { x :: b } => a -> b`. 
    212  
    213 When checking `qux`, the projection has type `alpha -> beta` and generates the constraint `alpha { y :: beta }`. However, the monomorphism restriction prevents this constraint from being generalised. There is only one `y` field in scope, so defaulting specialises the type to `S -> Bool`. If the `x` field was used, it would instead give rise to an ambiguity error. 
     222When checking `foo`, `e` is a variable of unknown type `alpha`, and the projection generates the constraint `alpha { x :: beta }` where `beta` is fresh. This constraint cannot be solved immediately, so generalisation yields the type `a { x :: b } => a -> b`. 
    214223 
    215224When checking `bar`, the application of `foo` gives rise to the constraint `T { x :: Bool }`, which is solved since `Bool` is an instance of `forall a . a` (the type `T` gives to `x`).