parallel

For two computations run in parallel: Parallel l r k runs l and r in parallel, and goes on with k of their answers. A higher-order operation: how its computations run — one after the other, taking turns, or truly at once — is the handler’s to say. The types of what runs in parallel are the effect’s (parallel a b): a program that runs other types in parallel too has another parallel in its effect.

ParallelF

data ParallelF a b (m : Type -> Type) x = Parallel (m a) (m b) (a -> b -> x)

parallel

parallel : (a : Type) -> (b : Type) -> HFunctor

For two computations run in parallel, an a and a b: how, the handler says.

parallelIn

parallelIn : {a b : Type}
           -> {e : HFunctor}
           -> {{inj : parallel a b <: e}}
           -> Co e a
           -> Co e b
           -> Co e (a, b)

l and r in parallel, and both their answers, in any effect that has parallel a b (inj puts the operation there: a higher-order operation is made where it is, not lifted). Each side is handled first, its pure work done then: a handler into Co e that runs a side elsewhere runs there only what comes after an operation, or after later — parallelIn (later (\u -> fib n)) ....

inOrder

inOrder : {a b x : Type} -> {e : HFunctor} -> ParallelF a b (Co e) x -> Co e x

Parallel into Co e, one side after the other

inTurn

inTurn : (a : Type)
       -> (b : Type)
       -> (e : HFunctor)
       -> Handler (parallel a b <+> e)

Parallel handled one side after the other, into Co e: the rest of the world left as it is

runParallel

runParallel : {a b x : Type} -> ParallelF a b (\y -> y) x -> x

turns

turns : (a : Type) -> (b : Type) -> Handler (parallel a b)

Parallel handled one side after the other, in no monad: the answer

bothSides

bothSides : (Int -> Co (parallel Int Int <+> parallel Int Int) Int)
          -> Co (parallel Int Int <+> parallel Int Int) (Int, Int)

>>> const "handled" (handle (inTurn Int Int (parallel Int Int)) (bothSides (\n -> bind (val n) (\m -> pure (if m > 0 then abandon else m)))))
<abandoned>
>>> const "handled" (handle (inTurn Int Int (parallel Int Int)) (bothSides (\n -> later (\u -> if n > 0 then abandon else n))))
"handled"
>>> handle (turns Int Int) (handle (inTurn Int Int (parallel Int Int)) (bothSides (\n -> later (\u -> if n > 0 then abandon else n))))
<abandoned>
>>> handle (turns Int Int) (handle (inTurn Int Int (parallel Int Int)) (bothSides (\n -> later (\u -> n * 10))))
MkPair 10 20