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.
34For example, the ``Show`` implementation for ``Nat`` could be defined as:
40 show (S k) = "s" ++ show k
44 Idris> show (S (S (S Z)))
47Only one implementation of an interface can be given for a type — implementations may
48not overlap. Implementation declarations can themselves have constraints.
49To help with resolution, the arguments of an implementation must be
50constructors (either data or type constructors) or variables
51(i.e. you cannot give an implementation for a function). For
52example, to define a ``Show`` implementation for vectors, we need to know
53that there is a ``Show`` implementation for the element type, because we are
54going to use it to convert each element to a ``String``:
58 Show a => Show (Vect n a) where
59 show xs = "[" ++ show' xs ++ "]" where
60 show' : Vect n a -> String
62 show' (x :: Nil) = show x
63 show' (x :: xs) = show x ++ ", " ++ show' xs
68The library defines an ``Eq`` interface which provides methods for
69comparing values for equality or inequality, with implementations for all of
78To declare an implementation for a type, we have to give definitions of all
79of the methods. For example, for an implementation of ``Eq`` for ``Nat``:
85 (S x) == (S y) = x == y
91It is hard to imagine many cases where the ``/=`` method will be
92anything other than the negation of the result of applying the ``==``
93method. It is therefore convenient to give a default definition for
94each method in the interface declaration, in terms of the other method:
100 (/=) : a -> a -> Bool
102 x /= y = not (x == y)
103 x == y = not (x /= y)
105A minimal complete implementation of ``Eq`` requires either
106``==`` or ``/=`` to be defined, but does not require both. If a method
107definition is missing, and there is a default definition for it, then
108the default is used instead.
113Interfaces can also be extended. A logical next step from an equality
114relation ``Eq`` is to define an ordering relation ``Ord``. We can
115define an ``Ord`` interface which inherits methods from ``Eq`` as well as
116defining some of its own:
120 data Ordering = LT | EQ | GT
124 interface Eq a => Ord a where
125 compare : a -> a -> Ordering
129 (<=) : a -> a -> Bool
130 (>=) : a -> a -> Bool
134The ``Ord`` interface allows us to compare two values and determine their
135ordering. Only the ``compare`` method is required; every other method
136has a default definition. Using this we can write functions such as
137``sort``, a function which sorts a list into increasing order,
138provided that the element type of the list is in the ``Ord`` interface. We
139give the constraints on the type variables left of the fat arrow
140``=>``, and the function type to the right of the fat arrow:
144 sort : Ord a => List a -> List a
146Functions, interfaces and implementations can have multiple
147constraints. Multiple constraints are written in brackets in a comma
148separated list, for example:
152 sortAndShow : (Ord a, Show a) => List a -> String
153 sortAndShow xs = show (sort xs)
155Note: Interfaces and ``mutual`` blocks
156~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
158Idris is strictly "define before use", except in ``mutual`` blocks.
159In a ``mutual`` block, Idris elaborates in two passes: types on the first
160pass and definitions on the second. When the mutual block contains an
161interface declaration, it elaborates the interface header but none of the
162method types on the first pass, and elaborates the method types and any
163default definitions on the second pass.
165Functors and Applicatives
166=========================
168So far, we have seen single parameter interfaces, where the parameter
169is of type ``Type``. In general, there can be any number of parameters
170(even zero), and the parameters can have *any* type. If the type
171of the parameter is not ``Type``, we need to give an explicit type
172declaration. For example, the ``Functor`` interface is defined in the
177 interface Functor (f : Type -> Type) where
178 map : (m : a -> b) -> f a -> f b
180A functor allows a function to be applied across a structure, for
181example to apply a function to every element in a ``List``:
187 map f (x::xs) = f x :: map f xs
191 Idris> map (*2) [1..10]
192 [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
194Having defined ``Functor``, we can define ``Applicative`` which
195abstracts the notion of function application:
201 interface Functor f => Applicative (f : Type -> Type) where
203 (<*>) : f (a -> b) -> f a -> f b
207Monads and ``do``-notation
208==========================
210The ``Monad`` interface allows us to encapsulate binding and computation,
211and is the basis of ``do``-notation introduced in Section
212:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
217 interface Applicative m => Monad (m : Type -> Type) where
218 (>>=) : m a -> (a -> m b) -> m b
220Inside a ``do`` block, the following syntactic transformations are
223- ``x <- v; e`` becomes ``v >>= (\x => e)``
225- ``v; e`` becomes ``v >>= (\_ => e)``
227- ``let x = v; e`` becomes ``let x = v in e``
229``IO`` has an implementation of ``Monad``, defined using primitive functions.
230We can also define an implementation for ``Maybe``, as follows:
235 Nothing >>= k = Nothing
238Using this we can, for example, define a function which adds two
239``Maybe Int``, using the monad to encapsulate the error handling:
243 m_add : Maybe Int -> Maybe Int -> Maybe Int
244 m_add x y = do x' <- x -- Extract value from x
245 y' <- y -- Extract value from y
246 pure (x' + y') -- Add them
248This function will extract the values from ``x`` and ``y``, if they
249are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
250``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
255 *Interfaces> m_add (Just 20) (Just 22)
257 *Interfaces> m_add (Just 20) Nothing
263Sometimes we want to pattern match immediately on the result of a function
264in ``do`` notation. For example, let's say we have a function ``readNumber``
265which reads a number from the console, returning a value of the form
266``Just x`` if the number is valid, or ``Nothing`` otherwise:
270 readNumber : IO (Maybe Nat)
273 if all isDigit (unpack input)
274 then pure (Just (cast input))
277If we then use it to write a function to read two numbers, returning
278``Nothing`` if neither are valid, then we would like to pattern match
279on the result of ``readNumber``:
283 readNumbers : IO (Maybe (Nat, Nat))
287 Nothing => pure Nothing
288 Just x_ok => do y <- readNumber
290 Nothing => pure Nothing
291 Just y_ok => pure (Just (x_ok, y_ok))
293If there's a lot of error handling, this could get deeply nested very quickly!
294So instead, we can combine the bind and the pattern match in one line. For example,
295we could try pattern matching on values of the form ``Just x_ok``:
299 readNumbers : IO (Maybe (Nat, Nat))
301 do Just x_ok <- readNumber
302 Just y_ok <- readNumber
303 pure (Just (x_ok, y_ok))
305There is still a problem, however, because we've now omitted the case for
306``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
311 readNumbers : IO (Maybe (Nat, Nat))
313 do Just x_ok <- readNumber | Nothing => pure Nothing
314 Just y_ok <- readNumber | Nothing => pure Nothing
315 pure (Just (x_ok, y_ok))
317The effect of this version of ``readNumbers`` is identical to the first (in
318fact, it is syntactic sugar for it and directly translated back into that form).
319The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
320the preferred binding - if this matches, execution will continue with the rest
321of the ``do`` block. The second part gives the alternative bindings, of which
322there may be more than one.
327In many cases, using ``do``-notation can make programs unnecessarily
328verbose, particularly in cases such as ``m_add`` above where the value
329bound is used once, immediately. In these cases, we can use a
330shorthand version, as follows:
334 m_add : Maybe Int -> Maybe Int -> Maybe Int
335 m_add x y = pure (!x + !y)
337The notation ``!expr`` means that the expression ``expr`` should be
338evaluated and then implicitly bound. Conceptually, we can think of
339``!`` as being a prefix function with the following type:
345Note, however, that it is not really a function, merely syntax! In
346practice, a subexpression ``!expr`` will lift ``expr`` as high as
347possible within its current scope, bind it to a fresh name ``x``, and
348replace ``!expr`` with ``x``. Expressions are lifted depth first, left
349to right. In practice, ``!``-notation allows us to program in a more
350direct style, while still giving a notational clue as to which
351expressions are monadic.
353For example, the expression:
357 let y = 42 in f !(g !(print y) !x)
363 let y = 42 in do y' <- print y
371The list comprehension notation we saw in Section
372:ref:`sect-more-expr` is more general, and applies to anything which
373has an implementation of both ``Monad`` and ``Alternative``:
377 interface Applicative f => Alternative (f : Type -> Type) where
379 (<|>) : f a -> f a -> f a
381In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
382qualn ]`` where ``quali`` can be one of:
384- A generator ``x <- e``
386- A *guard*, which is an expression of type ``Bool``
388- A let binding ``let x = e``
390To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
391any qualifier ``qual`` which is a *guard* is translated to ``guard
392qual``, using the following function:
396 guard : Alternative f => Bool -> f ()
398Then the comprehension is converted to ``do`` notation:
402 do { qual1; qual2; ...; qualn; pure exp; }
404Using monad comprehensions, an alternative definition for ``m_add``
409 m_add : Maybe Int -> Maybe Int -> Maybe Int
410 m_add x y = [ x' + y' | x' <- x, y' <- y ]
415While ``do`` notation gives an alternative meaning to sequencing,
416idioms give an alternative meaning to *application*. The notation and
417larger example in this section is inspired by Conor McBride and Ross
418Paterson’s paper “Applicative Programming with Effects” [1]_.
420First, let us revisit ``m_add`` above. All it is really doing is
421applying an operator to two values extracted from ``Maybe Int``. We
422could abstract out the application:
426 m_app : Maybe (a -> b) -> Maybe a -> Maybe b
427 m_app (Just f) (Just a) = Just (f a)
430Using this, we can write an alternative ``m_add`` which uses this
431alternative notion of function application, with explicit calls to
436 m_add' : Maybe Int -> Maybe Int -> Maybe Int
437 m_add' x y = m_app (m_app (Just (+)) x) y
439Rather than having to insert ``m_app`` everywhere there is an
440application, we can use idiom brackets to do the job for us.
441To do this, we can give ``Maybe`` an implementation of ``Applicative``
442as follows, where ``<*>`` is defined in the same way as ``m_app``
443above (this is defined in the Idris library):
447 Applicative Maybe where
450 (Just f) <*> (Just a) = Just (f a)
453Using ``<*>`` we can use this implementation as follows, where a function
454application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
459 m_add' : Maybe Int -> Maybe Int -> Maybe Int
460 m_add' x y = [| x + y |]
462An error-handling interpreter
463~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
465Idiom notation is commonly useful when defining evaluators. McBride
466and Paterson describe such an evaluator [1]_, for a language similar
471 data Expr = Var String -- variables
473 | Add Expr Expr -- addition
475Evaluation will take place relative to a context mapping variables
476(represented as ``String``\s) to ``Int`` values, and can possibly fail.
477We define a data type ``Eval`` to wrap an evaluator:
481 data Eval : Type -> Type where
482 MkEval : (List (String, Int) -> Maybe a) -> Eval a
484Wrapping the evaluator in a data type means we will be able to provide
485implementations of interfaces for it later. We begin by defining a function to
486retrieve values from the context during evaluation:
490 fetch : String -> Eval Int
491 fetch x = MkEval (\e => fetchVal e) where
492 fetchVal : List (String, Int) -> Maybe Int
493 fetchVal [] = Nothing
494 fetchVal ((v, val) :: xs) = if (x == v)
498When defining an evaluator for the language, we will be applying functions in
499the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
500of ``Applicative``. Before ``Eval`` can have an implementation of
501``Applicative`` it is necessary for ``Eval`` to have an implementation of
507 map f (MkEval g) = MkEval (\e => map f (g e))
509 Applicative Eval where
510 pure x = MkEval (\e => Just x)
512 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
513 app : Maybe (a -> b) -> Maybe a -> Maybe b
514 app (Just fx) (Just gx) = Just (fx gx)
517Evaluating an expression can now make use of the idiomatic application
522 eval : Expr -> Eval Int
523 eval (Var x) = fetch x
524 eval (Val x) = [| x |]
525 eval (Add x y) = [| eval x + eval y |]
527 runEval : List (String, Int) -> Expr -> Maybe Int
528 runEval env e = case eval e of
529 MkEval envFn => envFn env
534It can be desirable to have multiple implementations of an interface for the
535same type, for example to provide alternative methods for sorting or printing
536values. To achieve this, implementations can be *named* as follows:
540 [myord] Ord Nat where
544 compare (S x) (S y) = compare @{myord} x y
546This declares an implementation as normal, but with an explicit name,
547``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
548``compare``, otherwise it would use the default implementation for ``Nat``. We
549can use this, for example, to sort a list of ``Nat`` in reverse.
550Given the following list:
557We can sort it using the default ``Ord`` implementation, then the named
558implementation ``myord`` as follows, at the Idris prompt:
562 *named_impl> show (sort testList)
563 "[sO, sssO, ssssO]" : String
564 *named_impl> show (sort @{myord} testList)
565 "[ssssO, sssO, sO]" : String
568Sometimes, we also need access to a named parent implementation. For example,
569the prelude defines the following ``Semigroup`` interface:
573 interface Semigroup ty where
574 (<+>) : ty -> ty -> ty
576Then it defines ``Monoid``, which extends ``Semigroup`` with a “neutral”
581 interface Semigroup ty => Monoid ty where
584We can define two different implementations of ``Semigroup`` and
585``Monoid`` for ``Nat``, one based on addition and one on multiplication:
589 [PlusNatSemi] Semigroup Nat where
592 [MultNatSemi] Semigroup Nat where
595The neutral value for addition is ``0``, but the neutral value for multiplication
596is ``1``. It's important, therefore, that when we define implementations
597of ``Monoid`` they extend the correct ``Semigroup`` implementation. We can
598do this with a ``using`` clause in the implementation as follows:
602 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
605 [MultNatMonoid] Monoid Nat using MultNatSemi where
608The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
609extend ``PlusNatSemi`` specifically.
611Determining Parameters
612======================
614When an interface has more than one parameter, it can help resolution if the
615parameters used to find an implementation are restricted. For example:
619 interface Monad m => MonadState s (m : Type -> Type) | m where
623In this interface, only ``m`` needs to be known to find an implementation of
624this interface, and ``s`` can then be determined from the implementation. This
625is declared with the ``| m`` after the interface declaration. We call ``m`` a
626*determining parameter* of the ``MonadState`` interface, because it is the
627parameter used to find an implementation.
630.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
631 with effects. J. Funct. Program. 18, 1 (January 2008),
632 1-13. DOI=10.1017/S0956796807006326
633 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