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 ``Double`` 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)
156Note: Interfaces and ``mutual`` blocks
157~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
159Idris is strictly "define before use", except in ``mutual`` blocks.
160In a ``mutual`` block, Idris elaborates in two passes: types on the first
161pass and definitions on the second. When the mutual block contains an
162interface declaration, it elaborates the interface header but none of the
163method types on the first pass, and elaborates the method types and any
164default definitions on the second pass.
166Functors and Applicatives
167=========================
169So far, we have seen single parameter interfaces, where the parameter
170is of type ``Type``. In general, there can be any number of parameters
171(even zero), and the parameters can have *any* type. If the type
172of the parameter is not ``Type``, we need to give an explicit type
173declaration. For example, the ``Functor`` interface is defined in the
178 interface Functor (f : Type -> Type) where
179 map : (m : a -> b) -> f a -> f b
181A functor allows a function to be applied across a structure, for
182example to apply a function to every element in a ``List``:
188 map f (x::xs) = f x :: map f xs
192 Idris> map (*2) [1..10]
193 [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
195Having defined ``Functor``, we can define ``Applicative`` which
196abstracts the notion of function application:
202 interface Functor f => Applicative (f : Type -> Type) where
204 (<*>) : f (a -> b) -> f a -> f b
206Monads and ``do``-notation
207==========================
209The ``Monad`` interface allows us to encapsulate binding and computation,
210and is the basis of ``do``-notation introduced in Section
211:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
216 interface Applicative m => Monad (m : Type -> Type) where
217 (>>=) : m a -> (a -> m b) -> m b
219Inside a ``do`` block, the following syntactic transformations are
222- ``x <- v; e`` becomes ``v >>= (\x => e)``
224- ``v; e`` becomes ``v >>= (\_ => e)``
226- ``let x = v; e`` becomes ``let x = v in e``
228``IO`` has an implementation of ``Monad``, defined using primitive functions.
229We can also define an implementation for ``Maybe``, as follows:
234 Nothing >>= k = Nothing
237Using this we can, for example, define a function which adds two
238``Maybe Int``, using the monad to encapsulate the error handling:
242 m_add : Maybe Int -> Maybe Int -> Maybe Int
243 m_add x y = do x' <- x -- Extract value from x
244 y' <- y -- Extract value from y
245 pure (x' + y') -- Add them
247This function will extract the values from ``x`` and ``y``, if they
248are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
249``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
254 *ifaces> m_add (Just 20) (Just 22)
256 *ifaces> m_add (Just 20) Nothing
262Sometimes we want to pattern match immediately on the result of a function
263in ``do`` notation. For example, let's say we have a function ``readNumber``
264which reads a number from the console, returning a value of the form
265``Just x`` if the number is valid, or ``Nothing`` otherwise:
269 readNumber : IO (Maybe Nat)
272 if all isDigit (unpack input)
273 then pure (Just (cast input))
276If we then use it to write a function to read two numbers, returning
277``Nothing`` if neither are valid, then we would like to pattern match
278on the result of ``readNumber``:
282 readNumbers : IO (Maybe (Nat, Nat))
286 Nothing => pure Nothing
287 Just x_ok => do y <- readNumber
289 Nothing => pure Nothing
290 Just y_ok => pure (Just (x_ok, y_ok))
292If there's a lot of error handling, this could get deeply nested very quickly!
293So instead, we can combine the bind and the pattern match in one line. For example,
294we could try pattern matching on values of the form ``Just x_ok``:
298 readNumbers : IO (Maybe (Nat, Nat))
300 do Just x_ok <- readNumber
301 Just y_ok <- readNumber
302 pure (Just (x_ok, y_ok))
304There is still a problem, however, because we've now omitted the case for
305``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
310 readNumbers : IO (Maybe (Nat, Nat))
312 do Just x_ok <- readNumber | Nothing => pure Nothing
313 Just y_ok <- readNumber | Nothing => pure Nothing
314 pure (Just (x_ok, y_ok))
316The effect of this version of ``readNumbers`` is identical to the first (in
317fact, it is syntactic sugar for it and directly translated back into that form).
318The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
319the preferred binding - if this matches, execution will continue with the rest
320of the ``do`` block. The second part gives the alternative bindings, of which
321there may be more than one.
326In many cases, using ``do``-notation can make programs unnecessarily
327verbose, particularly in cases such as ``m_add`` above where the value
328bound is used once, immediately. In these cases, we can use a
329shorthand version, as follows:
333 m_add : Maybe Int -> Maybe Int -> Maybe Int
334 m_add x y = pure (!x + !y)
336The notation ``!expr`` means that the expression ``expr`` should be
337evaluated and then implicitly bound. Conceptually, we can think of
338``!`` as being a prefix function with the following type:
344Note, however, that it is not really a function, merely syntax! In
345practice, a subexpression ``!expr`` will lift ``expr`` as high as
346possible within its current scope, bind it to a fresh name ``x``, and
347replace ``!expr`` with ``x``. Expressions are lifted depth first, left
348to right. In practice, ``!``-notation allows us to program in a more
349direct style, while still giving a notational clue as to which
350expressions are monadic.
352For example, the expression:
356 let y = 42 in f !(g !(print y) !x)
362 let y = 42 in do y' <- print y
370The list comprehension notation we saw in Section
371:ref:`sect-more-expr` is more general, and applies to anything which
372has an implementation of both ``Monad`` and ``Alternative``:
376 interface Applicative f => Alternative (f : Type -> Type) where
378 (<|>) : f a -> f a -> f a
380In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
381qualn ]`` where ``quali`` can be one of:
383- A generator ``x <- e``
385- A *guard*, which is an expression of type ``Bool``
387- A let binding ``let x = e``
389To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
390any qualifier ``qual`` which is a *guard* is translated to ``guard
391qual``, using the following function:
395 guard : Alternative f => Bool -> f ()
397Then the comprehension is converted to ``do`` notation:
401 do { qual1; qual2; ...; qualn; pure exp; }
403Using monad comprehensions, an alternative definition for ``m_add``
408 m_add : Maybe Int -> Maybe Int -> Maybe Int
409 m_add x y = [ x' + y' | x' <- x, y' <- y ]
414While ``do`` notation gives an alternative meaning to sequencing,
415idioms give an alternative meaning to *application*. The notation and
416larger example in this section is inspired by Conor McBride and Ross
417Paterson’s paper “Applicative Programming with Effects” [1]_.
419First, let us revisit ``m_add`` above. All it is really doing is
420applying an operator to two values extracted from ``Maybe Int``. We
421could abstract out the application:
425 m_app : Maybe (a -> b) -> Maybe a -> Maybe b
426 m_app (Just f) (Just a) = Just (f a)
429Using this, we can write an alternative ``m_add`` which uses this
430alternative notion of function application, with explicit calls to
435 m_add' : Maybe Int -> Maybe Int -> Maybe Int
436 m_add' x y = m_app (m_app (Just (+)) x) y
438Rather than having to insert ``m_app`` everywhere there is an
439application, we can use idiom brackets to do the job for us.
440To do this, we can give ``Maybe`` an implementation of ``Applicative``
441as follows, where ``<*>`` is defined in the same way as ``m_app``
442above (this is defined in the Idris library):
446 Applicative Maybe where
449 (Just f) <*> (Just a) = Just (f a)
452Using ``<*>`` we can use this implementation as follows, where a function
453application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
458 m_add' : Maybe Int -> Maybe Int -> Maybe Int
459 m_add' x y = [| x + y |]
461An error-handling interpreter
462-----------------------------
464Idiom notation is commonly useful when defining evaluators. McBride
465and Paterson describe such an evaluator [1]_, for a language similar
470 data Expr = Var String -- variables
472 | Add Expr Expr -- addition
474Evaluation will take place relative to a context mapping variables
475(represented as ``String``\s) to ``Int`` values, and can possibly fail.
476We define a data type ``Eval`` to wrap an evaluator:
480 data Eval : Type -> Type where
481 MkEval : (List (String, Int) -> Maybe a) -> Eval a
483Wrapping the evaluator in a data type means we will be able to provide
484implementations of interfaces for it later. We begin by defining a function to
485retrieve values from the context during evaluation:
489 fetch : String -> Eval Int
490 fetch x = MkEval (\e => fetchVal e) where
491 fetchVal : List (String, Int) -> Maybe Int
492 fetchVal [] = Nothing
493 fetchVal ((v, val) :: xs) = if (x == v)
497When defining an evaluator for the language, we will be applying functions in
498the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
499of ``Applicative``. Before ``Eval`` can have an implementation of
500``Applicative`` it is necessary for ``Eval`` to have an implementation of
506 map f (MkEval g) = MkEval (\e => map f (g e))
508 Applicative Eval where
509 pure x = MkEval (\e => Just x)
511 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
512 app : Maybe (a -> b) -> Maybe a -> Maybe b
513 app (Just fx) (Just gx) = Just (fx gx)
516Evaluating an expression can now make use of the idiomatic application
521 eval : Expr -> Eval Int
522 eval (Var x) = fetch x
523 eval (Val x) = [| x |]
524 eval (Add x y) = [| eval x + eval y |]
526 runEval : List (String, Int) -> Expr -> Maybe Int
527 runEval env e = case eval e of
528 MkEval envFn => envFn env
533It can be desirable to have multiple implementations of an interface for the
534same type, for example to provide alternative methods for sorting or printing
535values. To achieve this, implementations can be *named* as follows:
539 [myord] Ord Nat where
543 compare (S x) (S y) = compare @{myord} x y
545This declares an implementation as normal, but with an explicit name,
546``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
547``compare``, otherwise it would use the default implementation for ``Nat``. We
548can use this, for example, to sort a list of ``Nat`` in reverse.
549Given the following list:
556We can sort it using the default ``Ord`` implementation, then the named
557implementation ``myord`` as follows, at the Idris prompt:
561 *named_impl> show (sort testList)
562 "[sO, sssO, ssssO]" : String
563 *named_impl> show (sort @{myord} testList)
564 "[ssssO, sssO, sO]" : String
567Determining Parameters
568======================
570When an interface has more than one parameter, it can help resolution if the
571parameters used to find an implementation are restricted. For example:
575 interface Monad m => MonadState s (m : Type -> Type) | m where
579In this interface, only ``m`` needs to be known to find an implementation of
580this interface, and ``s`` can then be determined from the implementation. This
581is declared with the ``| m`` after the interface declaration. We call ``m`` a
582*determining parameter* of the ``MonadState`` interface, because it is the
583parameter used to find an implementation.
586.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
587 with effects. J. Funct. Program. 18, 1 (January 2008),
588 1-13. DOI=10.1017/S0956796807006326
589 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