More tutorial: useful types, type classes

lib/builtins.idr

@@ -94,8 +94,8 @@ class Eq a where {
     (==) : a -> a -> Bool;
     (/=) : a -> a -> Bool;
 
-    (/=) x y = not (x == y);
-    (==) x y = not (x /= y);
+    x /= y = not (x == y);
+    x == y = not (x /= y);
 }
 
 instance Eq Int where {

lib/prelude/vect.idr

@@ -32,7 +32,7 @@ app (x :: xs) ys = x :: app xs ys;
 
 filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
 filter p [] = ( _ ** [] );
-filter p (x :: xs) with (filter p xs) {
+filter p (x :: xs) with filter p xs {
   | ( _ ** xs' ) 
      = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
 }

tutorial/Makefile

@@ -2,7 +2,8 @@ PAPER = idris-tutorial
 
 all: ${PAPER}.pdf
 
-TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex
+TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \
+           classes.tex modules.tex
 
 DIAGS = 
 

tutorial/classes.tex

@@ -1,3 +1,242 @@
 \section{Type Classes}
 \label{sec:classes}
 
+We often want to define functions which work across several different data
+types. For example, we would like arithmetic operators to work on \texttt{Int},
+\texttt{Integer} and \texttt{Float} at the very least. We would like
+\texttt{==} to work on the majority of data types. We would like to be able to
+display different types in a uniform way.
+
+To achieve this, we use a feature which has proved to be effective in Haskell, namely
+\emph{type classes}. To define a type class, we provide a collection of overloaded
+operations which describe the interface for \emph{instances} of that class. A simple example
+is the \texttt{Show} type class, which is defined in the prelude and
+provides an interface for converting values to
+\texttt{String}s:
+
+\begin{SaveVerbatim}{showclass}
+
+class Show a where {
+    show : a -> String;
+}
+
+\end{SaveVerbatim}
+\useverb{showclass}
+
+\noindent
+This generates a function of the following type (which we call a \emph{method} of the 
+\texttt{Show} class):
+
+\begin{SaveVerbatim}{showty}
+
+show : Show a => a -> String;
+
+\end{SaveVerbatim}
+\useverb{showty}
+
+\noindent
+We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},
+take an \texttt{a} as input and return a \texttt{String}.'' An instance of a class
+is defined with an \texttt{instance} declaration, which provides implementations of
+the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}
+could be defined as:
+
+\begin{SaveVerbatim}{shownat}
+
+instance Show Nat where {
+    show O = "O";
+    show (S k) = "s" ++ show k;
+}
+
+Idris> show (S (S (S O))) 
+"sssO" : String
+
+\end{SaveVerbatim}
+\useverb{shownat}
+
+Instance declarations can themselves have constraints. For example, to define a
+\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show} 
+instance for the element type, because we are going to use it to convert each element
+to a \texttt{String}:
+
+\begin{SaveVerbatim}{showvec}
+
+instance Show a => Show (Vect a n) where {
+    show xs = "[" ++ show' xs ++ "]" where {
+        show' : Show a => Vect a n -> String;
+        show' VNil = "";
+        show' (x :: VNil) = show x;
+        show' (x :: xs) = show x ++ ", " ++ show' xs;
+    }
+}
+
+\end{SaveVerbatim}
+\useverb{showvec}
+
+\subsection{Default Definitions}
+
+The library defines an \texttt{Eq} class which provides an interface for comparing
+values for equality or inequality, with instances for all of the built-in types:
+
+\begin{SaveVerbatim}{eqbasic}
+
+class Eq a where {
+    (==) : a -> a -> Bool;
+    (/=) : a -> a -> Bool;
+}
+
+\end{SaveVerbatim}
+\useverb{eqbasic}
+
+\noindent
+To declare an instance of a type, we have to give definitions of all of the methods.
+For example, for an instance of \texttt{Eq} for \texttt{Nat}:
+
+\begin{SaveVerbatim}{eqnat}
+
+instance Eq Nat where {
+    O     == O     = True;
+    (S x) == (S y) = x == y;
+    O     == (S y) = False;
+    (S x) == O     = False;
+
+    x /= y = not (x == y);
+}
+
+\end{SaveVerbatim}
+\useverb{eqnat}
+
+\noindent
+It is hard to imagine many cases where the \texttt{/=} method will be anything other
+than the negation of the result of applying the \texttt{==} method. It is therefore
+convenient to give a default definition for each method in the class
+declaration, in terms of the other method:
+
+\begin{SaveVerbatim}{eqdefault}
+
+class Eq a where {
+    (==) : a -> a -> Bool;
+    (/=) : a -> a -> Bool;
+
+    x /= y = not (x == y);
+    y == y = not (x /= y);
+}
+
+\end{SaveVerbatim}
+\useverb{eqdefault}
+
+\noindent
+A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
+or \texttt{/=} to be defined, but does not require both. If a method definition is
+missing, and there is a default definition for it, then the default is used instead.
+
+\subsection{Extending Classes}
+
+Classes can also be extended. A logical next step from an equality relation \texttt{Eq}
+is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
+which inherits method from \texttt{Eq} as well as defining some of its own:
+
+\begin{SaveVerbatim}{ord}
+
+data Ordering = LT | EQ | GT;
+
+class Eq a => Ord a where {
+    compare : a -> a -> Ordering;
+
+    (<) : a -> a -> Bool;
+    (>) : a -> a -> Bool;
+    (<=) : a -> a -> Bool;
+    (>=) : a -> a -> Bool;
+    max : a -> a -> a;
+    min : a -> a -> a;
+}
+
+\end{SaveVerbatim}
+\useverb{ord}
+
+The \texttt{Ord} class allows us to compare two values and determine their ordering. 
+Only the \texttt{compare} method is required; every other method has a default definition.
+Using
+this we can write functions such as \texttt{sort}, a function which sorts a list into
+increasing order, provided that the element type of the list is in the \texttt{Ord} class:
+
+\begin{SaveVerbatim}{sortty}
+
+sort : Ord a => List a -> List a;
+
+\end{SaveVerbatim}
+
+\subsection{Monads and \texttt{do}-notation}
+
+So far, we have seen single parameter type classes, where the parameter is of type
+\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
+and the parameters can have \remph{any} type.
+If the type of the parameter is not \texttt{Set}, we need to give an explicit type
+declaration. For example:
+
+\begin{SaveVerbatim}{monad}
+
+class Monad (m : Set -> Set) where {
+    return : a -> m a;
+    (>>=)  : m a -> (a -> m b) -> m b;
+}
+
+\end{SaveVerbatim}
+\useverb{monad}
+
+The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
+basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
+\texttt{do} block, the following syntactic transformations are applied:
+
+\begin{itemize}
+\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}
+\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}
+\item \texttt{let x = v; e} becomes \texttt{let x = v in e}
+\end{itemize}
+
+\noindent
+\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
+We can also define an instance for \texttt{Maybe}, as follows:
+
+\begin{SaveVerbatim}{maybemonad}
+
+instance Monad Maybe where {
+    return = Just;
+
+    Nothing  >>= k = Nothing;
+    (Just x) >>= k = k x;
+}
+
+\end{SaveVerbatim}
+\useverb{maybemonad}
+
+\noindent
+Using this we can, for example, define a function which adds two 
+\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
+
+\begin{SaveVerbatim}{maybeadd}
+
+m_add : Maybe Int -> Maybe Int -> Maybe Int;
+m_add x y = do { x' <- x; -- Extract value from x
+                 y' <- y; -- Extract value from y
+                 return (x' + y'); -- Add them 
+               };
+
+\end{SaveVerbatim}
+\useverb{maybeadd}
+
+\noindent
+This function will extract the values from \texttt{x} and \texttt{y}, if they
+are available, or return \texttt{Nothing} if they are not. Managing the
+\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
+\texttt{do} notation.
+
+\begin{SaveVerbatim}{maybeaddt}
+
+*classes> m_add (Just 20) (Just 22) 
+Just 42 : Maybe Int
+*classes> m_add (Just 20) Nothing 
+Nothing : Maybe Int
+
+\end{SaveVerbatim}
+\useverb{maybeaddt}

