How does continuation monad really work

Question

I understand how Reader or Maybe or State monads work, but havig hard times with Continuations monad. Examples like below, blow my head

type ContinuationMonad() =
   member this.Bind (m, f) = fun c -> m (fun a -> f a c)
   member this.Return x = fun k -> k x

I think that my problem is that I cannot get what is a monadic type for Continuation (like Cont<'T>) and how i can unwrap it and wrap back. Any helpful examples or links are highly appreciated.

Answer 1

I will not repeat what has been said elsewhere - the post mentioned in the comments gives a lot of details about the continuation monad. But one thing that might help is to rewrite your code snippet with an explicit definition for Cont<'T>:

type Cont<'T> = 
  Cont of (('T -> unit) -> unit)

The type Cont<'T> represents a computation. You can start it by giving it a function 'T -> unit that takes the result and does something with it (say, prints it). When you start it, it returns unit and it will (at some point) produce a value 'T and call the continuation you provided.

With this more explicit definition, the builder can be defined as:

type ContinuationMonad() =
   member this.Bind (ma, f) = 
      Cont(fun k -> 
        let (Cont ca) = ma
        ca (fun a -> 
            let (Cont cb) = f a
            cb k))

   member this.Return x = 
      Cont(fun k -> k x)

• The Return member creates a computation that, when given a continuation k, calls this continuation immediately with the value x that we returned.

• The Bind member returns a new computation that, when given a continuation k, starts the computation specified by m; when this computation produces a value a, it calls the function f and then calls the computation returned by f with the original continuation k (which is the "final" continuation that should eventually be called with the final result).

Answer 2

I found Tomas's answer helpful, with a few important caveats:

• Using the name Cont to represent a computation is IMHO confusing because it suggests (incorrectly) that a Cont is a contination. I propose to use the name Inc instead, because it represents an "incomplete" computation. This computation contains a value (of type 'T) that it is ready to pass on to a continuation. Important point: An Inc is not the same thing as a continuation.

• I would also propose to define Inc without the pattern matching overhead of a discriminated union. This simplifies the implementation of Bind considerably.

• I'm also not sure why we should assume that a continuation always produces unit, but it certainly simplifies things considerably, so I'll keep this assumption in what follows.

So, we can define a continuation as any function with a signature of 'T -> unit, and we can define Inc as:

type Inc<'T> = 
    ('T -> unit) -> unit

In English, an Inc passes its wrapped 'T value to a given continuation function, resulting in unit.

Next, we need an explicit signature for the Bind function. Because it's a monad, we know it has to look like this:

let bind (inc : Inc<'T>) (wrap : 'T -> Inc<'U>) : Inc<'U> =

So bind takes an incomplete computation (of type 'T) and a function that can "wrap" a raw value in an incomplete computation (of type 'U), and returns a new incomplete computation of that type. Based on this signature, we know that bind has to return an Inc, and an Inc is a function that takes a continuation as input. So we know that implementation of bind has to start like this:

    fun (cont : 'U -> unit) -> ...

Our job is to extract the 'T value that's wrapped inside the given Inc, and then re-wrap it using the given wrapper function. Key insight: The only way to obtain this value is to ask the Inc to pass it to us via a continuation that we'll now write! Inside this "artificial" continuation, we re-wrap the extracted value and give it back to the caller. The completed bind function therefore looks like this:

let bind (inc : Inc<'T>) (wrap : 'T -> Inc<'U>) : Inc<'U> =
    fun (cont : 'U -> unit) ->   // return an Inc, which is a function that takes a continuation as input
        inc (fun t ->            // force the incomplete computation to cough up its wrapped value
            (wrap t) cont)       // wrap the raw value so it can be sent to the given continuation