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 whatST 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 thek -> Effect Unit
is only nominallyEffect
-ful, as by definition we'll have excluded all actual effects via themakeEffect
smart constructor whentf
istrue
. So we can safely callk -> Effect Unit
in anST Global
context; or - The boolean is
false
, which means we're inEffect
land. This means that every pure computation in the continuation is de facto lifted fromST
toEffect
, which allows us to runk -> 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 callsubscribePure add1
, which seems a bit silly, as the operation of adding 1 is pure. -
add1Pure
will wipe out anyEffect
-s ine
with its internal call tosubscribePure
. That means that, if we callsubscribe
on it, we'll lose all of theEffect
-s ine
.
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.
Top comments (0)