Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/PipeM.idr

Last active November 8, 2017 13:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save deque-blog/336eca363653ee71cf226bb5b29ca398 to your computer and use it in GitHub Desktop.
Save deque-blog/336eca363653ee71cf226bb5b29ca398 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment