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


Ignore:
Timestamp:
Jun 19, 2013 8:37:33 AM (2 years 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`).