Monads may be construed as forms of containers: list : aggregation of items from a given type bag : unordered aggregation set : unordered aggregation that ignores multiplicity Maybe : aggregation of at-most one item Reader e : aggregations of cardinality |e| I am wondering how continuations are interpreted in this view as forms of packages / containers, in a meaningful fashion. Thanks!

Reputation: 982

continuations as meaningful comprehensions

Monads may be construed as forms of containers:

list : aggregation of items from a given type
bag : unordered aggregation
set : unordered aggregation that ignores multiplicity
Maybe : aggregation of at-most one item
Reader e : aggregations of cardinality |e|

I am wondering how continuations are interpreted in this view as forms of packages / containers, in a meaningful fashion. Thanks!

Upvotes: 9

Answers (2)

Cirdec

Reputation: 24156

The real key to understanding monads is to stop trying to say

A monad is X

and instead start saying

X is a monad

Something is a monad if it has a certain structure and obeys certain laws. For the purpose of programming in Haskell, something is a Monad if it has the right kind and types and obeys the Monad laws.

 return a >>= f ≡ f a
 m >>= return   ≡ m
(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

Gabriel Gonzales points out that the monad laws are "the category laws in disguise". We can use >=>, which is defined as follow, instead of >>=.

(f >=> g) = \x -> f x >>= g

When we do, the monad laws become the category laws with identity return and associative composition >=>.

return >=> f    ≡ f
f >=> return    ≡ f
f >=> (g >=> h) ≡ (f >=> g) >=> h

In your examples you are already discussing two different things for a monad to be: an aggregation that flattens and an aggregation that prunes. Instead of trying to say that monad is both of these things we'll say that both of these things are monads. To develop intuition about what things are monads, let's talk about the largest class of things that are all monads.

Trees with grafting

The largest class that are Monads are trees with grafting and simplification. This class is so big that every Monad that I know of in Haskell is a tree with grafting. Each of these monads includes a return which constructs a tree holding the value at the leaves and a bind >>= which does two things. Bind replaces each leaf with a new tree, grafting the new tree onto the tree where the leaf was, and simplies the resulting tree. The examples that you mention differ in how they simplify the tree. Which simplifications are allowed are governed by the Monad laws.

If we have a simple tree holding values at its leaves, it is a monad.

data Tree a = Branch [Tree a] | Leaf a

Its return constucts a single Leaf. Here's return 1:

Its bind replaces leaves with entire trees. We start with the following tree:

          *
         / \
        0   1

And bind this to \x -> Branch [x*2, x*2 + 1]. We replace each leaf with the newly calculated tree.

        __*__
       /     \
      *       *
     / \     / \
    0   1   2   3

For ordinary trees, the grafting step doesn't perform any simplification. After checking that these operations obey the monad laws we can say

A tree with grafting and no simplification is a monad

Flatten

Lists, bags, sets, Maybe, and Identity flatten all the levels of the resulting tree into a single level. Everything grafted anywhere onto the tree ends up in the same list or bag or set or Just. Sets also remove any duplicates from the resulting single-layer tree.

          *
         / \
       [0,  1]

If we bind this to \x -> [x*2, x*2 + 1] we replace each leaf with the new tree

        __*__
       /     \
      *       *
     / \     / \
   [0,  1] [2,  3]

and then flatten the intermediate layer

      ____*____
     /  |   |  \
   [0,  1,  2,  3]

We can say that

An aggregation that flattens is a tree with grafting and simplification

And, after checking the monad laws we can say that

An aggregation that flattens is a monad

Prune

Reader e and pairs like data Pair a = Pair a a are a little different. They can't flatten all of the results into a single layer, or at least can't do so immediately. Instead they prune branches that didn't branch the same direction as the parent.

If we start with a pair

          *
         / \
       <0,  1>

When we bind this to \x -> <x*2, x*2 + 1> we replace each leaf with the new tree

        __*__
       /     \
      *       *
     / \     / \
   <0,  1> <2,  3>

We prune the branches that didn't branch the same direction

        __*__
       /     \
      *       *
     /         \
   <0,          3>

And then can additionally simplify this by flattening the layers

          *
         / \
       <0,  3>

As you pointed out, Reader e a branches a number of directions equal to the number of possible values of e.

We can say that

An aggregation that prunes and flattens is a tree with grafting and simplification

And, after checking the monad laws we can say that

An aggregation that prunes and flattens is a monad

Continuations

The continuation monad is a tree that has a branch for each of the possible continuations. We will adopt the terminology Philip JF suggested for continuations. The continuation monad is the whole (a -> r) -> r. The continuation is the a -> r function passed in as the first argument

--                               continuation                                 
--                               |------|            
data Cont r a = Cont {runCont :: (a -> r) -> r}
--                               |-----------|
--                               continuation monad

The continuation monad has a number of branches equal to |r| ^ |a|, the number of possible values of the continuation a -> r. Each branch is labeled with a corresponding function. A continuation always holds the same value in every leaf, which we will justify in a moment. We will also be adding labels to the internal nodes of the tree, a function r -> r, which I'll discuss later.

We'll use the following data type to write out an example tree.

data Tri = A | B | C

Our example tree will be for return A :: Cont Bool Tri. The type of the values held in the tree, Tri, has three constructors, and the result of the contination monad, Bool, has two constructors. There are 2 ^ 3 = 8 possible functions Tri -> Bool, each of which makes up one branch of the tree.

                               id *
      ____________________________|____________________________
false |     a |     b |     c |  aOrB |  aOrC |  bOrC |  true |
      A       A       A       A       A       A       A       A

"The way to a Monad's heart is through its Kleisli arrows". Kleisli arrows are the things you can pass to the second argument of >>=; they have the type a -> m b. We are going to study the Kleisli arrows of Cont which have the type a -> Cont r b, or, when we look through the Cont constructor

a -> (b -> r) -> r

We can break the Kleisli arrows of the contination monad a -> (b -> r) -> r into two parts. The first part is the function that decides what b to pass into the continuation b -> r. The only thing it has to work with is the a argument, so it must be one of the functions g :: a -> b. The second part is the function that combines the results. It can see the argument a and the result of passing g a into the continuation. We will call this second function r :: a -> r -> r. All functions of type a -> (b -> r) -> r can be written in the form

a  -> (b -> r) -> r
\x -> \f       -> r x (f (g x))

for some g :: a -> b and r :: a -> r -> r.

Similarly, every continuation monad (a -> r) -> r can be written in the form

(a -> r) -> r
\f       -> r (f a)

for some a :: a and r :: r -> r. Combined these make up the justification that a continuation monad always holds the same value in every leaf.

When we bind a function \x -> \f -> r x (f (g x)) onto a continuation monad tree we will record g x as the new leaves and record (r x, g x) as the label for the new intermediate node. The trees are really big, but we'll draw the corner of another complete example using \x -> \f -> r x (f (g x)) :: Tri -> (Bit -> Bool) -> Bool where Bit only has two constructors. The resulting continuation monad should only have |Bool| ^ |Bit| = 4 branches, but we haven't simplified it yet.

                                            id *  
                _______________________________|_...
          false |                         a |
            r A *                       r A *
       _________|____________          _____|_...
bfalse |  b0 |  b1 |  btrue |   bfalse |  b0 |  
      g A   g A   g A      g A        g A   g A

Since every leaf holds the same value, the only differences between the paths through the tree are the functions labeling each branch. We will drop the labels from the branches and only draw a single branch. Our first example for return a will now be drawn as

        id *
           |
           A

And the example of binding \x -> \f -> r x (f (g x)) onto return A will be drawn as

Any continuation monad written in the form \f -> r (f a) for some a :: a and r :: r -> r will be represented by the tree

         r *
           |
           a

When bound to \x -> \f' -> r' x (f' (g' x)), it will be represented by the following tree (this is just grafting)

