tutorial/classes.tex · Idris-dev

git.iko.soy/Idris-dev

on ebf9100 help sign in

Idris-dev/tutorial/classes.tex

257 lines 7.5 kB history raw

1\section{Type Classes}

2\label{sec:classes}

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

15\texttt{String}s:

17\begin{SaveVerbatim}{showclass}

19class Show a where {

20 show : a -> String;

21}

23\end{SaveVerbatim}

24\useverb{showclass}

26\noindent

27This generates a function of the following type (which we call a \emph{method} of the

28\texttt{Show} class):

30\begin{SaveVerbatim}{showty}

32show : Show a => a -> String;

34\end{SaveVerbatim}

35\useverb{showty}

37\noindent

38We can read this as ``under the constraint that \texttt{a} is an instance of \texttt{Show},

39take an \texttt{a} as input and return a \texttt{String}.'' An instance of a class

40is defined with an \texttt{instance} declaration, which provides implementations of

41the function for a specific type. For example, the \texttt{Show} instance for \texttt{Nat}

42could be defined as:

44\begin{SaveVerbatim}{shownat}

46instance Show Nat where {

47 show O = "O";

48 show (S k) = "s" ++ show k;

49}

51Idris> show (S (S (S O)))

52"sssO" : String

54\end{SaveVerbatim}

55\useverb{shownat}

57Instance declarations can themselves have constraints. For example, to define a

58\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}

59instance for the element type, because we are going to use it to convert each element

60to a \texttt{String}:

62\begin{SaveVerbatim}{showvec}

64instance Show a => Show (Vect a n) where {

65 show xs = "[" ++ show' xs ++ "]" where {

66 show' : Show a => Vect a n -> String;

67 show' VNil = "";

68 show' (x :: VNil) = show x;

69 show' (x :: xs) = show x ++ ", " ++ show' xs;

70 }

71}

73\end{SaveVerbatim}

74\useverb{showvec}

76\subsection{Default Definitions}

78The library defines an \texttt{Eq} class which provides an interface for comparing

79values for equality or inequality, with instances for all of the built-in types:

81\begin{SaveVerbatim}{eqbasic}

83class Eq a where {

84 (==) : a -> a -> Bool;

85 (/=) : a -> a -> Bool;

86}

88\end{SaveVerbatim}

89\useverb{eqbasic}

91\noindent

92To declare an instance of a type, we have to give definitions of all of the methods.

93For example, for an instance of \texttt{Eq} for \texttt{Nat}:

95\begin{SaveVerbatim}{eqnat}

97instance Eq Nat where {

98 O == O = True;

99 (S x) == (S y) = x == y;

100 O == (S y) = False;

101 (S x) == O = False;

102

103 x /= y = not (x == y);

104}

105

106\end{SaveVerbatim}

107\useverb{eqnat}

108

109\noindent

110It is hard to imagine many cases where the \texttt{/=} method will be anything other

111than the negation of the result of applying the \texttt{==} method. It is therefore

112convenient to give a default definition for each method in the class

113declaration, in terms of the other method:

114

115\begin{SaveVerbatim}{eqdefault}

116

117class Eq a where {

118 (==) : a -> a -> Bool;

119 (/=) : a -> a -> Bool;

120

121 x /= y = not (x == y);

122 y == y = not (x /= y);

123}

124

125\end{SaveVerbatim}

126\useverb{eqdefault}

127

128\noindent

129A minimal complete definition of an \texttt{Eq} instance requires either \texttt{==}

130or \texttt{/=} to be defined, but does not require both. If a method definition is

131missing, and there is a default definition for it, then the default is used instead.

132

133\subsection{Extending Classes}

134

135Classes can also be extended. A logical next step from an equality relation \texttt{Eq}

136is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class

137which inherits method from \texttt{Eq} as well as defining some of its own:

138

139\begin{SaveVerbatim}{ord}

140

141data Ordering = LT | EQ | GT;

142

143class Eq a => Ord a where {

144 compare : a -> a -> Ordering;

145

146 (<) : a -> a -> Bool;

147 (>) : a -> a -> Bool;

148 (<=) : a -> a -> Bool;

149 (>=) : a -> a -> Bool;

150 max : a -> a -> a;

151 min : a -> a -> a;

152}

153

154\end{SaveVerbatim}

155\useverb{ord}

156

157The \texttt{Ord} class allows us to compare two values and determine their ordering.

158Only the \texttt{compare} method is required; every other method has a default definition.

159Using

160this we can write functions such as \texttt{sort}, a function which sorts a list into

161increasing order, provided that the element type of the list is in the \texttt{Ord} class.

162We give the constraints on the type variables left of the fat arrow \texttt{=>}, and the

163function type to the right of the fat arrow:

164

165\begin{SaveVerbatim}{sortty}

166

167sort : Ord a => List a -> List a;

168

169\end{SaveVerbatim}

170\useverb{sortty}

171

172\noindent

173Functions, classes and instances can have multiple constraints. Multiple constaints are

174written in brackets in a comma separated list, for example:

175

176\begin{SaveVerbatim}{sortshow}

177

178sortAndShow : (Ord a, Show a) => List a -> String;

179sortAndShow xs = show (sort xs);

180

181\end{SaveVerbatim}

182\useverb{sortshow}

183

184\subsection{Monads and \texttt{do}-notation}

185

186So far, we have seen single parameter type classes, where the parameter is of type

187\texttt{Set}. In general, there can be any number (greater than 0) of parameters,

188and the parameters can have \remph{any} type.

189If the type of the parameter is not \texttt{Set}, we need to give an explicit type

190declaration. For example:

191

192\begin{SaveVerbatim}{monad}

193

194class Monad (m : Set -> Set) where {

195 return : a -> m a;

196 (>>=) : m a -> (a -> m b) -> m b;

197}

198

199\end{SaveVerbatim}

200\useverb{monad}

201

202The \texttt{Monad} class allows us to encapsulate binding and computation, and is the

203basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a

204\texttt{do} block, the following syntactic transformations are applied:

205

206\begin{itemize}

207\item \texttt{x <- v; e} becomes \texttt{v >>= ($\backslash$x => e)}

208\item \texttt{v; e} becomes \texttt{v >>= ($\backslash$\_ => e)}

209\item \texttt{let x = v; e} becomes \texttt{let x = v in e}

210\end{itemize}

211

212\noindent

213\texttt{IO} is an instance of \texttt{Monad}, defined using primitive functions.

214We can also define an instance for \texttt{Maybe}, as follows:

215

216\begin{SaveVerbatim}{maybemonad}

217

218instance Monad Maybe where {

219 return = Just;

220

221 Nothing >>= k = Nothing;

222 (Just x) >>= k = k x;

223}

224

225\end{SaveVerbatim}

226\useverb{maybemonad}

227

228\noindent

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:

231

232\begin{SaveVerbatim}{maybeadd}

233

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

238 };

239

240\end{SaveVerbatim}

241\useverb{maybeadd}

242

243\noindent

244This function will extract the values from \texttt{x} and \texttt{y}, if they

245are available, or return \texttt{Nothing} if they are not. Managing the

246\texttt{Nothing} cases is achieved by the \texttt{>>=} operator, hidden by the

247\texttt{do} notation.

248

249\begin{SaveVerbatim}{maybeaddt}

250

251*classes> m_add (Just 20) (Just 22)

252Just 42 : Maybe Int

253*classes> m_add (Just 20) Nothing

254Nothing : Maybe Int

255

256\end{SaveVerbatim}

257\useverb{maybeaddt}