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