PipeM.idr

data PipeM : (a, b, r1 : Type) -> (m : Type -> Type) -> (r2 : Type) -> Type where
  Pure    : r2 -> PipeM a b r1 m r2                                 -- Lift a value into the pipe
  Action  : m (Inf (PipeM a b r1 m r2)) -> PipeM a b r1 m r2        -- Interleave an effect
  Yield   : Inf (PipeM a b r1 m r2) -> b -> PipeM a b r1 m r2       -- Yield a value and next continuation
  Await   : (Either r1 a -> PipeM a b r1 m r2) -> PipeM a b r1 m r2 -- Yield a continuation (expecting a value)