idris-0.10: libs/effects/Effect/Trans.idr

module Effect.Trans

import Effects

%access public

data Trans : (Type -> Type) -> Effect where
  Lift : m a -> sig (Trans m) a

-- using (m : Type -> Type)
implementation Monad m => Handler (Trans m) m where
     handle st (Lift op) k = do x <- op
                                k x ()

TRANS : (Type -> Type) -> EFFECT
TRANS m = MkEff () (Trans m)

lift : m a -> Eff a [TRANS m]
lift op = call $ Lift op