Monads In The π-Calculus

Mar 9, 2009 at 9:10 AM
Post a comment

While I was in the shower this morning, it occurred to me that I should make a note for myself about how monads work in the polyadic D-fusion calculus.

The type construction is simply a channel (να) for sending a value of the underlying type.
The unit function is a channel (να λ(λ(να))) for sending a value of the underlying type and receiving a responsive channel that carries the resulting monadic value.
The binding operation is a channel (να ν(να λ(λ(νβ)))) λ(λ(νβ))) for sending two values, 1) a monadic value of type α and 2) a channel for sending a value of the underlying type α and receiving a responsive channel that carries the resulting value of monadic type β; the binding operation channel also permits receiving a responsive channel that carries the resulting value of monadic type β.

Easy as cake.

Note: the process defined according to the type above for the binding operation always starts when both inputs are available. There are two possible optimizations here: one where the process begins immediately when the value of monadic type α becomes available and one that begins immediately when the bound channel becomes available. The description of these types is left as an exercise.

Update: I made some consistency errors in the first revision of this post, so I went back and edited it to correct errors.