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
23This generates a function of the following type (which we call a \emph{method} of the
27show : Show a => a -> String
31We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},
32take an \texttt{a} as input and return a \texttt{String}.'' An instance of a class
33is defined with an \texttt{instance} declaration, which provides implementations of
34the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}
38instance Show Nat where
40 show (S k) = "s" ++ show k
44Idris> show (S (S (S Z)))
49Only one instance of a class can be given for a type --- instances may not overlap.
50Instance declarations can themselves have constraints. For example, to define a
51\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}
52instance for the element type, because we are going to use it to convert each element
56instance Show a => Show (Vect n a) where
57 show xs = "[" ++ show' xs ++ "]" where
58 show' : Vect n a -> String
60 show' (x :: Nil) = show x
61 show' (x :: xs) = show x ++ ", " ++ show' xs
65%\textbf{Remark: } The type of the auxiliary function \texttt{show'} is
66%important. The type variables \texttt{a} and \texttt{n} which are part of the
67%instance declaration for \texttt{Show (Vect a n)} are fixed across the entire
68%instance declaration. As a result, we do not have to constrain \texttt{a}
69%again. Furthermore, it means that if we use \texttt{n} in the type, it refers
70%to the (fixed) length of the outermost list \texttt{xs}. Therefore,
71%we use a different name for the length \texttt{n'} in \texttt{show'}.
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:
85To declare an instance of a type, we have to give definitions of all of the methods.
86For example, for an instance of \texttt{Eq} for \texttt{Nat}:
91 (S x) == (S y) = x == y
99It is hard to imagine many cases where the \texttt{/=} method will be anything other
100than the negation of the result of applying the \texttt{==} method. It is therefore
101convenient to give a default definition for each method in the class
102declaration, in terms of the other method:
106 (==) : a -> a -> Bool
107 (/=) : a -> a -> Bool
109 x /= y = not (x == y)
110 y == y = not (x /= y)
114A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}
115or \texttt{/=} to be defined, but does not require both. If a method definition is
116missing, and there is a default definition for it, then the default is used instead.
118\subsection{Extending Classes}
120Classes can also be extended. A logical next step from an equality relation \texttt{Eq}
121is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class
122which inherits methods from \texttt{Eq} as well as defining some of its own:
125data Ordering = LT | EQ | GT
129class Eq a => Ord a where
130 compare : a -> a -> Ordering
134 (<=) : a -> a -> Bool
135 (>=) : a -> a -> Bool
141The \texttt{Ord} class allows us to compare two values and determine their ordering.
142Only the \texttt{compare} method is required; every other method has a default definition.
144this we can write functions such as \texttt{sort}, a function which sorts a list into
145increasing order, provided that the element type of the list is in the \texttt{Ord} class.
146We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the
147function type to the right of the fat arrow:
150sort : Ord a => List a -> List a
154Functions, classes and instances can have multiple constraints. Multiple constaints are
155written in brackets in a comma separated list, for example:
158sortAndShow : (Ord a, Show a) => List a -> String
159sortAndShow xs = show (sort xs)
162\subsection{Monads and \texttt{do}-notation}
166So far, we have seen single parameter type classes, where the parameter is of type
167\texttt{Type}. In general, there can be any number (greater than 0) of parameters,
168and the parameters can have \remph{any} type.
169If the type of the parameter is not \texttt{Type}, we need to give an explicit type
170declaration. For example:
173class Monad (m : Type -> Type) where
175 (>>=) : m a -> (a -> m b) -> m b
179The \texttt{Monad} class allows us to encapsulate binding and computation, and is the
180basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a
181\texttt{do} block, the following syntactic transformations are applied:
184\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}
185\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}
186\item \texttt{let x = v; e} becomes \texttt{let x = v in e}
190\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.
191We can also define an instance for \texttt{Maybe}, as follows:
194instance Monad Maybe where
197 Nothing >>= k = Nothing
202Using this we can, for example, define a function which adds two
203\texttt{Maybe Int}s, using the monad to encapsulate the error handling:
206m_add : Maybe Int -> Maybe Int -> Maybe Int
207m_add x y = do x' <- x -- Extract value from x
208 y' <- y -- Extract value from y
209 return (x' + y') -- Add them
213This function will extract the values from \texttt{x} and \texttt{y}, if they
214are available, or return \texttt{Nothing} if they are not. Managing the
215\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the
219*classes> m_add (Just 20) (Just 22)
221*classes> m_add (Just 20) Nothing
225\subsubsection*{Monad comprehensions}
227The list comprehension notation we saw in Section \ref{sec:listcomp} is more
228general, and applies to anything which is an instance of \texttt{MonadPlus}:
231class Monad m => MonadPlus (m : Type -> Type) where
232 mplus : m a -> m a -> m a
237In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where
238\texttt{quali} can be one of:
241\item A generator \texttt{x <- e}
242\item A \emph{guard}, which is an expression of type \texttt{Bool}
243\item A let binding \texttt{let x = e}
247To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first
249\texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using
250the following function:
253guard : MonadPlus m => Bool -> m ()
257Then the comprehension is converted to \texttt{do} notation:
260do { qual1; qual2; ...; qualn; return exp; }
264Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:
267m_add : Maybe Int -> Maybe Int -> Maybe Int
268m_add x y = [ x' + y' | x' <- x, y' <- y ]
271\subsection{Idiom brackets}
273While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an
274alternative meaning to \emph{application}. The notation and larger example in this
275section is inspired by Conor McBride and Ross Paterson's paper "Applicative
276Programming with Effects"~\cite{idioms}.
278First, let us revisit \texttt{m\_add} above. All it is really doing is applying
279an operator to two values extracted from Maybe Ints. We could abstract out the
283m_app : Maybe (a -> b) -> Maybe a -> Maybe b
284m_app (Just f) (Just a) = Just (f a)
289Using this, we can write an alternative \texttt{m\_add} which uses this alternative
290notion of function application, with explicit calls to \texttt{m\_app}:
293m_add' : Maybe Int -> Maybe Int -> Maybe Int
294m_add' x y = m_app (m_app (Just (+)) x) y
298Rather than having to insert \texttt{m\_app} everywhere there is an
299application, we can use \remph{idiom brackets} to do the job for us. To do
300this, we use the \texttt{Applicative} class, which captures the notion of
301application for a data type:
306class Applicative (f : Type -> Type) where
308 (<$>) : f (a -> b) -> f a -> f b
312\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where
313\texttt{<\$>} is defined in the same way as \texttt{m\_app} above:
316instance Applicative Maybe where
319 (Just f) <$> (Just a) = Just (f a)
324Using \remph{idiom brackets} we can use this instance as follows, where a function
325application \texttt{[| f a1 ... an |]}
326is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
329m_add' : Maybe Int -> Maybe Int -> Maybe Int
330m_add' x y = [| x + y |]
333\subsubsection{An error-handling interpreter}
335Idiom notation is commonly useful when defining evaluators. McBride and
336Paterson describe such an evaluator~\cite{idioms}, for a language similar to
340data Expr = Var String -- variables
342 | Add Expr Expr -- addition
346Evaluation will take place relative to a context mapping variables (represented as
347\texttt{String}s) to integer values, and can possibly fail. We define a data type
348\texttt{Eval} to wrap an evaluator:
351data Eval : Type -> Type where
352 MkEval : (List (String, Int) -> Maybe a) -> Eval a
356Wrapping the evaluator in a data type means we will be able to make it an instance
357of a type class later. We begin by defining a function to retrieve values from
358the context during evaluation:
361fetch : String -> Eval Int
362fetch x = MkEval (\e => fetchVal e) where
363 fetchVal : List (String, Int) -> Maybe Int
364 fetchVal [] = Nothing
365 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
369When defining an evaluator for the language, we will be applying functions in
370the context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an
371instance of \texttt{Applicative}.
372Before \texttt{Eval} can be an instance of
373\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of
377instance Functor Eval where
378 fmap f (MkEval g) = MkEval (\e => fmap f (g e))
380instance Applicative Eval where
381 pure x = MkEval (\e => Just x)
383 (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
384 app : Maybe (a -> b) -> Maybe a -> Maybe b
385 app (Just fx) (Just gx) = Just (fx gx)
390Evaluating an expression can now make use of the idiomatic application to handle
394eval : Expr -> Eval Int
395eval (Var x) = fetch x
396eval (Val x) = [| x |]
397eval (Add x y) = [| eval x + eval y |]
399runEval : List (String, Int) -> Expr -> Maybe Int
400runEval env e = case eval e of
401 MkEval envFn => envFn env
404\subsection{Named Instances}
406It can be desirable to have multiple instances of a type class, for example to provide
407alternative methods for sorting or printing values. To achieve this, instances can
408be \remph{named} as follows:
411instance [myord] Ord Nat where
415 compare (S x) (S y) = compare @{myord} x y
419This declares an instance as normal, but with an explicit name, \texttt{myord}.
420The syntax \texttt{compare @\{myord\}} gives an explicit instance to
421\texttt{compare}, otherwise it would use the default instance for \texttt{Nat}.
422We can use this, for example, to sort a list of \texttt{Nat}s in reverse.
423Given the following list:
431\ldots we can sort it using the default \texttt{Ord} instance, then the named
432instance \texttt{myord} as follows, at the \Idris{} prompt:
435*named_instance> show (sort testList)
436"[sO, sssO, ssssO]" : String
437*named_instance> show (sort @{myord} testList)
438"[ssssO, sssO, sO]" : String
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