@@ -1,4 +1,4 @@
1−\section{Language Overview}
1+\section{Types and Functions}
22
33\subsection{Primitive Types}
44
@@ -174,6 +174,28 @@ efficiency. Fortunately, \Idris{} knows about the relationship between
174174\tTC{Nat} (and similarly structured types) and numbers, so optimises the
175175representation and functions such as \tFN{plus} and \tFN{mult}.
176176
177+\subsubsection*{\texttt{where} clauses}
178+
179+Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,
180+to define a function which reverses a list, we can use an auxiliary function which
181+accumulates the new, reversed list, and which does not need to be visible globally:
182+
183+\begin{SaveVerbatim}{revwhere}
184+
185+rev : List a -> List a;
186+rev xs = revAcc [] xs where {
187+ revAcc : List a -> List a -> List a;
188+ revAcc acc [] = acc;
189+ revAcc acc (x :: xs) = revAcc (x :: acc) xs;
190+}
191+
192+\end{SaveVerbatim}
193+\useverb{revwhere}
194+
195+\noindent
196+Any names which are visible in the outer scope are also visible in the \texttt{where}
197+clause (unless they have been redefined, such as \texttt{xs} here).
198+
177199\subsection{Dependent Types}
178200
179201\subsubsection{Vectors}
@@ -472,6 +494,8 @@ readFile : String -> IO String;
472494
473495\subsection{``\texttt{do}'' notation}
474496
497+\label{sect:do}
498+
475499I/O programs will typically need to sequence actions, feeding the output of one
476500computation into the input of the next. \texttt{IO} is an abstract type, however, so we
477501can't access the result of a computation directly. Instead, we sequence
@@ -509,8 +533,275 @@ overloaded.
509533
510534\subsection{Useful Data Types}
511535
512−Lists, syntactic sugar.
513−Maybe, Either.
514−Pairs, dependent pairs, syntactic sugar.
536+\Idris{} includes a number of useful data types and library functions (see the
537+\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
538+functions described here are imported automatically by every \Idris{} program, as
539+part of \texttt{prelude.idr}.
540+
541+\subsubsection{\texttt{List} and \texttt{Vect}}
542+
543+We have already seen the \texttt{List} and \texttt{Vect} data types:
544+
545+\begin{SaveVerbatim}{listvec}
546+
547+data List a = Nil | (::) a (List a);
548+
549+data Vect : Set -> Nat -> Set where
550+ Nil : Vect a O
551+ | (::) : a -> Vect a k -> Vect a (S k);
552+
553+\end{SaveVerbatim}
554+\useverb{listvec}
555+
556+Note that the constructor names are the same for each --- constructor names (in
557+fact, names in general) can be overloaded, provided that they are declared in
558+different namespaces (see Section \ref{sect:namespaces}), and will typically be
559+resolved according to their type. As syntactic sugar, any type with the constructor
560+names \texttt{Nil} and \texttt{::} can be written in list form. For example:
561+
562+\begin{itemize}
563+\item \texttt{[]} means \texttt{Nil}
564+\item \texttt{[1,2,3]} means \texttt{Cons 1 (Cons 2 (Cons 3 Nil))}
565+\end{itemize}
566+
567+The library also defines a number of functions for manipulating these types.
568+\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
569+and applies a function to every element of the list or vector.
570+
571+\begin{SaveVerbatim}{map}
572+
573+map : (a -> b) -> List a -> List b;
574+map f [] = [];
575+map f (x :: xs) = f x :: map f xs;
576+
577+map : (a -> b) -> Vect a n -> Vect b n;
578+map f [] = [];
579+map f (x :: xs) = f x :: map f xs;
580+
581+\end{SaveVerbatim}
582+\useverb{map}
583+
584+\noindent
585+For example, to double every element in a vector of integers:
586+
587+\begin{SaveVerbatim}{dvect}
588+
589+intVec : Vect Int 5;
590+intVec = [1, 2, 3, 4, 5];
591+
592+double : Int -> Int;
593+double x = x * 2;
594+
595+\end{SaveVerbatim}
596+\useverb{dvect}
597+
598+\noindent
599+You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
600+
601+\begin{SaveVerbatim}{rundvect}
602+
603+*usefultypes> show (map double intVec)
604+"[2, 4, 6, 8, 10]" : String
605+
606+\end{SaveVerbatim}
607+\useverb{rundvect}
608+
609+For more details of the functions available on \texttt{List} and \texttt{Vect},
610+look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
611+Functions include filtering, appending, reversing, and so on. Also remember
612+that \Idris{} is still in development, so if you don't see the function you
613+need, please feel free to add it and submit a patch!
614+
615+\subsubsection*{Aside: Anonymous functions and operator sections}
616+
617+There are actually neater ways to write the above expression. One way would be
618+to use an anonymous function:
619+
620+\begin{SaveVerbatim}{lam1}
621+
622+*usefultypes> show (map (\x => x * 2) intVec)
623+"[2, 4, 6, 8, 10]" : String
624+
625+\end{SaveVerbatim}
626+\useverb{lam1}
627+
628+The notation \texttt{$\backslash$x => val} constructs an anonymous function
629+which takes one argument, \texttt{x} and returns the expression \texttt{val}.
630+Anonymous functions may take several arguments, separated by commas, e.g.
631+\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
632+types, e.g. \texttt{$\backslash$x : Int => x * 2}.
633+
634+We could also use an operator section:
635+
636+\begin{SaveVerbatim}{sec1}
637+
638+*usefultypes> show (map (* 2) intVec)
639+"[2, 4, 6, 8, 10]" : String
640+
641+\end{SaveVerbatim}
642+\useverb{sec1}
643+
644+\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
645+\texttt{$\backslash$x => x * 2}.
646+Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
647+
648+\subsubsection{Maybe}
649+
650+\texttt{Maybe} describes an optional value. Either there is a value of the given type,
651+or there isn't:
652+
653+\begin{SaveVerbatim}{maybe}
654+
655+data Maybe a = Just a | Nothing;
656+
657+\end{SaveVerbatim}
658+\useverb{maybe}
659+
660+\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
661+looking something up in a \texttt{List} (rather than a vector) may result in an out of
662+bounds error:
663+
664+\begin{SaveVerbatim}{lookuplist}
515665
666+list_lookup : Nat -> List a -> Maybe a;
667+list_lookup _ Nil = Nothing;
668+list_lookup O (Cons x xs) = Just x;
669+list_lookup (S k) (Cons x xs) = list_lookup k xs;
670+
671+\end{SaveVerbatim}
672+\useverb{lookuplist}
673+
674+The \texttt{maybe} function is used to process values of type \texttt{Maybe},
675+either by applying a function to the value, if there is one, or by providing a default value:
676+
677+\begin{SaveVerbatim}{maybefn}
678+
679+maybe : Maybe a -> |(default:b) -> (a -> b) -> b;
680+
681+\end{SaveVerbatim}
682+\useverb{maybefn}
683+
684+The vertical bar $\mid$ before the default value is a laziness annotation. Normally
685+expressions are evaluated before being passed to a function. This is typically
686+the most efficient behaviour. However, in this case, the default value might
687+not be used and if it is a large expression, evaluating it will be wasteful.
688+The $\mid$ annotation tells the compiler not to evaluate the argument until it is
689+needed.
690+
691+\subsubsection{Tuples and Dependent Pairs}
692+
693+Values can be paired with the following built-in data type:
694+
695+\begin{SaveVerbatim}{mkpair}
696+
697+data Pair a b = MkPair a b;
698+
699+\end{SaveVerbatim}
700+\useverb{mkpair}
701+
702+As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
703+means either \texttt{Pair a b} or \texttt{MkPair a b}.
704+Tuples can contain an arbitrary number of values, represented as nested pairs:
705+
706+\begin{SaveVerbatim}{tuple}
707+
708+fred : (String, Int);
709+fred = ("Fred", 42);
710+
711+jim : (String, Int, String);
712+jim = ("Jim", 25, "Cambridge");
713+
714+\end{SaveVerbatim}
715+\useverb{tuple}
716+
717+\subsubsection*{Dependent Pairs}
718+
719+Dependent pairs allow the type of the second element of a pair to depend on
720+the value of the first element:
721+
722+\begin{SaveVerbatim}{sigma}
723+
724+data Exists : (A : Set) -> (P : A -> Set) -> Set where
725+ Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P;
726+
727+\end{SaveVerbatim}
728+\useverb{sigma}
729+
730+Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
731+A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p (}
732+constructs a value of this type. For example, we can pair a number with a
733+\texttt{Vect} of a particular length.
734+
735+\begin{SaveVerbatim}{dvec}
736+
737+vec : (n : Nat ** Vect Int n);
738+vec = (2 ** [3, 4]);
739+
740+\end{SaveVerbatim}
741+\useverb{dvec}
742+
743+\noindent
744+The type checker could of course infer the value of the first element from the
745+length of the vector. We can write an underscore \texttt{\_} in place of values which we
746+expect the type checker to fill in, so the above definition could also be
747+written as:
748+
749+\begin{SaveVerbatim}{dvec1}
750+
751+vec : (n : Nat ** Vect Int n);
752+vec = (_ ** [3, 4]);
753+
754+\end{SaveVerbatim}
755+\useverb{dvec1}
756+
757+\noindent
758+We might also prefer to omit the type of the first element of the pair, since,
759+again, it can be inferred:
760+
761+\begin{SaveVerbatim}{dvec2}
762+
763+vec : (n ** Vect Int n);
764+vec = (_ ** [3, 4]);
765+
766+\end{SaveVerbatim}
767+\useverb{dvec2}
768+
769+One use for dependent pairs is to return values of dependent types where the
770+index is not necessarily known in advance. For example, if we filter elements
771+out of a \texttt{Vect} according to some predicate, we will not know in advance what the
772+length of the resulting vector will be:
773+
774+\begin{SaveVerbatim}{vfilter}
775+
776+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
777+
778+\end{SaveVerbatim}
779+\useverb{vfilter}
780+
781+\noindent
782+If the \texttt{Vect} is empty, the result is easy:
783+
784+\begin{SaveVerbatim}{vfilternil}
785+
786+vfilter p VNil = (_ , []);
787+
788+\end{SaveVerbatim}
789+\useverb{vfilternil}
790+
791+In the \texttt{::} case, we need to inspect the result of a recursive call to
792+\texttt{filter} to
793+extract the length and the vector from the result. To do this, we use \texttt{with}
794+notation. with allows pattern matching on intermediate values:
795+
796+\begin{SaveVerbatim}{vfiltercons}
797+
798+filter p (x :: xs) with filter p xs {
799+ | (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs');
800+}
801+
802+\end{SaveVerbatim}
803+\useverb{vfiltercons}
804+
805+\noindent
806+We will see more on \texttt{with} notation later.
516807