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
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
ST Globalis 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 Globaldoes, 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
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 (
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 Unitis only nominally
Effect-ful, as by definition we'll have excluded all actual effects via the
makeEffectsmart constructor when
true. So we can safely call
k -> Effect Unitin an
ST Globalcontext; or
- The boolean is
false, which means we're in
Effectland. This means that every pure computation in the continuation is de facto lifted from
Effect, which allows us to run
k -> Effect Unitas-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:
add1Impurewill make the operation unreachable if we call
subscribePure add1, which seems a bit silly, as the operation of adding 1 is pure.
add1Purewill wipe out any
ewith its internal call to
subscribePure. That means that, if we call
subscribeon it, we'll lose all of the
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)
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)
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.
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.
Top comments (0)