1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
|
.. _record-field-selector-polymorphism:
Record field selector polymorphism
----------------------------------
The module :base-ref:`GHC.Records.` defines the following: ::
class HasField (x :: k) r a | x r -> a where
getField :: r -> a
A ``HasField x r a`` constraint represents the fact that ``x`` is a
field of type ``a`` belonging to a record type ``r``. The
``getField`` method gives the record selector function.
This allows definitions that are polymorphic over record types with a specified
field. For example, the following works with any record type that has a field
``name :: String``: ::
foo :: HasField "name" r String => r -> String
foo r = reverse (getField @"name" r)
``HasField`` is a magic built-in typeclass (similar to ``Coercible``, for
example). It is given special treatment by the constraint solver (see
:ref:`solving-hasfield-constraints`). Users may define their own instances of
``HasField`` also (see :ref:`virtual-record-fields`).
.. _solving-hasfield-constraints:
Solving HasField constraints
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the constraint solver encounters a constraint ``HasField x r a``
where ``r`` is a concrete datatype with a field ``x`` in scope, it
will automatically solve the constraint using the field selector as
the dictionary, unifying ``a`` with the type of the field if
necessary. This happens irrespective of which extensions are enabled.
For example, if the following datatype is in scope ::
data Person = Person { name :: String }
the end result is rather like having an instance ::
instance HasField "name" Person String where
getField = name
except that this instance is not actually generated anywhere, rather
the constraint is solved directly by the constraint solver.
A field must be in scope for the corresponding ``HasField`` constraint
to be solved. This retains the existing representation hiding
mechanism, whereby a module may choose not to export a field,
preventing client modules from accessing or updating it directly.
Solving ``HasField`` constraints depends on the field selector functions that
are generated for each datatype definition:
- If a record field does not have a selector function because its type would allow
an existential variable to escape, the corresponding ``HasField`` constraint
will not be solved. For example, ::
{-# LANGUAGE ExistentialQuantification #-}
data Exists t = forall x . MkExists { unExists :: t x }
does not give rise to a selector ``unExists :: Exists t -> t x`` and we will not
solve ``HasField "unExists" (Exists t) a`` automatically.
- If a record field has a polymorphic type (and hence the selector function is
higher-rank), the corresponding ``HasField`` constraint will not be solved,
because doing so would violate the functional dependency on ``HasField`` and/or
require impredicativity. For example, ::
{-# LANGUAGE RankNTypes #-}
data Higher = MkHigher { unHigher :: forall t . t -> t }
gives rise to a selector ``unHigher :: Higher -> (forall t . t -> t)`` but does
not lead to solution of the constraint ``HasField "unHigher" Higher a``.
- A record GADT may have a restricted type for a selector function, which may lead
to additional unification when solving ``HasField`` constraints. For example, ::
{-# LANGUAGE GADTs #-}
data Gadt t where
MkGadt :: { unGadt :: Maybe v } -> Gadt [v]
gives rise to a selector ``unGadt :: Gadt [v] -> Maybe v``, so the solver will reduce
the constraint ``HasField "unGadt" (Gadt t) b`` by unifying ``t ~ [v]`` and
``b ~ Maybe v`` for some fresh metavariable ``v``, rather as if we had an instance ::
instance (t ~ [v], b ~ Maybe v) => HasField "unGadt" (Gadt t) b
- If a record type has an old-fashioned datatype context, the ``HasField``
constraint will be reduced to solving the constraints from the context.
For example, ::
{-# LANGUAGE DatatypeContexts #-}
data Eq a => Silly a = MkSilly { unSilly :: a }
gives rise to a selector ``unSilly :: Eq a => Silly a -> a``, so
the solver will reduce the constraint ``HasField "unSilly" (Silly a) b`` to
``Eq a`` (and unify ``a`` with ``b``), rather as if we had an instance ::
instance (Eq a, a ~ b) => HasField "unSilly" (Silly a) b
.. _virtual-record-fields:
Virtual record fields
~~~~~~~~~~~~~~~~~~~~~
Users may define their own instances of ``HasField``, provided they do
not conflict with the built-in constraint solving behaviour. This
allows "virtual" record fields to be defined for datatypes that do not
otherwise have them.
For example, this instance would make the ``name`` field of ``Person``
accessible using ``#fullname`` as well: ::
instance HasField "fullname" Person String where
getField = name
More substantially, an anonymous records library could provide
``HasField`` instances for its anonymous records, and thus be
compatible with the polymorphic record selectors introduced by this
proposal. For example, something like this makes it possible to use
``getField`` to access ``Record`` values with the appropriate
string in the type-level list of fields: ::
data Record (xs :: [(k, Type)]) where
Nil :: Record '[]
Cons :: Proxy x -> a -> Record xs -> Record ('(x, a) ': xs)
instance HasField x (Record ('(x, a) ': xs)) a where
getField (Cons _ v _) = v
instance HasField x (Record xs) a => HasField x (Record ('(y, b) ': xs)) a where
getField (Cons _ _ r) = getField @x r
r :: Record '[ '("name", String) ]
r = Cons Proxy "R" Nil)
x = getField @"name" r
Since representations such as this can support field labels with kinds other
than ``Symbol``, the ``HasField`` class is poly-kinded (even though the built-in
constraint solving works only at kind ``Symbol``). In particular, this allows
users to declare scoped field labels such as in the following example: ::
data PersonFields = Name
s :: Record '[ '(Name, String) ]
s = Cons Proxy "S" Nil
y = getField @Name s
In order to avoid conflicting with the built-in constraint solving,
the following user-defined ``HasField`` instances are prohibited (in
addition to the usual rules, such as the prohibition on type
families appearing in instance heads):
- ``HasField _ r _`` where ``r`` is a variable;
- ``HasField _ (T ...) _`` if ``T`` is a data family (because it
might have fields introduced later, using data instance declarations);
- ``HasField x (T ...) _`` if ``x`` is a variable and ``T`` has any
fields at all (but this instance is permitted if ``T`` has no fields);
- ``HasField "foo" (T ...) _`` if ``T`` has a field ``foo`` (but this
instance is permitted if it does not).
If a field has a higher-rank or existential type, the corresponding ``HasField``
constraint will not be solved automatically (as described above), but in the
interests of simplicity we do not permit users to define their own instances
either. If a field is not in scope, the corresponding instance is still
prohibited, to avoid conflicts in downstream modules.
|
