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) or variables
52(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
208Monads and ``do``-notation
209==========================
211The ``Monad`` interface allows us to encapsulate binding and computation,
212and is the basis of ``do``-notation introduced in Section
213:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
218 interface Applicative m => Monad (m : Type -> Type) where
219 (>>=) : m a -> (a -> m b) -> m b
221Inside a ``do`` block, the following syntactic transformations are
224- ``x <- v; e`` becomes ``v >>= (\x => e)``
226- ``v; e`` becomes ``v >>= (\_ => e)``
228- ``let x = v; e`` becomes ``let x = v in e``
230``IO`` has an implementation of ``Monad``, defined using primitive functions.
231We can also define an implementation for ``Maybe``, as follows:
236 Nothing >>= k = Nothing
239Using this we can, for example, define a function which adds two
240``Maybe Int``, using the monad to encapsulate the error handling:
244 m_add : Maybe Int -> Maybe Int -> Maybe Int
245 m_add x y = do x' <- x -- Extract value from x
246 y' <- y -- Extract value from y
247 pure (x' + y') -- Add them
249This function will extract the values from ``x`` and ``y``, if they
250are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
251``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
256 *Interfaces> m_add (Just 20) (Just 22)
258 *Interfaces> m_add (Just 20) Nothing
264Sometimes we want to pattern match immediately on the result of a function
265in ``do`` notation. For example, let's say we have a function ``readNumber``
266which reads a number from the console, returning a value of the form
267``Just x`` if the number is valid, or ``Nothing`` otherwise:
271 readNumber : IO (Maybe Nat)
274 if all isDigit (unpack input)
275 then pure (Just (cast input))
278If we then use it to write a function to read two numbers, returning
279``Nothing`` if neither are valid, then we would like to pattern match
280on the result of ``readNumber``:
284 readNumbers : IO (Maybe (Nat, Nat))
288 Nothing => pure Nothing
289 Just x_ok => do y <- readNumber
291 Nothing => pure Nothing
292 Just y_ok => pure (Just (x_ok, y_ok))
294If there's a lot of error handling, this could get deeply nested very quickly!
295So instead, we can combine the bind and the pattern match in one line. For example,
296we could try pattern matching on values of the form ``Just x_ok``:
300 readNumbers : IO (Maybe (Nat, Nat))
302 do Just x_ok <- readNumber
303 Just y_ok <- readNumber
304 pure (Just (x_ok, y_ok))
306There is still a problem, however, because we've now omitted the case for
307``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
312 readNumbers : IO (Maybe (Nat, Nat))
314 do Just x_ok <- readNumber | Nothing => pure Nothing
315 Just y_ok <- readNumber | Nothing => pure Nothing
316 pure (Just (x_ok, y_ok))
318The effect of this version of ``readNumbers`` is identical to the first (in
319fact, it is syntactic sugar for it and directly translated back into that form).
320The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
321the preferred binding - if this matches, execution will continue with the rest
322of the ``do`` block. The second part gives the alternative bindings, of which
323there may be more than one.
328In many cases, using ``do``-notation can make programs unnecessarily
329verbose, particularly in cases such as ``m_add`` above where the value
330bound is used once, immediately. In these cases, we can use a
331shorthand version, as follows:
335 m_add : Maybe Int -> Maybe Int -> Maybe Int
336 m_add x y = pure (!x + !y)
338The notation ``!expr`` means that the expression ``expr`` should be
339evaluated and then implicitly bound. Conceptually, we can think of
340``!`` as being a prefix function with the following type:
346Note, however, that it is not really a function, merely syntax! In
347practice, a subexpression ``!expr`` will lift ``expr`` as high as
348possible within its current scope, bind it to a fresh name ``x``, and
349replace ``!expr`` with ``x``. Expressions are lifted depth first, left
350to right. In practice, ``!``-notation allows us to program in a more
351direct style, while still giving a notational clue as to which
352expressions are monadic.
354For example, the expression:
358 let y = 42 in f !(g !(print y) !x)
364 let y = 42 in do y' <- print y
372The list comprehension notation we saw in Section
373:ref:`sect-more-expr` is more general, and applies to anything which
374has an implementation of both ``Monad`` and ``Alternative``:
378 interface Applicative f => Alternative (f : Type -> Type) where
380 (<|>) : f a -> f a -> f a
382In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
383qualn ]`` where ``quali`` can be one of:
385- A generator ``x <- e``
387- A *guard*, which is an expression of type ``Bool``
389- A let binding ``let x = e``
391To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
392any qualifier ``qual`` which is a *guard* is translated to ``guard
393qual``, using the following function:
397 guard : Alternative f => Bool -> f ()
399Then the comprehension is converted to ``do`` notation:
403 do { qual1; qual2; ...; qualn; pure exp; }
405Using monad comprehensions, an alternative definition for ``m_add``
410 m_add : Maybe Int -> Maybe Int -> Maybe Int
411 m_add x y = [ x' + y' | x' <- x, y' <- y ]
416While ``do`` notation gives an alternative meaning to sequencing,
417idioms give an alternative meaning to *application*. The notation and
418larger example in this section is inspired by Conor McBride and Ross
419Paterson’s paper “Applicative Programming with Effects” [1]_.
421First, let us revisit ``m_add`` above. All it is really doing is
422applying an operator to two values extracted from ``Maybe Int``. We
423could abstract out the application:
427 m_app : Maybe (a -> b) -> Maybe a -> Maybe b
428 m_app (Just f) (Just a) = Just (f a)
431Using this, we can write an alternative ``m_add`` which uses this
432alternative notion of function application, with explicit calls to
437 m_add' : Maybe Int -> Maybe Int -> Maybe Int
438 m_add' x y = m_app (m_app (Just (+)) x) y
440Rather than having to insert ``m_app`` everywhere there is an
441application, we can use idiom brackets to do the job for us.
442To do this, we can give ``Maybe`` an implementation of ``Applicative``
443as follows, where ``<*>`` is defined in the same way as ``m_app``
444above (this is defined in the Idris library):
448 Applicative Maybe where
451 (Just f) <*> (Just a) = Just (f a)
454Using ``<*>`` we can use this implementation as follows, where a function
455application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
460 m_add' : Maybe Int -> Maybe Int -> Maybe Int
461 m_add' x y = [| x + y |]
463An error-handling interpreter
464~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
466Idiom notation is commonly useful when defining evaluators. McBride
467and Paterson describe such an evaluator [1]_, for a language similar
472 data Expr = Var String -- variables
474 | Add Expr Expr -- addition
476Evaluation will take place relative to a context mapping variables
477(represented as ``String``\s) to ``Int`` values, and can possibly fail.
478We define a data type ``Eval`` to wrap an evaluator:
482 data Eval : Type -> Type where
483 MkEval : (List (String, Int) -> Maybe a) -> Eval a
485Wrapping the evaluator in a data type means we will be able to provide
486implementations of interfaces for it later. We begin by defining a function to
487retrieve values from the context during evaluation:
491 fetch : String -> Eval Int
492 fetch x = MkEval (\e => fetchVal e) where
493 fetchVal : List (String, Int) -> Maybe Int
494 fetchVal [] = Nothing
495 fetchVal ((v, val) :: xs) = if (x == v)
499When defining an evaluator for the language, we will be applying functions in
500the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
501of ``Applicative``. Before ``Eval`` can have an implementation of
502``Applicative`` it is necessary for ``Eval`` to have an implementation of
508 map f (MkEval g) = MkEval (\e => map f (g e))
510 Applicative Eval where
511 pure x = MkEval (\e => Just x)
513 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
514 app : Maybe (a -> b) -> Maybe a -> Maybe b
515 app (Just fx) (Just gx) = Just (fx gx)
518Evaluating an expression can now make use of the idiomatic application
523 eval : Expr -> Eval Int
524 eval (Var x) = fetch x
525 eval (Val x) = [| x |]
526 eval (Add x y) = [| eval x + eval y |]
528 runEval : List (String, Int) -> Expr -> Maybe Int
529 runEval env e = case eval e of
530 MkEval envFn => envFn env
535It can be desirable to have multiple implementations of an interface for the
536same type, for example to provide alternative methods for sorting or printing
537values. To achieve this, implementations can be *named* as follows:
541 [myord] Ord Nat where
545 compare (S x) (S y) = compare @{myord} x y
547This declares an implementation as normal, but with an explicit name,
548``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
549``compare``, otherwise it would use the default implementation for ``Nat``. We
550can use this, for example, to sort a list of ``Nat`` in reverse.
551Given the following list:
558We can sort it using the default ``Ord`` implementation, then the named
559implementation ``myord`` as follows, at the Idris prompt:
563 *named_impl> show (sort testList)
564 "[sO, sssO, ssssO]" : String
565 *named_impl> show (sort @{myord} testList)
566 "[ssssO, sssO, sO]" : String
569Sometimes, we also need access to a named parent implementation. For example,
570the prelude defines the following ``Semigroup`` interface:
574 interface Semigroup ty where
575 (<+>) : ty -> ty -> ty
577Then it defines ``Monoid``, which extends ``Semigroup`` with a "neutral"
582 interface Semigroup ty => Monoid ty where
585We can define two different implementations of ``Semigroup`` and
586``Monoid`` for ``Nat``, one based on addition and one on multiplication:
590 [PlusNatSemi] Semigroup Nat where
593 [MultNatSemi] Semigroup Nat where
596The neutral value for addition is ``0``, but the neutral value for multiplication
597is ``1``. It's important, therefore, that when we define implementations
598of ``Monoid`` they extend the correct ``Semigroup`` implementation. We can
599do this with a ``using`` clause in the implementation as follows:
603 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
606 [MultNatMonoid] Monoid Nat using MultNatSemi where
609The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
610extend ``PlusNatSemi`` specifically.
612Determining Parameters
613======================
615When an interface has more than one parameter, it can help resolution if the
616parameters used to find an implementation are restricted. For example:
620 interface Monad m => MonadState s (m : Type -> Type) | m where
624In this interface, only ``m`` needs to be known to find an implementation of
625this interface, and ``s`` can then be determined from the implementation. This
626is declared with the ``| m`` after the interface declaration. We call ``m`` a
627*determining parameter* of the ``MonadState`` interface, because it is the
628parameter used to find an implementation.
631.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
632 with effects. J. Funct. Program. 18, 1 (January 2008),
633 1-13. DOI=10.1017/S0956796807006326
634 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