@@ -247,6 +247,7 @@ 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
250Dependent Types
251Dependent Types
251===============
252===============
@@ -393,10 +394,10 @@ elements. ``Fin`` is indexed by a ``Nat``, which represents the number
393of elements in the set. Since we can’t construct an element of an
394of elements in the set. Since we can’t construct an element of an
394empty set, neither constructor targets ``Fin Z``.
395empty set, neither constructor targets ``Fin Z``.
396−As mentioned above, a useful application of the ``Fin`` family is to represent bounded
397+As mentioned above, a useful application of the ``Fin`` family is to
397−natural numbers. Since the first ``n`` natural numbers form a finite
398+represent bounded natural numbers. Since the first ``n`` natural
398−set of ``n`` elements, we can treat ``Fin n`` as the set of integers
399+numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
399−greater than or equal to zero and less than ``n``.
400+the set of integers greater than or equal to zero and less than ``n``.
401For example, the following function which looks up an element in a
402For example, the following function which looks up an element in a
402``Vect``, by a bounded index given as a ``Fin n``, is defined in the
403``Vect``, by a bounded index given as a ``Fin n``, is defined in the
@@ -505,7 +506,7 @@ appear within the block:
505 There : Elem x xs -> Elem x (y :: xs)
506 There : Elem x xs -> Elem x (y :: xs)
507Note: Declaration Order and ``mutual`` blocks
508Note: Declaration Order and ``mutual`` blocks
508−---------------------------------------------
509+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
510In general, functions and data types must be defined before use, since
511In general, functions and data types must be defined before use, since
511dependent types allow functions to appear as part of types, and their
512dependent 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
737the function you need, please feel free to add it and submit a patch!
738the function you need, please feel free to add it and submit a patch!
739Aside: Anonymous functions and operator sections
740Aside: Anonymous functions and operator sections
740−------------------------------------------------
741+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
742There are actually neater ways to write the above expression. One way
743There are actually neater ways to write the above expression. One way
743would be to use an anonymous function:
744would be to use an anonymous function:
@@ -797,8 +798,8 @@ simply ``b``. Since the default value might not be used, we mark it as
797``Lazy`` in case it is a large expression where evaluating it then
798``Lazy`` in case it is a large expression where evaluating it then
798discarding it would be wasteful.
799discarding it would be wasteful.
800−Tuples and Dependent Pairs
801+Tuples
801−--------------------------
802+------
803Values can be paired with the following built-in data type:
804Values can be paired with the following built-in data type:
@@ -894,6 +895,142 @@ intermediate values:
895We 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
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:
1005+.. code-block:: idris
1007+ record Prod a b where
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.
1019+.. code-block:: idris
1021+ record SizedClass (size : Nat) where
1022+ constructor SizedClassInfo
1023+ students : Vect size Person
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.
1029+.. code-block:: idris
1031+ addStudent : Person -> SizedClass n -> SizedClass (S n)
1032+ addStudent p c = record { students = p :: students c } c
897.. _sect-more-expr:
1034.. _sect-more-expr:
899More Expressions
1036More Expressions
@@ -1004,126 +1141,3 @@ matching ``let`` and lambda bindings. It will *only* work if:
1004- The type of the result is "known". i.e. the type of the expression
1141- The type of the result is "known". i.e. the type of the expression
1005 can be determined *without* type checking the ``case``-expression
1142 can be determined *without* type checking the ``case``-expression
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
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:
1110−.. code-block:: idris
1112− record Prod a b where
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
1121−.. code-block:: idris
1123− record SizedClass (size : Nat) where
1124− constructor SizedClassInfo
1125− students : Vect size Person
1128−Note that it is no longer possible to write ``addStudent`` for this
1129−type, as that would change the size of the class.