posts `for_` publish

ContT, withLifted and resetContIO (II)


Introduction

This is the second article in a series about continuations, forking, and monad transformers. Previous article. Today we will solve the “withLifted” riddle we posed at the very end of the last article.

Motivation

Recapitulating the conclusion from the last article. Given:

we can fork and “move”/“fork” any monadic operations who have a base of ContT () IO, allowing us for example to write this:

And we noted that in general, the “host” that runs the remaining effectful/stateful computation (in the above example forkIO) requires no knowledge of the specific monad at work - the interface of the host is a plain IO ().

With this somewhat surprising result, we started to wonder: How powerful exactly is ContT () IO, and can it solve other similar problems in the area of “lifting and unlifting” of transformer-stacks? The first thing we will consider in this area are “with” functions. Let us phrase the problem in haskell:

withLifted

Desired Semantics

Sometimes the type signature already is half of the solution, but in this case I will go ahead and directly propose:

If this has an implementation, then our motivating example could be written as:

Testcases:

  1. Proper ordering of acquire/release/what comes after:

    should print “acquire myResource, inside, release myResource, outside”

  2. Effects to pass through properly:

    should print “acquire myResource; release myResource; 1”

  3. Nesting poses no problem:

    should print “acquire a; acquire b; release b; release a; 1”

Towards a Solution

We will approach this in a few steps, because these steps help building intuition regarding expressiveness of ContT () IO in general. But feel free to step to the next section for the completed solution.

We will start with the blank template:

The first thing to note about this is that c is in m-monadic context, so any approaches where we have dropped down to IO will not work. For example, we will not be able to use c a in the right part of ContT $ \k ->. This directly mandates that our solution looks like this:

Focus on the first hole. We must get an a out, but our only “a-provider” is with :: forall r . (a -> IO r) -> IO r. So we need to drop to IO somehow anyway. So we are probably fine doing just that:

This directly leads to

attempt number 1

which type-checks. But does not work. Consider that k captures the entire remaining computation, including anything “below”. Meaning that

would print “acquire myResource; inside; outside; release myResource”.

Back to the drawing-board!

There is one escape-hatch we have not considered so far: The “second application” from the last article - we can “move” to a different thread. And we can move back. And nothing stops us from forking the “host” in beforehand as a first step. And from aligning things so that lifetime of this host thread aligns with that of resource allocated via with. Start with slightly modifying the relevant bits from the previous article:

We use MVars because only a single continuation will need to be processed.

Taking into account that the with currently (again) captures all that comes “below”, but the remaining hole should escape that, it is clear that we need some sort of interaction with code from above the forkIO. We can just write this:

So we pass something down, but we need to pass something up (the continuation at the point of invoking escape). So, another MVar. We will focus on the operation that produces escape and define it separately:

We will make one minor adjustment that makes both implementation and usage a bit shorter:

Which gives us:

attempt number 2 (almost!)

This comes close, but suffers from race-conditions. To explain, we visualize the nested resource acquisition example:

main thread
║                            resource "a" thread
║ evalContT                                                 resource "b" thread
║ │                          created
║ │                          ║ acquire a
║ └───── move via MVar ────┐ ║ takeMVar
┊                          │ ║ start running continuation
(blocked on takeMVar)      │ ║                              created
┊                          │ ║                              ║ acquire b
┊                          └───── move via MVar ──────────┐ ║ takeMVar
┊                            ┊                            │ ║ 
┊                            (blocked on takeMVar)        │ ║ inner part
┊                            ┊                            │ ║ 
┊                          ┌──────────────────────────────┘ ║ move back
┊ ┌────────────────────────┘ ║ directly move back           ║ release b
┊ │                          ║ release a                    x
║ │ any "outside" stuff      x
║ │

Note that the ordering of release a and release b is not in any way guaranteed. (Nor that of “outside stuff” versus the releases.) We could start throwing some more MVars at this - but we can also notice that we do not actually want any concurrency: The important stuff happens in createReturnPoint, while forkIO is superfluous:

