Monad.ds

module Class.Monad
export  
{       dFunctorOfMonad; dApplicativeOfMonad;
        return; bind
}
import Class.Functor
import Class.Applicative
where


-- | Class of types that support associative sequencing.
data Monad (m: Data -> Data) where
        Monad
         :  Applicative m
         -> ([a: Data].   a   -> m a)                   -- return
         -> ([a b: Data]. m a -> (a -> m b) -> m b)     -- bind
         -> Monad m


-- | Take the Functor dictionary from a Monad dictionary.
dFunctorOfMonad 
        : [m: Data -> Data]
        . Monad m -> Functor m

dFunctorOfMonad dMonad
        = dFunctorOfApplicative (dApplicativeOfMonad dMonad)


-- | Take the Applicative dictionary from a Monad dictionary.
dApplicativeOfMonad
        : [m: Data -> Data]
        . Monad m -> Applicative m

dApplicativeOfMonad (Monad dApplicative _ _)
        = dApplicative


-- | Return a value in a monad.
return  : [m: Data -> Data]. [a: Data]
        . Monad m -> a -> m a

return (Monad _ return' _) x
 = return' x


-- | Evaluate a monadic compuation and pass the result to 
--   a function that produces a new monadic computation.
bind    : [m: Data -> Data]. [a b: Data]
        . Monad m -> m a -> (a -> m b) -> m b

bind    (Monad _ _ bind') ma mf 
 = bind' ma mf