Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/PipeM.idr

Last active Nov 8, 2017
Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment