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 ysHowever, 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
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 = returnNow, 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.
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.