git.iko.soy/Idris-dev
on fc6eb53 help sign in
Idris-dev/tutorial/classes.tex
315 lines 8.9 kB history raw
1\section{Type Classes}
2\label{sec:classes}
4We often want to define functions which work across several different data
5types. 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
8display different types in a uniform way.
10To 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
12operations which describe the interface for \emph{instances} of that class. A simple example
13is the \texttt{Show} type class, which is defined in the prelude and
14provides an interface for converting values to
15\texttt{String}s:
17\begin{SaveVerbatim}{showclass}
19class Show a where
20 show : a -> String
22\end{SaveVerbatim}
23\useverb{showclass}
25\noindent
26This generates a function of the following type (which we call a \emph{method} of the
27\texttt{Show} class):
29\begin{SaveVerbatim}{showty}
31show : Show a => a -> String
33\end{SaveVerbatim}
34\useverb{showty}
36\noindent
37We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},
38take an \texttt{a} as input and return a \texttt{String}.'' An instance of a class
39is defined with an \texttt{instance} declaration, which provides implementations of
40the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}
41could be defined as:
43\begin{SaveVerbatim}{shownat}
45instance Show Nat where
46 show O = "O"
47 show (S k) = "s" ++ show k
49Idris> show (S (S (S O)))
50"sssO" : String
52\end{SaveVerbatim}
53\useverb{shownat}
55\noindent
56Instance declarations can themselves have constraints. For example, to define a
57\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}
58instance for the element type, because we are going to use it to convert each element
59to a \texttt{String}:
61\begin{SaveVerbatim}{showvec}
63instance Show a => Show (Vect a n) where
64 show xs = "[" ++ show' xs ++ "]" where
65 show' : Show a => Vect a n -> String
66 show' Nil = ""
67 show' (x :: Nil) = show x
68 show' (x :: xs) = show x ++ ", " ++ show' xs
70\end{SaveVerbatim}
71\useverb{showvec}
73\subsection{Default Definitions}
75The library defines an \texttt{Eq} class which provides an interface for comparing
76values for equality or inequality, with instances for all of the built-in types:
78\begin{SaveVerbatim}{eqbasic}
80class Eq a where
81 (==) : a -> a -> Bool
82 (/=) : a -> a -> Bool
84\end{SaveVerbatim}
85\useverb{eqbasic}
87\noindent
88To declare an instance of a type, we have to give definitions of all of the methods.
89For example, for an instance of \texttt{Eq} for \texttt{Nat}:
91\begin{SaveVerbatim}{eqnat}
93instance Eq Nat where
94 O == O = True
95 (S x) == (S y) = x == y
96 O == (S y) = False
97 (S x) == O = False
99 x /= y = not (x == y)
101\end{SaveVerbatim}
102\useverb{eqnat}
104\noindent
105It is hard to imagine many cases where the \texttt{/=} method will be anything other
106than the negation of the result of applying the \texttt{==} method. It is therefore
107convenient to give a default definition for each method in the class
108declaration, in terms of the other method:
110\begin{SaveVerbatim}{eqdefault}
112class Eq a where
113 (==) : a -> a -> Bool
114 (/=) : a -> a -> Bool
116 x /= y = not (x == y)
117 y == y = not (x /= y)
119\end{SaveVerbatim}
120\useverb{eqdefault}
122\noindent
123A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
124or \texttt{/=} to be defined, but does not require both. If a method definition is
125missing, and there is a default definition for it, then the default is used instead.
127\subsection{Extending Classes}
129Classes can also be extended. A logical next step from an equality relation \texttt{Eq}
130is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
131which inherits method from \texttt{Eq} as well as defining some of its own:
133\begin{SaveVerbatim}{ord}
135data Ordering = LT | EQ | GT
137\end{SaveVerbatim}
138\useverb{ord}
140\begin{SaveVerbatim}{eqord}
142class Eq a => Ord a where
143 compare : a -> a -> Ordering
145 (<) : a -> a -> Bool
146 (>) : a -> a -> Bool
147 (<=) : a -> a -> Bool
148 (>=) : a -> a -> Bool
149 max : a -> a -> a
150 min : a -> a -> a
152\end{SaveVerbatim}
153\useverb{eqord}
155\noindent
156The \texttt{Ord} class allows us to compare two values and determine their ordering.
157Only the \texttt{compare} method is required; every other method has a default definition.
158Using
159this we can write functions such as \texttt{sort}, a function which sorts a list into
160increasing order, provided that the element type of the list is in the \texttt{Ord} class.
161We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
162function type to the right of the fat arrow:
164\begin{SaveVerbatim}{sortty}
166sort : Ord a => List a -> List a
168\end{SaveVerbatim}
169\useverb{sortty}
171\noindent
172Functions, classes and instances can have multiple constraints. Multiple constaints are
173written in brackets in a comma separated list, for example:
175\begin{SaveVerbatim}{sortshow}
177sortAndShow : (Ord a, Show a) => List a -> String
178sortAndShow xs = show (sort xs)
180\end{SaveVerbatim}
181\useverb{sortshow}
183\subsection{Monads and \texttt{do}-notation}
185\label{sec:monad}
187So far, we have seen single parameter type classes, where the parameter is of type
188\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
189and the parameters can have \remph{any} type.
190If the type of the parameter is not \texttt{Set}, we need to give an explicit type
191declaration. For example:
193\begin{SaveVerbatim}{monad}
195class Monad (m : Set -> Set) where
196 return : a -> m a
197 (>>=) : m a -> (a -> m b) -> m b
199\end{SaveVerbatim}
200\useverb{monad}
202\noindent
203The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
204basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
205\texttt{do} block, the following syntactic transformations are applied:
207\begin{itemize}
208\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}
209\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}
210\item \texttt{let x = v; e} becomes \texttt{let x = v in e}
211\end{itemize}
213\noindent
214\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
215We can also define an instance for \texttt{Maybe}, as follows:
217\begin{SaveVerbatim}{maybemonad}
219instance Monad Maybe where
220 return = Just
222 Nothing >>= k = Nothing
223 (Just x) >>= k = k x
225\end{SaveVerbatim}
226\useverb{maybemonad}
228\noindent
229Using this we can, for example, define a function which adds two
230\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
232\begin{SaveVerbatim}{maybeadd}
234m_add : Maybe Int -> Maybe Int -> Maybe Int
235m_add x y = do x' <- x -- Extract value from x
236 y' <- y -- Extract value from y
237 return (x' + y') -- Add them
239\end{SaveVerbatim}
240\useverb{maybeadd}
242\noindent
243This function will extract the values from \texttt{x} and \texttt{y}, if they
244are available, or return \texttt{Nothing} if they are not. Managing the
245\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
246\texttt{do} notation.
248\begin{SaveVerbatim}{maybeaddt}
250*classes> m_add (Just 20) (Just 22)
251Just 42 : Maybe Int
252*classes> m_add (Just 20) Nothing
253Nothing : Maybe Int
255\end{SaveVerbatim}
256\useverb{maybeaddt}
258\subsubsection*{Monad comprehensions}
260The list comprehension notation we saw in Section \ref{sec:listcomp} is more
261general, and applies to anything which is an instance of \texttt{MonadPlus}:
263\begin{SaveVerbatim}{monadplus}
265class Monad m => MonadPlus (m : Set -> Set) where
266 mplus : m a -> m a -> m a
267 mzero : m a
269\end{SaveVerbatim}
270\useverb{monadplus}
272\noindent
273In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
274\texttt{quali} can be one of:
276\begin{itemize}
277\item A generator \texttt{x <- e}
278\item A \emph{guard}, which is an expression of type \texttt{Bool}
279\item A let binding \texttt{let x = e}
280\end{itemize}
282\noindent
283To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first
284any qualifier
285\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
286the following function:
288\begin{SaveVerbatim}{guardq}
290guard : MonadPlus m => Bool -> m ()
292\end{SaveVerbatim}
293\useverb{guardq}
295\noindent
296Then the comprehension is converted to \texttt{do} notation:
298\begin{SaveVerbatim}{comptrans}
300do { qual1; qual2; ...; qualn; return exp; }
302\end{SaveVerbatim}
303\useverb{comptrans}
305\noindent
306Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
308\begin{SaveVerbatim}{maddb}
310m_add : Maybe Int -> Maybe Int -> Maybe Int
311m_add x y = [ x' + y' | x' <- x, y' <- y ]
312\end{SaveVerbatim}
313\useverb{maddb}