Home

Monads in Action

Monads in Action, Andrzej Filinski, POPL 2010.

In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be evaluated according to an effect-free semantics. Any effect-specific operations expressible in the monad are also given purely functional definitions, but these definitions are only directly executable in the context of an already translated program. This approach thus takes an inherently Church-style view of effects: the nominal meaning of every effectful term in the program depends crucially on its type.

We present here a complementary, operational view of monadic effects, in which an effect definition directly induces an imperative behavior of the new operations expressible in the monad. This behavior is formalized as additional operational rules for only the new constructs; it does not require any structural changes to the evaluation judgment. Specifically, we give a small-step operational semantics of a prototypical functional language supporting programmer-definable, layered effects, and show how this semantics naturally supports reasoning by familiar syntactic techniques, such as showing soundness of a Curry-style effect-type system by the progress+preservation method.

The idea of monadic reflection was one I never felt I really understood properly until I read this paper, so now I'll have to go back and re-read some of his older papers on the subject.

By neelk at 2010-02-03 13:17 | Semantics | Type Theory | other blogs | 13658 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Denotational versus non-denotational monads?

Out of curiousity, is there terminology for monads that represent computational effects that can be understood denotationally in the pure lambda calculus, and those that cannot?

For example, state, continuations and all the other familiar members of the Monad Transformer Library would be denotational monads, whereas IO and true randomness would not.

By Leon P Smith at Thu, 2010-02-04 19:52 | login or register to post comments

Expressible Monads

You might be interested in this nice result (also by Filinski).

I hope this answer wasn't cyclic.

By Ohad Kammar at Thu, 2010-02-04 20:33 | login or register to post comments

Representing Monads

Aye, I'm familiar with Filinski's paper. However, it's only concerned with "denotational" monads, and it's not clear (to me anyway) whether or not the result generalizes to lazy evaluation, as I've written about here and here.

By Leon P Smith at Thu, 2010-02-04 21:00 | login or register to post comments

Representing Monads

My understanding is that Filinski's work doesn't aim at actual evaluation but reasoning about monads, their composition and interaction. The "meta" word seems to be the guiding idea. Which is not to say that he didn't try to write a kind of emulation of monads at one point but that didn't seem to land anywhere. Representing doesn't equal evaluating and especially not evaluating in the pure functional context.

Monad Transformers can be better understood as composition constructs which ultimately require at least one actual monad as a terminal so to speak. That's the diff between representing/reasoning and evaluating/executing.

By Zarko at Wed, 2010-08-04 06:45 | login or register to post comments