@@ -0,0 +1,1048 @@
1+.. _sect-typefuns:
2+
3+===================
4+Types and Functions
5+===================
6+
7+Primitive Types
8+---------------
9+
10+``Idris`` defines several primitive types: ``Int``, ``Integer`` and
11+``Float`` for numeric operations, ``Char`` and ``String`` for text
12+manipulation, and ``Ptr`` which represents foreign pointers. There are
13+also several data types declared in the library, including ``Bool``,
14+with values ``True`` and ``False``. We can declare some constants with
15+these types. Enter the following into a file ``prims.idr`` and load it
16+into the ``Idris`` interactive environment by typing ``idris
17+prims.idr``:
18+
19+.. code-block:: idris
20+
21+ module prims
22+
23+ x : Int
24+ x = 42
25+
26+ foo : String
27+ foo = "Sausage machine"
28+
29+ bar : Char
30+ bar = 'Z'
31+
32+ quux : Bool
33+ quux = False
34+
35+An ``Idris`` file consists of an optional module declaration (here
36+``module prims``) followed by an optional list of imports (none here,
37+however ``Idris`` programs can consist of several modules, and the
38+definitions in each module each have their own namespace, as we will
39+discuss in Section :ref:`sect-namespaces`) and a collection of
40+declarations and definitions. The order of definitions is significant
41+— functions and data types must be defined before use. Each definition
42+must have a type declaration, for example see ``x : Int``, ``foo :
43+String``, from the above listing. Indentation is significant — a new
44+declaration begins at the same level of indentation as the preceding
45+declaration. Alternatively, declarations may be terminated with a
46+semicolon.
47+
48+A library module ``prelude`` is automatically imported by every
49+``Idris`` program, including facilities for IO, arithmetic, data
50+structures and various common functions. The prelude defines several
51+arithmetic and comparison operators, which we can use at the prompt.
52+Evaluating things at the prompt gives an answer, and the type of the
53+answer. For example:
54+
55+::
56+
57+ *prims> 6*6+6
58+ 42 : Int
59+ *prims> x == 6*6+6
60+ True : Bool
61+
62+All of the usual arithmetic and comparison operators are defined for
63+the primitive types. They are overloaded using type classes, as we
64+will discuss in Section :ref:`sect-classes` and can be extended to
65+work on user defined types. Boolean expressions can be tested with the
66+``if...then...else`` construct:
67+
68+::
69+
70+ *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
71+ "The answer!" : String
72+
73+Data Types
74+----------
75+
76+Data types are declared in a similar way to Haskell data types, with a
77+similar syntax. Natural numbers and lists, for example, can be
78+declared as follows:
79+
80+.. code-block:: idris
81+
82+ data Nat = Z | S Nat -- Natural numbers
83+ -- (zero and successor)
84+ data List a = Nil | (::) a (List a) -- Polymorphic lists
85+
86+The above declarations are taken from the standard library. Unary
87+natural numbers can be either zero (``Z``), or the successor of
88+another natural number (``S k``). Lists can either be empty (``Nil``)
89+or a value added to the front of another list (``x :: xs``). In the
90+declaration for ``List``, we used an infix operator ``::``. New
91+operators such as this can be added using a fixity declaration, as
92+follows:
93+
94+::
95+
96+ infixr 10 ::
97+
98+Functions, data constructors and type constructors may all be given
99+infix operators as names. They may be used in prefix form if enclosed
100+in brackets, e.g. ``(::)``. Infix operators can use any of the
101+symbols:
102+
103+::
104+
105+ :+-*/=_.?|&><!@$%^~.
106+
107+Functions
108+---------
109+
110+Functions are implemented by pattern matching, again using a similar
111+syntax to Haskell. The main difference is that ``Idris`` requires type
112+declarations for all functions, using a single colon ``:`` (rather
113+than Haskell’s double colon ``::``). Some natural number arithmetic
114+functions can be defined as follows, again taken from the standard
115+library:
116+
117+.. code-block:: idris
118+
119+ -- Unary addition
120+ plus : Nat -> Nat -> Nat
121+ plus Z y = y
122+ plus (S k) y = S (plus k y)
123+
124+ -- Unary multiplication
125+ mult : Nat -> Nat -> Nat
126+ mult Z y = Z
127+ mult (S k) y = plus y (mult k y)
128+
129+The standard arithmetic operators ``+`` and ``*`` are also overloaded
130+for use by ``Nat``, and are implemented using the above functions.
131+Unlike Haskell, there is no restriction on whether types and function
132+names must begin with a capital letter or not. Function names
133+(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
134+``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
135+all part of the same namespace. We can test these functions at the
136+``Idris`` prompt:
137+
138+::
139+
140+ Idris> plus (S (S Z)) (S (S Z))
141+ 4 : Nat
142+ Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
143+ 12 : Nat
144+
145+.. note::
146+
147+ ``Idris`` automatically desugars the ``Nat`` representation into a
148+ more human readable format. The result of ``plus (S (S Z)) (S (S Z))``
149+ is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be
150+ checked at the ``Idris`` prompt:
151+
152+::
153+
154+ Idris> (S (S (S (S Z))))
155+ 4 : Nat
156+
157+Like arithmetic operations, integer literals are also overloaded using
158+type classes, meaning that we can also test the functions as follows:
159+
160+::
161+
162+ Idris> plus 2 2
163+ 4 : Nat
164+ Idris> mult 3 (plus 2 2)
165+ 12 : Nat
166+
167+You may wonder, by the way, why we have unary natural numbers when our
168+computers have perfectly good integer arithmetic built in. The reason
169+is primarily that unary numbers have a very convenient structure which
170+is easy to reason about, and easy to relate to other data structures
171+as we will see later. Nevertheless, we do not want this convenience to
172+be at the expense of efficiency. Fortunately, ``Idris`` knows about
173+the relationship between ``Nat`` (and similarly structured types) and
174+numbers. This means it can optimise the representation, and functions
175+such as ``plus`` and ``mult``.
176+
177+``where`` clauses
178+~~~~~~~~~~~~~~~~~
179+
180+Functions can also be defined *locally* using ``where`` clauses. For
181+example, to define a function which reverses a list, we can use an
182+auxiliary function which accumulates the new, reversed list, and which
183+does not need to be visible globally:
184+
185+.. code-block:: idris
186+
187+ reverse : List a -> List a
188+ reverse xs = revAcc [] xs where
189+ revAcc : List a -> List a -> List a
190+ revAcc acc [] = acc
191+ revAcc acc (x :: xs) = revAcc (x :: acc) xs
192+
193+Indentation is significant — functions in the ``where`` block must be
194+indented further than the outer function.
195+
196+**Scope:** Any names which are visible in the outer scope are also
197+visible in the ``where`` clause (unless they have been redefined, such
198+as ``xs`` here). A name which appears only in the type will be in scope
199+in the ``where`` clause if it is a *parameter* to one of the types,
200+i.e. it is fixed across the entire structure.
201+
202+As well as functions, ``where`` blocks can include local data
203+declarations, such as the following where ``MyLT`` is not accessible
204+outside the definition of ``foo``:
205+
206+.. code-block:: idris
207+
208+ foo : Int -> Int
209+ foo x = case isLT of
210+ Yes => x*2
211+ No => x*4
212+ where
213+ data MyLT = Yes | No
214+
215+ isLT : MyLT
216+ isLT = if x < 20 then Yes else No
217+
218+In general, functions defined in a ``where`` clause need a type
219+declaration just like any top level function. However, the type
220+declaration for a function ``f`` *can* be omitted if:
221+
222+- ``f`` appears in the right hand side of the top level definition
223+
224+- The type of ``f`` can be completely determined from its first
225+ application
226+
227+So, for example, the following definitions are legal:
228+
229+.. code-block:: idris
230+
231+ even : Nat -> Bool
232+ even Z = True
233+ even (S k) = odd k where
234+ odd Z = False
235+ odd (S k) = even k
236+
237+ test : List Nat
238+ test = [c (S 1), c Z, d (S Z)]
239+ where c x = 42 + x
240+ d y = c (y + 1 + z y)
241+ where z w = y + w
242+
243+Dependent Types
244+---------------
245+
246+Vectors
247+~~~~~~~
248+
249+A standard example of a dependent type is the type of “lists with
250+length”, conventionally called vectors in the dependent type
251+literature. They are available as part of the ``Idris`` library, by
252+importing ``Data.Vect``, or we can declare them as follows:
253+
254+.. code-block:: idris
255+
256+ data Vect : Nat -> Type -> Type where
257+ Nil : Vect Z a
258+ (::) : a -> Vect k a -> Vect (S k) a
259+
260+Note that we have used the same constructor names as for ``List``.
261+Ad-hoc name overloading such as this is accepted by ``Idris``,
262+provided that the names are declared in different namespaces (in
263+practice, normally in different modules). Ambiguous constructor names
264+can normally be resolved from context.
265+
266+This declares a family of types, and so the form of the declaration is
267+rather different from the simple type declarations above. We
268+explicitly state the type of the type constructor ``Vect`` — it takes
269+a ``Nat`` and a type as an argument, where ``Type`` stands for the
270+type of types. We say that ``Vect`` is *indexed* over ``Nat`` and
271+*parameterised* by ``Type``. Each constructor targets a different part
272+of the family of types. ``Nil`` can only be used to construct vectors
273+with zero length, and ``::`` to construct vectors with non-zero
274+length. In the type of ``::``, we state explicitly that an element of
275+type ``a`` and a tail of type ``Vect k a`` (i.e., a vector of length
276+``k``) combine to make a vector of length ``S k``.
277+
278+We can define functions on dependent types such as ``Vect`` in the same
279+way as on simple types such as ``List`` and ``Nat`` above, by pattern
280+matching. The type of a function over ``Vect`` will describe what
281+happens to the lengths of the vectors involved. For example, ``++``,
282+defined as follows, appends two ``Vect``:
283+
284+.. code-block:: idris
285+
286+ (++) : Vect n a -> Vect m a -> Vect (n + m) a
287+ (++) Nil ys = ys
288+ (++) (x :: xs) ys = x :: xs ++ ys
289+
290+The type of ``(++)`` states that the resulting vector’s length will be
291+the sum of the input lengths. If we get the definition wrong in such a
292+way that this does not hold, ``Idris`` will not accept the definition.
293+For example:
294+
295+.. code-block:: idris
296+
297+ (++) : Vect n a -> Vect m a -> Vect (n + m) a
298+ (++) Nil ys = ys
299+ (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
300+
301+When run through the ``Idris`` type checker, this results in the
302+following:
303+
304+::
305+
306+ $ idris vbroken.idr --check
307+ vbroken.idr:9:23:When elaborating right hand side of Vect.++:
308+ When elaborating an application of constructor Vect.:::
309+ Can't unify
310+ Vect (k + k) a
311+ with
312+ Vect (plus k m) a
313+
314+ Specifically:
315+ Can't unify
316+ plus k k
317+ with
318+ plus k m
319+
320+This error message suggests that there is a length mismatch between
321+two vectors — we needed a vector of length ``k + m``, but provided a
322+vector of length ``k + k``.
323+
324+The Finite Sets
325+~~~~~~~~~~~~~~~
326+
327+Finite sets, as the name suggests, are sets with a finite number of
328+elements. They are available as part of the ``Idris`` library, by
329+importing ``Data.Fin``, or can be declared as follows:
330+
331+.. code-block:: idris
332+
333+ data Fin : Nat -> Type where
334+ FZ : Fin (S k)
335+ FS : Fin k -> Fin (S k)
336+
337+``FZ`` is the zeroth element of a finite set with ``S k`` elements;
338+``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
339+elements. ``Fin`` is indexed by a ``Nat``, which represents the number
340+of elements in the set. Obviously we can’t construct an element of an
341+empty set, so neither constructor targets ``Fin Z``.
342+
343+A useful application of the ``Fin`` family is to represent bounded
344+natural numbers. Since the first ``n`` natural numbers form a finite
345+set of ``n`` elements, we can treat ``Fin n`` as the set of natural
346+numbers bounded by ``n``.
347+
348+For example, the following function which looks up an element in a
349+``Vect``, by a bounded index given as a ``Fin n``, is defined in the
350+prelude:
351+
352+.. code-block:: idris
353+
354+ index : Fin n -> Vect n a -> a
355+ index FZ (x :: xs) = x
356+ index (FS k) (x :: xs) = index k xs
357+
358+This function looks up a value at a given location in a vector. The
359+location is bounded by the length of the vector (``n`` in each case),
360+so there is no need for a run-time bounds check. The type checker
361+guarantees that the location is no larger than the length of the
362+vector.
363+
364+Note also that there is no case for ``Nil`` here. This is because it
365+is impossible. Since there is no element of ``Fin Z``, and the
366+location is a ``Fin n``, then ``n`` can not be ``Z``. As a result,
367+attempting to look up an element in an empty vector would give a
368+compile time type error, since it would force ``n`` to be ``Z``.
369+
370+Implicit Arguments
371+~~~~~~~~~~~~~~~~~~
372+
373+Let us take a closer look at the type of ``index``:
374+
375+.. code-block:: idris
376+
377+ index : Fin n -> Vect n a -> a
378+
379+It takes two arguments, an element of the finite set of ``n`` elements,
380+and a vector with ``n`` elements of type ``a``. But there are also two
381+names, ``n`` and ``a``, which are not declared explicitly. These are
382+*implicit* arguments to ``index``. We could also write the type of
383+``index`` as:
384+
385+.. code-block:: idris
386+
387+ index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
388+
389+Implicit arguments, given in braces ``{}`` in the type declaration,
390+are not given in applications of ``index``; their values can be
391+inferred from the types of the ``Fin n`` and ``Vect n a``
392+arguments. Any name with a which appears as a parameter or index in a
393+type declaration, but which is otherwise free, will be automatically
394+bound as an implicit argument. Implicit arguments can still be given
395+explicitly in applications, using ``{a=value}`` and ``{n=value}``, for
396+example:
397+
398+.. code-block:: idris
399+
400+ index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
401+
402+In fact, any argument, implicit or explicit, may be given a name. We
403+could have declared the type of ``index`` as:
404+
405+.. code-block:: idris
406+
407+ index : (i:Fin n) -> (xs:Vect n a) -> a
408+
409+It is a matter of taste whether you want to do this — sometimes it can
410+help document a function by making the purpose of an argument more
411+clear.
412+
413+“``using``” notation
414+~~~~~~~~~~~~~~~~~~~~
415+
416+Sometimes it is useful to provide types of implicit arguments,
417+particularly where there is a dependency ordering, or where the
418+implicit arguments themselves have dependencies. For example, we may
419+wish to state the types of the implicit arguments in the following
420+definition, which defines a predicate on vectors:
421+
422+.. code-block:: idris
423+
424+ data Elem : a -> Vect n a -> Type where
425+ Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
426+ There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
427+
428+An instance of ``Elem x xs`` states that ``x`` is an element of
429+``xs``. We can construct such a predicate if the required element is
430+``Here``, at the head of the vector, or ``There``, in the tail of the
431+vector. For example:
432+
433+.. code-block:: idris
434+
435+ testVec : Vect 4 Int
436+ testVec = 3 :: 4 :: 5 :: 6 :: Nil
437+
438+ inVect : Elem 5 testVec
439+ inVect = There (There Here)
440+
441+If the same implicit arguments are being used a lot, it can make a
442+definition difficult to read. To avoid this problem, a ``using`` block
443+gives the types and ordering of any implicit arguments which can
444+appear within the block:
445+
446+.. code-block:: idris
447+
448+ using (x:a, y:a, xs:Vect n a)
449+ data Elem : a -> Vect n a -> Type where
450+ Here : Elem x (x :: xs)
451+ There : Elem x xs -> Elem x (y :: xs)
452+
453+Note: Declaration Order and ``mutual`` blocks
454+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
455+
456+In general, functions and data types must be defined before use, since
457+dependent types allow functions to appear as part of types, and their
458+reduction behaviour to affect type checking. However, this restriction
459+can be relaxed by using a ``mutual`` block, which allows data types
460+and functions to be defined simultaneously:
461+
462+.. code-block:: idris
463+
464+ mutual
465+ even : Nat -> Bool
466+ even Z = True
467+ even (S k) = odd k
468+
469+ odd : Nat -> Bool
470+ odd Z = False
471+ odd (S k) = even k
472+
473+In a ``mutual`` block, first all of the type declarations are added,
474+then the function bodies. As a result, none of the function types can
475+depend on the reduction behaviour of any of the functions in the
476+block.
477+
478+I/O
479+---
480+
481+Computer programs are of little use if they do not interact with the
482+user or the system in some way. The difficulty in a pure language such
483+as ``Idris`` — that is, a language where expressions do not have
484+side-effects — is that I/O is inherently side-effecting. Therefore in
485+``Idris``, such interactions are encapsulated in the type ``IO``:
486+
487+.. code-block:: idris
488+
489+ data IO a -- IO operation returning a value of type a
490+
491+We’ll leave the definition of ``IO`` abstract, but effectively it
492+describes what the I/O operations to be executed are, rather than how
493+to execute them. The resulting operations are executed externally, by
494+the run-time system. We’ve already seen one IO program:
495+
496+.. code-block:: idris
497+
498+ main : IO ()
499+ main = putStrLn "Hello world"
500+
501+The type of ``putStrLn`` explains that it takes a string, and returns
502+an element of the unit type ``()`` via an I/O action. There is a
503+variant ``putStr`` which outputs a string without a newline:
504+
505+.. code-block:: idris
506+
507+ putStrLn : String -> IO ()
508+ putStr : String -> IO ()
509+
510+We can also read strings from user input:
511+
512+.. code-block:: idris
513+
514+ getLine : IO String
515+
516+A number of other I/O operations are defined in the prelude, for
517+example for reading and writing files, including:
518+
519+.. code-block:: idris
520+
521+ data File -- abstract
522+ data Mode = Read | Write | ReadWrite
523+
524+ openFile : String -> Mode -> IO File
525+ closeFile : File -> IO ()
526+
527+ fread : File -> IO String
528+ fwrite : File -> String -> IO ()
529+ feof : File -> IO Bool
530+
531+ readFile : String -> IO String
532+
533+.. _sect-do:
534+
535+“``do``” notation
536+-----------------
537+
538+I/O programs will typically need to sequence actions, feeding the
539+output of one computation into the input of the next. ``IO`` is an
540+abstract type, however, so we can’t access the result of a computation
541+directly. Instead, we sequence operations with ``do`` notation:
542+
543+.. code-block:: idris
544+
545+ greet : IO ()
546+ greet = do putStr "What is your name? "
547+ name <- getLine
548+ putStrLn ("Hello " ++ name)
549+
550+The syntax ``x <- iovalue`` executes the I/O operation ``iovalue``, of
551+type ``IO a``, and puts the result, of type ``a`` into the variable
552+``x``. In this case, ``getLine`` returns an ``IO String``, so ``name``
553+has type ``String``. Indentation is significant — each statement in
554+the do block must begin in the same column. The ``return`` operation
555+allows us to inject a value directly into an IO operation:
556+
557+.. code-block:: idris
558+
559+ return : a -> IO a
560+
561+As we will see later, ``do`` notation is more general than this, and
562+can be overloaded.
563+
564+.. _sect-lazy:
565+
566+Laziness
567+--------
568+
569+Normally, arguments to functions are evaluated before the function
570+itself (that is, ``Idris`` uses *eager* evaluation). However, this is
571+not always the best approach. Consider the following function:
572+
573+.. code-block:: idris
574+
575+ boolCase : Bool -> a -> a -> a;
576+ boolCase True t e = t;
577+ boolCase False t e = e;
578+
579+This function uses one of the ``t`` or ``e`` arguments, but not both
580+(in fact, this is used to implement the ``if...then...else`` construct
581+as we will see later. We would prefer if *only* the argument which was
582+used was evaluated. To achieve this, ``Idris`` provides a ``Lazy``
583+data type, which allows evaluation to be suspended:
584+
585+.. code-block:: idris
586+
587+ data Lazy : Type -> Type where
588+ Delay : (val : a) -> Lazy a
589+
590+ Force : Lazy a -> a
591+
592+A value of type ``Lazy a`` is unevaluated until it is forced by
593+``Force``. The ``Idris`` type checker knows about the ``Lazy`` type,
594+and inserts conversions where necessary between ``Lazy a`` and ``a``,
595+and vice versa. We can therefore write ``boolCase`` as follows,
596+without any explicit use of ``Force`` or ``Delay``:
597+
598+.. code-block:: idris
599+
600+ boolCase : Bool -> Lazy a -> Lazy a -> a;
601+ boolCase True t e = t;
602+ boolCase False t e = e;
603+
604+Useful Data Types
605+-----------------
606+
607+``Idris`` includes a number of useful data types and library functions
608+(see the ``libs/`` directory in the distribution). This chapter
609+describes a few of these. The functions described here are imported
610+automatically by every ``Idris`` program, as part of ``Prelude.idr``.
611+
612+``List`` and ``Vect``
613+~~~~~~~~~~~~~~~~~~~~~
614+
615+We have already seen the ``List`` and ``Vect`` data types:
616+
617+.. code-block:: idris
618+
619+ data List a = Nil | (::) a (List a)
620+
621+ data Vect : Nat -> Type -> Type where
622+ Nil : Vect Z a
623+ (::) : a -> Vect k a -> Vect (S k) a
624+
625+Note that the constructor names are the same for each — constructor
626+names (in fact, names in general) can be overloaded, provided that
627+they are declared in different namespaces (see Section
628+:ref:`sect-namespaces`), and will typically be resolved according to
629+their type. As syntactic sugar, any type with the constructor names
630+``Nil`` and ``::`` can be written in list form. For example:
631+
632+- ``[]`` means ``Nil``
633+
634+- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
635+
636+The library also defines a number of functions for manipulating these
637+types. ``map`` is overloaded both for ``List`` and ``Vect`` and
638+applies a function to every element of the list or vector.
639+
640+.. code-block:: idris
641+
642+ map : (a -> b) -> List a -> List b
643+ map f [] = []
644+ map f (x :: xs) = f x :: map f xs
645+
646+ map : (a -> b) -> Vect n a -> Vect n b
647+ map f [] = []
648+ map f (x :: xs) = f x :: map f xs
649+
650+For example, given the following vector of integers, and a function to
651+double an integer:
652+
653+.. code-block:: idris
654+
655+ intVec : Vect 5 Int
656+ intVec = [1, 2, 3, 4, 5]
657+
658+ double : Int -> Int
659+ double x = x * 2
660+
661+the function ``map`` can be used as follows to double every element in
662+the vector:
663+
664+::
665+
666+ *usefultypes> show (map double intVec)
667+ "[2, 4, 6, 8, 10]" : String
668+
669+You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
670+directory. For more details of the functions available on ``List`` and
671+``Vect``, look in the library files:
672+
673+- ``libs/prelude/Prelude/List.idr``
674+
675+- ``libs/base/Data/List.idr``
676+
677+- ``libs/base/Data/Vect.idr``
678+
679+- ``libs/base/Data/VectType.idr``
680+
681+Functions include filtering, appending, reversing, and so on. Also
682+remember that ``Idris`` is still in development, so if you don’t see
683+the function you need, please feel free to add it and submit a patch!
684+
685+Aside: Anonymous functions and operator sections
686+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
687+
688+There are actually neater ways to write the above expression. One way
689+would be to use an anonymous function:
690+
691+::
692+
693+ *usefultypes> show (map (\x => x * 2) intVec)
694+ "[2, 4, 6, 8, 10]" : String
695+
696+The notation ``\x => val`` constructs an anonymous function which takes
697+one argument, ``x`` and returns the expression ``val``. Anonymous
698+functions may take several arguments, separated by commas,
699+e.g. ``\x, y, z => val``. Arguments may also be given explicit types,
700+e.g. ``\x : Int => x * 2``, and can pattern match,
701+e.g. ``\(x, y) => x + y``. We could also use an operator section:
702+
703+::
704+
705+ *usefultypes> show (map (* 2) intVec)
706+ "[2, 4, 6, 8, 10]" : String
707+
708+``(*2)`` is shorthand for a function which multiplies a number
709+by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
710+to ``\x => 2 * x``.
711+
712+Maybe
713+~~~~~
714+
715+``Maybe`` describes an optional value. Either there is a value of the
716+given type, or there isn’t:
717+
718+.. code-block:: idris
719+
720+ data Maybe a = Just a | Nothing
721+
722+``Maybe`` is one way of giving a type to an operation that may
723+fail. For example, looking something up in a ``List`` (rather than a
724+vector) may result in an out of bounds error:
725+
726+.. code-block:: idris
727+
728+ list_lookup : Nat -> List a -> Maybe a
729+ list_lookup _ Nil = Nothing
730+ list_lookup Z (x :: xs) = Just x
731+ list_lookup (S k) (x :: xs) = list_lookup k xs
732+
733+The ``maybe`` function is used to process values of type ``Maybe``,
734+either by applying a function to the value, if there is one, or by
735+providing a default value:
736+
737+.. code-block:: idris
738+
739+ maybe : Lazy b -> (a -> b) -> Maybe a -> b
740+
741+Note that the type of the first argument is ``Lazy b`` rather than
742+simply ``b``. Since the default value might not be used, we mark it as
743+``Lazy`` in case it is a large expression where evaluating it then
744+discarding it would be wasteful.
745+
746+Tuples and Dependent Pairs
747+~~~~~~~~~~~~~~~~~~~~~~~~~~
748+
749+Values can be paired with the following built-in data type:
750+
751+.. code-block:: idris
752+
753+ data Pair a b = MkPair a b
754+
755+As syntactic sugar, we can write ``(a, b)`` which, according to
756+context, means either ``Pair a b`` or ``MkPair a b``. Tuples can
757+contain an arbitrary number of values, represented as nested pairs:
758+
759+.. code-block:: idris
760+
761+ fred : (String, Int)
762+ fred = ("Fred", 42)
763+
764+ jim : (String, Int, String)
765+ jim = ("Jim", 25, "Cambridge")
766+
767+Dependent Pairs
768+~~~~~~~~~~~~~~~
769+
770+Dependent pairs allow the type of the second element of a pair to depend
771+on the value of the first element. Traditionally, these are referred to
772+as “sigma types”:
773+
774+.. code-block:: idris
775+
776+ data Sigma : (A : Type) -> (P : A -> Type) -> Type where
777+ MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
778+
779+Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
780+of a pair of A and P, where the name ``a`` can occur inside ``P``.
781+``( a ** p )`` constructs a value of this type. For example, we can
782+pair a number with a ``Vect`` of a particular length.
783+
784+.. code-block:: idris
785+
786+ vec : (n : Nat ** Vect n Int)
787+ vec = (2 ** [3, 4])
788+
789+If you like, you can write it out the long way, the two are precisely
790+equivalent.
791+
792+.. code-block:: idris
793+
794+ vec : Sigma Nat (\n => Vect n Int)
795+ vec = MkSigma 2 [3, 4]
796+
797+The type checker could of course infer the value of the first element
798+from the length of the vector. We can write an underscore ``_`` in
799+place of values which we expect the type checker to fill in, so the
800+above definition could also be written as:
801+
802+.. code-block:: idris
803+
804+ vec : (n : Nat ** Vect n Int)
805+ vec = (_ ** [3, 4])
806+
807+We might also prefer to omit the type of the first element of the
808+pair, since, again, it can be inferred:
809+
810+.. code-block:: idris
811+
812+ vec : (n ** Vect n Int)
813+ vec = (_ ** [3, 4])
814+
815+One use for dependent pairs is to return values of dependent types
816+where the index is not necessarily known in advance. For example, if
817+we filter elements out of a ``Vect`` according to some predicate, we
818+will not know in advance what the length of the resulting vector will
819+be:
820+
821+.. code-block:: idris
822+
823+ filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
824+
825+If the ``Vect`` is empty, the result is easy:
826+
827+.. code-block:: idris
828+
829+ filter p Nil = (_ ** [])
830+
831+In the ``::`` case, we need to inspect the result of a recursive call
832+to ``filter`` to extract the length and the vector from the result. To
833+do this, we use ``with`` notation, which allows pattern matching on
834+intermediate values:
835+
836+.. code-block:: idris
837+
838+ filter p (x :: xs) with (filter p xs)
839+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
840+
841+We will see more on ``with`` notation later.
842+
843+.. _sect-more-expr:
844+
845+More Expressions
846+----------------
847+
848+``let`` bindings
849+~~~~~~~~~~~~~~~~
850+
851+Intermediate values can be calculated using ``let`` bindings:
852+
853+.. code-block:: idris
854+
855+ data Person = MkPerson String Int
856+
857+ showPerson : Person -> String
858+ showPerson p = let MkPerson name age = p in
859+ name ++ " is " ++ show age ++ " years old"
860+
861+ splitAt : Char -> String -> (String, String)
862+ splitAt c x = case break (== c) x of
863+ (x, y) => (x, strTail y)
864+
865+We can do simple pattern matching in ``let`` bindings too. For
866+example, we can extract fields from a record as follows, as well as by
867+pattern matching at the top level:
868+
869+.. code-block:: idris
870+
871+ data Person = MkPerson String Int
872+
873+ showPerson : Person -> String
874+ showPerson p = let MkPerson name age = p in
875+ name ++ " is " ++ show age ++ " years old"
876+
877+List comprehensions
878+~~~~~~~~~~~~~~~~~~~
879+
880+``Idris`` provides *comprehension* notation as a convenient shorthand
881+for building lists. The general form is:
882+
883+::
884+
885+ [ expression | qualifiers ]
886+
887+This generates the list of values produced by evaluating the
888+``expression``, according to the conditions given by the comma
889+separated ``qualifiers``. For example, we can build a list of
890+Pythagorean triples as follows:
891+
892+.. code-block:: idris
893+
894+ pythag : Int -> List (Int, Int, Int)
895+ pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
896+ x*x + y*y == z*z ]
897+
898+The ``[a..b]`` notation is another shorthand which builds a list of
899+numbers between ``a`` and ``b``. Alternatively ``[a,b..c]`` builds a
900+list of numbers between ``a`` and ``c`` with the increment specified
901+by the difference between ``a`` and ``b``. This works for any numeric
902+type, using the ``count`` function from the prelude.
903+
904+``case`` expressions
905+~~~~~~~~~~~~~~~~~~~~
906+
907+Another way of inspecting intermediate values of *simple* types is to
908+use a ``case`` expression. The following function, for example, splits
909+a string into two at a given character:
910+
911+.. code-block:: idris
912+
913+ splitAt : Char -> String -> (String, String)
914+ splitAt c x = case break (== c) x of
915+ (x, y) => (x, strTail y)
916+
917+``break`` is a library function which breaks a string into a pair of
918+strings at the point where the given function returns true. We then
919+deconstruct the pair it returns, and remove the first character of the
920+second string.
921+
922+A ``case`` expression can match several cases, for example, to inspect
923+an intermediate value of type ``Maybe a``. Recall ``list_lookup``
924+which looks up an index in a list, returning ``Nothing`` if the index
925+is out of bounds. We can use this to write ``lookup_default``, which
926+looks up an index and returns a default value if the index is out of
927+bounds:
928+
929+.. code-block:: idris
930+
931+ lookup_default : Nat -> List a -> a -> a
932+ lookup_default i xs def = case list_lookup i xs of
933+ Nothing => def
934+ Just x => x
935+
936+If the index is in bounds, we get the value at that index, otherwise
937+we get a default value:
938+
939+::
940+
941+ *usefultypes> lookup_default 2 [3,4,5,6] (-1)
942+ 5 : Integer
943+ *usefultypes> lookup_default 4 [3,4,5,6] (-1)
944+ -1 : Integer
945+
946+**Restrictions:** The ``case`` construct is intended for simple
947+analysis of intermediate expressions to avoid the need to write
948+auxiliary functions, and is also used internally to implement pattern
949+matching ``let`` and lambda bindings. It will *only* work if:
950+
951+- Each branch *matches* a value of the same type, and *returns* a value
952+ of the same type.
953+
954+- The type of the result is “known”. i.e. the type of the expression
955+ can be determined *without* type checking the ``case``-expression
956+ itself.
957+
958+Dependent Records
959+-----------------
960+
961+*Records* are data types which collect several values (the record’s
962+*fields*) together. ``Idris`` provides syntax for defining records and
963+*automatically generating field access and update functions. For
964+*example, we can represent a person’s name and age in a record:
965+
966+.. code-block:: idris
967+
968+ record Person : Type where
969+ MkPerson : (name : String) ->
970+ (age : Int) -> Person
971+
972+ fred : Person
973+ fred = MkPerson "Fred" 30
974+
975+Record declarations are like ``data`` declarations, except that they
976+are introduced by the ``record`` keyword, and can only have one
977+constructor. The names of the binders in the constructor type
978+(``name`` and ``age``) here are the field names, which we can use to
979+access the field values:
980+
981+::
982+
983+ *record> name fred
984+ "Fred" : String
985+ *record> age fred
986+ 30 : Int
987+ *record> :t name
988+ name : Person -> String
989+
990+We can also use the field names to update a record (or, more
991+precisely, produce a new record with the given fields updated).
992+
993+.. code-block:: bash
994+
995+ *record> record { name = "Jim" } fred
996+ MkPerson "Jim" 30 : Person
997+ *record> record { name = "Jim", age = 20 } fred
998+ MkPerson "Jim" 20 : Person
999+
1000+The syntax ``record { field = val, ... }`` generates a function which
1001+updates the given fields in a record.
1002+
1003+Records, and fields within records, can have dependent types. Updates
1004+are allowed to change the type of a field, provided that the result is
1005+well-typed, and the result does not affect the type of the record as a
1006+whole. For example:
1007+
1008+.. code-block:: idris
1009+
1010+ record Class : Type where
1011+ ClassInfo : (students : Vect n Person) ->
1012+ (className : String) ->
1013+ Class
1014+
1015+It is safe to update the ``students`` field to a vector of a different
1016+length because it will not affect the type of the record:
1017+
1018+.. code-block:: idris
1019+
1020+ addStudent : Person -> Class -> Class
1021+ addStudent p c = record { students = p :: students c } c
1022+
1023+::
1024+
1025+ *record> addStudent fred (ClassInfo [] "CS")
1026+ ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1027+ : Class
1028+
1029+Nested record update
1030+~~~~~~~~~~~~~~~~~~~~
1031+
1032+``Idris`` also provides a convenient syntax for accessing and updating
1033+nested records. For example, if a field is accessible with the
1034+expression ``c (b (a x))``, it can be updated using the following
1035+syntax:
1036+
1037+.. code-block:: idris
1038+
1039+ record { a->b->c = val } x
1040+
1041+This returns a new record, with the field accessed by the path
1042+``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
1043+a->b->c = val }`` itself has a function type. Symmetrically, the field
1044+can also be accessed with the following syntax:
1045+
1046+.. code-block:: idris
1047+
1048+ record { a->b->c } x