@@ -248,104 +248,6 @@ So, for example, the following definitions are legal:
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
349Dependent Types
251Dependent Types
350===============
252===============
@@ -993,6 +895,105 @@ intermediate values:
994We will see more on ``with`` notation later.
896We will see more on ``with`` notation later.
902+*Records* are data types which collect several values (the record's
903+*fields*) together. Idris provides syntax for defining records and
904+*automatically generating field access and update functions*. Unlike
905+*the syntax used for data structures, records in Idris follow a
906+*different syntax to that seen with Haskell. For example, we can
907+*represent a person's name and age in a record:
909+.. code-block:: idris
912+ constructor MkPerson
913+ firstName, middleName, lastName : String
917+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
920+The constructor name is provided using the ``constructor`` keyword,
921+and the *fields* are then given which are in an indented block
922+following the `where` keyword (here, ``firstName``, ``middleName``,
923+``lastName``, and ``age``). You can declare multiple fields on a
924+single line, provided that they have the same type. The field names
925+can be used to access the field values:
929+ *record> firstName fred
933+ *record> :t firstName
934+ firstName : Person -> String
936+We can also use the field names to update a record (or, more
937+precisely, produce a copy of the record with the given fields
942+ *record> record { firstName = "Jim" } fred
943+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person
944+ *record> record { firstName = "Jim", age = 20 } fred
945+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person
947+The syntax ``record { field = val, ... }`` generates a function which
948+updates the given fields in a record.
950+Records, and fields within records, can have dependent types. Updates
951+are allowed to change the type of a field, provided that the result is
954+.. code-block:: idris
957+ constructor ClassInfo
958+ students : Vect n Person
961+It is safe to update the ``students`` field to a vector of a different
962+length because it will not affect the type of the record:
964+.. code-block:: idris
966+ addStudent : Person -> Class -> Class
967+ addStudent p c = record { students = p :: students c } c
971+ *record> addStudent fred (ClassInfo [] "CS")
972+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
978+Idris also provides a convenient syntax for accessing and updating
979+nested records. For example, if a field is accessible with the
980+expression ``c (b (a x))``, it can be updated using the following
983+.. code-block:: idris
985+ record { a->b->c = val } x
987+This returns a new record, with the field accessed by the path
988+``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
989+a->b->c = val }`` itself has a function type. Symmetrically, the field
990+can also be accessed with the following syntax:
992+.. code-block:: idris
994+ record { a->b->c } x
996Dependent Records
997Dependent Records
997-----------------
998-----------------