tutorial/examples/classes.idr

@@ -0,0 +1,5 @@
+m_add : Maybe Int -> Maybe Int -> Maybe Int;
+m_add x y = do { x' <- x; -- Extract value from x
+                 y' <- y; -- Extract value from y
+                 return (x' + y'); -- Add them 
+               };

tutorial/examples/usefultypes.idr

@@ -0,0 +1,9 @@
+
+intVec : Vect Int 5;
+intVec = [1, 2, 3, 4, 5];
+
+double : Int -> Int;
+double x = x * 2;
+
+vec : (n ** Vect Int n);
+vec = (_ ** [3, 4]);

tutorial/idris-tutorial.tex

@@ -23,10 +23,10 @@
 \input{starting}
 \input{typesfuns}
 \input{classes}
+\input{modules}
 
 %Planned sections
 
-\section{Modules and Namespaces}
 \section{Example: The Well-Typed Interpreter}
 \section{Views}
 \section{Theorem Proving}

tutorial/intro.tex

@@ -54,3 +54,10 @@ OCaml. In particular, a certain amount of familiarity with Haskell syntax is
 assumed, although most concepts will at least be explained briefly.  The reader
 is also assumed to have some interest in using dependent types for writing and
 verifying systems software.
+
+\subsection{Example Code}
+
+This tutorial includes some example code. The files are available in the \Idris{} distribution,
+so that you can try them out easily,
+under \texttt{idris-tutorial/examples}. However, it is strongly recommended that you
+type them in yourself, rather than simply loading and reading them.

