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 class,
17which is defined in the prelude and provides an interface for converting
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 of
33``Show``, take an input ``a`` and return a ``String``.” An instance of a
34class 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 not
50overlap. Instance declarations can themselves have constraints. For
51example, to define a ``Show`` instance for vectors, we need to know that
52there is a ``Show`` instance for the element type, because we are going
53to use it to convert each element to a ``String``:
57 instance Show a => Show (Vect n a) where
58 show xs = "[" ++ show' xs ++ "]" where
59 show' : Vect n a -> String
61 show' (x :: Nil) = show x
62 show' (x :: xs) = show x ++ ", " ++ show' xs
67The library defines an ``Eq`` class which provides an interface for
68comparing values for equality or inequality, with instances for all of
77To declare an instance of a type, we have to give definitions of all of
78the methods. For example, for an instance of ``Eq`` for ``Nat``:
84 (S x) == (S y) = x == y
90It is hard to imagine many cases where the ``/=`` method will be
91anything other than the negation of the result of applying the ``==``
92method. It is therefore convenient to give a default definition for each
93method in the class declaration, in terms of the other method:
101 x /= y = not (x == y)
102 x == y = not (x /= y)
104A minimal complete definition of an ``Eq`` instance requires either
105``==`` or ``/=`` to be defined, but does not require both. If a method
106definition is missing, and there is a default definition for it, then
107the default is used instead.
112Classes can also be extended. A logical next step from an equality
113relation ``Eq`` is to define an ordering relation ``Ord``. We can define
114an ``Ord`` class which inherits methods from ``Eq`` as well as defining
119 data Ordering = LT | EQ | GT
123 class Eq a => Ord a where
124 compare : a -> a -> Ordering
128 (<=) : a -> a -> Bool
129 (>=) : a -> a -> Bool
133The ``Ord`` class allows us to compare two values and determine their
134ordering. Only the ``compare`` method is required; every other method
135has a default definition. Using this we can write functions such as
136``sort``, a function which sorts a list into increasing order, provided
137that the element type of the list is in the ``Ord`` class. We give the
138constraints on the type variables left of the fat arrow ``=>``, and the
139function type to the right of the fat arrow:
143 sort : Ord a => List a -> List a
145Functions, classes and instances can have multiple constraints. Multiple
146constaints are written in brackets in a comma separated list, for
151 sortAndShow : (Ord a, Show a) => List a -> String
152 sortAndShow xs = show (sort xs)
154Functors and Applicatives
155-------------------------
157So far, we have seen single parameter type classes, where the parameter
158is of type ``Type``. In general, there can be any number (greater than
1590) of parameters, and the parameters can have *any* type. If the type of
160the parameter is not ``Type``, we need to give an explicit type
161declaration. For example, the ``Functor`` class is defined in the
166 class Functor (f : Type -> Type) where
167 map : (m : a -> b) -> f a -> f b
169A functor allows a function to be applied across a structure, for
170example to apply a function to every element in a ``List``:
174 instance Functor List where
176 map f (x::xs) = f x :: map f xs
180 Idris> map (*2) [1..10]
181 [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
183Having defined ``Functor``, we can define ``Applicative`` which
184abstracts the notion of function application:
190 class Functor f => Applicative (f : Type -> Type) where
192 (<*>) : f (a -> b) -> f a -> f b
194Monads and ``do``-notation
195--------------------------
197The ``Monad`` class allows us to encapsulate binding and computation,
198and is the basis of ``do``-notation introduced in Section [sect:do]. It
199extends ``Applicative`` as defined above, and is defined as follows:
203 class Applicative m => Monad (m : Type -> Type) where
204 (>>=) : m a -> (a -> m b) -> m b
206Inside a ``do`` block, the following syntactic transformations are
209- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``
211- ``v; e`` becomes ``v >>= (\backslash_ => e)``
213- ``let x = v; e`` becomes ``let x = v in e``
215``IO`` is an instance of ``Monad``, defined using primitive functions.
216We can also define an instance for ``Maybe``, as follows:
220 instance Monad Maybe where
221 Nothing >>= k = Nothing
224Using this we can, for example, define a function which adds two
225``Maybe Int``\ s, using the monad to encapsulate the error handling:
229 m_add : Maybe Int -> Maybe Int -> Maybe Int
230 m_add x y = do x' <- x -- Extract value from x
231 y' <- y -- Extract value from y
232 return (x' + y') -- Add them
234This function will extract the values from ``x`` and ``y``, if they are
235available, or return ``Nothing`` if they are not. Managing the
236``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
241 *classes> m_add (Just 20) (Just 22)
243 *classes> m_add (Just 20) Nothing
249In many cases, using ``do``-notation can make programs unnecessarily
250verbose, particularly in cases such as ``m_add`` above where the value
251bound is used once, immediately. In these cases, we can use a shorthand
256 m_add : Maybe Int -> Maybe Int -> Maybe Int
257 m_add x y = return (!x + !y)
259The notation ``!expr`` means that the expression ``expr`` should be
260evaluated and then implicitly bound. Conceptually, we can think of ``!``
261as being a prefix function with the following type:
267Note, however, that it is not really a function, merely syntax! In
268practice, a subexpression ``!expr`` will lift ``expr`` as high as
269possible within its current scope, bind it to a fresh name ``x``, and
270replace ``!expr`` with ``x``. Expressions are lifted depth first, left
271to right. In practice, ``!``-notation allows us to program in a more
272direct style, while still giving a notational clue as to which
273expressions are monadic.
275For example, the expression…
279 let y = 42 in f !(g !(print y) !x)
285 let y = 42 in do y' <- print y
293The list comprehension notation we saw in Section :ref:`sect-more-expr` is more
294general, and applies to anything which is an instance of both ``Monad``
299 class Applicative f => Alternative (f : Type -> Type) where
301 (<|>) : f a -> f a -> f a
303In general, a comprehension takes the form
304``[ exp | qual1, qual2, …, qualn ]`` where ``quali`` can be one of:
306- A generator ``x <- e``
308- A *guard*, which is an expression of type ``Bool``
310- A let binding ``let x = e``
312To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
313any qualifier ``qual`` which is a *guard* is translated to
314``guard qual``, using the following function:
318 guard : Alternative f => Bool -> f ()
320Then the comprehension is converted to ``do`` notation:
324 do { qual1; qual2; ...; qualn; return exp; }
326Using monad comprehensions, an alternative definition for ``m_add``
331 m_add : Maybe Int -> Maybe Int -> Maybe Int
332 m_add x y = [ x' + y' | x' <- x, y' <- y ]
337While ``do`` notation gives an alternative meaning to sequencing, idioms
338give an alternative meaning to *application*. The notation and larger
339example in this section is inspired by Conor McBride and Ross Paterson’s
340paper “Applicative Programming with Effects” [1]_.
342First, let us revisit ``m_add`` above. All it is really doing is
343applying an operator to two values extracted from ``Maybe Int``\ ’s. We
344could abstract out the application:
348 m_app : Maybe (a -> b) -> Maybe a -> Maybe b
349 m_app (Just f) (Just a) = Just (f a)
352Using this, we can write an alternative ``m_add`` which uses this
353alternative notion of function application, with explicit calls to
358 m_add' : Maybe Int -> Maybe Int -> Maybe Int
359 m_add' x y = m_app (m_app (Just (+)) x) y
361Rather than having to insert ``m_app`` everywhere there is an
362application, we can use to do the job for us. To do this, we can make
363``Maybe`` an instance of ``Applicative`` as follows, where ``<>`` is
364defined in the same way as ``m_app`` above (this is defined in the ``Idris``
369 instance Applicative Maybe where
372 (Just f) <*> (Just a) = Just (f a)
375Using we can use this instance as follows, where a function application
376``[| f a1 …an |]`` is translated into ``pure f <> a1 <> …<> an``:
380 m_add' : Maybe Int -> Maybe Int -> Maybe Int
381 m_add' x y = [| x + y |]
383An error-handling interpreter
384~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
386Idiom notation is commonly useful when defining evaluators. McBride and
387Paterson describe such an evaluator [1], for a language similar to the
392 data Expr = Var String -- variables
394 | Add Expr Expr -- addition
396Evaluation will take place relative to a context mapping variables
397(represented as ``String``s) to integer values, and can possibly fail.
398We define a data type ``Eval`` to wrap an evaluator:
402 data Eval : Type -> Type where
403 MkEval : (List (String, Int) -> Maybe a) -> Eval a
405Wrapping the evaluator in a data type means we will be able to make it
406an instance of a type class later. We begin by defining a function to
407retrieve values from the context during evaluation:
411 fetch : String -> Eval Int
412 fetch x = MkEval (\e => fetchVal e) where
413 fetchVal : List (String, Int) -> Maybe Int
414 fetchVal [] = Nothing
415 fetchVal ((v, val) :: xs) = if (x == v)
419When defining an evaluator for the language, we will be applying
420functions in the context of an ``Eval``, so it is natural to make
421``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an
422instance of ``Applicative`` it is necessary to make ``Eval`` an instance
427 instance Functor Eval where
428 map f (MkEval g) = MkEval (\e => map f (g e))
430 instance Applicative Eval where
431 pure x = MkEval (\e => Just x)
433 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
434 app : Maybe (a -> b) -> Maybe a -> Maybe b
435 app (Just fx) (Just gx) = Just (fx gx)
438Evaluating an expression can now make use of the idiomatic application
443 eval : Expr -> Eval Int
444 eval (Var x) = fetch x
445 eval (Val x) = [| x |]
446 eval (Add x y) = [| eval x + eval y |]
448 runEval : List (String, Int) -> Expr -> Maybe Int
449 runEval env e = case eval e of
450 MkEval envFn => envFn env
455It can be desirable to have multiple instances of a type class, for
456example to provide alternative methods for sorting or printing values.
457To achieve this, instances can be *named* as follows:
461 instance [myord] Ord Nat where
465 compare (S x) (S y) = compare @{myord} x y
467This declares an instance as normal, but with an explicit name,
468``myord``. The syntax ``compare @{myord}`` gives an explicit instance to
469``compare``, otherwise it would use the default instance for ``Nat``. We
470can use this, for example, to sort a list of ``Nat`` s in reverse.
471Given the following list:
478…e can sort it using the default ``Ord`` instance, then the named
479instance ``myord`` as follows, at the ``Idris`` prompt:
483 *named_instance> show (sort testList)
484 "[sO, sssO, ssssO]" : String
485 *named_instance> show (sort @{myord} testList)
486 "[ssssO, sssO, sO]" : String
490.. [1] Conor Mcbride and Ross Paterson. 2008. Applicative programming
491 with effects. J. Funct. Program. 18, 1 (January 2008),
492 1-13. DOI=10.1017/S0956796807006326
493 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