... | ... | @@ -41,6 +41,11 @@ Previous versions of this proposal suggested changing the lexical syntax so that |
|
|
|
|
|
In the light of feedback, we propose **no changes to dot syntax** for the time being. In the future, we could add a separate extension to treat [dot as postfix function application](records/declared-overloaded-record-fields/dot-postfix). Note that the [ lens](http://hackage.haskell.org/package/lens) library encourages the use of dot with no spaces, as composition is used to chain lenses.
|
|
|
|
|
|
### Projections
|
|
|
|
|
|
|
|
|
Record field constraints are introduced by projections. If there are two or more fields `x` in scope, then an occurrence of `x` has type `a { x :: b } => a -> b` instead of generating an ambiguity error. If there is a single field `x` in scope, then it refers to the usual monomorphic record selector (ensuring backwards compatibility). If there are any normal identifiers `x` in scope (as well as fields) then a use of `x` leads to an ambiguity error.
|
|
|
|
|
|
### Record field constraints
|
|
|
|
|
|
|
... | ... | @@ -55,7 +60,7 @@ class Has (r :: *) (x :: Symbol) (t :: *) where |
|
|
Recall that `Symbol` is the kind of type-level strings. The notation 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])`.
|
|
|
|
|
|
|
|
|
Instances for the `Has` typeclass are implicitly generated, corresponding to fields in datatype definitions. For example, the data type
|
|
|
Instances for the `Has` typeclass are automatically generated (for modules with `-XOverloadedRecordFields` enabled) using the record fields that are in scope. For example, the data type
|
|
|
|
|
|
```wiki
|
|
|
data T a = MkT { x :: [a] }
|
... | ... | @@ -72,18 +77,13 @@ instance (b ~ [a]) => Has (T a) "x" b where |
|
|
|
|
|
The `(b ~ [a])` in the instance is important, so that we get an instance match from the first two fields only. 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])`.
|
|
|
|
|
|
### Projections: the dot operator
|
|
|
|
|
|
|
|
|
Record field constraints are introduced by projections. If there are two or more fields `x` in scope, then an occurrence of `x` has type `a { x :: b } => a -> b` instead of generating an ambiguity error. If there is a single field `x` in scope, then it refers to the usual monomorphic record selector (ensuring backwards compatibility). If there are any normal identifiers `x` in scope (as well as fields) then a use of `x` leads to an ambiguity error.
|
|
|
|
|
|
### Representation hiding
|
|
|
|
|
|
|
|
|
At present, a datatype in one module can declare a field, but if the selector function is not exported, then the field is hidden from clients of the module. It is important to support this. Typeclasses in general have no controls over their scope, but for implicitly generated `Has` instances, the instance is in scope iff the record field selector function is.
|
|
|
At present, a datatype in one module can declare a field, but if the selector function is not exported, then the field is hidden from clients of the module. It is important to support this. Typeclasses in general have no controls over their scope, but for implicitly generated `Has` instances, the instance is available for a module if `-XOverloadedRecordFields` is enabled for that module and the record field selector function is in scope.
|
|
|
|
|
|
|
|
|
This enables representation hiding: exporting the field selector is a proxy for permitting access to the field. For example, consider the following module:
|
|
|
This enables representation hiding: just like at present, exporting the field selector permits access to the field. For example, consider the following module:
|
|
|
|
|
|
```wiki
|
|
|
module M ( R(x) ) where
|
... | ... | @@ -93,187 +93,163 @@ data S = S { x :: Bool } |
|
|
```
|
|
|
|
|
|
|
|
|
Any 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.
|
|
|
Any 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.
|
|
|
|
|
|
### Record update
|
|
|
### Multiple modules and automatic instance generation
|
|
|
|
|
|
|
|
|
Supporting polymorphic record update is rather more complex than polymorphic lookup. In particular:
|
|
|
Note that `Has` instances are generated on a per-module basis, using the fields that are in scope for that module, and automatically generated instances are never exported. Thus it doesn't matter whether `-XOverloadedRecordFields` was on in the module that defined the datatype. The availability of the instances in a particular module depends only on whether the flag is enabled for that module.
|
|
|
|
|
|
- the type of the record may change as a result of the update;
|
|
|
- multiple fields must be updated simultaneously for an update to be type correct (so iterated single update is not enough); and
|
|
|
- records may include higher-rank components.
|
|
|
|
|
|
Suppose module `M` imports module `N`, `N` imports module `O`, and only `N` has the extension enabled. Now `N` can project any field in scope (including those defined in `O`), but `M` cannot access any `Has` instances.
|
|
|
|
|
|
These problems have already been [described in some detail](records/overloaded-record-fields#record-updates). In the interests of doing something, even if imperfect, we plan to support only monomorphic record update. For overloaded fields to be updated, a type signature may be required in order to specify the type being updated. For example,
|
|
|
|
|
|
```wiki
|
|
|
e { x = t }
|
|
|
```
|
|
|
|
|
|
This means that
|
|
|
|
|
|
currently relies on the name `x` to determine the datatype of the record. If this is ambiguous, a type signature can be given either to `e` or to the whole expression. Thus either
|
|
|
- the extension is required whenever a `Has` constraint must be solved;
|
|
|
- no new mechanism for hiding instances is required; and
|
|
|
- records defined in existing modules (or other packages) without the extension can still be overloaded.
|
|
|
|
|
|
```wiki
|
|
|
e :: T Int { x = t }
|
|
|
```
|
|
|
### Higher-rank fields
|
|
|
|
|
|
|
|
|
or
|
|
|
If a field has a rank-1 type, the `Has` encoding works fine: for example,
|
|
|
|
|
|
```wiki
|
|
|
e { x = t } :: T Int
|
|
|
data T = MkT { x :: forall a . a -> a }
|
|
|
```
|
|
|
|
|
|
|
|
|
will be accepted. (Really only the type constructor is needed, whereas this approach requires the whole type to be specified, but it seems simpler than inventing a whole new syntax.)
|
|
|
|
|
|
## Design choices
|
|
|
gives rise to the instance
|
|
|
|
|
|
### Record update: avoiding redundant annotations
|
|
|
```wiki
|
|
|
instance (b ~ a -> a) => Has T "x" b
|
|
|
```
|
|
|
|
|
|
|
|
|
If `e` is a variable, whose type is given explicitly in the context, we could look it up rather than requiring it to be given again. Thus
|
|
|
However, if a field has a rank-2 type or higher (so the selector function has rank at least 3), things are looking dangerously impredicative:
|
|
|
|
|
|
```wiki
|
|
|
f :: T Int -> T Int
|
|
|
f v = v { x = 5 }
|
|
|
data T b = MkT { x :: (forall a . a -> a) -> b }
|
|
|
```
|
|
|
|
|
|
|
|
|
would not require an extra annotation. On the other hand, we would need an annotation on the update in
|
|
|
would give
|
|
|
|
|
|
```wiki
|
|
|
\v -> (v { x = 4 }, [v, w :: T Int])
|
|
|
instance (c ~ ((forall a . a -> a) -> b)) => Has (T b) "x" c
|
|
|
```
|
|
|
|
|
|
|
|
|
because the type of `v` is only determined later, by constraint solving.
|
|
|
but 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 `x e`, but overloaded record fields prevent this. Non-overloaded field names are likely to be needed in this case.
|
|
|
|
|
|
### Record update
|
|
|
|
|
|
Annoyingly, nested updates will require some annotations. In the following example, the outer update need not be annotated (since `v` is a variable that is explicitly given a type by the context) but the inner update must be (since `x v` is not a variable):
|
|
|
|
|
|
```wiki
|
|
|
f :: T Int -> T Int
|
|
|
f v = v { x = (x v){ y = 6 } }
|
|
|
```
|
|
|
Supporting polymorphic record update is rather more complex than polymorphic lookup. In particular:
|
|
|
|
|
|
### Virtual record fields
|
|
|
- the type of the record may change as a result of the update;
|
|
|
- multiple fields must be updated simultaneously for an update to be type correct (so iterated single update is not enough); and
|
|
|
- records may include higher-rank components.
|
|
|
|
|
|
|
|
|
It is easy to support virtual record fields, by permitting explicit `Has` instances:
|
|
|
These problems have already been [described in some detail](records/overloaded-record-fields#record-updates). In the interests of doing something, even if imperfect, we plan to support only monomorphic record update. For overloaded fields to be updated, a type signature may be required in order to specify the type being updated. For example,
|
|
|
|
|
|
```wiki
|
|
|
instance ctx => Has r "x" t where
|
|
|
getFld = blah :: r -> t
|
|
|
e { x = t }
|
|
|
```
|
|
|
|
|
|
|
|
|
Note that if `r` is a datatype with a field `x`, the virtual field will overlap, and the usual rules about overlap checking apply. Explicit instances follow the usual instance scope rules, so a virtual record field instance is always exported and imported.
|
|
|
|
|
|
`Has` constraints are slightly more general than the syntactic sugar suggests: one could imagine building constraints of the form `Has r l t` where `l` is non-canonical, for example a variable or type family. It's hard to imagine uses for such constraints, though. One idea is giving virtual fields of all possible names to a type:
|
|
|
currently relies on the name `x` to determine the datatype of the record. If this is ambiguous, a type signature can be given either to `e` or to the whole expression. Thus either
|
|
|
|
|
|
```wiki
|
|
|
instance Has T l () where
|
|
|
getFld _ = ()
|
|
|
e :: T Int { x = t }
|
|
|
```
|
|
|
|
|
|
### Record selectors
|
|
|
|
|
|
|
|
|
Even with `-XOverloadedRecordFields` enabled, monomorphic record selector functions will be generated by default for backwards compatibility reasons, and for use when there is no ambiguity. They will not be usable if multiple selectors with the same name are in scope.
|
|
|
|
|
|
|
|
|
Optionally, we could [add a flag \`-XNoMonoRecordFields\`](records/declared-overloaded-record-fields/no-mono-record-fields) 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**). 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 [representation hiding](records/overloaded-record-fields/plan#representation-hiding) section).
|
|
|
|
|
|
|
|
|
We could also add a flag `-XPolyRecordFields` to generate polymorphic selector functions. This implies `-XNoMonoRecordFields`. For example, if a record with field `x` is declared then the function
|
|
|
or
|
|
|
|
|
|
```wiki
|
|
|
x :: Has r "x" t => r -> t
|
|
|
x = getFld
|
|
|
e { x = t } :: T Int
|
|
|
```
|
|
|
|
|
|
|
|
|
would be generated. However, these have slightly odd behaviour: if two independent imported modules declare fields with the same label, they will both generate identical polymorphic selectors, so only one of them should be brought into scope.
|
|
|
will be accepted. (Really only the type constructor is needed, whereas this approach requires the whole type to be specified, but it seems simpler than inventing a whole new syntax.)
|
|
|
|
|
|
### Monomorphism restriction and defaulting
|
|
|
## Design choices
|
|
|
|
|
|
### Record update: avoiding redundant annotations
|
|
|
|
|
|
|
|
|
The monomorphism restriction may cause annoyance, since
|
|
|
If `e` is a variable, whose type is given explicitly in the context, we could look it up rather than requiring it to be given again. Thus
|
|
|
|
|
|
```wiki
|
|
|
foo = \ e -> x e
|
|
|
f :: T Int -> T Int
|
|
|
f v = v { x = 5 }
|
|
|
```
|
|
|
|
|
|
|
|
|
would naturally be assigned a polymorphic type. If there is only one `x` in scope, perhaps the constraint solver should pick that one (analogously to the other defaulting rules). However, this would mean that bringing a new `x` into scope (e.g. adding an import) could break code. Of course, it is already the case that bringing new identifiers into scope can create ambiguity!
|
|
|
|
|
|
|
|
|
For example, suppose the following definitions are in scope:
|
|
|
would not require an extra annotation. On the other hand, we would need an annotation on the update in
|
|
|
|
|
|
```wiki
|
|
|
data T = MkT { x :: Int, y :: Int }
|
|
|
data S = MkS { y :: Bool }
|
|
|
\v -> (v { x = 4 }, [v, w :: T Int])
|
|
|
```
|
|
|
|
|
|
|
|
|
Inferring the type of `foo = \ e -> x e` results in `alpha -> beta` subject to the constraint `alpha { x :: beta }`. However, the monomorphism restriction prevents this constraint from being generalised. There is only one `x` field in scope, so defaulting specialises the type to `T -> Int`. If the `y` field was used, it would instead give rise to an ambiguity error.
|
|
|
|
|
|
### Higher-rank fields
|
|
|
because the type of `v` is only determined later, by constraint solving.
|
|
|
|
|
|
|
|
|
If a field has a rank-1 type, the `Has` encoding works fine: for example,
|
|
|
Annoyingly, nested updates will require some annotations. In the following example, the outer update need not be annotated (since `v` is a variable that is explicitly given a type by the context) but the inner update must be (since `x v` is not a variable):
|
|
|
|
|
|
```wiki
|
|
|
data T = MkT { x :: forall a . a -> a }
|
|
|
f :: T Int -> T Int
|
|
|
f v = v { x = (x v){ y = 6 } }
|
|
|
```
|
|
|
|
|
|
### Polymorphic record update for lenses
|
|
|
|
|
|
gives rise to the instance
|
|
|
|
|
|
As noted above, supporting a polymorphic version of the existing record update syntax (in its full generality) is difficult. However, even if the existing record update syntax remains monomorphic, an additional motivation for polymorphic update comes from [ lens](http://hackage.haskell.org/package/lens). If we automatically generate instances of an extra class like
|
|
|
|
|
|
```wiki
|
|
|
instance (b ~ a -> a) => Has T "x" b
|
|
|
class Set (r :: *) (x :: Symbol) (t :: *) where
|
|
|
setFld :: r -> t -> r
|
|
|
```
|
|
|
|
|
|
|
|
|
However, if a field has a rank-2 type or higher (so the selector function has rank at least 3), things are looking dangerously impredicative:
|
|
|
and supply the instance (where `&x` is used for explicit type application of the `x` argument)
|
|
|
|
|
|
```wiki
|
|
|
data T b = MkT { x :: (forall a . a -> a) -> b }
|
|
|
instance (Functor f, Has s x a, Set s x a, fs ~ f s, fa ~ f a) => Has (a -> fa) x (s -> fs) where
|
|
|
getFld f r = setFld &s &x &a r <$> f (getFld &s &x &a r)
|
|
|
```
|
|
|
|
|
|
|
|
|
would give
|
|
|
then every record field (for which a `Set` instance can be generated) is automagically a lens. This reduces the need for the current name-mangling Template Haskell implemented in the lens library. (Note that this instance requires explicit type application, or a proxy-based workaround, in order to supply the `x` argument.)
|
|
|
|
|
|
```wiki
|
|
|
instance (c ~ ((forall a . a -> a) -> b)) => Has (T b) "x" c
|
|
|
```
|
|
|
|
|
|
More work is needed to identify the right way to formulate the `Set` class: type-changing update requires a slightly more general version, and there is a story for [ multiple update](https://github.com/ekmett/lens/issues/197). Higher-rank fields remain problematic.
|
|
|
|
|
|
but 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 `x e`, but overloaded record fields prevent this. Traditional monomorphic selector functions are likely to be needed in this case.
|
|
|
### User-defined `Has` instances
|
|
|
|
|
|
### Multiple modules and implicit instance generation
|
|
|
|
|
|
Should the user be allowed to write explicit `Has` instances? For example:
|
|
|
|
|
|
When should `Has` instances be implicitly generated? I can think of three options:
|
|
|
|
|
|
1. If the extension is on for a module, generate instances for all datatypes in that module when checking their declarations. This means that record projections are not available to code that imports a datatype definition from a module without the flag. Some mechanism will need to restrict the scope of instances based on import/export of selectors.
|
|
|
1. If the extension is on for a module, generate instances for all record selectors that are in scope, but do not export them. Thus it doesn't matter whether the flag was on in the module that defined the datatype, and the availability of the instances in a particular module depends only on whether the flag is enabled.
|
|
|
1. If the extension is on for a module, generate and export instances for all record selectors that are in scope and do not already have instances. This is a hybrid of (1) and (2), and also requires a mechanism to restrict instance scope based on import/export of selectors.
|
|
|
```wiki
|
|
|
instance ctx => Has r "x" t where
|
|
|
getFld = blah :: r -> t
|
|
|
```
|
|
|
|
|
|
|
|
|
Note that (2) can be equivalently implemented (as far as the user is concerned) by not really generating instances at all, but solving `Has` constraints directly based on the selectors in scope, much as `SingI` constraints are solved on-the-fly.
|
|
|
Even with an explicit `Has` instance as above, the name `x` will not be in scope unless a datatype has a field with name `x`. Thus it is not really useful. The previous proposal, where `(.x)` always meant "project out the `x` field", used explicit `Has` instances for virtual fields.
|
|
|
|
|
|
### Hiding record selectors
|
|
|
|
|
|
Suppose module `M` imports module `N`, `N` imports module `O`, and only `N` has the extension enabled. Under (1), `N` can project fields it defines (but not those defined in `O`), and `M` also has access to the `Has` instances for `N` (but not the dot syntax). Under (2), `N` can project any field in scope (including those defined in `O`), but `M` cannot access any `Has` instances. Under (3), `N` can project any field in scope, and `M` has access to the `Has` instances for `N` and `O` (but not fields defined in `M`).
|
|
|
|
|
|
Optionally, we could [add a flag \`-XNoMonoRecordFields\`](records/declared-overloaded-record-fields/no-mono-record-fields) to suppress the record selectors. Just as `-XOverloadedRecordFields` applies to a client module, and generates `Has` instances for that module, so `-XNoMonoRecordFields` in a client module would hide all the record selectors that should otherwise be in scope. The idea is that another record system could use Template Haskell to generate functions in place of selectors, and these would not clash.
|
|
|
|
|
|
I think (2) is probably the right choice here, because
|
|
|
|
|
|
- the extension is required whenever dot notation is used or a `Has` constraint must be solved;
|
|
|
- no new mechanism for hiding instances is required; and
|
|
|
- records defined in existing modules (or other packages) without the extension can still be used with dot notation.
|
|
|
Since the selectors are hidden by clients (on import) rather than on export, fields can still be mentioned in import and export lists, to control access to them (as discussed in the [representation hiding](records/overloaded-record-fields/plan#representation-hiding) section), and used for record update.
|
|
|
|
|
|
## Example of constraint solving
|
|
|
|
... | ... | @@ -296,6 +272,8 @@ module N where |
|
|
bar = foo T
|
|
|
|
|
|
baz = foo S
|
|
|
|
|
|
quux = y
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -306,3 +284,6 @@ When checking `bar`, the application of `foo` gives rise to the constraint `T { |
|
|
|
|
|
|
|
|
When checking `baz`, the constraint `S { x :: gamma }` is generated and rejected, since the `x` from `S` is not in scope.
|
|
|
|
|
|
|
|
|
When checking `quux`, the only `y` field in scope is of type `S -> Bool` so that is its type. |