Lifting continuations

In effect systems, there's a notion of "lifting" a collection of effects into a superset collection. For example, if there's an effect system that writes to and reads from a hard disk, it can be lifted into an effect system that writes to and reads from a hard disk and accesses environment variables.

There are a few canonical examples of lifting in functional programming. The lift function in the monad transformers library (mtl) lifts a monad into another one called a "transformer" that inherits and enriches the lifted monad's effects. For example, something of type IO () that represents synchronous interactions with the operating system can be lifted into Reader IO () that represents synchronous interactions with the OS and accessing some environment provided by the reader monad.

Lifting also happens in Variant-s with the function expand. We can take a Variant of type Variant r and expand it to type Variant s provided that r is a subset of s. Translated to natural language semantics, if one says "I'll go to the store or sleep", then it's legal to say "I'll go to the store or sleep or fly to Mars."

In most circumstances, lifting can't go the other direction. You can't "unlift" something of type Reader IO () to IO () - you need to provide some sort of environment to get out the IO (). Similarly, you can't automatically shrink Variant s to Variant r because whatever was in s that's not in r might still happen, at which point you'd get a runtime error. Whenever unlifting occurs, like the contract function in the Variant package, there is a cost. For example, contract may return an empty element at runtime.

myContract
  :: Variant (foo :: Int, bar :: Unit)
  -> Maybe (Variant (foo :: Int))
myContract = contract

myContract (inj (Proxy :: _ "foo") 1)
  -- Just (inj (Proxy :: _ "foo") 1)
myContract (inj (Proxy :: _ "bar") unit)
  -- Nothing

Lifting is useful when we have a bloc of code in the "lowered" monad and we need to raise it into some larger computation. It's often inefficient to perform many lift operations in a row, so lifting a bloc is a way to cut computational cost. It also makes it easier to refactor your code, as the unlifted side effects are mostly grouped together.

-- bad
do
  hello
  lift foo
  lift bar
  lift baz

-- good
do
  hello
  lift do
    foo
    bar
    baz

However, lifting becomes a challenge when we are working with continuation passing. This article will look at why lifting is useful in continuation passing, show some of the challenges with lifting in CPS, and show a solution we implemented in purescript-hyrule.

Lifting continuations

Lifting in continuation passing is useful for the same reason that it's useful in the contexts above: code that runs in a more lightweight effect system (ie IO ()) might be needed in the context of a more robust effect system (ie Reader IO ()). Specifically in our case with purescript-hyrule, we are working with two different effect systems: ST Global and Effect.

• ST Global is a purely functional effect system that allows for ad hoc memory locations to be created, read from and written to.
• Effect, in addition to doing what ST Global does, potentially interacts with the runtime, aka printing to the console, spawning threads, writing to a disk, and all sorts of unsafe-but-potent stuff that may crash a program.

hyrule originally implemented the Event type with a CPS signature (k -> Effect Unit) -> Effect (Effect Unit) whereby a continuation is passed in (k -> Effect Unit) that returns a subscriber (the outer Effect) that yields an unsubscriber (the inner Effect Unit). The type states, in rough terms, "if you give me a function k -> Effect Unit that I can call whenever an event comes down the pipe, I'll give you a way to turn me on and off.

A valid event type can also be written using ST Global instead of the effect via the signature (k -> ST Global Unit) -> ST Global (ST Global Unit). Events backed by ST Global are useful because we often times want to emit events in an entirely pure context, meaning one that exists (theoretically) outside of time. For example, when we are running large-scale simulations, we often do not want to use clock time but rather run the simulations as fast as possible. ST Global is a good candidate for these simulations. Another important use case for us is static site rendering. Static site rendering essentially captures the first burst of events on a website and renders them as HTML, which speeds up page loading substantially and helps with SEO.

ST in the land of Effect

Let's see if we can lift an event of type (k -> ST Global Unit) -> ST Global (ST Global Unit) to an event of type (k -> Effect Unit) -> Effect (Effect Unit). What we have to work with is a monadic lifting function, liftST, that takes us from ST Global to Effect.

Because our ST Global version of event is a function with ST Global in both the contravariant and covariant position, we need to do lifting in both places. We can start by trying to use dimap, which admits mapping functions for both positions.

liftSTEvent = dimap ? ?

The second question mark needs to take ST Global (ST Global Unit) to Effect (Effect Unit). This can be done with a function liftST <<< map liftST. So now we have:

liftSTEvent = dimap ? (liftST <<< map liftST)

But what about the first question mark? We need something from k -> Effect Unit to k -> ST Global Unit. A trivial way to do this is to simply ignore the k -> Effect Unit and use an "empty" function \_ -> pure unit for our k -> ST Global Unit. But this would stop the events from propagating, which defeats the purpose of the lifting. So we're stuck - while lifting works in the covariant position, the contravariant position leaves us scratching our heads. How do we get out of this con(travariant)undrum? Runtime proof to the rescue!

Proof of purity

The trick to make lifting in continuations work is to thread information about the purity of a computation through the continuation at runtime. This is similar to the shrinking we saw with the contract function from purescript-variant. We start with an event of type (k -> Effect Unit) -> Effect (Effect Unit) and we contract it to (k -> ST Global Unit) -> ST Global (ST Global Unit), making the decision to leave out some information in the process.

