@@ -1,5 +1,3 @@
1−.. _sect-typesfuns:
2−
31===================
42Types and Functions
53===================
@@ -190,7 +188,7 @@ indented further than the outer function.
190188visible in the ``where`` clause (unless they have been redefined, such
191189as ``xs`` here). A name which appears only in the type will be in scope
192190in 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.
194192
195193As well as functions, ``where`` blocks can include local data
196194declarations, such as the following where ``MyLT`` is not accessible
@@ -549,7 +547,283 @@ us to inject a value directly into an IO operation:
549547As we will see later, ``do`` notation is more general than this, and can
550548be overloaded.
551549
552−.. _sect-more-expr:
550+.. _sect-lazy:
551+
552+Laziness
553+--------
554+
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:
558+
559+.. code-block:: idris
560+
561+ boolCase : Bool -> a -> a -> a;
562+ boolCase True t e = t;
563+ boolCase False t e = e;
564+
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:
570+
571+.. code-block:: idris
572+
573+ data Lazy : Type -> Type where
574+ Delay : (val : a) -> Lazy a
575+
576+ Force : Lazy a -> a
577+
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``:
583+
584+.. code-block:: idris
585+
586+ boolCase : Bool -> Lazy a -> Lazy a -> a;
587+ boolCase True t e = t;
588+ boolCase False t e = e;
589+
590+Useful Data Types
591+-----------------
592+
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``.
597+
598+``List`` and ``Vect``
599+~~~~~~~~~~~~~~~~~~~~~
600+
601+We have already seen the ``List`` and ``Vect`` data types:
602+
603+.. code-block:: idris
604+
605+ data List a = Nil | (::) a (List a)
606+
607+ data Vect : Nat -> Type -> Type where
608+ Nil : Vect Z a
609+ (::) : a -> Vect k a -> Vect (S k) a
610+
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:
617+
618+- ``[]`` means ``Nil``
619+
620+- ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
621+
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.
625+
626+.. code-block:: idris
627+
628+ map : (a -> b) -> List a -> List b
629+ map f [] = []
630+ map f (x :: xs) = f x :: map f xs
631+
632+ map : (a -> b) -> Vect n a -> Vect n b
633+ map f [] = []
634+ map f (x :: xs) = f x :: map f xs
635+
636+For example, given the following vector of integers, and a function to
637+double an integer:
638+
639+.. code-block:: idris
640+
641+ intVec : Vect 5 Int
642+ intVec = [1, 2, 3, 4, 5]
643+
644+ double : Int -> Int
645+ double x = x * 2
646+
647+the function ``map`` can be used as follows to double every element in
648+the vector:
649+
650+::
651+
652+ *usefultypes> show (map double intVec)
653+ "[2, 4, 6, 8, 10]" : String
654+
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:
658+
659+- ``libs/prelude/Prelude/List.idr``
660+
661+- ``libs/base/Data/List.idr``
662+
663+- ``libs/base/Data/Vect.idr``
664+
665+- ``libs/base/Data/VectType.idr``
666+
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!
670+
671+Aside: Anonymous functions and operator sections
672+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
673+
674+There are actually neater ways to write the above expression. One way
675+would be to use an anonymous function:
676+
677+::
678+
679+ *usefultypes> show (map (\x => x * 2) intVec)
680+ "[2, 4, 6, 8, 10]" : String
681+
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:
688+
689+::
690+
691+ *usefultypes> show (map (* 2) intVec)
692+ "[2, 4, 6, 8, 10]" : String
693+
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
696+``\x => 2 * x``.
697+
698+Maybe
699+~~~~~
700+
701+``Maybe`` describes an optional value. Either there is a value of the
702+given type, or there isn’t:
703+
704+.. code-block:: idris
705+
706+ data Maybe a = Just a | Nothing
707+
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:
711+
712+.. code-block:: idris
713+
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
718+
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:
722+
723+.. code-block:: idris
724+
725+ maybe : Lazy b -> (a -> b) -> Maybe a -> b
726+
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.
731+
732+Tuples and Dependent Pairs
733+~~~~~~~~~~~~~~~~~~~~~~~~~~
734+
735+Values can be paired with the following built-in data type:
736+
737+.. code-block:: idris
738+
739+ data Pair a b = MkPair a b
740+
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:
744+
745+.. code-block:: idris
746+
747+ fred : (String, Int)
748+ fred = ("Fred", 42)
749+
750+ jim : (String, Int, String)
751+ jim = ("Jim", 25, "Cambridge")
752+
753+Dependent Pairs
754+~~~~~~~~~~~~~~~
755+
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
758+as “sigma types”:
759+
760+.. code-block:: idris
761+
762+ data Sigma : (A : Type) -> (P : A -> Type) -> Type where
763+ MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
764+
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.
769+
770+.. code-block:: idris
771+
772+ vec : (n : Nat ** Vect n Int)
773+ vec = (2 ** [3, 4])
774+
775+If you like, you can write it out the long way, the two are precisely
776+equivalent.
777+
778+.. code-block:: idris
779+
780+ vec : Sigma Nat (\n => Vect n Int)
781+ vec = MkSigma 2 [3, 4]
782+
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:
787+
788+.. code-block:: idris
789+
790+ vec : (n : Nat ** Vect n Int)
791+ vec = (_ ** [3, 4])
792+
793+We might also prefer to omit the type of the first element of the pair,
794+since, again, it can be inferred:
795+
796+.. code-block:: idris
797+
798+ vec : (n ** Vect n Int)
799+ vec = (_ ** [3, 4])
800+
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:
805+
806+.. code-block:: idris
807+
808+ filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
809+
810+If the ``Vect`` is empty, the result is easy:
811+
812+.. code-block:: idris
813+
814+ filter p Nil = (_ ** [])
815+
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
819+intermediate values:
820+
821+.. code-block:: idris
822+
823+ filter p (x :: xs) with (filter p xs)
824+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
825+
826+We will see more on ``with`` notation later.
553827
554828More Expressions
555829----------------
@@ -583,8 +857,6 @@ matching at the top level:
583857 showPerson p = let MkPerson name age = p in
584858 name ++ " is " ++ show age ++ " years old"
585859
586−
587−
588860List comprehensions
589861~~~~~~~~~~~~~~~~~~~
590862