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
17\begin{SaveVerbatim}{showclass}
26This generates a function of the following type (which we call a \emph{method} of the
29\begin{SaveVerbatim}{showty}
31show : Show a => a -> String
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}
43\begin{SaveVerbatim}{shownat}
45instance Show Nat where
47 show (S k) = "s" ++ show k
49Idris> show (S (S (S O)))
56Only one instance of a class can be given for a type --- instances may not overlap.
57Instance 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}
59instance for the element type, because we are going to use it to convert each element
62\begin{SaveVerbatim}{showvec}
64instance Show a => Show (Vect a n) where
65 show xs = "[" ++ show' xs ++ "]" where
66 show' : Vect a n -> String
68 show' (x :: Nil) = show x
69 show' (x :: xs) = show x ++ ", " ++ show' xs
75%\textbf{Remark: } The type of the auxiliary function \texttt{show'} is
76%important. The type variables \texttt{a} and \texttt{n} which are part of the
77%instance declaration for \texttt{Show (Vect a n)} are fixed across the entire
78%instance declaration. As a result, we do not have to constrain \texttt{a}
79%again. Furthermore, it means that if we use \texttt{n} in the type, it refers
80%to the (fixed) length of the outermost list \texttt{xs}. Therefore,
81%we use a different name for the length \texttt{n'} in \texttt{show'}.
83\subsection{Default Definitions}
85The library defines an \texttt{Eq} class which provides an interface for comparing
86values for equality or inequality, with instances for all of the built-in types:
88\begin{SaveVerbatim}{eqbasic}
98To declare an instance of a type, we have to give definitions of all of the methods.
99For example, for an instance of \texttt{Eq} for \texttt{Nat}:
101\begin{SaveVerbatim}{eqnat}
105 (S x) == (S y) = x == y
109 x /= y = not (x == y)
115It is hard to imagine many cases where the \texttt{/=} method will be anything other
116than the negation of the result of applying the \texttt{==} method. It is therefore
117convenient to give a default definition for each method in the class
118declaration, in terms of the other method:
120\begin{SaveVerbatim}{eqdefault}
123 (==) : a -> a -> Bool
124 (/=) : a -> a -> Bool
126 x /= y = not (x == y)
127 y == y = not (x /= y)
133A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
134or \texttt{/=} to be defined, but does not require both. If a method definition is
135missing, and there is a default definition for it, then the default is used instead.
137\subsection{Extending Classes}
139Classes can also be extended. A logical next step from an equality relation \texttt{Eq}
140is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
141which inherits methods from \texttt{Eq} as well as defining some of its own:
143\begin{SaveVerbatim}{ord}
145data Ordering = LT | EQ | GT
150\begin{SaveVerbatim}{eqord}
152class Eq a => Ord a where
153 compare : a -> a -> Ordering
157 (<=) : a -> a -> Bool
158 (>=) : a -> a -> Bool
166The \texttt{Ord} class allows us to compare two values and determine their ordering.
167Only the \texttt{compare} method is required; every other method has a default definition.
169this we can write functions such as \texttt{sort}, a function which sorts a list into
170increasing order, provided that the element type of the list is in the \texttt{Ord} class.
171We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
172function type to the right of the fat arrow:
174\begin{SaveVerbatim}{sortty}
176sort : Ord a => List a -> List a
182Functions, classes and instances can have multiple constraints. Multiple constaints are
183written in brackets in a comma separated list, for example:
185\begin{SaveVerbatim}{sortshow}
187sortAndShow : (Ord a, Show a) => List a -> String
188sortAndShow xs = show (sort xs)
193\subsection{Monads and \texttt{do}-notation}
197So far, we have seen single parameter type classes, where the parameter is of type
198\texttt{Type}. In general, there can be any number (greater than 0) of parameters,
199and the parameters can have \remph{any} type.
200If the type of the parameter is not \texttt{Type}, we need to give an explicit type
201declaration. For example:
203\begin{SaveVerbatim}{monad}
205class Monad (m : Type -> Type) where
207 (>>=) : m a -> (a -> m b) -> m b
213The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
214basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
215\texttt{do} block, the following syntactic transformations are applied:
218\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}
219\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}
220\item \texttt{let x = v; e} becomes \texttt{let x = v in e}
224\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
225We can also define an instance for \texttt{Maybe}, as follows:
227\begin{SaveVerbatim}{maybemonad}
229instance Monad Maybe where
232 Nothing >>= k = Nothing
239Using this we can, for example, define a function which adds two
240\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
242\begin{SaveVerbatim}{maybeadd}
244m_add : Maybe Int -> Maybe Int -> Maybe Int
245m_add x y = do x' <- x -- Extract value from x
246 y' <- y -- Extract value from y
247 return (x' + y') -- Add them
253This function will extract the values from \texttt{x} and \texttt{y}, if they
254are available, or return \texttt{Nothing} if they are not. Managing the
255\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
258\begin{SaveVerbatim}{maybeaddt}
260*classes> m_add (Just 20) (Just 22)
262*classes> m_add (Just 20) Nothing
268\subsubsection*{Monad comprehensions}
270The list comprehension notation we saw in Section \ref{sec:listcomp} is more
271general, and applies to anything which is an instance of \texttt{MonadPlus}:
273\begin{SaveVerbatim}{monadplus}
275class Monad m => MonadPlus (m : Type -> Type) where
276 mplus : m a -> m a -> m a
283In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
284\texttt{quali} can be one of:
287\item A generator \texttt{x <- e}
288\item A \emph{guard}, which is an expression of type \texttt{Bool}
289\item A let binding \texttt{let x = e}
293To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first
295\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
296the following function:
298\begin{SaveVerbatim}{guardq}
300guard : MonadPlus m => Bool -> m ()
306Then the comprehension is converted to \texttt{do} notation:
308\begin{SaveVerbatim}{comptrans}
310do { qual1; qual2; ...; qualn; return exp; }
316Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
318\begin{SaveVerbatim}{maddb}
320m_add : Maybe Int -> Maybe Int -> Maybe Int
321m_add x y = [ x' + y' | x' <- x, y' <- y ]
325\subsection{Idiom brackets}
327While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an
328alternative meaning to \emph{application}. The notation and larger example in this
329section is inspired by Conor McBride and Ross Paterson's paper "Applicative
330Programming with Effects"~\cite{idioms}.
332First, let us revisit \texttt{m\_add} above. All it is really doing is applying
333an operator to two values extracted from Maybe Ints. We could abstract out the
336\begin{SaveVerbatim}{mapp}
338m_app : Maybe (a -> b) -> Maybe a -> Maybe b
339m_app (Just f) (Just a) = Just (f a)
346Using this, we can write an alternative \texttt{m\_add} which uses this alternative
347notion of function application, with explicit calls to \texttt{m\_app}:
349\begin{SaveVerbatim}{maddb}
351m_add' : Maybe Int -> Maybe Int -> Maybe Int
352m_add' x y = m_app (m_app (Just (+)) x) y
358Rather than having to insert \texttt{m\_app} everywhere there is an
359application, we can use \remph{idiom brackets} to do the job for us. To do
360this, we use the \texttt{Applicative} class, which captures the notion of
361application for a data type:
363\begin{SaveVerbatim}{applicative}
367class Applicative (f : Type -> Type) where
369 (<$>) : f (a -> b) -> f a -> f b
375\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where
376\texttt{<\$>} is defined in the same way as \texttt{m\_app} above:
378\begin{SaveVerbatim}{maybeapp}
380instance Applicative Maybe where
383 (Just f) <$> (Just a) = Just (f a)
390Using \remph{idiom brackets} we can use this instance as follows, where a function
391application \texttt{[| f a1 ... an |]}
392is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
394\begin{SaveVerbatim}{maddc}
396m_add' : Maybe Int -> Maybe Int -> Maybe Int
397m_add' x y = [| x + y |]
402\subsubsection{An error-handling interpreter}
404Idiom notation is commonly useful when defining evaluators. McBride and
405Paterson describe such an evaluator~\cite{idioms}, for a language similar to
408\begin{SaveVerbatim}{idiomexpr}
410data Expr = Var String -- variables
412 | Add Expr Expr -- addition
418Evaluation will take place relative to a context mapping variables (represented as
419\texttt{String}s) to integer values, and can possibly fail. We define a data type
420\texttt{Eval} to wrap an evaluator:
422\begin{SaveVerbatim}{evalctxt}
424data Eval : Type -> Type where
425 MkEval : (List (String, Int) -> Maybe a) -> Eval a
431Wrapping the evaluator in a data type means we will be able to make it an instance
432of a type class later. We begin by defining a function to retrieve values from
433the context during evaluation:
435\begin{SaveVerbatim}{fetch}
437fetch : String -> Eval Int
438fetch x = MkEval (\e => fetchVal e) where
439 fetchVal : List (String, Int) -> Maybe Int
440 fetchVal [] = Nothing
441 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
447When defining an evaluator for the language, we will be applying functions in
448the context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an
449instance of \texttt{Applicative}.
450Before \texttt{Eval} can be an instance of
451\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of
454\begin{SaveVerbatim}{}
456instance Functor Eval where
457 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
459instance Applicative Eval where
460 pure x = MkEval (\e => Just x)
462 (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
463 app : Maybe (a -> b) -> Maybe a -> Maybe b
464 app (Just fx) (Just gx) = Just (fx gx)
470\begin{SaveVerbatim}{grr}
475Evaluating an expression can now make use of the idiomatic application to handle
478\begin{SaveVerbatim}{evalexpr}
480eval : Expr -> Eval Int
481eval (Var x) = fetch x
482eval (Val x) = [| x |]
483eval (Add x y) = [| eval x + eval y |]
485runEval : List (String, Int) -> Expr -> Maybe Int
486runEval env e = case eval e of
487 MkEval envFn => envFn env
492\subsection{Named Instances}
494It can be desirable to have multiple instances of a type class, for example to provide
495alternative methods for sorting or printing values. To achieve this, instances can
496be \remph{named} as follows:
498\begin{SaveVerbatim}{myord}
500instance [myord] Ord Nat where
504 compare (S x) (S y) = compare @{myord} x y
510This declares an instance as normal, but with an explicit name, \texttt{myord}.
511The syntax \texttt{compare @\{myord\}} gives an explicit instance to
512\texttt{compare}, otherwise it would use the default instance for \texttt{Nat}.
513We can use this, for example, to sort a list of \texttt{Nat}s in reverse.
514Given the following list:
516\begin{SaveVerbatim}{myordlist}
525\ldots we can sort it using the default \texttt{Ord} instance, then the named
526instance \texttt{myord} as follows, at the \Idris{} prompt:
528\begin{SaveVerbatim}{myordlistrun}
530*named_instance> show (sort testList)
531"[sO, sssO, ssssO]" : String
532*named_instance> show (sort @{myord} testList)
533"[ssssO, sssO, sO]" : String
536\useverb{myordlistrun}
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list