To do this, let's change the type of event to be Boolean -> (k -> Effect Unit) -> Effect (Effect Unit). The first Boolean is runtime information that a computation is either in ST Global (true) or Effect (false). This will be our source of truth about the purity of the event, and even though it is denoted in Effect, this type will be nominal - if the boolean is true, we'll be able to treat it as if it were ST Global (we'll see how when we visit the definition of subscribe later on).

To create events, we'll make two separate constructors - one in ST Global and one in Effect. Both constructors will hide the Boolean so that consumers of our library can't tamper with the purity or impurity of our computation.

Let's first look at the effectful constructor:

makeEvent
  :: ((k -> Effect Unit) -> Effect (Effect Unit))
  -> Booelan
  -> (k -> Effect Unit)
  -> Effect (Effect Unit)
makeEvent e tf k = if tf then pure (pure unit) else e k

What we're saying here is that, if our boolean flag is true (meaning the computation is pure), we don't run the impure side effects and instead return pure (pure unit). Otherwise, we can run the impure side effects.

Now let's look at the pure constructor.

makePureEvent
  :: ((k -> ST Global Unit) -> ST Global (ST Global Unit))
  -> Booelan
  -> (k -> Effect Unit)
  -> Effect (Effect Unit)
makePureEvent e _ = unsafeCoerce e

Woah woah woah, what?!? We suffered through a whole paragraph a few sections ago saying you can't "unlift" k -> Effect Unit to k -> ST Global Unit in our dimap and now you just use unsafeCoerce and prest-o change-o all of a sudden you can? What's the deal?

Let's zoom in on the k -> Effect Unit and convince ourselves that the unsafeCoerce is, in fact, safe here.

• Either the boolean is true, in which case we're performing a pure computation and everything can be treated as ST Global. That means that the k -> Effect Unit is only nominally Effect-ful, as by definition we'll have excluded all actual effects via the makeEffect smart constructor when tf is true. So we can safely call k -> Effect Unit in an ST Global context; or
• The boolean is false, which means we're in Effect land. This means that every pure computation in the continuation is de facto lifted from ST to Effect, which allows us to run k -> Effect Unit as-is.

By threading runtime information about purity through a computation, we're able to solve the lifting problem for continuation passing. However, there's one more thorny issue we have to tackle before our system is complete - that of subscriptions.

Subscribing in lifted continuations

As mentioned in the previous section, our events' smart constructors are of type (k -> ST Global Unit) -> ST Global (ST Global Unit) -> Event or (k -> Effect Unit) -> Effect (Effect Unit) -> Event. This obfuscates the internal Boolean represents purity at runtime. So how do we thread this information through a computation? That's where subscribe comes in. Just like we have two makeEvent functions, we'll also have two subscribe functions.

subscribePure
  :: Event
  -> (k -> ST Global Unit)
  -> ST Global (ST Global Unit)
subscribePure e f = unsafeCoerce $ e true (map liftST f)

We can use a similarly "safe" unsafe coerce to take our Effect (Effect Unit) to ST Global (ST Global Unit) because the true passed to the event guarantees that there won't be any impure computations thanks to the makeEvent smart constructor. The effectful subscription is more straightforward:

subscribe
  :: Event
  -> (k -> Effect Unit)
  -> Effect (Effect Unit)
subscribe e = e false

There's a snag here, though. What if I want to insert an intermediary computation in my chain? As a trivial example, let's say I want to add 1 to an event (there are easier ways to do this than what I'm showing here if you know that Event is a functor, but let's say we don't know that yet). I have two options:

add1Impure e = makeEvent
  \k -> subscribe e \i -> k (i + 1)
add1Pure e = makePureEvent
  \k -> subscribePure e \i -> k (i + 1)

They're both equally bad for opposite reasons:

• add1Impure will make the operation unreachable if we call subscribePure add1, which seems a bit silly, as the operation of adding 1 is pure.
• add1Pure will wipe out any Effect-s in e with its internal call to subscribePure. That means that, if we call subscribe on it, we'll lose all of the Effect-s in e.

PureFunctor from the PureScript community ran into this problem while hacking on the hyrule library and none of us could figure out a way to solve it. After thinking about it for a long, long time, I came up with makeLemmingEvent. The idea is that we inject a special subscriber s into our continuation passing chain. The subscriber punts on purity, deferring to the outer event.

add1 e = makeLemmingEvent
  \s k -> s e \i -> k (i + 1)

And makeLemmingEvent is defined as such:

makeLemmingEvent
  :: (
    (forall b. Event b -> (b -> ST Global Unit) -> ST Global (ST Global Unit))
     -> (a -> ST Global Unit)
     -> ST Global (ST Global Unit)
     )
  -> Event a
makeLemmingEvent f tf = f \e -> unsafeCoerce (e tf)

Here, the unsafeCoerce has the same signature as we saw in makePureEvent, and it follows the same logic - either the entire chain will be pure, in which case it's safe to consider an effect ST Global, or it will be impure, in which case all of the ST Global will become de facto Effect. The important bit is how tf is propagated: it is passed along to our special subscriber, which means that the subscriber doesn't make any assumptions about purity. This means that, if add1 is called in a pure context or impure context, it will always run and will not change the purity or impurity of the upstream subscription.

Continuation passing is already quite difficult to read, as you sort of have to turn your brain 90-degrees and inside-out to understand the control flow. makeLemmingEvent is even harder, as in addition to working with the continuation k, we need to work with s that continues the continuation. But it is the runtime key that unlocks lifting in a CPS context and allows us to write pure events that don't effect the purity or impurity of the entire computation.

Conclusion

We've been using this new CPS-lifting pattern in hyrule for a couple weeks now and it's allowed us to greatly simplify function signatures, speed up the implementation, and reduce the surface area of the API.

Lifting and CPS are core patterns in functional programming, but because of difficulties with lifting contravariant arguments, it's hard to do lift stuff in a CPS context. Hopefully, this article presents one way to solve that problem in your own CPS applications, allowing you to mix and match effect systems for fun and profit!

Many thanks to @monoidmusician, @purefunctor, @shanji, @xgrommx and @natefaubion for their ideas as I put this together.