on cd58dfb help sign in
20 lines 416 B history raw
1module Effect.Trans
3import Effects
5%access public export
7data Trans : (Type -> Type) -> Effect where
8 Lift : m a -> sig (Trans m) a
10-- using (m : Type -> Type)
11implementation Monad m => Handler (Trans m) m where
12 handle st (Lift op) k = do x <- op
13 k x ()
15TRANS : (Type -> Type) -> EFFECT
16TRANS m = MkEff () (Trans m)
18lift : m a -> Eff a [TRANS m]
19lift op = call $ Lift op