7We often want to define functions which work across several different
8data types. For example, we would like arithmetic operators to work on
9``Int``, ``Integer`` and ``Float`` at the very least. We would like
10``==`` to work on the majority of data types. We would like to be able
11to display different types in a uniform way.
13To achieve this, we use a feature which has proved to be effective in
14Haskell, namely *type classes*. To define a type class, we provide a
15collection of overloaded operations which describe the interface for
16*instances* of that class. A simple example is the ``Show`` type
17class, which is defined in the prelude and provides an interface for
18converting values to ``String``:
25This generates a function of the following type (which we call a
26*method* of the ``Show`` class):
30 show : Show a => a -> String
32We can read this as: “under the constraint that ``a`` is an instance
33of ``Show``, take an input ``a`` and return a ``String``.” An instance
34of a class is defined with an ``instance`` declaration, which provides
35implementations of the function for a specific type. For example, the
36``Show`` instance for ``Nat`` could be defined as:
40 instance Show Nat where
42 show (S k) = "s" ++ show k
46 Idris> show (S (S (S Z)))
49Only one instance of a class can be given for a type — instances may
50not overlap. Instance declarations can themselves have constraints.
51To help with resolution, the arguments of an instance must be
52constructors (either data or type constructors), variables or
53constants (i.e. you cannot give an instance for a function). For
54example, to define a ``Show`` instance for vectors, we need to know
55that there is a ``Show`` instance for the element type, because we are
56going to use it to convert each element to a ``String``:
60 instance Show a => Show (Vect n a) where
61 show xs = "[" ++ show' xs ++ "]" where
62 show' : Vect n a -> String
64 show' (x :: Nil) = show x
65 show' (x :: xs) = show x ++ ", " ++ show' xs
70The library defines an ``Eq`` class which provides an interface for
71comparing values for equality or inequality, with instances for all of
80To declare an instance of a type, we have to give definitions of all
81of the methods. For example, for an instance of ``Eq`` for ``Nat``:
87 (S x) == (S y) = x == y
93It is hard to imagine many cases where the ``/=`` method will be
94anything other than the negation of the result of applying the ``==``
95method. It is therefore convenient to give a default definition for
96each method in the class declaration, in terms of the other method:
101 (==) : a -> a -> Bool
102 (/=) : a -> a -> Bool
104 x /= y = not (x == y)
105 x == y = not (x /= y)
107A minimal complete definition of an ``Eq`` instance requires either
108``==`` or ``/=`` to be defined, but does not require both. If a method
109definition is missing, and there is a default definition for it, then
110the default is used instead.
115Classes can also be extended. A logical next step from an equality
116relation ``Eq`` is to define an ordering relation ``Ord``. We can
117define an ``Ord`` class which inherits methods from ``Eq`` as well as
118defining some of its own:
122 data Ordering = LT | EQ | GT
126 class Eq a => Ord a where
127 compare : a -> a -> Ordering
131 (<=) : a -> a -> Bool
132 (>=) : a -> a -> Bool
136The ``Ord`` class allows us to compare two values and determine their
137ordering. Only the ``compare`` method is required; every other method
138has a default definition. Using this we can write functions such as
139``sort``, a function which sorts a list into increasing order,
140provided that the element type of the list is in the ``Ord`` class. We
141give the constraints on the type variables left of the fat arrow
142``=>``, and the function type to the right of the fat arrow:
146 sort : Ord a => List a -> List a
148Functions, classes and instances can have multiple
149constraints. Multiple constraints are written in brackets in a comma
150separated list, for example:
154 sortAndShow : (Ord a, Show a) => List a -> String
155 sortAndShow xs = show (sort xs)
157Functors and Applicatives
158=========================
160So far, we have seen single parameter type classes, where the parameter
161is of type ``Type``. In general, there can be any number (greater than
1620) of parameters, and the parameters can have *any* type. If the type
163of the parameter is not ``Type``, we need to give an explicit type
164declaration. For example, the ``Functor`` class is defined in the
169 class Functor (f : Type -> Type) where
170 map : (m : a -> b) -> f a -> f b
172A functor allows a function to be applied across a structure, for
173example to apply a function to every element in a ``List``:
177 instance Functor List where
179 map f (x::xs) = f x :: map f xs
183 Idris> map (*2) [1..10]
184 [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
186Having defined ``Functor``, we can define ``Applicative`` which
187abstracts the notion of function application:
193 class Functor f => Applicative (f : Type -> Type) where
195 (<*>) : f (a -> b) -> f a -> f b
197Monads and ``do``-notation
198==========================
200The ``Monad`` class allows us to encapsulate binding and computation,
201and is the basis of ``do``-notation introduced in Section
202:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
207 class Applicative m => Monad (m : Type -> Type) where
208 (>>=) : m a -> (a -> m b) -> m b
210Inside a ``do`` block, the following syntactic transformations are
213- ``x <- v; e`` becomes ``v >>= (\x => e)``
215- ``v; e`` becomes ``v >>= (\_ => e)``
217- ``let x = v; e`` becomes ``let x = v in e``
219``IO`` is an instance of ``Monad``, defined using primitive functions.
220We can also define an instance for ``Maybe``, as follows:
224 instance Monad Maybe where
225 Nothing >>= k = Nothing
228Using this we can, for example, define a function which adds two
229``Maybe Int``, using the monad to encapsulate the error handling:
233 m_add : Maybe Int -> Maybe Int -> Maybe Int
234 m_add x y = do x' <- x -- Extract value from x
235 y' <- y -- Extract value from y
236 return (x' + y') -- Add them
238This function will extract the values from ``x`` and ``y``, if they
239are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
240``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
245 *classes> m_add (Just 20) (Just 22)
247 *classes> m_add (Just 20) Nothing
253In many cases, using ``do``-notation can make programs unnecessarily
254verbose, particularly in cases such as ``m_add`` above where the value
255bound is used once, immediately. In these cases, we can use a
256shorthand version, as follows:
260 m_add : Maybe Int -> Maybe Int -> Maybe Int
261 m_add x y = return (!x + !y)
263The notation ``!expr`` means that the expression ``expr`` should be
264evaluated and then implicitly bound. Conceptually, we can think of
265``!`` as being a prefix function with the following type:
271Note, however, that it is not really a function, merely syntax! In
272practice, a subexpression ``!expr`` will lift ``expr`` as high as
273possible within its current scope, bind it to a fresh name ``x``, and
274replace ``!expr`` with ``x``. Expressions are lifted depth first, left
275to right. In practice, ``!``-notation allows us to program in a more
276direct style, while still giving a notational clue as to which
277expressions are monadic.
279For example, the expression:
283 let y = 42 in f !(g !(print y) !x)
289 let y = 42 in do y' <- print y
297The list comprehension notation we saw in Section
298:ref:`sect-more-expr` is more general, and applies to anything which
299is an instance of both ``Monad`` and ``Alternative``:
303 class Applicative f => Alternative (f : Type -> Type) where
305 (<|>) : f a -> f a -> f a
307In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
308qualn ]`` where ``quali`` can be one of:
310- A generator ``x <- e``
312- A *guard*, which is an expression of type ``Bool``
314- A let binding ``let x = e``
316To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
317any qualifier ``qual`` which is a *guard* is translated to ``guard
318qual``, using the following function:
322 guard : Alternative f => Bool -> f ()
324Then the comprehension is converted to ``do`` notation:
328 do { qual1; qual2; ...; qualn; return exp; }
330Using monad comprehensions, an alternative definition for ``m_add``
335 m_add : Maybe Int -> Maybe Int -> Maybe Int
336 m_add x y = [ x' + y' | x' <- x, y' <- y ]
341While ``do`` notation gives an alternative meaning to sequencing,
342idioms give an alternative meaning to *application*. The notation and
343larger example in this section is inspired by Conor McBride and Ross
344Paterson’s paper “Applicative Programming with Effects” [1]_.
346First, let us revisit ``m_add`` above. All it is really doing is
347applying an operator to two values extracted from ``Maybe Int``. We
348could abstract out the application:
352 m_app : Maybe (a -> b) -> Maybe a -> Maybe b
353 m_app (Just f) (Just a) = Just (f a)
356Using this, we can write an alternative ``m_add`` which uses this
357alternative notion of function application, with explicit calls to
362 m_add' : Maybe Int -> Maybe Int -> Maybe Int
363 m_add' x y = m_app (m_app (Just (+)) x) y
365Rather than having to insert ``m_app`` everywhere there is an
366application, we can use idiom brackets to do the job for us.
367To do this, we can make ``Maybe`` an instance of ``Applicative``
368as follows, where ``<*>`` is defined in the same way as ``m_app``
369above (this is defined in the Idris library):
373 instance Applicative Maybe where
376 (Just f) <*> (Just a) = Just (f a)
379Using ``<*>`` we can use this instance as follows, where a function
380application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
385 m_add' : Maybe Int -> Maybe Int -> Maybe Int
386 m_add' x y = [| x + y |]
388An error-handling interpreter
389-----------------------------
391Idiom notation is commonly useful when defining evaluators. McBride
392and Paterson describe such an evaluator [1]_, for a language similar
397 data Expr = Var String -- variables
399 | Add Expr Expr -- addition
401Evaluation will take place relative to a context mapping variables
402(represented as ``String``\s) to ``Int`` values, and can possibly fail.
403We define a data type ``Eval`` to wrap an evaluator:
407 data Eval : Type -> Type where
408 MkEval : (List (String, Int) -> Maybe a) -> Eval a
410Wrapping the evaluator in a data type means we will be able to make it
411an instance of a type class later. We begin by defining a function to
412retrieve values from the context during evaluation:
416 fetch : String -> Eval Int
417 fetch x = MkEval (\e => fetchVal e) where
418 fetchVal : List (String, Int) -> Maybe Int
419 fetchVal [] = Nothing
420 fetchVal ((v, val) :: xs) = if (x == v)
424When defining an evaluator for the language, we will be applying
425functions in the context of an ``Eval``, so it is natural to make
426``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an
427instance of ``Applicative`` it is necessary to make ``Eval`` an
428instance of ``Functor``:
432 instance Functor Eval where
433 map f (MkEval g) = MkEval (\e => map f (g e))
435 instance Applicative Eval where
436 pure x = MkEval (\e => Just x)
438 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
439 app : Maybe (a -> b) -> Maybe a -> Maybe b
440 app (Just fx) (Just gx) = Just (fx gx)
443Evaluating an expression can now make use of the idiomatic application
448 eval : Expr -> Eval Int
449 eval (Var x) = fetch x
450 eval (Val x) = [| x |]
451 eval (Add x y) = [| eval x + eval y |]
453 runEval : List (String, Int) -> Expr -> Maybe Int
454 runEval env e = case eval e of
455 MkEval envFn => envFn env
460It can be desirable to have multiple instances of a type class, for
461example to provide alternative methods for sorting or printing values.
462To achieve this, instances can be *named* as follows:
466 instance [myord] Ord Nat where
470 compare (S x) (S y) = compare @{myord} x y
472This declares an instance as normal, but with an explicit name,
473``myord``. The syntax ``compare @{myord}`` gives an explicit instance to
474``compare``, otherwise it would use the default instance for ``Nat``. We
475can use this, for example, to sort a list of ``Nat`` in reverse.
476Given the following list:
483We can sort it using the default ``Ord`` instance, then the named
484instance ``myord`` as follows, at the Idris prompt:
488 *named_instance> show (sort testList)
489 "[sO, sssO, ssssO]" : String
490 *named_instance> show (sort @{myord} testList)
491 "[ssssO, sssO, sO]" : String
494Determining Parameters
495======================
497When a class has more than one parameter, it can help resolution if
498the parameters used to resolve the type class are restricted. For
503 class Monad m => MonadState s (m : Type -> Type) | m where
507In this class, only ``m`` needs to be known to resolve this class, and
508``s`` can then be determined from the instance. This is declared with
509the ``| m`` after the class declaration. We call ``m`` a *determining
510parameter* of the ``MonadState`` class, because it is the parameter
511used to resolve an instance.
514.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
515 with effects. J. Funct. Program. 18, 1 (January 2008),
516 1-13. DOI=10.1017/S0956796807006326
517 http://dx.doi.org/10.1017/S0956796807006326
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