Solution to the Riddle

The magic really lies within createReturnPoint: It runs the continuation, but passes it a “continuation-continuation” (consider the type a -> m a, where m is has a base that is ContT () IO). And afterwards, it grabs the continuation that the continuation-continuation has passed back upwards via MVar, and executes that. Crucially, this passing of the continuation back upwards escapes the scope of the with that we invoke in withLifted, resulting in exactly the desired ordering of IO (and non-IO) effects.

Properties and Interactions

Our implementation passes the three tests we wrote above. That gives us three properties already:

  1. withLifted retains the intended ordering of acquire/inner/release/outer effects.
  2. “inner” effects carry to the “outside”.
  3. nesting works - withLifted interacts well with withLifted.
    and we may mention that

  4. withLifted does not fork itself in any fashion (no uses of forkIO)
    Further, not too surprisingly:

  5. withLifted does not interact nicely with forkCont2 or plain moveTo-type functions. Consider

    or

    In the first case, there will be two threads writing to an MVar, but we only take (and continue) once. In the second case, “release” will fire as soon as moveToNewThread is reached, meaning that k happens concurrently/after the “release” part of the with. However this is not new - using forkIO in plain IO “with”-functions has the same behaviour, and invites use-after-free problems or similar. This really is not a downside of our implementation, but inherent property of “with” functions.

  6. In the same vein we have to assume that the user does only use actions that call the continuation exactly once - there is high risk for deadlocks and race-conditions otherwise.

createReturnPoint and resetContIO

Our usage of createReturnPoint suggest that there is one more notion in this area, because we can write:

Compare that to the resetT as defined in the transformers package:

So while they behave similar, there are two central differences:

  1. resetT is polymorphic over the monad “below” in the monad stack but assumes that ContT is on top, while resetContIO is polymorphic over the “above” transformers but assumes that ContT () IO is at the bottom.

  2. They behave the same in that they “return to the original host” which means that “host-final” operations are run (the “release” in withLifted). They behave different in that resetContIO blocks the original host, while resetT does not (see example below):

Interactions

withLifted interacts well with resetContIO, which is not surprising given that we implement the former using the latter and nesting already works.

In the interaction with moveTo type functions, resetT and resetContIO differ:

createReturnPoint on its own however can easily create deadlocks, for example the following code deadlocks:

On the other hand, creating a deadlock is not possible with resetContIO.

A Short Look at shiftT and callCC

Given the resetT/resetContIO pair, and the fact that MVars require the call-continuation-exactly-once constraint, we will now consider interactions of shiftT and callCC with the new constructs. For reference:

Bad news - deadlocks:

While the interaction with forkCont2 or moveToNewThread appears to be relatively harmless (no deadlocks, both remain in the same “host”), they do not bring much to the table either. Neither shiftT nor callCC can easily be lifted to our MonadContIO m => m level. Together with the potential for deadlocks this seems to be enough reason to stay away from these two functions in the context of ContT () IO.

Outlook

In the next article we will approach throw and try for ContT () IO. This time however I cannot pose a concise riddle, because the solution will be a good bit more complex - we will even have to switch to a somewhat more powerful base monad because ContT () IO is not good enough.

If you would like some exercise before continuing to the next article, I may suggest the following: Consider the types of try, throw, catch, finally, and bracket and how they change when being lifted. The easiest example is throw which would have a type like MonadContIO m => e -> m () (Clearly e would need to become an argument of MonadContIO somehow, otherwise this could not work, but we can ignore that for the moment). Next, think about which effects should propagate in what manner - for example we used modify (+ 1) above to highlight effect propagation. Now compare this intuition to how state propagates for existing “escape” type stacks, for example EitherT e (State s) or StateT s (Either e).

Posted by Lennart Spitzner on 2018-09-12. Feedback to (blog at thisdomain) welcome!
Tags: . Source.