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 *interfaces*, which are similar to type classes in
14Haskell or traits in Rust. To define an interface, we provide a collection of
15overloadable functions. A simple example is the ``Show``
16interface, which is defined in the prelude and provides an interface for
17converting values to ``String``:
21 interface Show a where
24This generates a function of the following type (which we call a
25*method* of the ``Show`` interface):
29 show : Show a => a -> String
31We can read this as: “under the constraint that ``a`` has an implementation
32of ``Show``, take an input ``a`` and return a ``String``.” An implementation
33of an interface is defined by giving definitions of the methods of the interface.
35``Show`` implementation for ``Nat`` could be defined as:
41 show (S k) = "s" ++ show k
45 Idris> show (S (S (S Z)))
48Only one implementation of an interface can be given for a type — implementations may
49not overlap. Implementation declarations can themselves have constraints.
50To help with resolution, the arguments of an implementation must be
51constructors (either data or type constructors), variables or
52constants (i.e. you cannot give an implementation for a function). For
53example, to define a ``Show`` implementation for vectors, we need to know
54that there is a ``Show`` implementation for the element type, because we are
55going to use it to convert each element to a ``String``:
59 Show a => Show (Vect n a) where
60 show xs = "[" ++ show' xs ++ "]" where
61 show' : Vect n a -> String
63 show' (x :: Nil) = show x
64 show' (x :: xs) = show x ++ ", " ++ show' xs
69The library defines an ``Eq`` interface which provides methods for
70comparing values for equality or inequality, with implementations for all of
79To declare an implementation for a type, we have to give definitions of all
80of the methods. For example, for an implementation of ``Eq`` for ``Nat``:
86 (S x) == (S y) = x == y
92It is hard to imagine many cases where the ``/=`` method will be
93anything other than the negation of the result of applying the ``==``
94method. It is therefore convenient to give a default definition for
95each method in the interface declaration, in terms of the other method:
100 (==) : a -> a -> Bool
101 (/=) : a -> a -> Bool
103 x /= y = not (x == y)
104 x == y = not (x /= y)
106A minimal complete implementation of ``Eq`` requires either
107``==`` or ``/=`` to be defined, but does not require both. If a method
108definition is missing, and there is a default definition for it, then
109the default is used instead.
114Interfaces can also be extended. A logical next step from an equality
115relation ``Eq`` is to define an ordering relation ``Ord``. We can
116define an ``Ord`` interface which inherits methods from ``Eq`` as well as
117defining some of its own:
121 data Ordering = LT | EQ | GT
125 interface Eq a => Ord a where
126 compare : a -> a -> Ordering
130 (<=) : a -> a -> Bool
131 (>=) : a -> a -> Bool
135The ``Ord`` interface allows us to compare two values and determine their
136ordering. Only the ``compare`` method is required; every other method
137has a default definition. Using this we can write functions such as
138``sort``, a function which sorts a list into increasing order,
139provided that the element type of the list is in the ``Ord`` interface. We
140give the constraints on the type variables left of the fat arrow
141``=>``, and the function type to the right of the fat arrow:
145 sort : Ord a => List a -> List a
147Functions, interfaces and implementations can have multiple
148constraints. Multiple constraints are written in brackets in a comma
149separated list, for example:
153 sortAndShow : (Ord a, Show a) => List a -> String
154 sortAndShow xs = show (sort xs)
156Functors and Applicatives
157=========================
159So far, we have seen single parameter interfaces, where the parameter
160is of type ``Type``. In general, there can be any number of parameters
161(even zero), and the parameters can have *any* type. If the type
162of the parameter is not ``Type``, we need to give an explicit type
163declaration. For example, the ``Functor`` interface is defined in the
168 interface Functor (f : Type -> Type) where
169 map : (m : a -> b) -> f a -> f b
171A functor allows a function to be applied across a structure, for
172example to apply a function to every element in a ``List``:
178 map f (x::xs) = f x :: map f xs
182 Idris> map (*2) [1..10]
183 [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
185Having defined ``Functor``, we can define ``Applicative`` which
186abstracts the notion of function application:
192 interface Functor f => Applicative (f : Type -> Type) where
194 (<*>) : f (a -> b) -> f a -> f b
196Monads and ``do``-notation
197==========================
199The ``Monad`` interface allows us to encapsulate binding and computation,
200and is the basis of ``do``-notation introduced in Section
201:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
206 interface Applicative m => Monad (m : Type -> Type) where
207 (>>=) : m a -> (a -> m b) -> m b
209Inside a ``do`` block, the following syntactic transformations are
212- ``x <- v; e`` becomes ``v >>= (\x => e)``
214- ``v; e`` becomes ``v >>= (\_ => e)``
216- ``let x = v; e`` becomes ``let x = v in e``
218``IO`` has an implementation of ``Monad``, defined using primitive functions.
219We can also define an implementation for ``Maybe``, as follows:
224 Nothing >>= k = Nothing
227Using this we can, for example, define a function which adds two
228``Maybe Int``, using the monad to encapsulate the error handling:
232 m_add : Maybe Int -> Maybe Int -> Maybe Int
233 m_add x y = do x' <- x -- Extract value from x
234 y' <- y -- Extract value from y
235 return (x' + y') -- Add them
237This function will extract the values from ``x`` and ``y``, if they
238are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
239``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
244 *ifaces> m_add (Just 20) (Just 22)
246 *ifaces> m_add (Just 20) Nothing
252Sometimes we want to pattern match immediately on the result of a function
253in ``do`` notation. For example, let's say we have a function ``readNumber``
254which reads a number from the console, returning a value of the form
255``Just x`` if the number is valid, or ``Nothing`` otherwise:
259 readNumber : IO (Maybe Nat)
262 if all isDigit (unpack input)
263 then pure (Just (cast input))
266If we then use it to write a function to read two numbers, returning
267``Nothing`` if neither are valid, then we would like to pattern match
268on the result of ``readNumber``:
272 readNumbers : IO (Maybe (Nat, Nat))
276 Nothing => pure Nothing
277 Just x_ok => do y <- readNumber
279 Nothing => pure Nothing
280 Just y_ok => pure (Just (x_ok, y_ok))
282If there's a lot of error handling, this could get deeply nested very quickly!
283So instead, we can combine the bind and the pattern match in one line. For example,
284we could try pattern matching on values of the form ``Just x_ok``:
288 readNumbers : IO (Maybe (Nat, Nat))
290 do Just x_ok <- readNumber
291 Just y_ok <- readNumber
292 pure (Just (x_ok, y_ok))
294There is still a problem, however, because we've now omitted the case for
295``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
300 readNumbers : IO (Maybe (Nat, Nat))
302 do Just x_ok <- readNumber | Nothing => pure Nothing
303 Just y_ok <- readNumber | Nothing => pure Nothing
304 pure (Just (x_ok, y_ok))
306The effect of this version of ``readNumbers`` is identical to the first (in
307fact, it is syntactic sugar for it and directly translated back into that form).
308The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
309the preferred binding - if this matches, execution will continue with the rest
310of the ``do`` block. The second part gives the alternative bindings, of which
311there may be more than one.
316In many cases, using ``do``-notation can make programs unnecessarily
317verbose, particularly in cases such as ``m_add`` above where the value
318bound is used once, immediately. In these cases, we can use a
319shorthand version, as follows:
323 m_add : Maybe Int -> Maybe Int -> Maybe Int
324 m_add x y = return (!x + !y)
326The notation ``!expr`` means that the expression ``expr`` should be
327evaluated and then implicitly bound. Conceptually, we can think of
328``!`` as being a prefix function with the following type:
334Note, however, that it is not really a function, merely syntax! In
335practice, a subexpression ``!expr`` will lift ``expr`` as high as
336possible within its current scope, bind it to a fresh name ``x``, and
337replace ``!expr`` with ``x``. Expressions are lifted depth first, left
338to right. In practice, ``!``-notation allows us to program in a more
339direct style, while still giving a notational clue as to which
340expressions are monadic.
342For example, the expression:
346 let y = 42 in f !(g !(print y) !x)
352 let y = 42 in do y' <- print y
360The list comprehension notation we saw in Section
361:ref:`sect-more-expr` is more general, and applies to anything which
362has an implementation of both ``Monad`` and ``Alternative``:
366 interface Applicative f => Alternative (f : Type -> Type) where
368 (<|>) : f a -> f a -> f a
370In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
371qualn ]`` where ``quali`` can be one of:
373- A generator ``x <- e``
375- A *guard*, which is an expression of type ``Bool``
377- A let binding ``let x = e``
379To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
380any qualifier ``qual`` which is a *guard* is translated to ``guard
381qual``, using the following function:
385 guard : Alternative f => Bool -> f ()
387Then the comprehension is converted to ``do`` notation:
391 do { qual1; qual2; ...; qualn; return exp; }
393Using monad comprehensions, an alternative definition for ``m_add``
398 m_add : Maybe Int -> Maybe Int -> Maybe Int
399 m_add x y = [ x' + y' | x' <- x, y' <- y ]
404While ``do`` notation gives an alternative meaning to sequencing,
405idioms give an alternative meaning to *application*. The notation and
406larger example in this section is inspired by Conor McBride and Ross
407Paterson’s paper “Applicative Programming with Effects” [1]_.
409First, let us revisit ``m_add`` above. All it is really doing is
410applying an operator to two values extracted from ``Maybe Int``. We
411could abstract out the application:
415 m_app : Maybe (a -> b) -> Maybe a -> Maybe b
416 m_app (Just f) (Just a) = Just (f a)
419Using this, we can write an alternative ``m_add`` which uses this
420alternative notion of function application, with explicit calls to
425 m_add' : Maybe Int -> Maybe Int -> Maybe Int
426 m_add' x y = m_app (m_app (Just (+)) x) y
428Rather than having to insert ``m_app`` everywhere there is an
429application, we can use idiom brackets to do the job for us.
430To do this, we can give ``Maybe`` an implementation of ``Applicative``
431as follows, where ``<*>`` is defined in the same way as ``m_app``
432above (this is defined in the Idris library):
436 Applicative Maybe where
439 (Just f) <*> (Just a) = Just (f a)
442Using ``<*>`` we can use this implementation as follows, where a function
443application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
448 m_add' : Maybe Int -> Maybe Int -> Maybe Int
449 m_add' x y = [| x + y |]
451An error-handling interpreter
452-----------------------------
454Idiom notation is commonly useful when defining evaluators. McBride
455and Paterson describe such an evaluator [1]_, for a language similar
460 data Expr = Var String -- variables
462 | Add Expr Expr -- addition
464Evaluation will take place relative to a context mapping variables
465(represented as ``String``\s) to ``Int`` values, and can possibly fail.
466We define a data type ``Eval`` to wrap an evaluator:
470 data Eval : Type -> Type where
471 MkEval : (List (String, Int) -> Maybe a) -> Eval a
473Wrapping the evaluator in a data type means we will be able to provide
474implementations of interfaces for it later. We begin by defining a function to
475retrieve values from the context during evaluation:
479 fetch : String -> Eval Int
480 fetch x = MkEval (\e => fetchVal e) where
481 fetchVal : List (String, Int) -> Maybe Int
482 fetchVal [] = Nothing
483 fetchVal ((v, val) :: xs) = if (x == v)
487When defining an evaluator for the language, we will be applying functions in
488the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
489of ``Applicative``. Before ``Eval`` can have an implementation of
490``Applicative`` it is necessary for ``Eval`` to have an implementation of
496 map f (MkEval g) = MkEval (\e => map f (g e))
498 Applicative Eval where
499 pure x = MkEval (\e => Just x)
501 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
502 app : Maybe (a -> b) -> Maybe a -> Maybe b
503 app (Just fx) (Just gx) = Just (fx gx)
506Evaluating an expression can now make use of the idiomatic application
511 eval : Expr -> Eval Int
512 eval (Var x) = fetch x
513 eval (Val x) = [| x |]
514 eval (Add x y) = [| eval x + eval y |]
516 runEval : List (String, Int) -> Expr -> Maybe Int
517 runEval env e = case eval e of
518 MkEval envFn => envFn env
523It can be desirable to have multiple implementations of an interface for the
524same type, for example to provide alternative methods for sorting or printing
525values. To achieve this, implementations can be *named* as follows:
529 [myord] Ord Nat where
533 compare (S x) (S y) = compare @{myord} x y
535This declares an implementation as normal, but with an explicit name,
536``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
537``compare``, otherwise it would use the default implementation for ``Nat``. We
538can use this, for example, to sort a list of ``Nat`` in reverse.
539Given the following list:
546We can sort it using the default ``Ord`` implementation, then the named
547implementation ``myord`` as follows, at the Idris prompt:
551 *named_impl> show (sort testList)
552 "[sO, sssO, ssssO]" : String
553 *named_impl> show (sort @{myord} testList)
554 "[ssssO, sssO, sO]" : String
557Determining Parameters
558======================
560When an interface has more than one parameter, it can help resolution if the
561parameters used to find an implementation are restricted. For example:
565 interface Monad m => MonadState s (m : Type -> Type) | m where
569In this interface, only ``m`` needs to be known to find an implementation of
570this interface, and ``s`` can then be determined from the implementation. This
571is declared with the ``| m`` after the interface declaration. We call ``m`` a
572*determining parameter* of the ``MonadState`` interface, because it is the
573parameter used to find an implementation.
576.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
577 with effects. J. Funct. Program. 18, 1 (January 2008),
578 1-13. DOI=10.1017/S0956796807006326
579 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