Concurrency = Lists of Kleisli arrows

I spend a lot of time thinking about concurrency and the more I study it the more I discover that concurrency is just a fancy name for merging lists. I'm going to use my Proxy type to demonstrate that this is not just a superficial analogy.

Merging lists

Let's imagine that a thread is just a list of values:

type Thread a = [a]

Each a represents one atomic step in our thread.

Now let's assume we have two such threads and we need to schedule them. The simplest way to schedule them would be to interleave them:

zip :: Thread a -> Thread a -> Thread a
zip [] ys = ys
zip xs [] = xs
zip (x:xs) (y:ys) = x:y:zip xs ys

However, I can think of three obvious problems with this approach. First, it is not associative:

(xs `zip` ys) `zip` zs /= xs `zip` (ys `zip` zs)

Second, it assumes that all thread actions have equal priority, which probably isn't the case.

We can fix this by switching to cooperative threads which can either provide a value, yield "left" or yield "right":

data Step a = YieldL | Step a | YieldR

type Thread a = [Step a]

Now, we can merge threads in such a way that respects their yields:

(<>) :: Thread a -> Thread a -> Thread a
        []  <>         ys  = []
(YieldL:xs) <>         ys  = YieldL:(xs <> ys)
(Step a:xs) <>         ys  = Step a:(xs <> ys)
(YieldR:xs) <> (YieldL:ys) =        (xs <> ys)
-- From this point onward, xs = YieldR:xs'
        xs  <> (Step a:ys) = Step a:(xs <> ys)
        xs  <> (YieldR:ys) = YieldR:(xs <> ys)
        xs  <>         []  = []

Interestingly, this new operation is associative:

(xs <> ys) <> zs = xs <> (ys <> zs)

It also has an empty thread which acts like an identity:

mempty = YieldR:YieldL:mempty

mempty <> xs = xs
xs <> mempty = xs

Proxies

While working on Proxys, I discovered they had certain nice mathematical properties:

         return  <-<               g  = return
(respond  >=> f) <-<               g  = respond  >=> (f <-< g)
(lift . k >=> f) <-<               g  = lift . k >=> (f <-< g)
(request  >=> f) <-< (respond  >=> g) =              (f <-< g)
-- For the following equations, f = request >=> f'
              f  <-< (lift . k >=> g) = lift . k >=> (f <-< g)
              f  <-< (request  >=> g) = request  >=> (f <-< g)
              f  <-<          return  = return

Now, where have I seen that before? Why, these are identical the equations for the above list merge, except we need to make the following substitutions to make the analogy complete:

(>=>)     ->  (++)
return    ->  []
respond   ->  [YieldL]
request   ->  [YieldR]
lift . k  ->  [], [Step a], [Step a, Step a'] ...
(<-<)     ->  (<>)

Well, if those substitutions were correct, we'd expect that we could use them to derive the correct form for idT:

mempty = YieldR:YieldL:mempty
mempty = [YieldR] ++  [YieldL] ++  mempty
idT    = request  >=> respond  >=> idT

... and it works!

This is what I mean when I say that Proxy composition is just merging lists of Kleisli arrows.

Conclusions

I was a little bit skeptical at first when I had to give Proxys an extra input parameter to get them to be composable. However, the surprising connection to lists of Kleisli arrows convinced me that the Kleisli arrow is the true currency of concurrency.