Monads and Arrows

Monads and Arrows may both be used for metaprogramming: programs which produce programs. However, as Pfenning and Davies write in their POPL'96 Paper ( author's mirror),

Moggi's computational λ-calculus only distinguishes values from computations and does not allow us to express stage separation.

I'd like to show what this means, by example. Consider an Arrow operation

This function has a static component which depends on the value of X. This static component involves bar, which might be a very large and computationally expensive function. The type of foo guarantees that this static component can be performed before the value of type Y is available: the decision about which Arrow values to compose via (>>>), what order to compose them in, etc, is guaranteed to be made independently of the Y-value, and this guarantee is enforced by the type system.

Now consider the monadic equivalent of the program above:

Simply by looking at the type of this function, we can't be sure that the choices about how (>>=) and return are used will be made independently of the value of type Y. For all we know, the definition might be:

This is why Pfenning and Davies say that monadic types do not capture stage separation.

Consequences

Swierstra and Duponcheel have shown how to use this stage separation to write combinator parsers which do not rely on backtracking, making them much more efficient than monadic parsers and also capable of providing better error messages.

My own work further generalizes Arrows to generalized arrows, which remove the assumption that every host-language (i.e., Haskell) function may be promoted to a guest-language function. Without the stage separation provided by Arrows, this generalization would have been impossible. Additionally, generalized arrows are often used to produce programs in a guest language which lacks first-class functions (for example, Verilog); the machinery of monads – which leans very heavily on first-class functions – breaks down in this context.

rendered from WIX