@@ -247,6 +247,7 @@ So, for example, the following definitions are legal:
247247 d y = c (y + 1 + z y)
248248 where z w = y + w
249249
250+
250251Dependent Types
251252===============
252253
@@ -393,10 +394,10 @@ elements. ``Fin`` is indexed by a ``Nat``, which represents the number
393394of elements in the set. Since we can’t construct an element of an
394395empty set, neither constructor targets ``Fin Z``.
395396
396−As mentioned above, a useful application of the ``Fin`` family is to represent bounded
397−natural numbers. Since the first ``n`` natural numbers form a finite
398−set of ``n`` elements, we can treat ``Fin n`` as the set of integers
399−greater than or equal to zero and less than ``n``.
397+As mentioned above, a useful application of the ``Fin`` family is to
398+represent bounded natural numbers. Since the first ``n`` natural
399+numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
400+the set of integers greater than or equal to zero and less than ``n``.
400401
401402For example, the following function which looks up an element in a
402403``Vect``, by a bounded index given as a ``Fin n``, is defined in the
@@ -505,7 +506,7 @@ appear within the block:
505506 There : Elem x xs -> Elem x (y :: xs)
506507
507508Note: Declaration Order and ``mutual`` blocks
508−---------------------------------------------
509+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
509510
510511In general, functions and data types must be defined before use, since
511512dependent types allow functions to appear as part of types, and their
@@ -737,7 +738,7 @@ remember that Idris is still in development, so if you don’t see
737738the function you need, please feel free to add it and submit a patch!
738739
739740Aside: Anonymous functions and operator sections
740−------------------------------------------------
741+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
741742
742743There are actually neater ways to write the above expression. One way
743744would be to use an anonymous function:
@@ -797,8 +798,8 @@ simply ``b``. Since the default value might not be used, we mark it as
797798``Lazy`` in case it is a large expression where evaluating it then
798799discarding it would be wasteful.
799800
800−Tuples and Dependent Pairs
801−--------------------------
801+Tuples
802+------
802803
803804Values can be paired with the following built-in data type:
804805
@@ -894,6 +895,142 @@ intermediate values:
894895
895896We will see more on ``with`` notation later.
896897
898+
899+Records
900+-------
901+
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:
908+
909+.. code-block:: idris
910+
911+ record Person where
912+ constructor MkPerson
913+ firstName, middleName, lastName : String
914+ age : Int
915+
916+ fred : Person
917+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
918+
919+
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:
926+
927+::
928+
929+ *record> firstName fred
930+ "Fred" : String
931+ *record> age fred
932+ 30 : Int
933+ *record> :t firstName
934+ firstName : Person -> String
935+
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
938+updated):
939+
940+.. code-block:: bash
941+
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
946+
947+The syntax ``record { field = val, ... }`` generates a function which
948+updates the given fields in a record.
949+
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
952+well-typed.
953+
954+.. code-block:: idris
955+
956+ record Class where
957+ constructor ClassInfo
958+ students : Vect n Person
959+ className : String
960+
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:
963+
964+.. code-block:: idris
965+
966+ addStudent : Person -> Class -> Class
967+ addStudent p c = record { students = p :: students c } c
968+
969+::
970+
971+ *record> addStudent fred (ClassInfo [] "CS")
972+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
973+
974+
975+Nested record update
976+~~~~~~~~~~~~~~~~~~~~
977+
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
981+syntax:
982+
983+.. code-block:: idris
984+
985+ record { a->b->c = val } x
986+
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:
991+
992+.. code-block:: idris
993+
994+ record { a->b->c } x
995+
996+
997+Dependent Records
998+-----------------
999+
1000+Records can also be dependent on values. Records *parameters*, which
1001+are not subject to field updates. The parameters appear as arguments
1002+to the resulting type, and are written following the record type
1003+name. For example, a pair type could be defined as follows:
1004+
1005+.. code-block:: idris
1006+
1007+ record Prod a b where
1008+ constructor Times
1009+ fst : a
1010+ snd : b
1011+
1012+
1013+Using the class record from the original introduction to records. The
1014+size of the class can be restricted using a ``Vect`` and the size
1015+promoted to the type level by parameterising the record with the size.
1016+Foe example:
1017+
1018+
1019+.. code-block:: idris
1020+
1021+ record SizedClass (size : Nat) where
1022+ constructor SizedClassInfo
1023+ students : Vect size Person
1024+ className : String
1025+
1026+**Note** that it is no longer possible to use the ``addStudent``
1027+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.
1028+
1029+.. code-block:: idris
1030+
1031+ addStudent : Person -> SizedClass n -> SizedClass (S n)
1032+ addStudent p c = record { students = p :: students c } c
1033+
8971034.. _sect-more-expr:
8981035
8991036More Expressions
@@ -1004,126 +1141,3 @@ matching ``let`` and lambda bindings. It will *only* work if:
10041141- The type of the result is "known". i.e. the type of the expression
10051142 can be determined *without* type checking the ``case``-expression
10061143 itself.
1007−
1008−Dependent Records
1009−=================
1010−
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:
1109−
1110−.. code-block:: idris
1111−
1112− record Prod a b where
1113− constructor Times
1114− fst : a
1115− snd : b
1116−
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:
1120−
1121−.. code-block:: idris
1122−
1123− record SizedClass (size : Nat) where
1124− constructor SizedClassInfo
1125− students : Vect size Person
1126− className : String
1127−
1128−Note that it is no longer possible to write ``addStudent`` for this
1129−type, as that would change the size of the class.