@@ -346,7 +346,6 @@ can also be accessed with the following syntax:
346 record { a->b->c } x
346 record { a->b->c } x
350Dependent Types
349Dependent Types
351===============
350===============
@@ -493,10 +492,10 @@ elements. ``Fin`` is indexed by a ``Nat``, which represents the number
493of elements in the set. Since we can’t construct an element of an
492of elements in the set. Since we can’t construct an element of an
494empty set, neither constructor targets ``Fin Z``.
493empty set, neither constructor targets ``Fin Z``.
496−As mentioned above, a useful application of the ``Fin`` family is to represent bounded
495+As mentioned above, a useful application of the ``Fin`` family is to
497−natural numbers. Since the first ``n`` natural numbers form a finite
496+represent bounded natural numbers. Since the first ``n`` natural
498−set of ``n`` elements, we can treat ``Fin n`` as the set of integers
497+numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
499−greater than or equal to zero and less than ``n``.
498+the set of integers greater than or equal to zero and less than ``n``.
501For example, the following function which looks up an element in a
500For example, the following function which looks up an element in a
502``Vect``, by a bounded index given as a ``Fin n``, is defined in the
501``Vect``, by a bounded index given as a ``Fin n``, is defined in the
@@ -605,7 +604,7 @@ appear within the block:
605 There : Elem x xs -> Elem x (y :: xs)
604 There : Elem x xs -> Elem x (y :: xs)
607Note: Declaration Order and ``mutual`` blocks
606Note: Declaration Order and ``mutual`` blocks
608−---------------------------------------------
607+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
610In general, functions and data types must be defined before use, since
609In general, functions and data types must be defined before use, since
611dependent types allow functions to appear as part of types, and their
610dependent types allow functions to appear as part of types, and their
@@ -837,7 +836,7 @@ remember that Idris is still in development, so if you don’t see
837the function you need, please feel free to add it and submit a patch!
836the function you need, please feel free to add it and submit a patch!
839Aside: Anonymous functions and operator sections
838Aside: Anonymous functions and operator sections
840−------------------------------------------------
839+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
842There are actually neater ways to write the above expression. One way
841There are actually neater ways to write the above expression. One way
843would be to use an anonymous function:
842would be to use an anonymous function:
@@ -897,8 +896,8 @@ simply ``b``. Since the default value might not be used, we mark it as
897``Lazy`` in case it is a large expression where evaluating it then
896``Lazy`` in case it is a large expression where evaluating it then
898discarding it would be wasteful.
897discarding it would be wasteful.
900−Tuples and Dependent Pairs
899+Tuples
901−--------------------------
900+------
903Values can be paired with the following built-in data type:
902Values can be paired with the following built-in data type:
@@ -994,6 +993,43 @@ intermediate values:
995We will see more on ``with`` notation later.
994We will see more on ``with`` notation later.
999+Records can also be dependent on values. Records *parameters*, which
1000+are not subject to field updates. The parameters appear as arguments
1001+to the resulting type, and are written following the record type
1002+name. For example, a pair type could be defined as follows:
1004+.. code-block:: idris
1006+ record Prod a b where
1012+Using the class record from the original introduction to records. The
1013+size of the class can be restricted using a ``Vect`` and the size
1014+promoted to the type level by parameterising the record with the size.
1018+.. code-block:: idris
1020+ record SizedClass (size : Nat) where
1021+ constructor SizedClassInfo
1022+ students : Vect size Person
1025+**Note** that it is no longer possible to use the ``addStudent``
1026+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+.. code-block:: idris
1030+ addStudent : Person -> SizedClass n -> SizedClass (S n)
1031+ addStudent p c = record { students = p :: students c } c
997.. _sect-more-expr:
1033.. _sect-more-expr:
999More Expressions
1035More Expressions
@@ -1104,40 +1140,3 @@ matching ``let`` and lambda bindings. It will *only* work if:
1104- The type of the result is "known". i.e. the type of the expression
1140- The type of the result is "known". i.e. the type of the expression
1105 can be determined *without* type checking the ``case``-expression
1141 can be determined *without* type checking the ``case``-expression
1111−Records can also be dependent on values. Records *parameters*, which
1112−are not subject to field updates. The parameters appear as arguments
1113−to the resulting type, and are written following the record type
1114−name. For example, a pair type could be defined as follows:
1116−.. code-block:: idris
1118− record Prod a b where
1124−Using the class record from the original introduction to records. The
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.
1130−.. code-block:: idris
1132− record SizedClass (size : Nat) where
1133− constructor SizedClassInfo
1134− students : Vect size Person
1137−**Note** that it is no longer possible to use the ``addStudent``
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