tutorial/modules.tex

@@ -0,0 +1,4 @@
+\section{Modules and Namespaces}
+\label{sect:namespaces}
+
+

tutorial/typesfuns.tex

@@ -1,4 +1,4 @@
-\section{Language Overview}
+\section{Types and Functions}
 
 \subsection{Primitive Types}
 
@@ -174,6 +174,28 @@ efficiency. Fortunately, \Idris{} knows about the relationship between
 \tTC{Nat} (and similarly structured types) and numbers, so optimises the
 representation and functions such as \tFN{plus} and \tFN{mult}.
 
+\subsubsection*{\texttt{where} clauses}
+
+Functions can also be defined \emph{locally} using \texttt{where} clauses. For example,
+to define a function which reverses a list, we can use an auxiliary function which
+accumulates the new, reversed list, and which does not need to be visible globally:
+
+\begin{SaveVerbatim}{revwhere}
+
+rev : List a -> List a;
+rev xs = revAcc [] xs where {
+  revAcc : List a -> List a -> List a;
+  revAcc acc [] = acc;
+  revAcc acc (x :: xs) = revAcc (x :: acc) xs;
+}
+
+\end{SaveVerbatim}
+\useverb{revwhere}
+
+\noindent
+Any names which are visible in the outer scope are also visible in the \texttt{where}
+clause (unless they have been redefined, such as \texttt{xs} here).
+
 \subsection{Dependent Types}
 
 \subsubsection{Vectors}
@@ -472,6 +494,8 @@ readFile : String -> IO String;
 
 \subsection{``\texttt{do}'' notation}
 
+\label{sect:do}
+
 I/O programs will typically need to sequence actions, feeding the output of one
 computation into the input of the next. \texttt{IO} is an abstract type, however, so we
 can't access the result of a computation directly. Instead, we sequence
@@ -509,8 +533,275 @@ overloaded.
 
 \subsection{Useful Data Types}
 
