Melding Monads

2009 December 20

Are continuations really the mother of all monads?

Filed under: continuations, haskell, monads — lpsmith @ 8:34 am

So Issue 14 of the Monad Reader is out, which includes my paper “Lloyd Allison’s Corecursive Queues” with a few significant revisions. Compared to earlier versions mentioned on this blog, I moved a few sections around to improve the flow: the first 8 pages now contain an uninterrupted informal derivation of the queue operators. I also demonstrated a new fixpoint operator on continuations, an implementation of the standard mfix fixpoint on the codensity monad, and argued that mapCont cannot be implemented in terms of callCC.

However, this post focuses on the section that I moved, entitled “Monad Transformers” from pages 51 to 56. It’s basically a short rant about why I don’t like monad transformers, an argument that later culminates in a mostly broken corecursive queue transformer. In retrospect, it’s somewhat unfortunate that I did not reread the classic paper Monad Transformers and Modular Interpreters sometime before Issue 14 came out. I did read that paper approximately nine or ten years ago. Although the paper was helpful in understanding how monads could be shaped to my own ends, now that I actually understand the contents of the paper, it feels rather crufty.

Section 8.1 defines correctness criteria for a monad transformer and associated lifted operations, which I quote as follows:

The basic requirement of lifting is that any program which does not use the added features should behave in the same way after a monad transformer is applied.

The thrust of my argument is that this requirement is indeed very basic; one would hope that certain properties useful for reasoning inside a given monadic language would also be preserved. This additional requirement seems rather hopeless. However, the pièce de résistance of the argument is that the continuation transformer is incorrect by their own criteria, at least in the context of a lazy language such as Haskell or Gofer.

I demonstrate an expression that depends on the laziness of the lazy state monad, and fails to terminate after a continuation transformer is applied. (As an aside, it doesn’t matter if this is a ContT r (StateT st Identity) monad or StateT st (ContT r Identity), they are the same monad with the same operations.) In retrospect, this seems obvious: something written in the continuation passing style specifies an evaluation order independent of the host language, and applying the continuation transformer corresponds to a call-by-value CPS transformation of part of the program.

The example involves a definition that computes a right fold over a level-order traversal of a tree:

foldrByLevel :: (MonadState (Queue a) m)
             => (a -> [a])
             -> (a -> b -> b) -> b -> [a] -> m b 
foldrByLevel childrenOf f b as = fold as 
  where
    fold []     = deQ >>= maybe (return b)
                          (\a -> fold (childrenOf a))
    fold (a:as) = do 
                     enQ a 
                     b <- fold as
                     return (f a b)

If we use this definition to traverse an infinite tree, it will be productive when run with Control.Monad.State.Lazy, but will get stuck in an infinite non-productive loop when combined with Control.Monad.Cont. You can download a complete file that demonstrates this phenomenon. There are “simpler” expressions that demonstrate this, but the example I gave is itself interesting because it is useful in other contexts.

As demonstrated in my paper, the laziness can be restored by tweaking the definition of foldrByLevel to use mapCont. However, this is a leaky abstraction: in order to maintain the same behavior, we must modify existing code to make use of the “added” features in ways that are not backwards compatible. I do not know how to write a lazy state monad using continuations, or a sensible way of writing a single definition of foldrByLevel that behaves the same on both the lazy state monad and the continuation state monad.

(I use the word “sensible” because one could provide a unfaithful definition of mapCont for the lazy state monad that happens to work in the case of foldrByLevel, but fails in other contexts.)

What impact does this have on the notion that continuations are the mother of all monads? Is there a monad that corresponds to a call-by-name CPS transformation? Is it even possible to express the lazy state monad using continuations?

I do not yet have answers to these questions. One thing is clear, however: its tricky to generalize Filinski’s Representing Monads to lazy evaluation, if indeed it is possible to do so fully.

About these ads

4 Comments »

  1. > One thing is clear, however: its tricky to generalize Filinski’s Representing Monads to lazy evaluation, if indeed it is possible to do so fully.

    You should read Lazy Evaluation and Delimited Control by Garcia, Lumsdaine and Sabry. I don’t fully understand the paper yet, but I think it gives some sort of affirmative answer.

    Comment by Noam Zeilberger — 2009 December 22 @ 3:22 pm

  2. It was pointed out to me by Russell O’Connor, Dan Doel, and others that StateT st (Cont r) is in fact the exact same monad as ContT r (State st) in the context of the Monad Transformer Library. However, Mauro Jaskelioff in his paper Modular Monad Transformers argues in Section 4 that it is more natural for callCC to be lifted differently in the StateT st (Cont r) case, so that it differs from the instance of callCC for ContT r (State st). According to Jaskelioff, the MTL’s lifting is correct in the second case, but not in the first.

    The two liftings are also mentioned in Monad Transformers and Modular Interpreters in Section 8.3, which includes a few other references to where each has appeared in the literature.

    Comment by lpsmith — 2010 February 6 @ 4:47 pm

  3. In a conversation with Edward Kmett, he suggested that the Lazy State Monad is, arguably, not a monad in the categorical sense, because fmap id ≠ id. In particular, fmap id ⊥ = λ _ → (⊥,⊥).

    Comment by lpsmith — 2011 July 31 @ 11:09 am

  4. I’d like to clarify the comment by lpsmith. My point in Modular Monad Transformers, is that the lifting in the MTL of callCC through StateT behaved differently than other liftings of callCC in the library (that’s why I argue is not the correct one). Furthermore I provided a uniform way of lifting callCC through *any* monad transformer, which I think is the correct, uniform, way of doing it.
    Consequently, lifting callCC (as defined in the paper) should be a simple matter of post-composing lift.

    Comment by Mauro Jaskelioff — 2011 November 24 @ 10:03 am


RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

The Shocking Blue Green Theme. Blog at WordPress.com.

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: