@@ -0,0 +1,1048 @@
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
27+ foo = "Sausage machine"
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
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
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:
70+ *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
71+ "The answer!" : String
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
82+ data Nat = Z | S Nat -- Natural numbers
83+ -- (zero and successor)
84+ data List a = Nil | (::) a (List a) -- Polymorphic lists
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
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
105+ :+-*/=_.?|&><!@$%^~.
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
117+.. code-block:: idris
120+ plus : Nat -> Nat -> Nat
122+ plus (S k) y = S (plus k y)
124+ -- Unary multiplication
125+ mult : Nat -> Nat -> Nat
127+ mult (S k) y = plus y (mult k y)
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
140+ Idris> plus (S (S Z)) (S (S Z))
142+ Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
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:
154+ Idris> (S (S (S (S Z))))
157+Like arithmetic operations, integer literals are also overloaded using
158+type classes, meaning that we can also test the functions as follows:
164+ Idris> mult 3 (plus 2 2)
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``.
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:
185+.. code-block:: idris
187+ reverse : List a -> List a
188+ reverse xs = revAcc [] xs where
189+ revAcc : List a -> List a -> List a
191+ revAcc acc (x :: xs) = revAcc (x :: acc) xs
193+Indentation is significant — functions in the ``where`` block must be
194+indented further than the outer function.
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.
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``:
206+.. code-block:: idris
209+ foo x = case isLT of
213+ data MyLT = Yes | No
216+ isLT = if x < 20 then Yes else No
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:
222+- ``f`` appears in the right hand side of the top level definition
224+- The type of ``f`` can be completely determined from its first
227+So, for example, the following definitions are legal:
229+.. code-block:: idris
233+ even (S k) = odd k where
238+ test = [c (S 1), c Z, d (S Z)]
240+ d y = c (y + 1 + z y)
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:
254+.. code-block:: idris
256+ data Vect : Nat -> Type -> Type where
258+ (::) : a -> Vect k a -> Vect (S k) a
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.
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``.
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``:
284+.. code-block:: idris
286+ (++) : Vect n a -> Vect m a -> Vect (n + m) a
288+ (++) (x :: xs) ys = x :: xs ++ ys
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.
295+.. code-block:: idris
297+ (++) : Vect n a -> Vect m a -> Vect (n + m) a
299+ (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
301+When run through the ``Idris`` type checker, this results in the
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.:::
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``.
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:
331+.. code-block:: idris
333+ data Fin : Nat -> Type where
335+ FS : Fin k -> Fin (S k)
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``.
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``.
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
352+.. code-block:: idris
354+ index : Fin n -> Vect n a -> a
355+ index FZ (x :: xs) = x
356+ index (FS k) (x :: xs) = index k xs
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
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``.
373+Let us take a closer look at the type of ``index``:
375+.. code-block:: idris
377+ index : Fin n -> Vect n a -> a
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
385+.. code-block:: idris
387+ index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
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
398+.. code-block:: idris
400+ index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
402+In fact, any argument, implicit or explicit, may be given a name. We
403+could have declared the type of ``index`` as:
405+.. code-block:: idris
407+ index : (i:Fin n) -> (xs:Vect n a) -> a
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
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:
422+.. code-block:: idris
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)
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
433+.. code-block:: idris
435+ testVec : Vect 4 Int
436+ testVec = 3 :: 4 :: 5 :: 6 :: Nil
438+ inVect : Elem 5 testVec
439+ inVect = There (There Here)
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:
446+.. code-block:: idris
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)
453+Note: Declaration Order and ``mutual`` blocks
454+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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:
462+.. code-block:: idris
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
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``:
487+.. code-block:: idris
489+ data IO a -- IO operation returning a value of type a
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:
496+.. code-block:: idris
499+ main = putStrLn "Hello world"
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:
505+.. code-block:: idris
507+ putStrLn : String -> IO ()
508+ putStr : String -> IO ()
510+We can also read strings from user input:
512+.. code-block:: idris
516+A number of other I/O operations are defined in the prelude, for
517+example for reading and writing files, including:
519+.. code-block:: idris
521+ data File -- abstract
522+ data Mode = Read | Write | ReadWrite
524+ openFile : String -> Mode -> IO File
525+ closeFile : File -> IO ()
527+ fread : File -> IO String
528+ fwrite : File -> String -> IO ()
529+ feof : File -> IO Bool
531+ readFile : String -> IO String
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:
543+.. code-block:: idris
546+ greet = do putStr "What is your name? "
548+ putStrLn ("Hello " ++ name)
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:
557+.. code-block:: idris
561+As we will see later, ``do`` notation is more general than this, and
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:
573+.. code-block:: idris
575+ boolCase : Bool -> a -> a -> a;
576+ boolCase True t e = t;
577+ boolCase False t e = e;
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:
585+.. code-block:: idris
587+ data Lazy : Type -> Type where
588+ Delay : (val : a) -> Lazy a
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``:
598+.. code-block:: idris
600+ boolCase : Bool -> Lazy a -> Lazy a -> a;
601+ boolCase True t e = t;
602+ boolCase False t e = e;
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``.
612+``List`` and ``Vect``
613+~~~~~~~~~~~~~~~~~~~~~
615+We have already seen the ``List`` and ``Vect`` data types:
617+.. code-block:: idris
619+ data List a = Nil | (::) a (List a)
621+ data Vect : Nat -> Type -> Type where
623+ (::) : a -> Vect k a -> Vect (S k) a
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:
632+- ``[]`` means ``Nil``
634+- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
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.
640+.. code-block:: idris
642+ map : (a -> b) -> List a -> List b
644+ map f (x :: xs) = f x :: map f xs
646+ map : (a -> b) -> Vect n a -> Vect n b
648+ map f (x :: xs) = f x :: map f xs
650+For example, given the following vector of integers, and a function to
653+.. code-block:: idris
656+ intVec = [1, 2, 3, 4, 5]
661+the function ``map`` can be used as follows to double every element in
666+ *usefultypes> show (map double intVec)
667+ "[2, 4, 6, 8, 10]" : String
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:
673+- ``libs/prelude/Prelude/List.idr``
675+- ``libs/base/Data/List.idr``
677+- ``libs/base/Data/Vect.idr``
679+- ``libs/base/Data/VectType.idr``
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!
685+Aside: Anonymous functions and operator sections
686+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688+There are actually neater ways to write the above expression. One way
689+would be to use an anonymous function:
693+ *usefultypes> show (map (\x => x * 2) intVec)
694+ "[2, 4, 6, 8, 10]" : String
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:
705+ *usefultypes> show (map (* 2) intVec)
706+ "[2, 4, 6, 8, 10]" : String
708+``(*2)`` is shorthand for a function which multiplies a number
709+by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
715+``Maybe`` describes an optional value. Either there is a value of the
716+given type, or there isn’t:
718+.. code-block:: idris
720+ data Maybe a = Just a | Nothing
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:
726+.. code-block:: idris
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
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:
737+.. code-block:: idris
739+ maybe : Lazy b -> (a -> b) -> Maybe a -> b
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.
746+Tuples and Dependent Pairs
747+~~~~~~~~~~~~~~~~~~~~~~~~~~
749+Values can be paired with the following built-in data type:
751+.. code-block:: idris
753+ data Pair a b = MkPair a b
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:
759+.. code-block:: idris
761+ fred : (String, Int)
764+ jim : (String, Int, String)
765+ jim = ("Jim", 25, "Cambridge")
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
774+.. code-block:: idris
776+ data Sigma : (A : Type) -> (P : A -> Type) -> Type where
777+ MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
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.
784+.. code-block:: idris
786+ vec : (n : Nat ** Vect n Int)
789+If you like, you can write it out the long way, the two are precisely
792+.. code-block:: idris
794+ vec : Sigma Nat (\n => Vect n Int)
795+ vec = MkSigma 2 [3, 4]
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:
802+.. code-block:: idris
804+ vec : (n : Nat ** Vect n Int)
807+We might also prefer to omit the type of the first element of the
808+pair, since, again, it can be inferred:
810+.. code-block:: idris
812+ vec : (n ** Vect n Int)
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
821+.. code-block:: idris
823+ filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
825+If the ``Vect`` is empty, the result is easy:
827+.. code-block:: idris
829+ filter p Nil = (_ ** [])
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
836+.. code-block:: idris
838+ filter p (x :: xs) with (filter p xs)
839+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
841+We will see more on ``with`` notation later.
851+Intermediate values can be calculated using ``let`` bindings:
853+.. code-block:: idris
855+ data Person = MkPerson String Int
857+ showPerson : Person -> String
858+ showPerson p = let MkPerson name age = p in
859+ name ++ " is " ++ show age ++ " years old"
861+ splitAt : Char -> String -> (String, String)
862+ splitAt c x = case break (== c) x of
863+ (x, y) => (x, strTail y)
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:
869+.. code-block:: idris
871+ data Person = MkPerson String Int
873+ showPerson : Person -> String
874+ showPerson p = let MkPerson name age = p in
875+ name ++ " is " ++ show age ++ " years old"
880+``Idris`` provides *comprehension* notation as a convenient shorthand
881+for building lists. The general form is:
885+ [ expression | qualifiers ]
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:
892+.. code-block:: idris
894+ pythag : Int -> List (Int, Int, Int)
895+ pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
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.
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:
911+.. code-block:: idris
913+ splitAt : Char -> String -> (String, String)
914+ splitAt c x = case break (== c) x of
915+ (x, y) => (x, strTail y)
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
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
929+.. code-block:: idris
931+ lookup_default : Nat -> List a -> a -> a
932+ lookup_default i xs def = case list_lookup i xs of
936+If the index is in bounds, we get the value at that index, otherwise
937+we get a default value:
941+ *usefultypes> lookup_default 2 [3,4,5,6] (-1)
943+ *usefultypes> lookup_default 4 [3,4,5,6] (-1)
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:
951+- Each branch *matches* a value of the same type, and *returns* a value
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
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:
966+.. code-block:: idris
968+ record Person : Type where
969+ MkPerson : (name : String) ->
970+ (age : Int) -> Person
973+ fred = MkPerson "Fred" 30
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:
988+ name : Person -> String
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).
995+ *record> record { name = "Jim" } fred
996+ MkPerson "Jim" 30 : Person
997+ *record> record { name = "Jim", age = 20 } fred
998+ MkPerson "Jim" 20 : Person
1000+The syntax ``record { field = val, ... }`` generates a function which
1001+updates the given fields in a record.
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
1008+.. code-block:: idris
1010+ record Class : Type where
1011+ ClassInfo : (students : Vect n Person) ->
1012+ (className : String) ->
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:
1018+.. code-block:: idris
1020+ addStudent : Person -> Class -> Class
1021+ addStudent p c = record { students = p :: students c } c
1025+ *record> addStudent fred (ClassInfo [] "CS")
1026+ ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1029+Nested record update
1030+~~~~~~~~~~~~~~~~~~~~
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
1037+.. code-block:: idris
1039+ record { a->b->c = val } x
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:
1046+.. code-block:: idris
1048+ record { a->b->c } x