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)))
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
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
67 show' (x :: Nil) = show x
68 show' (x :: xs) = show x ++ ", " ++ show' xs
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}
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}
95 (S x) == (S y) = x == y
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}
113 (==) : a -> a -> Bool
114 (/=) : a -> a -> Bool
116 x /= y = not (x == y)
117 y == y = not (x /= y)
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
140\begin{SaveVerbatim}{eqord}
142class Eq a => Ord a where
143 compare : a -> a -> Ordering
147 (<=) : a -> a -> Bool
148 (>=) : a -> a -> Bool
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.
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
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)
183\subsection{Monads and \texttt{do}-notation}
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
197 (>>=) : m a -> (a -> m b) -> m b
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:
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}
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
222 Nothing >>= k = Nothing
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
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
248\begin{SaveVerbatim}{maybeaddt}
250*classes> m_add (Just 20) (Just 22)
252*classes> m_add (Just 20) Nothing
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
273In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
274\texttt{quali} can be one of:
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}
283To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first
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 ()
296Then the comprehension is converted to \texttt{do} notation:
298\begin{SaveVerbatim}{comptrans}
300do { qual1; qual2; ...; qualn; return exp; }
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 ]
315\subsection{Idiom brackets}
317While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an
318alternative meaning to \emph{application}. The notation and larger example in this
319section is inspired by Conor McBride and Ross Paterson's paper "Applicative
320Programming with Effects"~\cite{idioms}.
322First, let us revisit \texttt{m\_add} above. All it is really doing is applying
323an operator to two values extracted from Maybe Ints. We could abstract out the
326\begin{SaveVerbatim}{mapp}
328m_app : Maybe (a -> b) -> Maybe a -> Maybe b
329m_app (Just f) (Just a) = Just (f a)
336Using this, we can write an alternative \texttt{m\_add} which uses this alternative
337notion of function application, with explicit calls to \texttt{m\_app}:
339\begin{SaveVerbatim}{maddb}
341m_add' : Maybe Int -> Maybe Int -> Maybe Int
342m_add' x y = m_app (m_app (Just (+)) x) y
348Rather than having to insert \texttt{m\_app} everywhere there is an application, we can
349use \remph{idiom brackets} to do the job for us. To do this, we use the \texttt{Applicative}
350class, which captures the notion of application for a data type:
352\begin{SaveVerbatim}{applicative}
356class Applicative (f : Set -> Set) where
358 (<$>) : f (a -> b) -> f a -> f b
364\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where \texttt{<\$>}
365is defined in the same way as \texttt{m\_app} above:
367\begin{SaveVerbatim}{maybeapp}
369instance Applicative Maybe where
372 (Just f) <$> (Just a) = Just (f a)
379Using \remph{idiom brackets} we can use this instance as follows, where a function
380application \texttt{[| f a1 ... an |]}
381is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
383\begin{SaveVerbatim}{maddc}
385m_add' : Maybe Int -> Maybe Int -> Maybe Int
386m_add' x y = [| x + y |]
391\subsubsection{An error-handling interpreter}
393Idiom notation is commonly useful when defining evaluators. McBride and
394Paterson describe such an evaluator~\cite{idioms}, for a language similar to
397\begin{SaveVerbatim}{idiomexpr}
399data Expr = Var String -- variables
401 | Add Expr Expr -- addition
407Evaluation will take place relative to a context mapping variables (represented as
408\texttt{String}s) to integer values, and can possibly fail. We define a data type
409\texttt{Eval} to wrap an evaluator:
411\begin{SaveVerbatim}{evalctxt}
413data Eval : Set -> Set where
414 MkEval : (List (String, Int) -> Maybe a) -> Eval a
420Wrapping the evaluator in a data type means we will be able to make it an instance
421of a type class later. We begin by defining a function to retrieve values from
422the context during evaluation:
424\begin{SaveVerbatim}{fetch}
426fetch : String -> Eval Int
427fetch x = MkEval (\e => fetchVal e) where
428 fetchVal : List (String, Int) -> Maybe Int
429 fetchVal [] = Nothing
430 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
436When defining an evaluator for the language, we will be applying functions in the
437context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an instance
438of \texttt{Applicative}:
440\begin{SaveVerbatim}{}
442instance Applicative Eval where
443 pure x = MkEval (\e => Just x)
445 (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
446 app : Maybe (a -> b) -> Maybe a -> Maybe b
447 app (Just fx) (Just gx) = Just (fx gx)
453\begin{SaveVerbatim}{grr}
458Evaluating an expression can now make use of the idiomatic application to handle
461\begin{SaveVerbatim}{evalexpr}
463eval : Expr -> Eval Int
464eval (Var x) = fetch x
465eval (Val x) = [| x |]
466eval (Add x y) = [| eval x + eval y |]
468runEval : List (String, Int) -> Expr -> Maybe Int
469runEval env e = case eval e of
470 MkEval envFn => envFn env
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