@@ -1,11 +1,11 @@
1.. _sect-typefuns:
1.. _sect-typefuns:
3−===================
3+*******************
4Types and Functions
4Types and Functions
5−===================
5+*******************
7Primitive Types
7Primitive Types
8−---------------
8+===============
10Idris defines several primitive types: ``Int``, ``Integer`` and
10Idris defines several primitive types: ``Int``, ``Integer`` and
11``Float`` for numeric operations, ``Char`` and ``String`` for text
11``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
71 "The answer!" : String
71 "The answer!" : String
74−----------
74+==========
76Data types are declared in a similar way to Haskell data types, with a
76Data types are declared in a similar way to Haskell data types, with a
77similar syntax. Natural numbers and lists, for example, can be
77similar syntax. Natural numbers and lists, for example, can be
@@ -105,7 +105,7 @@ symbols:
105 :+-*/=_.?|&><!@$%^~.
105 :+-*/=_.?|&><!@$%^~.
108−---------
108+=========
110Functions are implemented by pattern matching, again using a similar
110Functions are implemented by pattern matching, again using a similar
111syntax to Haskell. The main difference is that Idris requires type
111syntax to Haskell. The main difference is that Idris requires type
@@ -175,7 +175,7 @@ numbers. This means it can optimise the representation, and functions
175such as ``plus`` and ``mult``.
175such as ``plus`` and ``mult``.
177``where`` clauses
177``where`` clauses
178−~~~~~~~~~~~~~~~~~
178+-----------------
180Functions can also be defined *locally* using ``where`` clauses. For
180Functions can also be defined *locally* using ``where`` clauses. For
181example, to define a function which reverses a list, we can use an
181example, to define a function which reverses a list, we can use an
@@ -241,10 +241,10 @@ So, for example, the following definitions are legal:
241 where z w = y + w
241 where z w = y + w
243Dependent Types
243Dependent Types
244−---------------
244+===============
249A standard example of a dependent type is the type of “lists with
249A standard example of a dependent type is the type of “lists with
250length”, conventionally called vectors in the dependent type
250length”, conventionally called vectors in the dependent type
@@ -322,7 +322,7 @@ two vectors — we needed a vector of length ``k + m``, but provided a
322vector of length ``k + k``.
322vector of length ``k + k``.
324The Finite Sets
324The Finite Sets
325−~~~~~~~~~~~~~~~
325+---------------
327Finite sets, as the name suggests, are sets with a finite number of
327Finite sets, as the name suggests, are sets with a finite number of
328elements. They are available as part of the Idris library, by
328elements. They are available as part of the Idris library, by
@@ -337,12 +337,12 @@ importing ``Data.Fin``, or can be declared as follows:
337From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
337From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
338So this is not a set in the sense of a collection that is a container of objects,
338So this is not a set in the sense of a collection that is a container of objects,
339rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
339rather 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
341``n`` is the argument used to instantiate the ``Fin`` type.
341``n`` is the argument used to instantiate the ``Fin`` type.
342For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
342For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
344Let us look at the constructors in greater detail.
344Let us look at the constructors in greater detail.
346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
348elements. ``Fin`` is indexed by a ``Nat``, which represents the number
348elements. ``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
377compile time type error, since it would force ``n`` to be ``Z``.
377compile time type error, since it would force ``n`` to be ``Z``.
379Implicit Arguments
379Implicit Arguments
380−~~~~~~~~~~~~~~~~~~
380+------------------
382Let us take a closer look at the type of ``index``:
382Let us take a closer look at the type of ``index``:
@@ -420,7 +420,7 @@ help document a function by making the purpose of an argument more
422“``using``” notation
422“``using``” notation
423−~~~~~~~~~~~~~~~~~~~~
423+--------------------
425Sometimes it is useful to provide types of implicit arguments,
425Sometimes it is useful to provide types of implicit arguments,
426particularly where there is a dependency ordering, or where the
426particularly where there is a dependency ordering, or where the
@@ -460,7 +460,7 @@ appear within the block:
460 There : Elem x xs -> Elem x (y :: xs)
460 There : Elem x xs -> Elem x (y :: xs)
462Note: Declaration Order and ``mutual`` blocks
462Note: Declaration Order and ``mutual`` blocks
463−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
463+---------------------------------------------
465In general, functions and data types must be defined before use, since
465In general, functions and data types must be defined before use, since
466dependent types allow functions to appear as part of types, and their
466dependent 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
490Computer programs are of little use if they do not interact with the
490Computer programs are of little use if they do not interact with the
491user or the system in some way. The difficulty in a pure language such
491user or the system in some way. The difficulty in a pure language such
@@ -542,7 +542,7 @@ example for reading and writing files, including:
542.. _sect-do:
542.. _sect-do:
544“``do``” notation
544“``do``” notation
545−-----------------
545+=================
547I/O programs will typically need to sequence actions, feeding the
547I/O programs will typically need to sequence actions, feeding the
548output of one computation into the input of the next. ``IO`` is an
548output of one computation into the input of the next. ``IO`` is an
@@ -573,7 +573,7 @@ can be overloaded.
573.. _sect-lazy:
573.. _sect-lazy:
578Normally, arguments to functions are evaluated before the function
578Normally, arguments to functions are evaluated before the function
579itself (that is, Idris uses *eager* evaluation). However, this is
579itself (that is, Idris uses *eager* evaluation). However, this is
@@ -611,7 +611,7 @@ without any explicit use of ``Force`` or ``Delay``:
611 boolCase False t e = e;
611 boolCase False t e = e;
613Useful Data Types
613Useful Data Types
614−-----------------
614+=================
616Idris includes a number of useful data types and library functions
616Idris includes a number of useful data types and library functions
617(see the ``libs/`` directory in the distribution). This chapter
617(see the ``libs/`` directory in the distribution). This chapter
@@ -619,7 +619,7 @@ describes a few of these. The functions described here are imported
619automatically by every Idris program, as part of ``Prelude.idr``.
619automatically by every Idris program, as part of ``Prelude.idr``.
621``List`` and ``Vect``
621``List`` and ``Vect``
622−~~~~~~~~~~~~~~~~~~~~~
622+---------------------
624We have already seen the ``List`` and ``Vect`` data types:
624We have already seen the ``List`` and ``Vect`` data types:
@@ -692,7 +692,7 @@ remember that Idris is still in development, so if you don’t see
692the function you need, please feel free to add it and submit a patch!
692the function you need, please feel free to add it and submit a patch!
694Aside: Anonymous functions and operator sections
694Aside: Anonymous functions and operator sections
695−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
695+------------------------------------------------
697There are actually neater ways to write the above expression. One way
697There are actually neater ways to write the above expression. One way
698would be to use an anonymous function:
698would be to use an anonymous function:
@@ -719,7 +719,7 @@ by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
719to ``\x => 2 * x``.
719to ``\x => 2 * x``.
724``Maybe`` describes an optional value. Either there is a value of the
724``Maybe`` describes an optional value. Either there is a value of the
725given type, or there isn’t:
725given type, or there isn’t:
@@ -753,7 +753,7 @@ simply ``b``. Since the default value might not be used, we mark it as
753discarding it would be wasteful.
753discarding it would be wasteful.
755Tuples and Dependent Pairs
755Tuples and Dependent Pairs
756−~~~~~~~~~~~~~~~~~~~~~~~~~~
756+--------------------------
758Values can be paired with the following built-in data type:
758Values can be paired with the following built-in data type:
@@ -774,7 +774,7 @@ contain an arbitrary number of values, represented as nested pairs:
774 jim = ("Jim", 25, "Cambridge")
774 jim = ("Jim", 25, "Cambridge")
776Dependent Pairs
776Dependent Pairs
777−~~~~~~~~~~~~~~~
777+---------------
779Dependent pairs allow the type of the second element of a pair to depend
779Dependent pairs allow the type of the second element of a pair to depend
780on the value of the first element. Traditionally, these are referred to
780on the value of the first element. Traditionally, these are referred to
@@ -852,10 +852,10 @@ We will see more on ``with`` notation later.
852.. _sect-more-expr:
852.. _sect-more-expr:
854More Expressions
854More Expressions
855−----------------
855+================
857``let`` bindings
857``let`` bindings
858−~~~~~~~~~~~~~~~~
858+----------------
860Intermediate values can be calculated using ``let`` bindings:
860Intermediate values can be calculated using ``let`` bindings:
@@ -884,7 +884,7 @@ pattern matching at the top level:
884 name ++ " is " ++ show age ++ " years old"
884 name ++ " is " ++ show age ++ " years old"
886List comprehensions
886List comprehensions
887−~~~~~~~~~~~~~~~~~~~
887+-------------------
889Idris provides *comprehension* notation as a convenient shorthand
889Idris provides *comprehension* notation as a convenient shorthand
890for building lists. The general form is:
890for building lists. The general form is:
@@ -911,7 +911,7 @@ by the difference between ``a`` and ``b``. This works for any numeric
911type, using the ``count`` function from the prelude.
911type, using the ``count`` function from the prelude.
913``case`` expressions
913``case`` expressions
914−~~~~~~~~~~~~~~~~~~~~
914+--------------------
916Another way of inspecting intermediate values of *simple* types is to
916Another way of inspecting intermediate values of *simple* types is to
917use a ``case`` expression. The following function, for example, splits
917use a ``case`` expression. The following function, for example, splits
@@ -965,7 +965,7 @@ matching ``let`` and lambda bindings. It will *only* work if:
967Dependent Records
967Dependent Records
968−-----------------
968+=================
970*Records* are data types which collect several values (the record's
970*Records* are data types which collect several values (the record's
971*fields*) together. Idris provides syntax for defining records and
971*fields*) together. Idris provides syntax for defining records and
@@ -1036,7 +1036,7 @@ length because it will not affect the type of the record:
1038Nested record update
1038Nested record update
1039−~~~~~~~~~~~~~~~~~~~~
1039+--------------------
1041Idris also provides a convenient syntax for accessing and updating
1041Idris also provides a convenient syntax for accessing and updating
1042nested records. For example, if a field is accessible with the
1042nested records. For example, if a field is accessible with the