Monad.idr

module Prelude.Monad

-- Monads and Functors

import Builtins
import Prelude.Functor
import public Prelude.Applicative
import Prelude.Basics
import IO

%access public export

infixl 5 >>=

interface Applicative m => Monad (m : Type -> Type) where
    ||| Also called `bind`.
    (>>=)  : m a -> ((result : a) -> m b) -> m b

    ||| Also called `flatten` or mu
    join : m (m a) -> m a

    -- default implementations
    (>>=) x f = join (f <$> x)
    join x = x >>= id

||| For compatibility with Haskell. Note that monads are **not** free to
||| define `return` and `pure` differently!
return : Monad m => a -> m a
return = pure
%deprecate return "Please use `pure`, which is equivalent."

flatten : Monad m => m (m a) -> m a
flatten = join
%deprecate flatten "Please use `join`, which is the standard name."

-- Annoyingly, these need to be here, so that we can use them in other
-- Prelude modules other than the top level.

Functor (IO' ffi) where
    map f io = io_bind io (\b => io_pure (f b))

Applicative (IO' ffi) where
    pure x = io_pure x
    f <*> a = io_bind f (\f' =>
                io_bind a (\a' =>
                  io_pure (f' a')))


Monad (IO' ffi) where
    b >>= k = io_bind b k