.. _sect-interfaces: **********Interfaces********** We often want to define functions which work across several differentdata types. For example, we would like arithmetic operators to work on``Int``, ``Integer`` and ``Double`` at the very least. We would like``==`` to work on the majority of data types. We would like to be ableto display different types in a uniform way. To achieve this, we use *interfaces*, which are similar to type classes inHaskell or traits in Rust. To define an interface, we provide a collection ofoverloadable functions. A simple example is the ``Show``interface, which is defined in the prelude and provides an interface forconverting values to ``String``: .. code-block:: idris     interface Show a where        show : a -> String This generates a function of the following type (which we call a*method* of the ``Show`` interface): .. code-block:: idris     show : Show a => a -> String We can read this as: “under the constraint that ``a`` has an implementationof ``Show``, take an input ``a`` and return a ``String``.” An implementationof an interface is defined by giving definitions of the methods of the interface.For example, the ``Show`` implementation for ``Nat`` could be defined as: .. code-block:: idris     Show Nat where        show Z = "Z"        show (S k) = "s" ++ show k ::     Main> show (S (S (S Z)))    "sssZ" : String Only one implementation of an interface can be given for a type — implementations maynot overlap. Implementation declarations can themselves have constraints.To help with resolution, the arguments of an implementation must beconstructors (either data or type constructors) or variables(i.e. you cannot give an implementation for a function). Forexample, to define a ``Show`` implementation for vectors, we need to knowthat there is a ``Show`` implementation for the element type, because we aregoing to use it to convert each element to a ``String``: .. code-block:: idris     Show a => Show (Vect n a) where        show xs = "[" ++ show' xs ++ "]" where            show' : forall n . Vect n a -> String            show' Nil        = ""            show' (x :: Nil) = show x            show' (x :: xs)  = show x ++ ", " ++ show' xs Note that we need the explicit ``forall n .`` in the ``show'`` functionbecause otherwise the ``n`` is already in scope, and fixed to the value ofthe top level ``n``. Default Definitions=================== The Prelude defines an ``Eq`` interface which provides methods forcomparing values for equality or inequality, with implementations for all ofthe built-in types: .. code-block:: idris     interface Eq a where        (==) : a -> a -> Bool        (/=) : a -> a -> Bool To declare an implementation for a type, we have to give definitions of allof the methods. For example, for an implementation of ``Eq`` for ``Nat``: .. code-block:: idris     Eq Nat where        Z     == Z     = True        (S x) == (S y) = x == y        Z     == (S y) = False        (S x) == Z     = False         x /= y = not (x == y) It is hard to imagine many cases where the ``/=`` method will beanything other than the negation of the result of applying the ``==``method. It is therefore convenient to give a default definition foreach method in the interface declaration, in terms of the other method: .. code-block:: idris     interface Eq a where        (==) : a -> a -> Bool        (/=) : a -> a -> Bool         x /= y = not (x == y)        x == y = not (x /= y) A minimal complete implementation of ``Eq`` requires either``==`` or ``/=`` to be defined, but does not require both. If a methoddefinition is missing, and there is a default definition for it, thenthe default is used instead. Extending Interfaces==================== Interfaces can also be extended. A logical next step from an equalityrelation ``Eq`` is to define an ordering relation ``Ord``. We candefine an ``Ord`` interface which inherits methods from ``Eq`` as well asdefining some of its own: .. code-block:: idris     data Ordering = LT | EQ | GT .. code-block:: idris     interface Eq a => Ord a where        compare : a -> a -> Ordering         (<) : a -> a -> Bool        (>) : a -> a -> Bool        (<=) : a -> a -> Bool        (>=) : a -> a -> Bool        max : a -> a -> a        min : a -> a -> a The ``Ord`` interface allows us to compare two values and determine theirordering. Only the ``compare`` method is required; every other methodhas a default definition. Using this we can write functions such as``sort``, a function which sorts a list into increasing order,provided that the element type of the list is in the ``Ord`` interface. Wegive the constraints on the type variables left of the fat arrow``=>``, and the function type to the right of the fat arrow: .. code-block:: idris     sort : Ord a => List a -> List a Functions, interfaces and implementations can have multipleconstraints. Multiple constraints are written in brackets in a commaseparated list, for example: .. code-block:: idris     sortAndShow : (Ord a, Show a) => List a -> String    sortAndShow xs = show (sort xs) Constraints are, like types, first class objects in the language. You cansee this at the REPL: ::     Main> :t Ord    Prelude.Ord : Type -> Type So, ``(Ord a, Show a)`` is an ordinary pair of ``Types``, with two constraintsas the first and second element of the pair. Note: Interfaces and ``mutual`` blocks~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Idris is strictly "define before use", except in ``mutual`` blocks.In a ``mutual`` block, Idris elaborates in two passes: types on the firstpass and definitions on the second. When the mutual block contains aninterface declaration, it elaborates the interface header but none of themethod types on the first pass, and elaborates the method types and anydefault definitions on the second pass. Functors and Applicatives========================= So far, we have seen single parameter interfaces, where the parameteris of type ``Type``. In general, there can be any number of parameters(even zero), and the parameters can have *any* type. If the typeof the parameter is not ``Type``, we need to give an explicit typedeclaration. For example, the ``Functor`` interface is defined in theprelude: .. code-block:: idris     interface Functor (f : Type -> Type) where        map : (m : a -> b) -> f a -> f b A functor allows a function to be applied across a structure, forexample to apply a function to every element in a ``List``: .. code-block:: idris     Functor List where      map f []      = []      map f (x::xs) = f x :: map f xs ::     Idris> map (*2) [1..10]    [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer Having defined ``Functor``, we can define ``Applicative`` whichabstracts the notion of function application: .. code-block:: idris     infixl 2 <*>     interface Functor f => Applicative (f : Type -> Type) where        pure  : a -> f a        (<*>) : f (a -> b) -> f a -> f b .. _monadsdo: Monads and ``do``-notation========================== The ``Monad`` interface allows us to encapsulate binding and computation,and is the basis of ``do``-notation introduced in Section:ref:`sect-do`. It extends ``Applicative`` as defined above, and isdefined as follows: .. code-block:: idris     interface Applicative m => Monad (m : Type -> Type) where        (>>=)  : m a -> (a -> m b) -> m b Inside a ``do`` block, the following syntactic transformations areapplied: - ``x <- v; e`` becomes ``v >>= (\x => e)`` - ``v; e`` becomes ``v >>= (\_ => e)`` - ``let x = v; e`` becomes ``let x = v in e`` ``IO`` has an implementation of ``Monad``, defined using primitive functions.We can also define an implementation for ``Maybe``, as follows: .. code-block:: idris     Monad Maybe where        Nothing  >>= k = Nothing        (Just x) >>= k = k x Using this we can, for example, define a function which adds two``Maybe Int``, using the monad to encapsulate the error handling: .. code-block:: idris     m_add : Maybe Int -> Maybe Int -> Maybe Int    m_add x y = do x' <- x -- Extract value from x                   y' <- y -- Extract value from y                   pure (x' + y') -- Add them This function will extract the values from ``x`` and ``y``, if theyare both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the``do`` notation. ::     Main> m_add (Just 82) (Just 22)    Just 94    Main> m_add (Just 82) Nothing    Nothing Pattern Matching Bind~~~~~~~~~~~~~~~~~~~~~ Sometimes we want to pattern match immediately on the result of a functionin ``do`` notation. For example, let's say we have a function ``readNumber``which reads a number from the console, returning a value of the form``Just x`` if the number is valid, or ``Nothing`` otherwise: .. code-block:: idris     import Data.Strings     readNumber : IO (Maybe Nat)    readNumber = do      input <- getLine      if all isDigit (unpack input)         then pure (Just (stringToNatOrZ input))         else pure Nothing If we then use it to write a function to read two numbers, returning``Nothing`` if neither are valid, then we would like to pattern matchon the result of ``readNumber``: .. code-block:: idris     readNumbers : IO (Maybe (Nat, Nat))    readNumbers =      do x <- readNumber         case x of              Nothing => pure Nothing              Just x_ok => do y <- readNumber                              case y of                                   Nothing => pure Nothing                                   Just y_ok => pure (Just (x_ok, y_ok)) If there's a lot of error handling, this could get deeply nested very quickly!So instead, we can combine the bind and the pattern match in one line. For example,we could try pattern matching on values of the form ``Just x_ok``: .. code-block:: idris     readNumbers : IO (Maybe (Nat, Nat))    readNumbers      = do Just x_ok <- readNumber           Just y_ok <- readNumber           pure (Just (x_ok, y_ok)) There is still a problem, however, because we've now omitted the case for``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``case back as follows: .. code-block:: idris     readNumbers : IO (Maybe (Nat, Nat))    readNumbers      = do Just x_ok <- readNumber                | Nothing => pure Nothing           Just y_ok <- readNumber                | Nothing => pure Nothing           pure (Just (x_ok, y_ok)) The effect of this version of ``readNumbers`` is identical to the first (infact, it is syntactic sugar for it and directly translated back into that form).The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) givesthe preferred binding - if this matches, execution will continue with the restof the ``do`` block. The second part gives the alternative bindings, of whichthere may be more than one. ``!``-notation~~~~~~~~~~~~~~ In many cases, using ``do``-notation can make programs unnecessarilyverbose, particularly in cases such as ``m_add`` above where the valuebound is used once, immediately. In these cases, we can use ashorthand version, as follows: .. code-block:: idris     m_add : Maybe Int -> Maybe Int -> Maybe Int    m_add x y = pure (!x + !y) The notation ``!expr`` means that the expression ``expr`` should beevaluated and then implicitly bound. Conceptually, we can think of``!`` as being a prefix function with the following type: .. code-block:: idris     (!) : m a -> a Note, however, that it is not really a function, merely syntax! Inpractice, a subexpression ``!expr`` will lift ``expr`` as high aspossible within its current scope, bind it to a fresh name ``x``, andreplace ``!expr`` with ``x``. Expressions are lifted depth first, leftto right. In practice, ``!``-notation allows us to program in a moredirect style, while still giving a notational clue as to whichexpressions are monadic. For example, the expression: .. code-block:: idris     let y = 94 in f !(g !(print y) !x) is lifted to: .. code-block:: idris     let y = 94 in do y' <- print y                     x' <- x                     g' <- g y' x'                     f g' Monad comprehensions~~~~~~~~~~~~~~~~~~~~ The list comprehension notation we saw in Section:ref:`sect-more-expr` is more general, and applies to anything whichhas an implementation of both ``Monad`` and ``Alternative``: .. code-block:: idris     interface Applicative f => Alternative (f : Type -> Type) where        empty : f a        (<|>) : f a -> f a -> f a In general, a comprehension takes the form ``[ exp | qual1, qual2, …,qualn ]`` where ``quali`` can be one of: - A generator ``x <- e`` - A *guard*, which is an expression of type ``Bool`` - A let binding ``let x = e`` To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, firstany qualifier ``qual`` which is a *guard* is translated to ``guardqual``, using the following function: .. code-block:: idris     guard : Alternative f => Bool -> f () Then the comprehension is converted to ``do`` notation: .. code-block:: idris     do { qual1; qual2; ...; qualn; pure exp; } Using monad comprehensions, an alternative definition for ``m_add``would be: .. code-block:: idris     m_add : Maybe Int -> Maybe Int -> Maybe Int    m_add x y = [ x' + y' | x' <- x, y' <- y ] Idiom brackets============== While ``do`` notation gives an alternative meaning to sequencing,idioms give an alternative meaning to *application*. The notation andlarger example in this section is inspired by Conor McBride and RossPaterson’s paper “Applicative Programming with Effects” [#ConorRoss]_. First, let us revisit ``m_add`` above. All it is really doing isapplying an operator to two values extracted from ``Maybe Int``. Wecould abstract out the application: .. code-block:: idris     m_app : Maybe (a -> b) -> Maybe a -> Maybe b    m_app (Just f) (Just a) = Just (f a)    m_app _        _        = Nothing Using this, we can write an alternative ``m_add`` which uses thisalternative notion of function application, with explicit calls to``m_app``: .. code-block:: idris     m_add' : Maybe Int -> Maybe Int -> Maybe Int    m_add' x y = m_app (m_app (Just (+)) x) y Rather than having to insert ``m_app`` everywhere there is anapplication, we can use idiom brackets to do the job for us.To do this, we can give ``Maybe`` an implementation of ``Applicative``as follows, where ``<*>`` is defined in the same way as ``m_app``above (this is defined in the Idris library): .. code-block:: idris     Applicative Maybe where        pure = Just         (Just f) <*> (Just a) = Just (f a)        _        <*> _        = Nothing Using ``<*>`` we can use this implementation as follows, where a functionapplication ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>… <*> an``: .. code-block:: idris     m_add' : Maybe Int -> Maybe Int -> Maybe Int    m_add' x y = [| x + y |] An error-handling interpreter~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Idiom notation is commonly useful when defining evaluators. McBrideand Paterson describe such an evaluator [#ConorRoss]_, for a language similarto the following: .. code-block:: idris     data Expr = Var String      -- variables              | Val Int         -- values              | Add Expr Expr   -- addition Evaluation will take place relative to a context mapping variables(represented as ``String``\s) to ``Int`` values, and can possibly fail.We define a data type ``Eval`` to wrap an evaluator: .. code-block:: idris     data Eval : Type -> Type where

Lines 1–500 of 661. Load more