\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{Type}. 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{Type}, we need to give an explicit type
declaration. For example:

\begin{SaveVerbatim}{monad}

class Monad (m : Type -> Type) 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 : Type -> Type) 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 : Type -> Type) 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 : Type -> Type 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}.
Before \texttt{Eval} can be an instance of
\texttt{Applicative} it is necessary to make \texttt{Eval} an instance of
\texttt{Functor}:

\begin{SaveVerbatim}{}

instance Functor Eval where
    fmap f (MkEval g) = MkEval (\e => fmap f (g e))

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{myordlistrun}