@@ -1,5 +1,3 @@
3===================
1===================
4Types and Functions
2Types and Functions
5===================
3===================
@@ -190,7 +188,7 @@ indented further than the outer function.
190visible in the ``where`` clause (unless they have been redefined, such
188visible in the ``where`` clause (unless they have been redefined, such
191as ``xs`` here). A name which appears only in the type will be in scope
189as ``xs`` here). A name which appears only in the type will be in scope
192in the ``where`` clause if it is a *parameter* to one of the types,
190in the ``where`` clause if it is a *parameter* to one of the types,
193−i.e. it is fixed across the entire structure.
191+i.e. it is fixed across the entire structure.
195As well as functions, ``where`` blocks can include local data
193As well as functions, ``where`` blocks can include local data
196declarations, such as the following where ``MyLT`` is not accessible
194declarations, such as the following where ``MyLT`` is not accessible
@@ -549,7 +547,283 @@ us to inject a value directly into an IO operation:
549As we will see later, ``do`` notation is more general than this, and can
547As we will see later, ``do`` notation is more general than this, and can
550be overloaded.
548be overloaded.
552−.. _sect-more-expr:
550+.. _sect-lazy:
555+Normally, arguments to functions are evaluated before the function
556+itself (that is, ``Idris`` uses *eager* evaluation). However, this is
557+not always the best approach. Consider the following function:
559+.. code-block:: idris
561+ boolCase : Bool -> a -> a -> a;
562+ boolCase True t e = t;
563+ boolCase False t e = e;
565+This function uses one of the ``t`` or ``e`` arguments, but not both (in
566+fact, this is used to implement the ``if...then...else`` construct as we
567+will see later. We would prefer if *only* the argument which was used
568+was evaluated. To achieve this, ``Idris`` provides a ``Lazy`` data type,
569+which allows evaluation to be suspended:
571+.. code-block:: idris
573+ data Lazy : Type -> Type where
574+ Delay : (val : a) -> Lazy a
578+A value of type ``Lazy a`` is unevaluated until it is forced by
579+``Force``. The ``Idris`` type checker knows about the ``Lazy`` type, and
580+inserts conversions where necessary between ``Lazy a`` and ``a``, and
581+vice versa. We can therefore write ``boolCase`` as follows, without any
582+explicit use of ``Force`` or ``Delay``:
584+.. code-block:: idris
586+ boolCase : Bool -> Lazy a -> Lazy a -> a;
587+ boolCase True t e = t;
588+ boolCase False t e = e;
593+``Idris`` includes a number of useful data types and library functions
594+(see the ``libs/`` directory in the distribution). This chapter
595+describes a few of these. The functions described here are imported
596+automatically by every ``Idris`` program, as part of ``Prelude.idr``.
598+``List`` and ``Vect``
599+~~~~~~~~~~~~~~~~~~~~~
601+We have already seen the ``List`` and ``Vect`` data types:
603+.. code-block:: idris
605+ data List a = Nil | (::) a (List a)
607+ data Vect : Nat -> Type -> Type where
609+ (::) : a -> Vect k a -> Vect (S k) a
611+Note that the constructor names are the same for each — constructor
612+names (in fact, names in general) can be overloaded, provided that they
613+are declared in different namespaces (see Section :ref:`sect-namespaces`),
614+and will typically be resolved according to their type. As syntactic
615+sugar, any type with the constructor names ``Nil`` and ``::`` can be
616+written in list form. For example:
618+- ``[]`` means ``Nil``
620+- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
622+The library also defines a number of functions for manipulating these
623+types. ``map`` is overloaded both for ``List`` and ``Vect`` and applies
624+a function to every element of the list or vector.
626+.. code-block:: idris
628+ map : (a -> b) -> List a -> List b
630+ map f (x :: xs) = f x :: map f xs
632+ map : (a -> b) -> Vect n a -> Vect n b
634+ map f (x :: xs) = f x :: map f xs
636+For example, given the following vector of integers, and a function to
639+.. code-block:: idris
642+ intVec = [1, 2, 3, 4, 5]
647+the function ``map`` can be used as follows to double every element in
652+ *usefultypes> show (map double intVec)
653+ "[2, 4, 6, 8, 10]" : String
655+You’ll find these examples in ``usefultypes.idr`` in the ``examples/``
656+directory. For more details of the functions available on ``List`` and
657+``Vect``, look in the library files:
659+- ``libs/prelude/Prelude/List.idr``
661+- ``libs/base/Data/List.idr``
663+- ``libs/base/Data/Vect.idr``
665+- ``libs/base/Data/VectType.idr``
667+Functions include filtering, appending, reversing, and so on. Also
668+remember that ``Idris`` is still in development, so if you don’t see the
669+function you need, please feel free to add it and submit a patch!
671+Aside: Anonymous functions and operator sections
672+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
674+There are actually neater ways to write the above expression. One way
675+would be to use an anonymous function:
679+ *usefultypes> show (map (\x => x * 2) intVec)
680+ "[2, 4, 6, 8, 10]" : String
682+The notation ``\x => val`` constructs an anonymous function which takes
683+one argument, ``x`` and returns the expression ``val``. Anonymous
684+functions may take several arguments, separated by commas,
685+e.g. \ ``\x, y, z => val``. Arguments may also be given explicit types,
686+e.g. \ ``\x : Int => x * 2``, and can pattern match,
687+e.g. \ ``\(x, y) => x + y``. We could also use an operator section:
691+ *usefultypes> show (map (* 2) intVec)
692+ "[2, 4, 6, 8, 10]" : String
694+``(*2)`` is shorthand for a function which multiplies a number by 2. It
695+expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand to
701+``Maybe`` describes an optional value. Either there is a value of the
702+given type, or there isn’t:
704+.. code-block:: idris
706+ data Maybe a = Just a | Nothing
708+``Maybe`` is one way of giving a type to an operation that may fail. For
709+example, looking something up in a ``List`` (rather than a vector) may
710+result in an out of bounds error:
712+.. code-block:: idris
714+ list_lookup : Nat -> List a -> Maybe a
715+ list_lookup _ Nil = Nothing
716+ list_lookup Z (x :: xs) = Just x
717+ list_lookup (S k) (x :: xs) = list_lookup k xs
719+The ``maybe`` function is used to process values of type ``Maybe``,
720+either by applying a function to the value, if there is one, or by
721+providing a default value:
723+.. code-block:: idris
725+ maybe : Lazy b -> (a -> b) -> Maybe a -> b
727+Note that the type of the first argument is ``Lazy b`` rather than
728+simply ``b``. Since the default value might not be used, we mark it as
729+``Lazy`` in case it is a large expression where evaluating it then
730+discarding it would be wasteful.
732+Tuples and Dependent Pairs
733+~~~~~~~~~~~~~~~~~~~~~~~~~~
735+Values can be paired with the following built-in data type:
737+.. code-block:: idris
739+ data Pair a b = MkPair a b
741+As syntactic sugar, we can write ``(a, b)`` which, according to context,
742+means either ``Pair a b`` or ``MkPair a b``. Tuples can contain an
743+arbitrary number of values, represented as nested pairs:
745+.. code-block:: idris
747+ fred : (String, Int)
750+ jim : (String, Int, String)
751+ jim = ("Jim", 25, "Cambridge")
756+Dependent pairs allow the type of the second element of a pair to depend
757+on the value of the first element. Traditionally, these are referred to
760+.. code-block:: idris
762+ data Sigma : (A : Type) -> (P : A -> Type) -> Type where
763+ MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
765+Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
766+of a pair of A and P, where the name ``a`` can occur inside ``P``.
767+``( a ** p )`` constructs a value of this type. For example, we can pair
768+a number with a ``Vect`` of a particular length.
770+.. code-block:: idris
772+ vec : (n : Nat ** Vect n Int)
775+If you like, you can write it out the long way, the two are precisely
778+.. code-block:: idris
780+ vec : Sigma Nat (\n => Vect n Int)
781+ vec = MkSigma 2 [3, 4]
783+The type checker could of course infer the value of the first element
784+from the length of the vector. We can write an underscore ``_`` in place
785+of values which we expect the type checker to fill in, so the above
786+definition could also be written as:
788+.. code-block:: idris
790+ vec : (n : Nat ** Vect n Int)
793+We might also prefer to omit the type of the first element of the pair,
794+since, again, it can be inferred:
796+.. code-block:: idris
798+ vec : (n ** Vect n Int)
801+One use for dependent pairs is to return values of dependent types where
802+the index is not necessarily known in advance. For example, if we filter
803+elements out of a ``Vect`` according to some predicate, we will not know
804+in advance what the length of the resulting vector will be:
806+.. code-block:: idris
808+ filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
810+If the ``Vect`` is empty, the result is easy:
812+.. code-block:: idris
814+ filter p Nil = (_ ** [])
816+In the ``::`` case, we need to inspect the result of a recursive call to
817+``filter`` to extract the length and the vector from the result. To do
818+this, we use ``with`` notation, which allows pattern matching on
821+.. code-block:: idris
823+ filter p (x :: xs) with (filter p xs)
824+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
826+We will see more on ``with`` notation later.
554More Expressions
828More Expressions
555----------------
829----------------
@@ -583,8 +857,6 @@ matching at the top level:
583 showPerson p = let MkPerson name age = p in
857 showPerson p = let MkPerson name age = p in
584 name ++ " is " ++ show age ++ " years old"
858 name ++ " is " ++ show age ++ " years old"
588List comprehensions
860List comprehensions
589~~~~~~~~~~~~~~~~~~~
861~~~~~~~~~~~~~~~~~~~