@@ -2,20 +2,27 @@ module Effect.Monad
22
33import Effects
44
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
67
7−using (xs : List EFFECT, m : Type -> Type)
8− instance Functor (\a => EffM m a xs (\v => xs)) where
9− map f prog = do t <- prog
10− value (f t)
8+instance Functor (MonadEffT xs f) where
9+ map f (MkMonadEffT x) = MkMonadEffT (do x' <- x
10+ pure (f x'))
1111
12− instance Applicative (\a => EffM m a xs (\v => xs)) where
13− pure = value
14− (<*>) f a = do f' <- f
15− a' <- a
16− value (f' a')
12+instance Applicative (MonadEffT xs f) where
13+ pure x = MkMonadEffT (pure x)
14+ (<*>) (MkMonadEffT f) (MkMonadEffT x)
15+ = MkMonadEffT (do f' <- f
16+ x' <- x
17+ pure (f' x'))
1718
18− instance Monad (\a => Eff m a xs (\v => xs)) where
19− (>>=) = Effects.(>>=)
19+instance Monad (MonadEffT xs f) where
20+ (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x
21+ let MkMonadEffT fx = f x'
22+ fx)
2023
24+implicit monadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a
25+monadEffT = MkMonadEffT
2126
27+MonadEff : List EFFECT -> Type -> Type
28+MonadEff xs = MonadEffT xs id