We are going to figure out what the simplification step is from the definition of >>= for Cont.

m >>= k = Cont $ \ c -> runCont m (\x -> runCont (k x) c)

(\f -> r (f a)) >>= (\x' -> \f' -> r' x' (f' (g' x')))
= \c -> (\f -> r (f a)) (\x -> (\x' -> \f' -> r' x' (f' (g' x'))) x c) -- by definition
= \c -> (\f -> r (f a)) (\x -> (       \f' -> r' x  (f' (g' x )))   c) -- beta reduction
= \c -> (\f -> r (f a)) (\x ->                r' x  (c  (g' x ))     ) -- beta reduction
= \c ->        r ((\x -> r' x  (c  (g' x))) a) -- beta reduction
= \c ->        r (       r' a  (c  (g' a))   ) -- beta reduction
= \c ->       (r .       r' a) (c  (g' a))     -- f (g x) = (f . g) x
= \c -> (r . r' a) (c (g' a))                  -- whitespace

which is in the form \f -> r (f a). Our tree will be simplified to

    r . r' a *
             |
           g' a

The continuation monad is a tree whose internal nodes are labeled with functions. Its bind operation is tree grafting followed by a simplification step. The simplification step composes the functions on the internal nodes. We can say that

The continuation monad is a tree with grafting and simplification

And, after checking the monad laws we can say that

The continuation monad is a monad

Upvotes: 6

jtobin

Reputation: 3273

I like to think of continuations as programs with holes in them. I think I originally gleaned this insight from Tekmo's blog.

Check out this little continuation:

import Control.Monad.Trans.Cont

program :: ContT () IO Char
program = ContT $ \doThing -> do
  c <- getChar
  doThing c

It's a program that's 'missing a piece' - namely, what to do with the Char retrieved from getChar. We can run it by filling the missing piece with something like putChar; evaluating the continuation via runContT program putChar will get a character and then print it to stdout.

If you're comfortable with representing programs by abstract syntax trees the container analogy might be intuitive.

To make it clearer, you can build up a little AST containing a DoThing term that represents a hole that needs to be filled:

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad.Free

data ExprF a =
    GetChar (Char -> a)
  | DoThing Char a
  deriving Functor

type Expr = Free ExprF

getChar' :: Expr Char
getChar' = liftF (GetChar id)

doThing' :: Char -> Expr ()
doThing' c = liftF (DoThing c ())

program' :: Expr ()
program' = do
  c <- getChar'
  doThing' c

program' is hopefully more clearly a container; to run it we need to process the AST in a similar fashion as we would any other recursive container:

eval :: Expr () -> (Char -> IO ()) -> IO ()
eval prog f = iterM alg prog where
  alg (GetChar k)   = getChar >>= k
  alg (DoThing c k) = f c >> k

Evaluating program' via eval program' putChar is analogous to running program via runContT program putChar.

Upvotes: 8

continuations as meaningful comprehensions

Answers (2)

Trees with grafting

Flatten

Prune

Continuations

Related Questions