@@ -247,6 +247,106 @@ So, for example, the following definitions are legal:
247 d y = c (y + 1 + z y)
247 d y = c (y + 1 + z y)
248 where z w = y + w
248 where z w = y + w
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:
261+.. code-block:: idris
264+ constructor MkPerson
265+ firstName, middleName, lastName : String
269+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
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:
281+ *record> firstName fred
285+ *record> :t firstName
286+ firstName : Person -> String
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
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
299+The syntax ``record { field = val, ... }`` generates a function which
300+updates the given fields in a record.
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
306+.. code-block:: idris
309+ constructor ClassInfo
310+ students : Vect n Person
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:
316+.. code-block:: idris
318+ addStudent : Person -> Class -> Class
319+ addStudent p c = record { students = p :: students c } c
323+ *record> addStudent fred (ClassInfo [] "CS")
324+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
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
335+.. code-block:: idris
337+ record { a->b->c = val } x
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:
344+.. code-block:: idris
346+ record { a->b->c } x
250Dependent Types
350Dependent Types
251===============
351===============
@@ -1008,104 +1108,10 @@ matching ``let`` and lambda bindings. It will *only* work if:
1008Dependent Records
1108Dependent Records
1009=================
1109=================
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:
1016−.. code-block:: idris
1018− record Person where
1019− constructor MkPerson
1020− firstName, middleName, lastName : String
1024− fred = MkPerson "Fred" "Joe" "Bloggs" 30
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:
1036− *record> firstName fred
1040− *record> :t firstName
1041− firstName : Person -> String
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
1047−.. code-block:: bash
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
1054−The syntax ``record { field = val, ... }`` generates a function which
1055−updates the given fields in a record.
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
1061−.. code-block:: idris
1064− constructor ClassInfo
1065− students : Vect n Person
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:
1071−.. code-block:: idris
1073− addStudent : Person -> Class -> Class
1074− addStudent p c = record { students = p :: students c } c
1078− *record> addStudent fred (ClassInfo [] "CS")
1079− ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1081−Nested record update
1082−--------------------
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
1089−.. code-block:: idris
1091− record { a->b->c = val } x
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:
1098−.. code-block:: idris
1100− record { a->b->c } x
1102−Parameters and Fields
1103−---------------------
1105−Records can have *parameters*, which are not subject to field
1111+Records can also be dependent on values. Records *parameters*, which
1106−updates. The parameters appear as arguments to the resulting type, and
1112+are not subject to field updates. The parameters appear as arguments
1107−are written following the record type name. For example, a pair type
1113+to the resulting type, and are written following the record type
1108−could be defined as follows:
1114+name. For example, a pair type could be defined as follows:
1110.. code-block:: idris
1116.. code-block:: idris
@@ -1114,9 +1120,12 @@ could be defined as follows:
1117−The parameters to a record type need not be types. For example, we can
1123+
1118−restrict the size of classes using a ``Nat`` parameter to the
1124+Using the class record from the original introduction to records. The
1119−``Class`` record:
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.
1121.. code-block:: idris
1130.. code-block:: idris
@@ -1125,5 +1134,10 @@ restrict the size of classes using a ``Nat`` parameter to the
1125 students : Vect size Person
1134 students : Vect size Person
1126 className : String
1135 className : String
1128−Note that it is no longer possible to write ``addStudent`` for this
1137+**Note** that it is no longer possible to use the ``addStudent``
1129−type, as that would change the size of the class.
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.
1140+.. code-block:: idris
1142+ addStudent : Person -> SizedClass n -> SizedClass (S n)
1143+ addStudent p c = record { students = p :: students c } c