# edwinb/Idris-dev forked from idris-lang/Idris-dev

### Subversion checkout URL

You can clone with
or
.
Fetching contributors…

Cannot retrieve contributors at this time

531 lines (377 sloc) 15.214 kB
 \section{Type Classes} \label{sec:classes} We often want to define functions which work across several different data types. For example, we would like arithmetic operators to work on \texttt{Int}, \texttt{Integer} and \texttt{Float} at the very least. We would like \texttt{==} to work on the majority of data types. We would like to be able to display different types in a uniform way. To achieve this, we use a feature which has proved to be effective in Haskell, namely \emph{type classes}. To define a type class, we provide a collection of overloaded operations which describe the interface for \emph{instances} of that class. A simple example is the \texttt{Show} type class, which is defined in the prelude and provides an interface for converting values to \texttt{String}s: \begin{SaveVerbatim}{showclass} class Show a where show : a -> String \end{SaveVerbatim} \useverb{showclass} \noindent This generates a function of the following type (which we call a \emph{method} of the \texttt{Show} class): \begin{SaveVerbatim}{showty} show : Show a => a -> String \end{SaveVerbatim} \useverb{showty} \noindent We can read this as under the constraint that \texttt{a} is an instance of \texttt{Show}, take an \texttt{a} as input and return a \texttt{String}.'' An instance of a class is defined with an \texttt{instance} declaration, which provides implementations of the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat} could be defined as: \begin{SaveVerbatim}{shownat} instance Show Nat where show O = "O" show (S k) = "s" ++ show k Idris> show (S (S (S O))) "sssO" : String \end{SaveVerbatim} \useverb{shownat} \noindent Only one instance of a class can be given for a type --- instances may not overlap. Instance declarations can themselves have constraints. For example, to define a \texttt{Show} instance for vectors, we need to know that there is a \texttt{Show} instance for the element type, because we are going to use it to convert each element to a \texttt{String}: \begin{SaveVerbatim}{showvec} instance Show a => Show (Vect a n) where show xs = "[" ++ show' xs ++ "]" where show' : Vect a n' -> String show' Nil = "" show' (x :: Nil) = show x show' (x :: xs) = show x ++ ", " ++ show' xs \end{SaveVerbatim} \useverb{showvec} \noindent \textbf{Remark: } The type of the auxiliary function \texttt{show'} is important. The type variables \texttt{a} and \texttt{n} which are part of the instance declaration for \texttt{Show (Vect a n)} are fixed across the entire instance declaration. As a result, we do not have to constrain \texttt{a} again. Furthermore, it means that if we use \texttt{n} in the type, it refers to the (fixed) length of the outermost list \texttt{xs}. Therefore, we use a different name for the length \texttt{n'} in \texttt{show'}. \subsection{Default Definitions} The library defines an \texttt{Eq} class which provides an interface for comparing values for equality or inequality, with instances for all of the built-in types: \begin{SaveVerbatim}{eqbasic} class Eq a where (==) : a -> a -> Bool (/=) : a -> a -> Bool \end{SaveVerbatim} \useverb{eqbasic} \noindent To declare an instance of a type, we have to give definitions of all of the methods. For example, for an instance of \texttt{Eq} for \texttt{Nat}: \begin{SaveVerbatim}{eqnat} instance Eq Nat where O == O = True (S x) == (S y) = x == y O == (S y) = False (S x) == O = False x /= y = not (x == y) \end{SaveVerbatim} \useverb{eqnat} \noindent It is hard to imagine many cases where the \texttt{/=} method will be anything other than the negation of the result of applying the \texttt{==} method. It is therefore convenient to give a default definition for each method in the class declaration, in terms of the other method: \begin{SaveVerbatim}{eqdefault} class Eq a where (==) : a -> a -> Bool (/=) : a -> a -> Bool x /= y = not (x == y) y == y = not (x /= y) \end{SaveVerbatim} \useverb{eqdefault} \noindent A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==} or \texttt{/=} to be defined, but does not require both. If a method definition is missing, and there is a default definition for it, then the default is used instead. \subsection{Extending Classes} Classes can also be extended. A logical next step from an equality relation \texttt{Eq} is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class which inherits methods from \texttt{Eq} as well as defining some of its own: \begin{SaveVerbatim}{ord} data Ordering = LT | EQ | GT \end{SaveVerbatim} \useverb{ord} \begin{SaveVerbatim}{eqord} class Eq a => Ord a where compare : a -> a -> Ordering (<) : a -> a -> Bool (>) : a -> a -> Bool (<=) : a -> a -> Bool (>=) : a -> a -> Bool max : a -> a -> a min : a -> a -> a \end{SaveVerbatim} \useverb{eqord} \noindent The \texttt{Ord} class allows us to compare two values and determine their ordering. Only the \texttt{compare} method is required; every other method has a default definition. Using this we can write functions such as \texttt{sort}, a function which sorts a list into increasing order, provided that the element type of the list is in the \texttt{Ord} class. We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the function type to the right of the fat arrow: \begin{SaveVerbatim}{sortty} sort : Ord a => List a -> List a \end{SaveVerbatim} \useverb{sortty} \noindent Functions, classes and instances can have multiple constraints. Multiple constaints are written in brackets in a comma separated list, for example: \begin{SaveVerbatim}{sortshow} sortAndShow : (Ord a, Show a) => List a -> String sortAndShow xs = show (sort xs) \end{SaveVerbatim} \useverb{sortshow} \subsection{Monads and \texttt{do}-notation} \label{sec:monad} So far, we have seen single parameter type classes, where the parameter is of type \texttt{Set}. In general, there can be any number (greater than 0) of parameters, and the parameters can have \remph{any} type. If the type of the parameter is not \texttt{Set}, we need to give an explicit type declaration. For example: \begin{SaveVerbatim}{monad} class Monad (m : Set -> Set) where return : a -> m a (>>=) : m a -> (a -> m b) -> m b \end{SaveVerbatim} \useverb{monad} \noindent The \texttt{Monad} class allows us to encapsulate binding and computation, and is the basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a \texttt{do} block, the following syntactic transformations are applied: \begin{itemize} \item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)} \item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)} \item \texttt{let x = v; e} becomes \texttt{let x = v in e} \end{itemize} \noindent \texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions. We can also define an instance for \texttt{Maybe}, as follows: \begin{SaveVerbatim}{maybemonad} instance Monad Maybe where return = Just Nothing >>= k = Nothing (Just x) >>= k = k x \end{SaveVerbatim} \useverb{maybemonad} \noindent Using this we can, for example, define a function which adds two \texttt{Maybe Int}s, using the monad to encapsulate the error handling: \begin{SaveVerbatim}{maybeadd} m_add : Maybe Int -> Maybe Int -> Maybe Int m_add x y = do x' <- x -- Extract value from x y' <- y -- Extract value from y return (x' + y') -- Add them \end{SaveVerbatim} \useverb{maybeadd} \noindent This function will extract the values from \texttt{x} and \texttt{y}, if they are available, or return \texttt{Nothing} if they are not. Managing the \texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the \texttt{do} notation. \begin{SaveVerbatim}{maybeaddt} *classes> m_add (Just 20) (Just 22) Just 42 : Maybe Int *classes> m_add (Just 20) Nothing Nothing : Maybe Int \end{SaveVerbatim} \useverb{maybeaddt} \subsubsection*{Monad comprehensions} The list comprehension notation we saw in Section \ref{sec:listcomp} is more general, and applies to anything which is an instance of \texttt{MonadPlus}: \begin{SaveVerbatim}{monadplus} class Monad m => MonadPlus (m : Set -> Set) where mplus : m a -> m a -> m a mzero : m a \end{SaveVerbatim} \useverb{monadplus} \noindent In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where \texttt{quali} can be one of: \begin{itemize} \item A generator \texttt{x <- e} \item A \emph{guard}, which is an expression of type \texttt{Bool} \item A let binding \texttt{let x = e} \end{itemize} \noindent To translate a comprehension \texttt{[exp | qual1, qual2, ..., qualn]}, first any qualifier \texttt{qual} which is a \emph{guard} is translated to \texttt{guard qual}, using the following function: \begin{SaveVerbatim}{guardq} guard : MonadPlus m => Bool -> m () \end{SaveVerbatim} \useverb{guardq} \noindent Then the comprehension is converted to \texttt{do} notation: \begin{SaveVerbatim}{comptrans} do { qual1; qual2; ...; qualn; return exp; } \end{SaveVerbatim} \useverb{comptrans} \noindent Using monad comprehensions, an alternative definition for \texttt{m\_add} would be: \begin{SaveVerbatim}{maddb} m_add : Maybe Int -> Maybe Int -> Maybe Int m_add x y = [ x' + y' | x' <- x, y' <- y ] \end{SaveVerbatim} \useverb{maddb} \subsection{Idiom brackets} While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an alternative meaning to \emph{application}. The notation and larger example in this section is inspired by Conor McBride and Ross Paterson's paper "Applicative Programming with Effects"~\cite{idioms}. First, let us revisit \texttt{m\_add} above. All it is really doing is applying an operator to two values extracted from Maybe Ints. We could abstract out the application: \begin{SaveVerbatim}{mapp} m_app : Maybe (a -> b) -> Maybe a -> Maybe b m_app (Just f) (Just a) = Just (f a) m_app _ _ = Nothing \end{SaveVerbatim} \useverb{mapp} \noindent Using this, we can write an alternative \texttt{m\_add} which uses this alternative notion of function application, with explicit calls to \texttt{m\_app}: \begin{SaveVerbatim}{maddb} m_add' : Maybe Int -> Maybe Int -> Maybe Int m_add' x y = m_app (m_app (Just (+)) x) y \end{SaveVerbatim} \useverb{maddb} \noindent Rather than having to insert \texttt{m\_app} everywhere there is an application, we can use \remph{idiom brackets} to do the job for us. To do this, we use the \texttt{Applicative} class, which captures the notion of application for a data type: \begin{SaveVerbatim}{applicative} infixl 2 <$> class Applicative (f : Set -> Set) where pure : a -> f a (<$>) : f (a -> b) -> f a -> f b \end{SaveVerbatim} \useverb{applicative} \noindent \texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where \texttt{<\$>} is defined in the same way as \texttt{m\_app} above: \begin{SaveVerbatim}{maybeapp} instance Applicative Maybe where pure = Just (Just f) <$> (Just a) = Just (f a) _ <$> _ = Nothing \end{SaveVerbatim} \useverb{maybeapp} \noindent Using \remph{idiom brackets} we can use this instance as follows, where a function application \texttt{[| f a1 ... an |]} is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}: \begin{SaveVerbatim}{maddc} m_add' : Maybe Int -> Maybe Int -> Maybe Int m_add' x y = [| x + y |] \end{SaveVerbatim} \useverb{maddc} \subsubsection{An error-handling interpreter} Idiom notation is commonly useful when defining evaluators. McBride and Paterson describe such an evaluator~\cite{idioms}, for a language similar to the following: \begin{SaveVerbatim}{idiomexpr} data Expr = Var String -- variables | Val Int -- values | Add Expr Expr -- addition \end{SaveVerbatim} \useverb{idiomexpr} \noindent Evaluation will take place relative to a context mapping variables (represented as \texttt{String}s) to integer values, and can possibly fail. We define a data type \texttt{Eval} to wrap an evaluator: \begin{SaveVerbatim}{evalctxt} data Eval : Set -> Set where MkEval : (List (String, Int) -> Maybe a) -> Eval a \end{SaveVerbatim} \useverb{evalctxt} \noindent Wrapping the evaluator in a data type means we will be able to make it an instance of a type class later. We begin by defining a function to retrieve values from the context during evaluation: \begin{SaveVerbatim}{fetch} fetch : String -> Eval Int fetch x = MkEval (\e => fetchVal e) where fetchVal : List (String, Int) -> Maybe Int fetchVal [] = Nothing fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs) \end{SaveVerbatim} \useverb{fetch} \noindent When defining an evaluator for the language, we will be applying functions in the context of an \texttt{Eval}, so it is natural to make \texttt{Eval} an instance of \texttt{Applicative}: \begin{SaveVerbatim}{} instance Applicative Eval where pure x = MkEval (\e => Just x) (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where app : Maybe (a -> b) -> Maybe a -> Maybe b app (Just fx) (Just gx) = Just (fx gx) app _ _ = Nothing \end{SaveVerbatim} \useverb{} \begin{SaveVerbatim}{grr} <$> \end{SaveVerbatim} \noindent Evaluating an expression can now make use of the idiomatic application to handle errors: \begin{SaveVerbatim}{evalexpr} eval : Expr -> Eval Int eval (Var x) = fetch x eval (Val x) = [| x |] eval (Add x y) = [| eval x + eval y |] runEval : List (String, Int) -> Expr -> Maybe Int runEval env e = case eval e of MkEval envFn => envFn env \end{SaveVerbatim} \useverb{evalexpr} \subsection{Named Instances} It can be desirable to have multiple instances of a type class, for example to provide alternative methods for sorting or printing values. To achieve this, instances can be \remph{named} as follows: \begin{SaveVerbatim}{myord} instance [myord] Ord Nat where compare O (S n) = GT compare (S n) O = LT compare O O = EQ compare (S x) (S y) = compare @{myord} x y \end{SaveVerbatim} \useverb{myord} \noindent This declares an instance as normal, but with an explicit name, \texttt{myord}. The syntax \texttt{compare @\{myord\}} gives an explicit instance to \texttt{compare}, otherwise it would use the default instance for \texttt{Nat}. We can use this, for example, to sort a list of \texttt{Nat}s in reverse. Given the following list: \begin{SaveVerbatim}{myordlist} testList : List Nat testList = [3,4,1] \end{SaveVerbatim} \useverb{myordlist} \noindent \ldots we can sort it using the default \texttt{Ord} instance, then the named instance \texttt{myord} as follows, at the \Idris{} prompt: \begin{SaveVerbatim}{myordlistrun} *named_instance> show (sort testList) "[sO, sssO, ssssO]" : String *named_instance> show (sort @{myord} testList) "[ssssO, sssO, sO]" : String \end{SaveVerbatim} \useverb{myordlist}
Something went wrong with that request. Please try again.