-Lists, syntactic sugar.
-Maybe, Either.
-Pairs, dependent pairs, syntactic sugar.
+\Idris{} includes a number of useful data types and library functions (see the
+\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
+functions described here are imported automatically by every \Idris{} program, as
+part of \texttt{prelude.idr}.
 
+\subsubsection{\texttt{List} and \texttt{Vect}}
+
+We have already seen the \texttt{List} and \texttt{Vect} data types:
+
+\begin{SaveVerbatim}{listvec}
+
+data List a = Nil | (::) a (List a);
+
+data Vect : Set -> Nat -> Set where
+   Nil  : Vect a O
+ | (::) : a -> Vect a k -> Vect a (S k);
+
+\end{SaveVerbatim}
+\useverb{listvec}
+
+Note that the constructor names are the same for each --- constructor names (in
+fact, names in general) can be overloaded, provided that they are declared in
+different namespaces (see Section \ref{sect:namespaces}), and will typically be
+resolved according to their type. As syntactic sugar, any type with the constructor
+names \texttt{Nil} and \texttt{::} can be written in list form. For example:
+
+\begin{itemize}
+\item \texttt{[]} means \texttt{Nil}
+\item \texttt{[1,2,3]} means \texttt{Cons 1 (Cons 2 (Cons 3 Nil))}
+\end{itemize}
+
+The library also defines a number of functions for manipulating these types.
+\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}
+and applies a function to every element of the list or vector.
+
+\begin{SaveVerbatim}{map}
+
+map : (a -> b) -> List a -> List b;
+map f []        = [];
+map f (x :: xs) = f x :: map f xs;
+
+map : (a -> b) -> Vect a n -> Vect b n;
+map f []        = [];
+map f (x :: xs) = f x :: map f xs;
+
+\end{SaveVerbatim}
+\useverb{map}
+
+\noindent
+For example, to double every element in a vector of integers:
+
+\begin{SaveVerbatim}{dvect}
+
+intVec : Vect Int 5;
+intVec = [1, 2, 3, 4, 5];
+
+double : Int -> Int;
+double x = x * 2;
+
+\end{SaveVerbatim}
+\useverb{dvect}
+
+\noindent
+You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/} directory:
+
+\begin{SaveVerbatim}{rundvect}
+
+*usefultypes> show (map double intVec) 
+"[2, 4, 6, 8, 10]" : String
+
+\end{SaveVerbatim}
+\useverb{rundvect}
+
+For more details of the functions available on \texttt{List} and \texttt{Vect},
+look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.
+Functions include filtering, appending, reversing, and so on. Also remember
+that \Idris{} is still in development, so if you don't see the function you
+need, please feel free to add it and submit a patch!
+
+\subsubsection*{Aside: Anonymous functions and operator sections}
+
+There are actually neater ways to write the above expression. One way would be
+to use an anonymous function:
+
+\begin{SaveVerbatim}{lam1}
+
+*usefultypes> show (map (\x => x * 2) intVec)
+"[2, 4, 6, 8, 10]" : String
+
+\end{SaveVerbatim}
+\useverb{lam1}
+
+The notation \texttt{$\backslash$x => val} constructs an anonymous function
+which takes one argument, \texttt{x} and returns the expression \texttt{val}.
+Anonymous functions may take several arguments, separated by commas, e.g.
+\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit
+types, e.g. \texttt{$\backslash$x : Int => x * 2}.
+
+We could also use an operator section:
+
+\begin{SaveVerbatim}{sec1}
+
+*usefultypes> show (map (* 2) intVec)
+"[2, 4, 6, 8, 10]" : String
+
+\end{SaveVerbatim}
+\useverb{sec1}
+
+\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to
+\texttt{$\backslash$x => x * 2}. 
+Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.
+
+\subsubsection{Maybe}
+
+\texttt{Maybe} describes an optional value. Either there is a value of the given type,
+or there isn't:
+
+\begin{SaveVerbatim}{maybe}
+
+data Maybe a = Just a | Nothing;
+
+\end{SaveVerbatim}
+\useverb{maybe}
+
+\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,
+looking something up in a \texttt{List} (rather than a vector) may result in an out of
+bounds error:
+
+\begin{SaveVerbatim}{lookuplist}
+
+list_lookup : Nat -> List a -> Maybe a;
+list_lookup _     Nil         = Nothing;
+list_lookup O     (Cons x xs) = Just x;
+list_lookup (S k) (Cons x xs) = list_lookup k xs;
+
+\end{SaveVerbatim}
+\useverb{lookuplist}
+
+The \texttt{maybe} function is used to process values of type \texttt{Maybe}, 
+either by applying a function to the value, if there is one, or by providing a default value:
+
+\begin{SaveVerbatim}{maybefn}
+
+maybe : Maybe a -> |(default:b) -> (a -> b) -> b;
+
+\end{SaveVerbatim}
+\useverb{maybefn}
+
+The vertical bar $\mid$ before the default value is a laziness annotation. Normally
+expressions are evaluated before being passed to a function. This is typically
+the most efficient behaviour. However, in this case, the default value might
+not be used and if it is a large expression, evaluating it will be wasteful.
+The $\mid$ annotation tells the compiler not to evaluate the argument until it is
+needed.
+
+\subsubsection{Tuples and Dependent Pairs}
+
+Values can be paired with the following built-in data type:
+
+\begin{SaveVerbatim}{mkpair}
+
+data Pair a b = MkPair a b;
+
+\end{SaveVerbatim}
+\useverb{mkpair}
+
+As syntactic sugar, we can write \texttt{(a, b)} which, according to context,
+means either \texttt{Pair a b} or \texttt{MkPair a b}.
+Tuples can contain an arbitrary number of values, represented as nested pairs:
+
+\begin{SaveVerbatim}{tuple}
+
+fred : (String, Int);
+fred = ("Fred", 42);
+
+jim : (String, Int, String);
+jim = ("Jim", 25, "Cambridge");
+
+\end{SaveVerbatim}
+\useverb{tuple}
+
+\subsubsection*{Dependent Pairs}
+
+Dependent pairs allow the type of the second element of a pair to depend on
+the value of the first element:
+
+\begin{SaveVerbatim}{sigma}
+
+data Exists : (A : Set) -> (P : A -> Set) -> Set where
+   Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P;
+
+\end{SaveVerbatim}
+\useverb{sigma}
+
+Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of
+A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p (} 
+constructs a value of this type. For example, we can pair a number with a 
+\texttt{Vect} of a particular length.
+
+\begin{SaveVerbatim}{dvec}
+
+vec : (n : Nat ** Vect Int n);
+vec = (2 ** [3, 4]);
+
+\end{SaveVerbatim}
+\useverb{dvec}
+
+\noindent
+The type checker could of course infer the value of the first element from the
+length of the vector. We can write an underscore \texttt{\_} in place of values which we
+expect the type checker to fill in, so the above definition could also be
+written as:
+
+\begin{SaveVerbatim}{dvec1}
+
+vec : (n : Nat ** Vect Int n);
+vec = (_ ** [3, 4]);
+
+\end{SaveVerbatim}
+\useverb{dvec1}
+
+\noindent
+We might also prefer to omit the type of the first element of the pair, since,
+again, it can be inferred:
+
+\begin{SaveVerbatim}{dvec2}
+
+vec : (n ** Vect Int n);
+vec = (_ ** [3, 4]);
+
+\end{SaveVerbatim}
+\useverb{dvec2}
+
+One use for dependent pairs is to return values of dependent types where the
+index is not necessarily known in advance. For example, if we filter elements
+out of a \texttt{Vect} according to some predicate, we will not know in advance what the
+length of the resulting vector will be:
+
+\begin{SaveVerbatim}{vfilter}
+
+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
+
+\end{SaveVerbatim}
+\useverb{vfilter}
+
+\noindent
+If the \texttt{Vect} is empty, the result is easy:
+
+\begin{SaveVerbatim}{vfilternil}
+
+vfilter p VNil = (_ , []);
+
+\end{SaveVerbatim}
+\useverb{vfilternil}
+
+In the \texttt{::} case, we need to inspect the result of a recursive call to 
+\texttt{filter} to
+extract the length and the vector from the result. To do this, we use \texttt{with}
+notation. with allows pattern matching on intermediate values:
+
+\begin{SaveVerbatim}{vfiltercons}
+
+filter p (x :: xs) with filter p xs {
+   | (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs');
+}
+
+\end{SaveVerbatim}
+\useverb{vfiltercons}
+
+\noindent
+We will see more on \texttt{with} notation later.