Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/CombiningPipeM.idr

Last active November 8, 2017 13:23
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/0fc4e0b7dd6c78b6bebd03217a70b54c to your computer and use it in GitHub Desktop.
Save deque-blog/0fc4e0b7dd6c78b6bebd03217a70b54c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
CombiningPipeM.idr
(.|) : (Monad m) => PipeM a b r1 m r2 -> PipeM b c r2 m r3 -> PipeM a c r1 m r3
(.|) = pull where
mutual
pull : (Monad m) => PipeM a b r1 m r2 -> PipeM b c r2 m r3 -> PipeM a c r1 m r3
pull up (Yield next c) = Yield (up `pull` next) c -- Yield downstream
pull up (Action a) = lift a >>= \next => up `pull` next -- Produce effect downstream
pull up (Await cont) = up `push` cont -- Ask upstream for a value
pull up (Pure r) = Pure r
push : (Monad m) => PipeM a b r1 m r2 -> (Either r2 b -> PipeM b c r2 m r3) -> PipeM a c r1 m r3
push (Await cont) down = Await (\a => cont a `push` down) -- Await upstream
push (Action a) down = lift a >>= \next => next `push` down -- Produce effect upstream
push (Yield next b) down = next `pull` down (Right b) -- Give back control downstream
push (Pure r) down = Pure r `pull` down (Left r) -- Termination, send pipe result downstream
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment