@@ -2,20 +2,27 @@ module Effect.Monad
3import Effects
3import Effects
5−-- Eff is a monad too, so we can happily use it in a monad transformer.
5+data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where
6+ MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
7−using (xs : List EFFECT, m : Type -> Type)
8− instance Functor (\a => EffM m a xs (\v => xs)) where
8+instance Functor (MonadEffT xs f) where
9− map f prog = do t <- prog
9+ map f (MkMonadEffT x) = MkMonadEffT (do x' <- x
10− value (f t)
10+ pure (f x'))
12− instance Applicative (\a => EffM m a xs (\v => xs)) where
12+instance Applicative (MonadEffT xs f) where
13− pure = value
13+ pure x = MkMonadEffT (pure x)
14− (<*>) f a = do f' <- f
14+ (<*>) (MkMonadEffT f) (MkMonadEffT x)
15− a' <- a
15+ = MkMonadEffT (do f' <- f
16− value (f' a')
16+ x' <- x
18− instance Monad (\a => Eff m a xs (\v => xs)) where
19+instance Monad (MonadEffT xs f) where
19− (>>=) = Effects.(>>=)
20+ (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x
21+ let MkMonadEffT fx = f x'
24+implicit monadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
25+monadEffT = MkMonadEffT
27+MonadEff : List EFFECT -> Type -> Type
28+MonadEff xs = MonadEffT xs id