@@ -1,11 +1,11 @@
11.. _sect-typefuns:
22
3−===================
3+*******************
44Types and Functions
5−===================
5+*******************
66
77Primitive Types
8−---------------
8+===============
99
1010Idris defines several primitive types: ``Int``, ``Integer`` and
1111``Float`` for numeric operations, ``Char`` and ``String`` for text
@@ -71,7 +71,7 @@ work on user defined types. Boolean expressions can be tested with the
7171 "The answer!" : String
7272
7373Data Types
74−----------
74+==========
7575
7676Data types are declared in a similar way to Haskell data types, with a
7777similar syntax. Natural numbers and lists, for example, can be
@@ -105,7 +105,7 @@ symbols:
105105 :+-*/=_.?|&><!@$%^~.
106106
107107Functions
108−---------
108+=========
109109
110110Functions are implemented by pattern matching, again using a similar
111111syntax to Haskell. The main difference is that Idris requires type
@@ -175,7 +175,7 @@ numbers. This means it can optimise the representation, and functions
175175such as ``plus`` and ``mult``.
176176
177177``where`` clauses
178−~~~~~~~~~~~~~~~~~
178+-----------------
179179
180180Functions can also be defined *locally* using ``where`` clauses. For
181181example, to define a function which reverses a list, we can use an
@@ -241,10 +241,10 @@ So, for example, the following definitions are legal:
241241 where z w = y + w
242242
243243Dependent Types
244−---------------
244+===============
245245
246246Vectors
247−~~~~~~~
247+-------
248248
249249A standard example of a dependent type is the type of “lists with
250250length”, conventionally called vectors in the dependent type
@@ -322,7 +322,7 @@ two vectors — we needed a vector of length ``k + m``, but provided a
322322vector of length ``k + k``.
323323
324324The Finite Sets
325−~~~~~~~~~~~~~~~
325+---------------
326326
327327Finite sets, as the name suggests, are sets with a finite number of
328328elements. They are available as part of the Idris library, by
@@ -337,12 +337,12 @@ importing ``Data.Fin``, or can be declared as follows:
337337From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
338338So this is not a set in the sense of a collection that is a container of objects,
339339rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
340−Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
340+Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
341341``n`` is the argument used to instantiate the ``Fin`` type.
342342For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
343343
344344Let us look at the constructors in greater detail.
345−
345+
346346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
347347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
348348elements. ``Fin`` is indexed by a ``Nat``, which represents the number
@@ -377,7 +377,7 @@ attempting to look up an element in an empty vector would give a
377377compile time type error, since it would force ``n`` to be ``Z``.
378378
379379Implicit Arguments
380−~~~~~~~~~~~~~~~~~~
380+------------------
381381
382382Let us take a closer look at the type of ``index``:
383383
@@ -420,7 +420,7 @@ help document a function by making the purpose of an argument more
420420clear.
421421
422422“``using``” notation
423−~~~~~~~~~~~~~~~~~~~~
423+--------------------
424424
425425Sometimes it is useful to provide types of implicit arguments,
426426particularly where there is a dependency ordering, or where the
@@ -460,7 +460,7 @@ appear within the block:
460460 There : Elem x xs -> Elem x (y :: xs)
461461
462462Note: Declaration Order and ``mutual`` blocks
463−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
463+---------------------------------------------
464464
465465In general, functions and data types must be defined before use, since
466466dependent types allow functions to appear as part of types, and their
@@ -485,7 +485,7 @@ depend on the reduction behaviour of any of the functions in the
485485block.
486486
487487I/O
488−---
488+===
489489
490490Computer programs are of little use if they do not interact with the
491491user or the system in some way. The difficulty in a pure language such
@@ -542,7 +542,7 @@ example for reading and writing files, including:
542542.. _sect-do:
543543
544544“``do``” notation
545−-----------------
545+=================
546546
547547I/O programs will typically need to sequence actions, feeding the
548548output of one computation into the input of the next. ``IO`` is an
@@ -573,7 +573,7 @@ can be overloaded.
573573.. _sect-lazy:
574574
575575Laziness
576−--------
576+========
577577
578578Normally, arguments to functions are evaluated before the function
579579itself (that is, Idris uses *eager* evaluation). However, this is
@@ -611,7 +611,7 @@ without any explicit use of ``Force`` or ``Delay``:
611611 boolCase False t e = e;
612612
613613Useful Data Types
614−-----------------
614+=================
615615
616616Idris includes a number of useful data types and library functions
617617(see the ``libs/`` directory in the distribution). This chapter
@@ -619,7 +619,7 @@ describes a few of these. The functions described here are imported
619619automatically by every Idris program, as part of ``Prelude.idr``.
620620
621621``List`` and ``Vect``
622−~~~~~~~~~~~~~~~~~~~~~
622+---------------------
623623
624624We have already seen the ``List`` and ``Vect`` data types:
625625
@@ -692,7 +692,7 @@ remember that Idris is still in development, so if you don’t see
692692the function you need, please feel free to add it and submit a patch!
693693
694694Aside: Anonymous functions and operator sections
695−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
695+------------------------------------------------
696696
697697There are actually neater ways to write the above expression. One way
698698would be to use an anonymous function:
@@ -719,7 +719,7 @@ by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
719719to ``\x => 2 * x``.
720720
721721Maybe
722−~~~~~
722+-----
723723
724724``Maybe`` describes an optional value. Either there is a value of the
725725given type, or there isn’t:
@@ -753,7 +753,7 @@ simply ``b``. Since the default value might not be used, we mark it as
753753discarding it would be wasteful.
754754
755755Tuples and Dependent Pairs
756−~~~~~~~~~~~~~~~~~~~~~~~~~~
756+--------------------------
757757
758758Values can be paired with the following built-in data type:
759759
@@ -774,7 +774,7 @@ contain an arbitrary number of values, represented as nested pairs:
774774 jim = ("Jim", 25, "Cambridge")
775775
776776Dependent Pairs
777−~~~~~~~~~~~~~~~
777+---------------
778778
779779Dependent pairs allow the type of the second element of a pair to depend
780780on the value of the first element. Traditionally, these are referred to
@@ -852,10 +852,10 @@ We will see more on ``with`` notation later.
852852.. _sect-more-expr:
853853
854854More Expressions
855−----------------
855+================
856856
857857``let`` bindings
858−~~~~~~~~~~~~~~~~
858+----------------
859859
860860Intermediate values can be calculated using ``let`` bindings:
861861
@@ -884,7 +884,7 @@ pattern matching at the top level:
884884 name ++ " is " ++ show age ++ " years old"
885885
886886List comprehensions
887−~~~~~~~~~~~~~~~~~~~
887+-------------------
888888
889889Idris provides *comprehension* notation as a convenient shorthand
890890for building lists. The general form is:
@@ -911,7 +911,7 @@ by the difference between ``a`` and ``b``. This works for any numeric
911911type, using the ``count`` function from the prelude.
912912
913913``case`` expressions
914−~~~~~~~~~~~~~~~~~~~~
914+--------------------
915915
916916Another way of inspecting intermediate values of *simple* types is to
917917use a ``case`` expression. The following function, for example, splits
@@ -965,7 +965,7 @@ matching ``let`` and lambda bindings. It will *only* work if:
965965 itself.
966966
967967Dependent Records
968−-----------------
968+=================
969969
970970*Records* are data types which collect several values (the record's
971971*fields*) together. Idris provides syntax for defining records and
@@ -1036,7 +1036,7 @@ length because it will not affect the type of the record:
10361036 : Class
10371037
10381038Nested record update
1039−~~~~~~~~~~~~~~~~~~~~
1039+--------------------
10401040
10411041Idris also provides a convenient syntax for accessing and updating
10421042nested records. For example, if a field is accessible with the