git.iko.soy/Idris-dev
on master help sign in
More tutorial: useful types, type classes
c154f5cEdwin Brady
lib/builtins.idr+2−2
compare with master
unifiedsplit
@@ -94,8 +94,8 @@ class Eq a where {
94 (==) : a -> a -> Bool;
94 (==) : a -> a -> Bool;
95 (/=) : a -> a -> Bool;
95 (/=) : a -> a -> Bool;
96
96
97− (/=) x y = not (x == y);
97+ x /= y = not (x == y);
98− (==) x y = not (x /= y);
98+ x == y = not (x /= y);
99}
99}
100
100
101instance Eq Int where {
101instance Eq Int where {
lib/prelude/vect.idr+1−1
@@ -32,7 +32,7 @@ app (x :: xs) ys = x :: app xs ys;
32
32
33filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
33filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
34filter p [] = ( _ ** [] );
34filter p [] = ( _ ** [] );
35−filter p (x :: xs) with (filter p xs) {
35+filter p (x :: xs) with filter p xs {
36 | ( _ ** xs' )
36 | ( _ ** xs' )
37 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
37 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
38}
38}
tutorial/Makefile+2−1
@@ -2,7 +2,8 @@ PAPER = idris-tutorial
2
2
3all: ${PAPER}.pdf
3all: ${PAPER}.pdf
4
4
5−TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex
5+TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \
6+ classes.tex modules.tex
6
7
7DIAGS =
8DIAGS =
8
9
tutorial/classes.tex+239
@@ -1,3 +1,242 @@
1\section{Type Classes}
1\section{Type Classes}
2\label{sec:classes}
2\label{sec:classes}
3
3
4+We often want to define functions which work across several different data
5+types. For example, we would like arithmetic operators to work on \texttt{Int},
6+\texttt{Integer} and \texttt{Float} at the very least. We would like
7+\texttt{==} to work on the majority of data types. We would like to be able to
8+display different types in a uniform way.
9+
10+To achieve this, we use a feature which has proved to be effective in Haskell, namely
11+\emph{type classes}. To define a type class, we provide a collection of overloaded
12+operations which describe the interface for \emph{instances} of that class. A simple example
13+is the \texttt{Show} type class, which is defined in the prelude and
14+provides an interface for converting values to
15+\texttt{String}s:
16+
17+\begin{SaveVerbatim}{showclass}
18+
19+class Show a where {
20+ show : a -> String;
21+}
22+
23+\end{SaveVerbatim}
24+\useverb{showclass}
25+
26+\noindent
27+This generates a function of the following type (which we call a \emph{method} of the
28+\texttt{Show} class):
29+
30+\begin{SaveVerbatim}{showty}
31+
32+show : Show a => a -> String;
33+
34+\end{SaveVerbatim}
35+\useverb{showty}
36+
37+\noindent
38+We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},
39+take an \texttt{a} as input and return a \texttt{String}.'' An instance of a class
40+is defined with an \texttt{instance} declaration, which provides implementations of
41+the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}
42+could be defined as:
43+
44+\begin{SaveVerbatim}{shownat}
45+
46+instance Show Nat where {
47+ show O = "O";
48+ show (S k) = "s" ++ show k;
49+}
50+
51+Idris> show (S (S (S O)))
52+"sssO" : String
53+
54+\end{SaveVerbatim}
55+\useverb{shownat}
56+
57+Instance declarations can themselves have constraints. For example, to define a
58+\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}
59+instance for the element type, because we are going to use it to convert each element
60+to a \texttt{String}:
61+
62+\begin{SaveVerbatim}{showvec}
63+
64+instance Show a => Show (Vect a n) where {
65+ show xs = "[" ++ show' xs ++ "]" where {
66+ show' : Show a => Vect a n -> String;
67+ show' VNil = "";
68+ show' (x :: VNil) = show x;
69+ show' (x :: xs) = show x ++ ", " ++ show' xs;
70+ }
71+}
72+
73+\end{SaveVerbatim}
74+\useverb{showvec}
75+
76+\subsection{Default Definitions}
77+
78+The library defines an \texttt{Eq} class which provides an interface for comparing
79+values for equality or inequality, with instances for all of the built-in types:
80+
81+\begin{SaveVerbatim}{eqbasic}
82+
83+class Eq a where {
84+ (==) : a -> a -> Bool;
85+ (/=) : a -> a -> Bool;
86+}
87+
88+\end{SaveVerbatim}
89+\useverb{eqbasic}
90+
91+\noindent
92+To declare an instance of a type, we have to give definitions of all of the methods.
93+For example, for an instance of \texttt{Eq} for \texttt{Nat}:
94+
95+\begin{SaveVerbatim}{eqnat}
96+
97+instance Eq Nat where {
98+ O == O = True;
99+ (S x) == (S y) = x == y;
100+ O == (S y) = False;
101+ (S x) == O = False;
102+
103+ x /= y = not (x == y);
104+}
105+
106+\end{SaveVerbatim}
107+\useverb{eqnat}
108+
109+\noindent
110+It is hard to imagine many cases where the \texttt{/=} method will be anything other
111+than the negation of the result of applying the \texttt{==} method. It is therefore
112+convenient to give a default definition for each method in the class
113+declaration, in terms of the other method:
114+
115+\begin{SaveVerbatim}{eqdefault}
116+
117+class Eq a where {
118+ (==) : a -> a -> Bool;
119+ (/=) : a -> a -> Bool;
120+
121+ x /= y = not (x == y);
122+ y == y = not (x /= y);
123+}
124+
125+\end{SaveVerbatim}
126+\useverb{eqdefault}
127+
128+\noindent
129+A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
130+or \texttt{/=} to be defined, but does not require both. If a method definition is
131+missing, and there is a default definition for it, then the default is used instead.
132+
133+\subsection{Extending Classes}
134+
135+Classes can also be extended. A logical next step from an equality relation \texttt{Eq}
136+is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
137+which inherits method from \texttt{Eq} as well as defining some of its own:
138+
139+\begin{SaveVerbatim}{ord}
140+
141+data Ordering = LT | EQ | GT;
142+
143+class Eq a => Ord a where {
144+ compare : a -> a -> Ordering;
145+
146+ (<) : a -> a -> Bool;
147+ (>) : a -> a -> Bool;
148+ (<=) : a -> a -> Bool;
149+ (>=) : a -> a -> Bool;
150+ max : a -> a -> a;
151+ min : a -> a -> a;
152+}
153+
154+\end{SaveVerbatim}
155+\useverb{ord}
156+
157+The \texttt{Ord} class allows us to compare two values and determine their ordering.
158+Only the \texttt{compare} method is required; every other method has a default definition.
159+Using
160+this we can write functions such as \texttt{sort}, a function which sorts a list into
161+increasing order, provided that the element type of the list is in the \texttt{Ord} class:
162+
163+\begin{SaveVerbatim}{sortty}
164+
165+sort : Ord a => List a -> List a;
166+
167+\end{SaveVerbatim}
168+
169+\subsection{Monads and \texttt{do}-notation}
170+
171+So far, we have seen single parameter type classes, where the parameter is of type
172+\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
173+and the parameters can have \remph{any} type.
174+If the type of the parameter is not \texttt{Set}, we need to give an explicit type
175+declaration. For example:
176+
177+\begin{SaveVerbatim}{monad}
178+
179+class Monad (m : Set -> Set) where {
180+ return : a -> m a;
181+ (>>=) : m a -> (a -> m b) -> m b;
182+}
183+
184+\end{SaveVerbatim}
185+\useverb{monad}
186+
187+The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
188+basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
189+\texttt{do} block, the following syntactic transformations are applied:
190+
191+\begin{itemize}
192+\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}
193+\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}
194+\item \texttt{let x = v; e} becomes \texttt{let x = v in e}
195+\end{itemize}
196+
197+\noindent
198+\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
199+We can also define an instance for \texttt{Maybe}, as follows:
200+
201+\begin{SaveVerbatim}{maybemonad}
202+
203+instance Monad Maybe where {
204+ return = Just;
205+
206+ Nothing >>= k = Nothing;
207+ (Just x) >>= k = k x;
208+}
209+
210+\end{SaveVerbatim}
211+\useverb{maybemonad}
212+
213+\noindent
214+Using this we can, for example, define a function which adds two
215+\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
216+
217+\begin{SaveVerbatim}{maybeadd}
218+
219+m_add : Maybe Int -> Maybe Int -> Maybe Int;
220+m_add x y = do { x' <- x; -- Extract value from x
221+ y' <- y; -- Extract value from y
222+ return (x' + y'); -- Add them
223+ };
224+
225+\end{SaveVerbatim}
226+\useverb{maybeadd}
227+
228+\noindent
229+This function will extract the values from \texttt{x} and \texttt{y}, if they
230+are available, or return \texttt{Nothing} if they are not. Managing the
231+\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
232+\texttt{do} notation.
233+
234+\begin{SaveVerbatim}{maybeaddt}
235+
236+*classes> m_add (Just 20) (Just 22)
237+Just 42 : Maybe Int
238+*classes> m_add (Just 20) Nothing
239+Nothing : Maybe Int
240+
241+\end{SaveVerbatim}
242+\useverb{maybeaddt}
tutorial/examples/classes.idrnew file+5
@@ -0,0 +1,5 @@
1+m_add : Maybe Int -> Maybe Int -> Maybe Int;
2+m_add x y = do { x' <- x; -- Extract value from x
3+ y' <- y; -- Extract value from y
4+ return (x' + y'); -- Add them
5+ };
tutorial/examples/usefultypes.idrnew file+9
@@ -0,0 +1,9 @@
1+
2+intVec : Vect Int 5;
3+intVec = [1, 2, 3, 4, 5];
4+
5+double : Int -> Int;
6+double x = x * 2;
7+
8+vec : (n ** Vect Int n);
9+vec = (_ ** [3, 4]);
tutorial/idris-tutorial.tex+1−1
@@ -23,10 +23,10 @@
23\input{starting}
23\input{starting}
24\input{typesfuns}
24\input{typesfuns}
25\input{classes}
25\input{classes}
26+\input{modules}
26
27
27%Planned sections
28%Planned sections
28
29
29−\section{Modules and Namespaces}
30\section{Example: The Well-Typed Interpreter}
30\section{Example: The Well-Typed Interpreter}
31\section{Views}
31\section{Views}
32\section{Theorem Proving}
32\section{Theorem Proving}
tutorial/intro.tex+7
@@ -54,3 +54,10 @@ OCaml. In particular, a certain amount of familiarity with Haskell syntax is
54assumed, although most concepts will at least be explained briefly. The reader
54assumed, although most concepts will at least be explained briefly. The reader
55is also assumed to have some interest in using dependent types for writing and
55is also assumed to have some interest in using dependent types for writing and
56verifying systems software.
56verifying systems software.
57+
58+\subsection{Example Code}
59+
60+This tutorial includes some example code. The files are available in the \Idris{} distribution,
61+so that you can try them out easily,
62+under \texttt{idris-tutorial/examples}. However, it is strongly recommended that you
63+type them in yourself, rather than simply loading and reading them.
tutorial/modules.texnew file+4
@@ -0,0 +1,4 @@
1+\section{Modules and Namespaces}
2+\label{sect:namespaces}
3+
4+
tutorial/typesfuns.tex+295−4
@@ -1,4 +1,4 @@
1−\section{Language Overview}
1+\section{Types and Functions}
2
2
3\subsection{Primitive Types}
3\subsection{Primitive Types}
4
4
@@ -174,6 +174,28 @@ efficiency. Fortunately, \Idris{} knows about the relationship between
174\tTC{Nat} (and similarly structured types) and numbers, so optimises the
174\tTC{Nat} (and similarly structured types) and numbers, so optimises the
175representation and functions such as \tFN{plus} and \tFN{mult}.
175representation and functions such as \tFN{plus} and \tFN{mult}.
176
176
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+
177\subsection{Dependent Types}
199\subsection{Dependent Types}
178
200
179\subsubsection{Vectors}
201\subsubsection{Vectors}
@@ -472,6 +494,8 @@ readFile : String -> IO String;
472
494
473\subsection{``\texttt{do}'' notation}
495\subsection{``\texttt{do}'' notation}
474
496
497+\label{sect:do}
498+
475I/O programs will typically need to sequence actions, feeding the output of one
499I/O programs will typically need to sequence actions, feeding the output of one
476computation into the input of the next. \texttt{IO} is an abstract type, however, so we
500computation into the input of the next. \texttt{IO} is an abstract type, however, so we
477can't access the result of a computation directly. Instead, we sequence
501can't access the result of a computation directly. Instead, we sequence
@@ -509,8 +533,275 @@ overloaded.
509
533
510\subsection{Useful Data Types}
534\subsection{Useful Data Types}
511
535
512−Lists, syntactic sugar.
536+\Idris{} includes a number of useful data types and library functions (see the
513−Maybe, Either.
537+\texttt{lib/} directory in the distribution). This chapter describes a few of these. The
514−Pairs, dependent pairs, syntactic sugar.
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}
515
665
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.
516
807