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' : Vect a n' -> String
67 show' (x :: Nil) = show x
68 show' (x :: xs) = show x ++ ", " ++ show' xs
74\textbf{Remark: } The type of the auxiliary function \texttt{show'} is important. The type
75variables \texttt{a} and \texttt{n} which are part of the instance declaration for
76\texttt{Show (Vect a n)} are fixed across the entire instance declaration. As a result,
77we do not have to constrain \texttt{a} again. Furthermore, it means that if we use
78\texttt{n} in the type, it refers to the length of the outermost list \texttt{xs}. Therefore,
79we use a different name for the length \texttt{n'} in \texttt{show'}.
81\subsection{Default Definitions}
83The library defines an \texttt{Eq} class which provides an interface for comparing
84values for equality or inequality, with instances for all of the built-in types:
86\begin{SaveVerbatim}{eqbasic}
96To declare an instance of a type, we have to give definitions of all of the methods.
97For example, for an instance of \texttt{Eq} for \texttt{Nat}:
99\begin{SaveVerbatim}{eqnat}
103 (S x) == (S y) = x == y
107 x /= y = not (x == y)
113It is hard to imagine many cases where the \texttt{/=} method will be anything other
114than the negation of the result of applying the \texttt{==} method. It is therefore
115convenient to give a default definition for each method in the class
116declaration, in terms of the other method:
118\begin{SaveVerbatim}{eqdefault}
121 (==) : a -> a -> Bool
122 (/=) : a -> a -> Bool
124 x /= y = not (x == y)
125 y == y = not (x /= y)
131A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
132or \texttt{/=} to be defined, but does not require both. If a method definition is
133missing, and there is a default definition for it, then the default is used instead.
135\subsection{Extending Classes}
137Classes can also be extended. A logical next step from an equality relation \texttt{Eq}
138is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
139which inherits method from \texttt{Eq} as well as defining some of its own:
141\begin{SaveVerbatim}{ord}
143data Ordering = LT | EQ | GT
148\begin{SaveVerbatim}{eqord}
150class Eq a => Ord a where
151 compare : a -> a -> Ordering
155 (<=) : a -> a -> Bool
156 (>=) : a -> a -> Bool
164The \texttt{Ord} class allows us to compare two values and determine their ordering.
165Only the \texttt{compare} method is required; every other method has a default definition.
167this we can write functions such as \texttt{sort}, a function which sorts a list into
168increasing order, provided that the element type of the list is in the \texttt{Ord} class.
169We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
170function type to the right of the fat arrow:
172\begin{SaveVerbatim}{sortty}
174sort : Ord a => List a -> List a
180Functions, classes and instances can have multiple constraints. Multiple constaints are
181written in brackets in a comma separated list, for example:
183\begin{SaveVerbatim}{sortshow}
185sortAndShow : (Ord a, Show a) => List a -> String
186sortAndShow xs = show (sort xs)
191\subsection{Monads and \texttt{do}-notation}
195So far, we have seen single parameter type classes, where the parameter is of type
196\texttt{Set}. In general, there can be any number (greater than 0) of parameters,
197and the parameters can have \remph{any} type.
198If the type of the parameter is not \texttt{Set}, we need to give an explicit type
199declaration. For example:
201\begin{SaveVerbatim}{monad}
203class Monad (m : Set -> Set) where
205 (>>=) : m a -> (a -> m b) -> m b
211The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
212basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
213\texttt{do} block, the following syntactic transformations are applied:
216\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}
217\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}
218\item \texttt{let x = v; e} becomes \texttt{let x = v in e}
222\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
223We can also define an instance for \texttt{Maybe}, as follows:
225\begin{SaveVerbatim}{maybemonad}
227instance Monad Maybe where
230 Nothing >>= k = Nothing
237Using this we can, for example, define a function which adds two
238\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
240\begin{SaveVerbatim}{maybeadd}
242m_add : Maybe Int -> Maybe Int -> Maybe Int
243m_add x y = do x' <- x -- Extract value from x
244 y' <- y -- Extract value from y
245 return (x' + y') -- Add them
251This function will extract the values from \texttt{x} and \texttt{y}, if they
252are available, or return \texttt{Nothing} if they are not. Managing the
253\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
256\begin{SaveVerbatim}{maybeaddt}
258*classes> m_add (Just 20) (Just 22)
260*classes> m_add (Just 20) Nothing
266\subsubsection*{Monad comprehensions}
268The list comprehension notation we saw in Section \ref{sec:listcomp} is more
269general, and applies to anything which is an instance of \texttt{MonadPlus}:
271\begin{SaveVerbatim}{monadplus}
273class Monad m => MonadPlus (m : Set -> Set) where
274 mplus : m a -> m a -> m a
281In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
282\texttt{quali} can be one of:
285\item A generator \texttt{x <- e}
286\item A \emph{guard}, which is an expression of type \texttt{Bool}
287\item A let binding \texttt{let x = e}
291To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first
293\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
294the following function:
296\begin{SaveVerbatim}{guardq}
298guard : MonadPlus m => Bool -> m ()
304Then the comprehension is converted to \texttt{do} notation:
306\begin{SaveVerbatim}{comptrans}
308do { qual1; qual2; ...; qualn; return exp; }
314Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
316\begin{SaveVerbatim}{maddb}
318m_add : Maybe Int -> Maybe Int -> Maybe Int
319m_add x y = [ x' + y' | x' <- x, y' <- y ]
323\subsection{Idiom brackets}
325While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an
326alternative meaning to \emph{application}. The notation and larger example in this
327section is inspired by Conor McBride and Ross Paterson's paper "Applicative
328Programming with Effects"~\cite{idioms}.
330First, let us revisit \texttt{m\_add} above. All it is really doing is applying
331an operator to two values extracted from Maybe Ints. We could abstract out the
334\begin{SaveVerbatim}{mapp}
336m_app : Maybe (a -> b) -> Maybe a -> Maybe b
337m_app (Just f) (Just a) = Just (f a)
344Using this, we can write an alternative \texttt{m\_add} which uses this alternative
345notion of function application, with explicit calls to \texttt{m\_app}:
347\begin{SaveVerbatim}{maddb}
349m_add' : Maybe Int -> Maybe Int -> Maybe Int
350m_add' x y = m_app (m_app (Just (+)) x) y
356Rather than having to insert \texttt{m\_app} everywhere there is an application, we can
357use \remph{idiom brackets} to do the job for us. To do this, we use the \texttt{Applicative}
358class, which captures the notion of application for a data type:
360\begin{SaveVerbatim}{applicative}
364class Applicative (f : Set -> Set) where
366 (<$>) : f (a -> b) -> f a -> f b
372\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where \texttt{<\$>}
373is defined in the same way as \texttt{m\_app} above:
375\begin{SaveVerbatim}{maybeapp}
377instance Applicative Maybe where
380 (Just f) <$> (Just a) = Just (f a)
387Using \remph{idiom brackets} we can use this instance as follows, where a function
388application \texttt{[| f a1 ... an |]}
389is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
391\begin{SaveVerbatim}{maddc}
393m_add' : Maybe Int -> Maybe Int -> Maybe Int
394m_add' x y = [| x + y |]
399\subsubsection{An error-handling interpreter}
401Idiom notation is commonly useful when defining evaluators. McBride and
402Paterson describe such an evaluator~\cite{idioms}, for a language similar to
405\begin{SaveVerbatim}{idiomexpr}
407data Expr = Var String -- variables
409 | Add Expr Expr -- addition
415Evaluation will take place relative to a context mapping variables (represented as
416\texttt{String}s) to integer values, and can possibly fail. We define a data type
417\texttt{Eval} to wrap an evaluator:
419\begin{SaveVerbatim}{evalctxt}
421data Eval : Set -> Set where
422 MkEval : (List (String, Int) -> Maybe a) -> Eval a
428Wrapping the evaluator in a data type means we will be able to make it an instance
429of a type class later. We begin by defining a function to retrieve values from
430the context during evaluation:
432\begin{SaveVerbatim}{fetch}
434fetch : String -> Eval Int
435fetch x = MkEval (\e => fetchVal e) where
436 fetchVal : List (String, Int) -> Maybe Int
437 fetchVal [] = Nothing
438 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
444When defining an evaluator for the language, we will be applying functions in the
445context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an instance
446of \texttt{Applicative}:
448\begin{SaveVerbatim}{}
450instance Applicative Eval where
451 pure x = MkEval (\e => Just x)
453 (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
454 app : Maybe (a -> b) -> Maybe a -> Maybe b
455 app (Just fx) (Just gx) = Just (fx gx)
461\begin{SaveVerbatim}{grr}
466Evaluating an expression can now make use of the idiomatic application to handle
469\begin{SaveVerbatim}{evalexpr}
471eval : Expr -> Eval Int
472eval (Var x) = fetch x
473eval (Val x) = [| x |]
474eval (Add x y) = [| eval x + eval y |]
476runEval : List (String, Int) -> Expr -> Maybe Int
477runEval env e = case eval e of
478 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