@@ -979,18 +979,19 @@ example, we can represent a person's name and age in a record:
979979
980980.. code-block:: idris
981981
982− record Person : Type where
983− MkPerson : (name : String) ->
984− (age : Int) -> Person
982+ record Person where
983+ constructor MkPerson
984+ name : String
985+ age : Int
985986
986987 fred : Person
987988 fred = MkPerson "Fred" 30
988989
989−Record declarations are like ``data`` declarations, except that they
990−are introduced by the ``record`` keyword, and can only have one
991−constructor. The names of the binders in the constructor type
992−(``name`` and ``age``) here are the field names, which we can use to
993−access the field values:
990+Records can have *parameters*, which are listed between the record
991+name and the ``where`` keyword, and *fields*, which are in an indented
992+block following the `where` keyword (here, ``name`` and ``age``). The
993+constructor name is provided after the ``constructor`` keyword. The
994+field names can be used to access the field values:
994995
995996::
996997
@@ -1002,7 +1003,8 @@ access the field values:
10021003 name : Person -> String
10031004
10041005We can also use the field names to update a record (or, more
1005−precisely, produce a new record with the given fields updated).
1006+precisely, produce a copy of the record with the given fields
1007+updated):
10061008
10071009.. code-block:: bash
10081010
@@ -1016,15 +1018,14 @@ updates the given fields in a record.
10161018
10171019Records, and fields within records, can have dependent types. Updates
10181020are allowed to change the type of a field, provided that the result is
1019−well-typed, and the result does not affect the type of the record as a
1020−whole. For example:
1021+well-typed.
10211022
10221023.. code-block:: idris
10231024
1024− record Class : Type where
1025− ClassInfo : (students : Vect n Person) ->
1026− (className : String) ->
1027− Class
1025+ record Class where
1026+ constructor ClassInfo
1027+ students : Vect n Person
1028+ className : String
10281029
10291030It is safe to update the ``students`` field to a vector of a different
10301031length because it will not affect the type of the record:
@@ -1037,8 +1038,7 @@ length because it will not affect the type of the record:
10371038::
10381039
10391040 *record> addStudent fred (ClassInfo [] "CS")
1040− ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1041− : Class
1041+ ClassInfo [MkPerson "Fred" 30] "CS" : Class
10421042
10431043Nested record update
10441044--------------------
@@ -1060,3 +1060,32 @@ can also be accessed with the following syntax:
10601060.. code-block:: idris
10611061
10621062 record { a->b->c } x
1063+
1064+Parameters and Fields
1065+---------------------
1066+
1067+Records can have *parameters*, which are not subject to field
1068+updates. The parameters appear as arguments to the resulting type, and
1069+are written following the record type name. For example, a pair type
1070+could be defined as follows:
1071+
1072+.. code-block:: idris
1073+
1074+ record Prod a b where
1075+ constructor Times
1076+ fst : a
1077+ snd : b
1078+
1079+The parameters to a record type need not be types. For example, we can
1080+restrict the size of classes using a ``Nat`` parameter to the
1081+``Class`` record:
1082+
1083+.. code-block:: idris
1084+
1085+ record SizedClass (size : Nat) where
1086+ constructor SizedClassInfo
1087+ students : Vect size Person
1088+ className : String
1089+
1090+Note that it is no longer possible to write ``addStudent`` for this
1091+type, as that would change the size of the class.