@@ -247,6 +247,106 @@ So, for example, the following definitions are legal:
247247 d y = c (y + 1 + z y)
248248 where z w = y + w
249249
250+
251+Records
252+=======
253+
254+*Records* are data types which collect several values (the record's
255+*fields*) together. Idris provides syntax for defining records and
256+*automatically generating field access and update functions*. Unlike
257+*the syntax used for data structures, records in Idris follow a
258+*different syntax to that seen with Haskell. For example, we can
259+*represent a person's name and age in a record:
260+
261+.. code-block:: idris
262+
263+ record Person where
264+ constructor MkPerson
265+ firstName, middleName, lastName : String
266+ age : Int
267+
268+ fred : Person
269+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
270+
271+
272+The constructor name is provided using the ``constructor`` keyword,
273+and the *fields* are then given which are in an indented block
274+following the `where` keyword (here, ``firstName``, ``middleName``,
275+``lastName``, and ``age``). You can declare multiple fields on a
276+single line, provided that they have the same type. The field names
277+can be used to access the field values:
278+
279+::
280+
281+ *record> firstName fred
282+ "Fred" : String
283+ *record> age fred
284+ 30 : Int
285+ *record> :t firstName
286+ firstName : Person -> String
287+
288+We can also use the field names to update a record (or, more
289+precisely, produce a copy of the record with the given fields
290+updated):
291+
292+.. code-block:: bash
293+
294+ *record> record { firstName = "Jim" } fred
295+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person
296+ *record> record { firstName = "Jim", age = 20 } fred
297+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person
298+
299+The syntax ``record { field = val, ... }`` generates a function which
300+updates the given fields in a record.
301+
302+Records, and fields within records, can have dependent types. Updates
303+are allowed to change the type of a field, provided that the result is
304+well-typed.
305+
306+.. code-block:: idris
307+
308+ record Class where
309+ constructor ClassInfo
310+ students : Vect n Person
311+ className : String
312+
313+It is safe to update the ``students`` field to a vector of a different
314+length because it will not affect the type of the record:
315+
316+.. code-block:: idris
317+
318+ addStudent : Person -> Class -> Class
319+ addStudent p c = record { students = p :: students c } c
320+
321+::
322+
323+ *record> addStudent fred (ClassInfo [] "CS")
324+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
325+
326+
327+Nested record update
328+--------------------
329+
330+Idris also provides a convenient syntax for accessing and updating
331+nested records. For example, if a field is accessible with the
332+expression ``c (b (a x))``, it can be updated using the following
333+syntax:
334+
335+.. code-block:: idris
336+
337+ record { a->b->c = val } x
338+
339+This returns a new record, with the field accessed by the path
340+``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
341+a->b->c = val }`` itself has a function type. Symmetrically, the field
342+can also be accessed with the following syntax:
343+
344+.. code-block:: idris
345+
346+ record { a->b->c } x
347+
348+
349+
250350Dependent Types
251351===============
252352
@@ -1008,104 +1108,10 @@ matching ``let`` and lambda bindings. It will *only* work if:
10081108Dependent Records
10091109=================
10101110
1011−*Records* are data types which collect several values (the record's
1012−*fields*) together. Idris provides syntax for defining records and
1013−*automatically generating field access and update functions*. For
1014−example, we can represent a person's name and age in a record:
1015−
1016−.. code-block:: idris
1017−
1018− record Person where
1019− constructor MkPerson
1020− firstName, middleName, lastName : String
1021− age : Int
1022−
1023− fred : Person
1024− fred = MkPerson "Fred" "Joe" "Bloggs" 30
1025−
1026−Records can have *parameters*, which are listed between the record
1027−name and the ``where`` keyword, and *fields*, which are in an indented
1028−block following the `where` keyword (here, ``firstName``, ``middleName``,
1029−``lastName``, and ``age``). You can declare multiple fields on a single
1030−line, provided that they have the same type. The constructor name is
1031−provided after the ``constructor`` keyword. The field names can be used to
1032−access the field values:
1033−
1034−::
1035−
1036− *record> firstName fred
1037− "Fred" : String
1038− *record> age fred
1039− 30 : Int
1040− *record> :t firstName
1041− firstName : Person -> String
1042−
1043−We can also use the field names to update a record (or, more
1044−precisely, produce a copy of the record with the given fields
1045−updated):
1046−
1047−.. code-block:: bash
1048−
1049− *record> record { firstName = "Jim" } fred
1050− MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1051− *record> record { firstName = "Jim", age = 20 } fred
1052− MkPerson "Jim" "Joe" "Bloggs" 20 : Person
1053−
1054−The syntax ``record { field = val, ... }`` generates a function which
1055−updates the given fields in a record.
1056−
1057−Records, and fields within records, can have dependent types. Updates
1058−are allowed to change the type of a field, provided that the result is
1059−well-typed.
1060−
1061−.. code-block:: idris
1062−
1063− record Class where
1064− constructor ClassInfo
1065− students : Vect n Person
1066− className : String
1067−
1068−It is safe to update the ``students`` field to a vector of a different
1069−length because it will not affect the type of the record:
1070−
1071−.. code-block:: idris
1072−
1073− addStudent : Person -> Class -> Class
1074− addStudent p c = record { students = p :: students c } c
1075−
1076−::
1077−
1078− *record> addStudent fred (ClassInfo [] "CS")
1079− ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1080−
1081−Nested record update
1082−--------------------
1083−
1084−Idris also provides a convenient syntax for accessing and updating
1085−nested records. For example, if a field is accessible with the
1086−expression ``c (b (a x))``, it can be updated using the following
1087−syntax:
1088−
1089−.. code-block:: idris
1090−
1091− record { a->b->c = val } x
1092−
1093−This returns a new record, with the field accessed by the path
1094−``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
1095−a->b->c = val }`` itself has a function type. Symmetrically, the field
1096−can also be accessed with the following syntax:
1097−
1098−.. code-block:: idris
1099−
1100− record { a->b->c } x
1101−
1102−Parameters and Fields
1103−---------------------
1104−
1105−Records can have *parameters*, which are not subject to field
1106−updates. The parameters appear as arguments to the resulting type, and
1107−are written following the record type name. For example, a pair type
1108−could be defined as follows:
1111+Records can also be dependent on values. Records *parameters*, which
1112+are not subject to field updates. The parameters appear as arguments
1113+to the resulting type, and are written following the record type
1114+name. For example, a pair type could be defined as follows:
11091115
11101116.. code-block:: idris
11111117
@@ -1114,9 +1120,12 @@ could be defined as follows:
11141120 fst : a
11151121 snd : b
11161122
1117−The parameters to a record type need not be types. For example, we can
1118−restrict the size of classes using a ``Nat`` parameter to the
1119−``Class`` record:
1123+
1124+Using the class record from the original introduction to records. The
1125+size of the class can be restricted using a ``Vect`` and the size
1126+promoted to the type level by parameterising the record with the size.
1127+Foe example:
1128+
11201129
11211130.. code-block:: idris
11221131
@@ -1125,5 +1134,10 @@ restrict the size of classes using a ``Nat`` parameter to the
11251134 students : Vect size Person
11261135 className : String
11271136
1128−Note that it is no longer possible to write ``addStudent`` for this
1129−type, as that would change the size of the class.
1137+**Note** that it is no longer possible to use the ``addStudent``
1138+method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremeated using the successor constructor.
1139+
1140+.. code-block:: idris
1141+
1142+ addStudent : Person -> SizedClass n -> SizedClass (S n)
1143+ addStudent p c = record { students = p :: students c } c