Algebraic effect handlers is a programming paradigm where programmers can declare their own syntactic operations, and modularly define the semantics of these using effect handlers.
However, we cannot directly define algebraic effect handlers for many higher-order operations (or higher-order effects)—i.e., operations that have computations as parameters.
Examples of such higher-order effects include common programming features, such as try-catch exception handlers, function abstraction, and more.
In this paper we present a new kind of effect handler that addresses this shortcoming.
Our effect handler approach is closely related to previous work on scoped effect handlers, which also supports higher-order effects.
A key difference is that our effect handlers make it easy to understand separate (higher-order) effects as separate concerns, since effects do not interact.
In contrast, effect interaction is the default with scoped effect handlers.
While separate concerns is the default with our handlers, it is also possible to define handlers where effects interact.

§ INTRODUCTION

Algebraic effects and handlers <cit.> is an approach to separately define and modularly compose the syntax and semantics of effectful operations.
Using the approach, programmers can declare their own syntax of operations and use these to write concise and effectful programs.
For example, by declaring a  operation that represents generating a random number, and  and  operations that represent pushing and popping elements from a stack, we can write a small program that represents mutating the state of an underlying stack:

[3]prog_0=𝐥𝐞𝐭 x=rand 𝐢𝐧 push x;pop;pop[E]

We can give meaning to this program by writing two separate algebraic effect handlers; e.g., a handler  that defines the effects of the  operation, and a handler  that defines the effects of the  and  operations.
By applying these handlers one after the other to our small program, we get as output the value that is on top of the the initial stack of the program:

[3]hStack [1.5mu 11.5mu] (hRand prog_0) 1[E]
Many algebraic effect handlers, such as  and , can be defined in a way that the order we apply handlers in is irrelevant.
For example, we can safely swap the order of  and  in above to give the same final result, since  and  have separate concerns.
This support for separation of concerns makes algebraic effect handlers attractive as a programming paradigm, and as a paradigm for building (domain-specific) languages from modular language components whose syntax and semantics is modularly defined in terms of effect handlers.
However, using algebraic effect handlers alone, it is challenging to define language components for some common effects found in programming languages, such as exception handling.

Consider again our program above: what happens if we  from an empty stack?
One reasonable expectation is that  should raise an exception that we can catch in our program.
To this end, we wish to introduce a new  operation that we use as follows to catch a potential exception raised by :

[3]prog_1=𝐥𝐞𝐭 x=rand 𝐢𝐧 push x;catch pop;pop 0[E]

However,  is a higher-order operation; i.e., an operation that has computations as parameters.
Many higher-order operations, such as , are not algebraic, so we cannot directly declare such operations and define them in terms of an algebraic effect handlers.

An alternative way to declare and define  is to use scoped effect handlers <cit.>.
With scoped effects, we can define a handler  for .
Using that effect handler, what should be the result of running the following program if the initial stack is empty?

With scoped effects, the answer depends on what order you run handlers in.
Assuming  returns a  wrapped value if no exception propagates to the top-level and  otherwise, and assuming that  generates the number , these are the results of nesting the  and  handlers in different orders:

[3]hCatch (hStack [1.5mu 1.5mu] (hRand prog_2)) Just 1337[E]

[3]hStack [1.5mu 1.5mu] (hCatch (hRand prog_2)) Nothing[E]

The reason for this difference is that there is effect interaction between the  and  handlers.
By running  before , causes an exception being raised during evaluation of the first sub-computation in a  operation to “snap back” to the state it was in before the .

The example above illustrates how scoped effects provide integrated support for effect interaction, such as the interaction between the stateful stack and the exception catching effects.
This integrated support for effect interaction makes it possible to concisely define different semantics.
But it also precludes defining and understanding exception handling and other non-algebraic higher-order effects as separate concerns.

In this paper, we introduce , a core calculus for handlers of higher-order effects, that makes it possible to declare and handle higher-order operations, such as , in a way that we can understand their semantics as a concern that is separate from other effects.
That is, in a way that operations, such as , does not interact with other effects.

The key difference between scoped effect handlers and the handlers of higher-order effects in , is that our handlers treat sub-computations, such as  and  in  as “delayed” computations whose operations are only handled once the handler of  forces the sub-computations to run.
In contrast, scoped effects treat  and  as “scoped” computations that we may pre-apply handlers to, before the handler of  forces the sub-computations to run.
Thus, with our handlers, effects generally have a “global” interpretation, in contrast to the “scoped” interpretation of scoped effects.
However, as we illustrate in <ref>, handlers in  can also be used to encode a “scoped” effect semantics.

We make the following technical contributions:

* We illustrate in <ref> how common algebraic and higher-order effects can be defined using handlers of higher-order effects in , and how to encode handlers with a scoped effect interpretation using handlers of higher-order effects.

* We present (in <ref>) —a core calculus and type discipline for handlers of higher-order effects.  The paper is also accompanied by a prototype interpreter (attached as anonymous supplemental material) that encodes the reduction rules of the core calculus.

* We formalize in <ref> what it means for handlers to have separate concerns, and provide sufficient criteria for proving that a given handler provides separation of concerns.

* We prove in <ref> that handlers for common algebraic and higher-order effects provides separation of concerns, and illustrate how certain handlers inherently interact with other effects.

§ PROGRAMMING WITH HANDLERS OF (HIGHER-ORDER) EFFECTS

This section gives an informal overview of our approach and shows how it compares with closely related existing solutions.
We postpone a formal discussion of dynamic semantics and types to Section <ref>.

§.§ Handling State

As a first example we consider how to handle the state effect.
The example serves two purposes: (1) it acts as an introduction to effect handlers for the unfamiliar reader; and (2) it acts as an introduction to the  language whose core calculus we introduce in the next section.

The state effect has two operations,  and , which retrieve and store a value respectively.
We can use these operations to define a computation which increments the current state by one:

[B]incr={1.5mu 𝐥𝐞𝐭 x=get! 𝐢𝐧 (put (x+1))!1.5mu}[E]

Here,  and  delimit a suspension; i.e., a block of code that is treated as a value, akin to a 0-argument function value.[Our syntax and semantics of suspensions is inspired by the corresponding feature and syntax used in Frank <cit.>]
We use  to enact a suspension, akin to calling a 0-argument function value.
In , computations are pure by default, and only suspensions are allowed to invoke effectful operations.
(This purity restriction is enforced by the type discipline we introduce in <ref>.)
Since the  program calls the effectful operations  and , it is wrapped in a suspension.
Each of the calls to  and  operations are postfixed by  since operations in  are represented as suspensions.

In order to run the  program, we need to define a handler for the  and  operations.
Below we define a function  which takes as input an initial state  and a suspension  which may call  and :

[B]hState s_0 prog=[E]

[3]handle {1.5mu [E]

[5]get [13]
[13]s k[18]
[18]↦k s {1.5mu s1.5mu},[E]

[5]put s' [13]
[13]s k[18]
[18]↦k s' {1.5mu ()1.5mu},[E]

[5]return x s[18]
[18]↦{1.5mu (x,s)1.5mu}[E]

[3]1.5mu} s_0 prog![E]

When  is called, it enacts the suspended  argument in the context of a  expression, which installs a handler of the  and  operations (the  clause does not represent an operation; we describe its meaning shortly).
The installed handler is parameterized by a value , which represents the “current” state at the point where we start to evaluate .

When we encounter a  or  operation during evaluation of , we “jump” to the handler installed by , and evaluate the clause corresponding to the performed operation.
Each clause binds variables that represent the following: (1) the parameters that the operation being performed was applied to (e.g., the  parameter of the  clause); (2) the “current” parameter of the handler (e.g., the  bound in the  and  clauses); and (3) a continuation (the  bound in the  and  clauses).
The continuation represents the program context in which an operation is performed, and expects two arguments: an argument to be used instead of the “current” effect handler parameter, and a computation to be run in the “resumed” context.

We can think of an effect handler as behaving similarly to an exception handler: performing an operation is similar to throwing an exception, and handling an operation is similar to handling an exception.
The important difference between exception handlers and effect handlers is that effect handlers provide access to the continuation representing the program context where the operation is being performed.
In contrast, when we raise an exception, the program context that the exception was raised in is discarded, and can never be resumed.
By calling a continuation from an effect handler clause, effect handlers can “resume” the program in the context of a handler with an updated parameter.

For example, during evaluation of , when we encounter the  operation in , we evaluate the right hand side expression of the  clause of the installed  expression.
In this right hand side expression,  is bound to , and  is bound to a continuation .

A key difference between  and existing effect handlers that we are aware of, is that the continuation bound by handler clauses in existing effect handlers expect a value.
Effect handlers in  differ: continuations bound by handler clauses in  expect a suspension.
This suspension will be enacted in the context where the handled operation occurred.
The  handler does not make essential use of this added generality.
In <ref> we consider a different example where we do make use of it.

The  clause of  defines what should happen when a computation returns a pure value.
In this case we pack the return value  and the final state  together in a tuple.
This tuple is wrapped in a suspension, because in general all handler clauses return suspended computations (in the case of the  and  clauses, the continuation  returns a suspended computation).

Any algebraic effect handler can be expressed in our system as a handler that passes a suspended value to the continuation.
In the next section we discuss a handler for a more interesting effect where we pass a computation to a continuation instead.

§.§ Handling Exception Catching

A common higher-order effect is exception catching. The effect consists of two operations,  and . The  operation has no arguments and just raises an exception which “jumps” to the nearest exception handler, or aborts if there is none.
We say that the exception catching effect is a higher-order effect because the  operation has two higher-order arguments.
In Haskell, we might type this higher-order effect using the following type signature:[Haskell's popular monad transformer library defines similar type classes for an exception operation that can carry a value: <https://hackage.haskell.org/package/mtl/docs/Control-Monad-Except.html>]
[B]𝐜𝐥𝐚𝐬𝐬 MonadCatch m 𝐰𝐡𝐞𝐫𝐞[E]

[11]::m a[E]

[11]::m a→m a→m a[E]
The type of  tells us that the  operation is parameterized by computations that have the same type as the  operation itself, which is why we call it a “higher-order” operation.
Our  operation is higher-order in the same sense.
However, we save the discussion of how operations are typed in  to <ref>.
Here, we illustrate how we can define a handler for the exception catching operation.
Consider the following:

[B]catch {1.5mu 𝐥𝐞𝐭 x=throw! 𝐢𝐧 x+11.5mu} {1.5mu 11.5mu}[E]

Because the  operation is inside the  block, the program should produce the value 1 yielded by the second suspension argument of  (which we will call the fallback computation of ).
To match this behaviour, the  operation should be handled by running the computation in the first argument; and if that computation raises an exception, the fallback computation is run.
The following handler implements this behavior:

[B]hCatch prog=[E]

[3]handle {1.5mu [E]

[5]throw [18]
[18]k↦{1.5mu Nothing1.5mu},[E]

[5]catch m_1 m_2 [18]
[18]k↦k {1.5mu [E]

[7]match (hCatch m_1)![E]

[7]|Just x→x[E]

[5]return x↦{1.5mu Just x1.5mu}[E]

[3]1.5mu} prog![E]

The first clause of the handler discards the continuation  and simply returns a suspended .
As with the  handler, the  handler may not handle all the effects in , and since  may have more effects than the exception catching effect, the  handler yields a suspension that represents the computation resulting from handling all exception catching effects.

The second clause of  passes a suspension to  which matches on the result of calling  recursively on .
If  throws an exception, then the result of  will be .  In this case, we catch the exception and run  in the context given by the continuation .
Note that the continuation  may be a program context that itself contains handlers.
By passing the suspension to  which runs  and , these computations will be run in the context of the continuation .
This ensures that those operations performed during evaluation of  and  which  has handlers installed for, will be handled by the installed handlers in .

To see why it is necessary to run  and  in the context of , consider the following program:
[B](hCatch (hState 0 (catch (put 1) {1.5mu ()1.5mu})))![E]
After installing the  and  handlers, the  operation will be handled.
This causes the  clause of  to be run where  is bound to ,  is bound to , and  is bound to .
Now, if we were to run  directly, rather than pass it in a suspension to , the  operation would escape the  handler!
The static type discipline that we introduce in <ref> ensures that it is not possible for effects to escape in this way, and that the  handler above is well-typed and guaranteed to not go wrong.

If no exceptions are raised while evaluating the  that  accepts as argument, we wrap the return value of  in a .

§.§ Effect Interaction and Separation of Concerns

The  handler in the previous section treats exception catching as a separate concern, in the sense that the order in which we apply handlers is irrelevant for the  effect and other handlers that treat their effects as separate concerns.
In <ref> we define formally what it means for a handler to treat its effects as a separate concern.
Here, we illustrate it by example.
Consider the following program:

[B]transact={1.5mu [E]

[3]𝐥𝐞𝐭 ()=(put 1)! 𝐢𝐧[E]

[3]𝐥𝐞𝐭 ()=(catch {1.5mu 𝐥𝐞𝐭 ()=(put 2)! 𝐢𝐧 throw!1.5mu} {1.5mu ()1.5mu})! 𝐢𝐧[E]

The program produces similar results, independently of how we order  and :
[B](hCatch (hState 0 transact))! Just (2,2)[E]

[B](hState 0 (hCatch transact))! (Just 2,2)[E]
While changing the order of the handlers changes the type of the result, it does not change the essential final return value of the computation.
To put it differently, the  handler has no effect interaction.

The lack of effect interaction is both a blessing and a curse.
On one hand we do not have to worry about how we order our handlers in order to understand the semantics of .
On the other hand we seem to lose some expressiveness.
Concretely, for some applications, we may wish to treat exceptions in a “transactional” manner, where raising an exception represents aborting a transaction and snapping back the state to what it was before entering a .
With scoped effects and with Haskell's monad transformers <cit.>, we can get this transactional semantics by reordering handlers or monad transformers.
Thus, with scoped effect handlers, reordering handlers would give us two different semantics:

[B](hCatch (hState 0 transact))! Just (1,1)[E]

[B](hState 0 (hCatch transact))! (Just 2,2)[E]

In this subsection we show that we can define handlers in a way that we get a similar effect interaction by default, mimicking the semantics of scoped effect handlers and monad transformers.

A naive way to achieve interaction between the state effect and the exception catching effect, is to define an exception handler that explicitly interacts with state:

[B]hCatch_1 prog=[E]

[3]handle {1.5mu [E]

[5]throw [18]
[18]k↦{1.5mu Nothing1.5mu},[E]

[5]catch m_1 m_2 [18]
[18]k↦k {1.5mu [E]

[7] 𝐥𝐞𝐭 s=get! 𝐢𝐧 [E]

[7]match (hCatch_1 m_1)![E]

[7]|Nothing→ 𝐥𝐞𝐭 ()=(put s)! 𝐢𝐧  m_2![E]

[7]|Just x→x[E]

[5]return x↦{1.5mu Just x1.5mu}[E]

[3]1.5mu} prog![E]

This explicit interaction between exception and state has two drawbacks. Firstly, It forces us to always run  after . Secondly, it only provides interaction between these two effects.
We can, however, define a handler that provides a effect interaction in general.

The idea is to define the handler clause of a  operation in a way that it explicitly “restarts” the continuation in case  throws an exception.

To do so we add an additional  operation to our exception catching effect, which mediates this restarting.

[B]hCatch_2 prog=[E]

[3]handle {1.5mu [E]

[5]throw [18]
[18]k↦{1.5mu Nothing1.5mu},[E]

[5]catch m_1 m_2 [18]
[18]k↦k {1.5mu [E]

[7]match (hCatch_2 m_1)![E]

[7]|Nothing→(abort (k m_2))![E]

[7]|Just x→x[E]

[5]abort m k↦m,[E]

[5]return x↦{1.5mu Just x1.5mu}[E]

[3]1.5mu} prog![E]

Using this handler, evaluation of our  program first handles the  effect, to yield the following program state:

[B]hCatch_2 {1.5mu hState 1 {1.5mu [E]

[5]𝐥𝐞𝐭 ()=(catch {1.5mu 𝐥𝐞𝐭 ()=(put 2)! 𝐢𝐧 throw!1.5mu} {1.5mu ()1.5mu})! 𝐢𝐧[E]

Next, the  handler starts handling the , to give this sequence of steps, where the highlights indicate which operation synchronizes with which handler in each step.
[B]hCatch_2 {1.5mu hState 1 {1.5mu [E]

[5]𝐥𝐞𝐭 ()=match (hCatch_2 {1.5mu 𝐥𝐞𝐭 ()=(put 2)! 𝐢𝐧 throw!1.5mu})![E]

[7]|Nothing→(abort (hCatch_2 {1.5mu hState 1 {1.5mu 𝐥𝐞𝐭 ()={1.5mu ()1.5mu}! 𝐢𝐧 get!1.5mu}1.5mu}))![E]

[7]|Just x→x[E]

[5]𝐢𝐧 get!1.5mu}1.5mu}[E]

[B] ⟼[E]

[B]hCatch_2 {1.5mu hState 2 {1.5mu [E]

[5]𝐥𝐞𝐭 ()=match hCatch_2 {1.5mu throw!1.5mu}![E]

[7]|Nothing→(abort (hCatch_2 {1.5mu hState 1 {1.5mu 𝐥𝐞𝐭 ()={1.5mu ()1.5mu}! 𝐢𝐧 get!1.5mu}1.5mu}))![E]

[7]|Just x→x[E]

[5]𝐢𝐧 get!1.5mu}1.5mu}[E]

[B] ⟼[E]

[B]hCatch_2 {1.5mu hState 2 {1.5mu [E]

[5]𝐥𝐞𝐭 ()=match Nothing[E]

[7]|Nothing→(abort (hCatch_2 {1.5mu hState 1 {1.5mu 𝐥𝐞𝐭 ()={1.5mu ()1.5mu}! 𝐢𝐧 get!1.5mu}1.5mu}))![E]

[7]|Just x→x[E]

[5]𝐢𝐧 get!1.5mu}1.5mu}[E]

[B] ⟼[E]

[B]hCatch_2 {1.5mu hState 2 {1.5mu 𝐥𝐞𝐭 ()=(abort (hCatch_2 {1.5mu hState 1 {1.5mu 𝐥𝐞𝐭 ()={1.5mu ()1.5mu}! 𝐢𝐧 get!1.5mu}1.5mu}))! 𝐢𝐧 get!1.5mu}1.5mu}[E]

[B] ⟼[E]

[B](hCatch_2 {1.5mu hState 1 {1.5mu 𝐥𝐞𝐭 ()={1.5mu ()1.5mu}! 𝐢𝐧 get!1.5mu}1.5mu})![E]

[B] ⟼[E]

[B](hCatch_2 {1.5mu hState 1 {1.5mu 11.5mu}1.5mu})! ⟼(hCatch_2 {1.5mu (1,1)1.5mu})! ⟼Just (1,1)[E]

This demonstrates that  supports effect handling both with and without effect interaction.

§.§ Non-Determinism is not a Separate Concern

Not all effect handlers have separate concerns.
For example, the non-determinism effect, which has a single operation  which represents flipping a coin and returning a , non-deterministically.
For example:

[B]flippy={1.5mu [13]
[13]match flip![E]

Following <cit.>, the  effect is handled by running both the program where the  operation returns  and where it returns , to accumulate a list of all possible program results; i.e.:

[B]hND prog=[E]

[3]handle {1.5mu [E]

[5]flip k↦{1.5mu (k {1.5mu True1.5mu})!(k {1.5mu False1.5mu})!1.5mu},[E]

[5]return x↦{1.5mu [1.5mu x1.5mu]1.5mu}[E]

[3]1.5mu} prog![E]

The return clause returns a singleton list representing a single possible program result.

We illustrated in <ref> that the  handler treats the exception effect as a separate concern.
In this section we illustrate that the non-determinism effect is not treated as a separate concern by the  handler.
Concretely, by handling  and  in different orders, we get different results:

[B](hND (hCatch flippy))! [1.5mu Nothing,Just 11.5mu][E]

[B](hCatch (hND flippy))! Nothing[E]

We also get interaction if we handle  and  in different orders:

[B]flippy_1={1.5mu [14]
[14]match flip![E]

[14]|True→𝐥𝐞𝐭 ()=put 1 𝐢𝐧 0[E]

[B](hND (hState flippy_1))! [1.5mu (0,1),(0,0)1.5mu][E]

[B](hState (hND flippy_1))! ([1.5mu 0,11.5mu],1)[E]

These examples demonstrate that the  handler does not have separate concerns: the  value produced by the first ordering of  and  above represents a result that is not produced by the second ordering; and the  result produced by the first ordering of  and  represents a result that is not produced by the second ordering of those handlers.
The  handler generally affects the final results in a way that is fundamentally different from, e.g., the , , and many other effects.
We characterize this fundamental difference in <ref> where we give a formal definition of what it means to have separate concerns, and in <ref> we show that  does not have this property.

§.§ Lambda Abstraction as an Effect

In this section we further demonstrate the expressiveness of , by showing how to handle a lambda abstraction effect.
The effect has three operations: (1) a function abstraction operation  where  is a named parameter, and  is the suspended body of the function; (2) an operation representing a variable,  where  is a named identifier; and (3) a function application operation  where  and  are values.
Recent work by <cit.> argues that these higher-order operations are beyond what both algebraic effect handlers and scoped effect handlers can define, and they proposed a Haskell-based library called latent effects.
We relate to their work in <ref>.
Here, we show how to handle the higher-order operations for the lambda abstraction effect using .

Consider the following program which uses the state effect and the lambda abstraction effect:

[B]lammy={1.5mu [12]
[12]𝐥𝐞𝐭 ()[20]
[20]=(put 1)! 𝐢𝐧[E]

[12]𝐥𝐞𝐭 f[20]
[20]=(abs 34 x34 {1.5mu (var 34 x34)!+get!1.5mu})! 𝐢𝐧[E]

[12]𝐥𝐞𝐭 ()[20]
[20]=(put 2)! 𝐢𝐧[E]

[12](app f 3)![27]

We can interpret  in several ways, depending on how we handle the abstraction effect.
By handling the lambda effect in a way that provides separation of concerns, we can postpone the evaluation of the body of the lambda until it is called.
This treats the state effect as a dynamic effect, meaning the program returns .
The  handler below assumes that (1) there is a  function for looking up a name  in an environment ; and (2) the value type used by the abstraction effect has a data type constructor  where  is a named parameter,  is a suspended function body, and  is a closure environment:[The pattern match in the  clause of the handler is incomplete.  For the purpose of this subsection we assume a type system that would warn about this incomplete pattern, but accept the program as well-typed; similarly to how Haskell would type an incomplete  expression.]

[B]hLam_0 r_0 prog=[E]

[3]handle {1.5mu [E]

[5]abs x m [18]
[18]r k[23]
[23]↦k r {1.5mu Clo x m r1.5mu},[E]

[5]app v_1 v_2 [18]
[18]r k[23]
[23]↦k r {1.5mu [32]
[32]match v_1[E]

[32]|Clo x m r'→hLam_0 ((x,v_2)::r') m1.5mu},[E]

[5]var x [18]
[18]r k[23]
[23]↦𝐥𝐞𝐭 v=lookup x r 𝐢𝐧 k r {1.5mu v1.5mu},[E]

[5]return x r[23]
[23]↦{1.5mu x1.5mu}[E]

[3]1.5mu} r_0 prog![E]

As we argue in <ref>, this handler has separate concerns.

An alternative handler for the lambda effect could use a “scoped” semantics, where we can use effect interaction between the abstraction effect handler and the state handler to treat the state effect as a static effect, meaning the  inside of the  bound to  is dereferenced under the state that the  operation is first evaluated under.
This will cause the program above to return .
The handler below implements this semantics, using an  operation to reset a continuation, similarly to how we used  to give a scoped semantics of exception catching.

[B]hLam_1 r_0 prog=[E]

[3]handle {1.5mu [E]

[5]abs x m [18]
[18]r k[23]
[23]↦k r {1.5mu Clo x (λ r' . abort$^\prime$ (k (hLam_1 r' m))) r1.5mu},[E]

[5]app v_1 v_2 [18]
[18]r k[23]
[23]↦k r {1.5mu [32]
[32]match v_1[E]

[32]|Clo x m r'→m ((x,v_2)::r')1.5mu},[E]

[5]var x [18]
[18]r k[23]
[23]↦𝐥𝐞𝐭 v=lookup x r 𝐢𝐧 k r {1.5mu v1.5mu},[E]

[5]abort$^\prime$ m k↦m,[E]

[5]return x r↦{1.5mu x1.5mu}[E]

[3]1.5mu} r_0 prog![E]

It is also possible to define a handler for a function abstraction effect where application operations have a suspended argument, such that we can do call-by-need evaluation.
The code artifact accompanying this paper contains such a handler.

The examples in this section have demonstrated the expressiveness of  on several examples.
In the remainder of the paper, we introduce a core calculus for , and use that to define a separation of concerns property, and define criteria under which the separation of concerns property is guaranteed to hold.

§ A CALCULUS WITH HANDLERS FOR HIGHER-ORDER EFFECTS

In this section, we define the syntax and semantics of a calculus with row-typed
algebraic effects and handlers, called , that supports higher-order
operations. The calculus is founded on the call-by-value -calculus, but
maintains a distinction between values and computations in the
spirit of Levy's call-by-push-value <cit.>. Its
type-and-effect system (<ref>) features
Hindley/Milner-style <cit.> polymorphic abstraction
for types and effect rows, and draws inspiration from the core calculi defined
for Koka <cit.> and
Frank <cit.>. We specify the operational
semantics of  using a reduction semantics
(<ref>), and we show that the type-and-effect system
is sound with respect to this semantics (<ref>).

§.§ Syntax

\begin{align*}
\ensuremath{\Varid{ℓ}} & \ensuremath{\mathbin{∈}\Conid{String}} & \text{(Effect labels)} \\
\ensuremath{\Varid{x},\Varid{y},\Varid{p},\Varid{m},\Varid{k},\Varid{α},\Varid{r}} & \ensuremath{\mathbin{∈}\Conid{String}} & \text{(Variables)} \\
& & \\
\ensuremath{\Varid{k}} &::= \ensuremath{\mathbin{★}\mathbin{∣}\Conid{R}\mathbin{∣}\Varid{k}\to \Varid{k}}
& \text{(Kinds)} \\
\ensuremath{\Varid{τ}}  &::= \ensuremath{\Varid{α}\mathbin{∣}\Varid{τ}\;\Varid{τ}\mathbin{∣}\Varid{τ}\to \Varid{τ}\mathbin{∣}}\ann{ε \ensuremath{\mathbin{*}} ε}{\susp{τ}}\ensuremath{}
& \text{(Types)} \\
\ensuremath{\Varid{ε}}  &::= \ensuremath{\mathbin{⟨⟩}\mathbin{∣}\mathbin{⟨}\Varid{ℓ},\Varid{ε}\mathbin{⟩}\mathbin{∣}\Varid{r}} & \text{(Effect rows)} \\
\ensuremath{\Varid{σ}}  &::= \ensuremath{\mathbin{∀}}\ \overline{\ensuremath{\Varid{α}}}\ \overline{r}\ .\ \ensuremath{\Varid{τ}} & \text{(Type Schemes}) \\
\ensuremath{\Conid{Δ},\Conid{Γ}} &::= \ensuremath{\mathbin{∅}\mathbin{∣}\Conid{Γ},(\Varid{x}\mathrel{=}\Varid{v})} & \text{(Environments)} \\
& & \\
\ensuremath{\Varid{e}} &::= \ensuremath{\Varid{e}\;\Varid{e}\mathbin{∣}\mathbf{let}\;\Varid{x}\mathrel{=}\Varid{e}\;\mathbf{in}\;\Varid{e}\mathbin{∣}\kw{handle}^{\ell}\;\{\mskip1.5mu \overline{C}\mskip1.5mu\}\;\Varid{e}\;\Varid{e}\mathbin{∣}\Varid{v}\mathbin{∣}\Varid{e}\kw{!}}
& \text{(Expressions)} \\
\ensuremath{\Varid{v}} &::= \ensuremath{\Varid{x}\mathbin{∣}\Varid{λx}}.\ensuremath{\Varid{e}\mathbin{∣}\Varid{c}\mathbin{∣}}\susp{e}
& \text{(Values)} \\
\ensuremath{\Conid{C}} &::= \ensuremath{\op{op}^{\ell}\;\Varid{f}\;\overline{x}\;\overline{m}\;\Varid{p}\;\Varid{k}\mathbin{↦}\Varid{e}\mathbin{∣}\kw{return}\;\Varid{x}\;\Varid{p}\mathbin{↦}\Varid{e}} & \text{(Clauses)}
\end{align*}

Syntax of

<ref> shows the syntax of .

Notational conventions Variables can range over expressions (,
, , , ), types (), and rows (), potentially using subscripts
or primes to distinguish them. We use an overline (e.g., ) to denote a
collection of zero or more objects, and use a subscript  to iterate over all
objects in such a collection. Operations are treated internally as variables,
but we distinguish them visually:  denotes the operation  of the
effect . We write $e[\ensuremath{\Varid{x}}/\ensuremath{\Varid{v}}]$ for the capture-avoiding substitution of
for  in . Multiple substitutions are comma-separated, and we use overlines
again (e.g., $\overline{\ensuremath{\Varid{x}}/\ensuremath{\Varid{v}}}$) to indicate substitution of a collection of

Types and rows As shown in <ref>, types in  are
either variable, type applications, function types, or
suspensions. To keep the type syntax as simple as possible, it lacks an
introduction form for type constructors. Type constructors are really only
necessary for the types of handlers, which may decorate the resulting value.
For example, the exception handler decorates its result with a . We treat
type constructors like  as type variables, which we assume are bound with
kind  the context  (see <ref>).

A suspension type indicates a thunked computations whose side effects have yet
to take place. We denote suspensions as $\ann{\ensuremath{\Varid{ε}\mathbin{*}\epsilon_{l}}}{\susp{\ensuremath{\Varid{τ}}}}$: a
computation that, when enacted, returns a value of type  with side effects . Both  and  range over effect rows, where  indicates the
computation's immediate effects, and  the computation's latent
effects.[We use the term “latent effects” to mean something
different from <cit.>. We relate to their work in
<ref>.]  We discuss this distinction in more detail in
<ref>, but informally speaking the immediate effets are
the unhandled effects, while the latent effects have already been
handled. Effect rows themselves can be the empty row, a row extension with a
known effect label , or a row variable. We will occasionally abuse notation,
and denote rows using a list-like syntax (e.g., ).

Type well-formedness

Well-formedness rules for types

We use kinds to ensure that types are well-formed. The judgment  states that the type  is well-formed with kind  under context ,
where  contains mappings for both type and row variables. We present the
corresponding rules in <ref>. The rules for type variables
(WF-Var), type application (WF-App), and function types
(WF-Arrow) are entirely standard. The rule WF-Suspend asserts
well-formedness of a suspension type, and features additional requirements that
its effect annotations  and  are well-formed.

Well-formedness for effect rows is defined with the rules WF-Empty and
WF-Cons, declaring respectively that the empty row is well formed, and
that a non-empty row is well-formed if its head is a known effect and its tail
is well-formed. To assert that a label  is a known effect, we assume a global
context  containing all declared effects, which maps effect labels to the set
of operations of that effect.

Expressions and values The term syntax of , which
distinguishes expressions from values, takes its basic constructs from the
-calculus; i.e., abstraction, application, variables, let-bindings, and
constants. Additionally,  includes an introduction/elimination pair for
suspension types: $\susp{\ensuremath{\Varid{e}}}$ suspends the side effects of , while
enacts any suspended side effects.

The  construct installs a handler for the effect , and has three
arguments: a list of clauses () and two expressions. The first expression
argument is the handler parameter, which is distributed to all handler
clauses to allow us to define handlers that interpret into a function space
(e.g., a state effect which takes the initial state as input). The second
expression argument is the expression in which we handle the operations of
. The list of clauses, , defines the semantics of these operations,
and should contain exactly one operation clause for each operation of ,
together with a single  clause.

Row equivalence and concatenation

Effect row equivalence and concatenation

In the definition of 's type-and-effect system, we will work modulo a
notion of row equivalence. That is, whenever two terms are annotated with
equal rows, we only assume that these rows are equivalent up to
reordering. <ref> defines this equivalence relation, ,
for effect rows. Furthermore, we will occasionally need to refer to the
concatenation of two rows. Formally, we define (in
<ref>) row concatenation as a ternary relation, where a
proof of the form  witnesses that the concatenation of  and
is equal (up to reordering) to . In the typing rules
(<ref>), however, we leave row reorderings implicit, and write

§.§ Type-and-Effect System

The type-and-effect system is defined using a single judgment, for which we
present the rules in <ref>. A judgment of the form  asserts that the expression  has type  under context , and
side effects  (immediate) and  (latent). As we show in
<ref>, the effect annotations are a sound over-approximation
of an expression's side effects: the effects in the annotation may or may not
happen, but any side-effect that does happen is included in the annotation.

Variables do not have any side effects, as reflected in the rule T-Var,
which asserts that variable expressions are typeable under any effect
annotation. Similarly, -abstractions also do not produce any side effects,
and hence the rule T-Abs permits any effect annotation. The body of a
-abstraction, however, must by typeable with the empty set of effects, or in
other words: it must be pure. All functions in  are pure by
definition, and effectful functions can only be encoded by returning an
effect-annotated suspension. This also clarifies the T-App rule, where
only the effect-annotations of the function and argument expression inform the
effects of the resulting expression, but not the function type itself. We treat
the components of a let-expressions as pure expressions in a similar
fashion. The T-Gen and T-Inst rules are the familiar rules for
generalization and instantiation of the polymorphic -calculus.

Effect resurfacing
While annotations distinguish between an expression's immediate and latent
effects, latent effects may resurface and become immediate again with the
T-Resurface rule. The intuition behind resurfacing is that it allows us
to re-annotate an expression with a less precise approximation of its side
effects, in the sense that we lose the information that the effect  occurs
exclusively under at least one layer of suspension. Resurfacing is necessary to
type handlers that recurse on sub-computations, where the handled effect should
be discharged to the surrounding context instead of becoming latent. We discuss
the need for resurfacing in more detail in <ref>.

T-Suspend and T-Enact define respectively introduction and
elimination rules for suspension types. A suspended computation has no effects,
so we may annotate it however is most convenient: the effects of a suspension are
completely unrelated to its context. The opposite is true for enactment, where
it is required that the effects of the enacted computation exactly match the
effects provided by the surrounding context.

Typing rules

Before considering how to type effect handlers, we must say a few words about
the type of operations. While operations are typed using T-Var, we do
make some assumptions about their type. In general, we say that the operations
of an effect  return a computation with the following type:
$\ann{\ensuremath{\mathbin{⟨}\Varid{ℓ},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\Varid{τ}}}}$, where  is the return type of the
operation, and  and  are universally quantified row variables that are
instantiated at the call-site. Effectively, this means that the operations of
the effect  can be called in any context where the immediate effects contain
the label . For instance, consider the type of the  operation:

\begin{equation*}
\ensuremath{\op{throw}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;r_{l}}\ .\ \ann{\ensuremath{\mathbin{⟨}\Varid{exc},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\Varid{α}}}}
\end{equation*}

We assume that the type of every defined operation universally quantifies over
and , and that these denote respectively the immediate and latent
effects of the context of its handler. This implies that between an operation
and its handler, there must be handlers for all latent effects. This restricts
the usage of operations somewhat, as we discuss in <ref>.

Operations with one or more arguments are assigned a function type, where the
type of the arguments is determined by the operation's definition. Formally, we
do not distinguish sub-computations from “regular” parameters, but we reserve
the terminology for parameters that are suspended computations. To illustrate,
consider the  operation, which has one regular argument, and the
operation, which takes two sub-computations:

\begin{gather*}
\ensuremath{\op{put}\mathbin{:}\mathbin{∀}\Varid{r}\;r_{l}}\ .\ \ensuremath{\Varid{s}\to }\ann{\ensuremath{\mathbin{⟨}\Varid{state},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{()}}} \\
\ensuremath{\op{catch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;r_{l}}\ .\ \ann{\ensuremath{\mathbin{⟨}\Varid{exc},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\Varid{α}}}}\ \ensuremath{\to }\ann{\ensuremath{\mathbin{⟨}\Varid{exc},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\Varid{α}}}}\ensuremath{\to } \ann{\ensuremath{\mathbin{⟨}\Varid{exc},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\Varid{α}}}}
\end{gather*}

Typing handlers
Effect handlers are typed with T-Handle. This rule is quite a handful, so
let us unpack its definition. The conclusion states that handling the effect
produces a suspension, annotated with effects , where  and
depend on the context in which the handler is invoked. Similar to
T-Suspend, we say that the side effects of producing this suspension
are completely independent from the side effects of the returned
computation. Furthermore, in the conclusion we syntactically impose the
restriction that the clause list ends with a single return clause, and we assume
that the collection of operation clauses, , matches the operations
defined for  in .

In the premise of T-Handle, we first define the context  under
which operation clauses will be typed.  extends  with bindings for the
operation's arguments (), the handler parameter (), and the
continuation (). The continuation returns a suspension that matches the type
of the entire expression — i.e.  $\ann{\ensuremath{\Varid{ε}\mathbin{*}\mathbin{⟨}\Varid{ℓ},\epsilon_{l}\mathbin{⟩}}}{\susp{\ensuremath{\tau_{2}}}}$ — and
takes two arguments: the handler parameter and a computation argument of type
$\ann{\ensuremath{\mathbin{⟨}\Varid{ℓ},\Varid{ε}\mathbin{⊕}\epsilon_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\tau_{2}}}}$. At run-time, this computation
argument will be evaluated under the same evaluation context as the handled
operation, for which the type-and-effect system statically guarantees that it
contains handlers for all effects in . We substitute  and  in the
types of  precisely such that sub-computations will match the type of
this computation argument, providing an “escape hatch” for the effects in
, which are immediate in sub-computations, but latent in the handler's
context. These effects are discharged to the handlers in the evaluation context
of the handled operation. Indeed, the operation clause for  in
<ref> enacts its sub-computations as part of 's computational
argument. We discuss the operational semantics of  in more detail in

Furthermore, T-Handle asserts that the implementation of the
clause, , can be typed under context , and that the
implementations of all operation clauses, , can be typed under the
aforementioned context . Both  and  should have the same type as the
handle expression as a whole. Finally, we also assert that the parameter
expression, , and the handled expression, , are well-typed, where the
effect annotation of  matches the entire expression, and  that of the
returned suspension, with the label  shifted to the latent side.

§.§ On Immediate and Latent Effects

As described above, a suspension type  distinguishes a row of immediate effects () and a row of latent effects ().
The immediate effects describe the set of operations for which the suspension has no handler installed, whereas the latent effects describe the set of operations for which there is a handler installed inside the suspension.
We briefly discuss the need for tracking both immediate and latent effects, and how this affects what programs can and cannot be typed using our type-and-effect system.

The need to track immediate and latent effects
It is necessary to track latent effects because handlers do not eagerly propagate into suspensions.
For example, consider the following expression, where  is some higher-order operation:

\begin{equation*}
\ensuremath{\kw{handle}}^{\ensuremath{\Conid{State}}}\ \ensuremath{\{\mskip1.5mu }\ldots\ensuremath{\mskip1.5mu\}\;(\op{op}^{\ell}\;\{\mskip1.5mu (\op{put}\;\mathrm{0})\kw{!}\mskip1.5mu\})}
\end{equation*}

This expression has a suspension type:  for some τ and some ε, where ε contains at least the effect label of the  operation.
In conventional effect handler type systems, applying a handler such as $\ensuremath{\kw{handle}}^{State}$ would remove the  effect from the result type.
The reason  features as a latent effect in the type fo the expression above is that the  operation occurs in a sub-computation of .
In , the state handler is not automatically applied to sub-computations, so if a handler of the  operation enacts its sub-computation, the  effect becomes immediate again.
That is why our type system tracks latent effects: simply removing an effect from the annotation of suspensions when applying a handler loses information about the immediate effects of sub-computations.
To avoid this information loss, handlers “shift” a label from the immediate to the latent annotation (see T-Handle in <ref>).

Effect resurfacing
The relocation of annotations from the immediate to the latent annotation by
handlers has subtle implications for recursive handlers; i.e., a handler
that invokes itself. The handler  defined <ref> does
exactly this: the handler clause for  is implemented by recursively
invoking , and inspecting the result:

[3]catch m_1 m_2 k↦k {1.5mu [24]
[24]match (hCatch m_1)!|Nothing→m_2!|Just x→x1.5mu}[E]

Following T-Handle, this clause is part of a  expression annotated with .
Consequently, the continuation argument is annotated with .
The recursive invocation , however, has effects , which is incompatible with .
The T-Resurface rule mediates  from a latent effect into an immediate effect to make the recursive call typeable.
This mediation is essentially a form of up-casting.

Operation types restrict use of inline handlers
As discussed in <ref>, our type-and-effect system types operations of effect  as having a type $\ann{\ensuremath{\mathbin{⟨}\Varid{ℓ},\Varid{r}\mathbin{⊕}r_{l}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\Varid{τ}}}}$ where  and  are polymorphically-quantified row variables.
As a result, operations are only callable from a context with an empty latent effect row.
Without this restriction, we would be able to type a suspension to make it appear as if we have pre-applied a handler to a sub-computation.
For example, we could type the expression  as .
However, this type would suggest that the following program is safe, which it is not:

[B](hCatch (catch {1.5mu (put 0)!1.5mu} {1.5mu ()1.5mu}))![E]

This program gets stuck because the  operation in the first branch of  is unhandled.

This restrictive typing has implications beyond ruling out programs that go wrong.
It also rules out programs some that go right, and which readers familiar with, e.g., Koka <cit.> or Frank <cit.>, might expect to be well-typed.
For example, consider the following program:

[B]example=hState 0 {1.5mu 𝐥𝐞𝐭 ()=(put 1)!𝐢𝐧 (hLocal 2 {1.5mu ask!1.5mu})!1.5mu}[E]

Evaluation of this program will not get stuck: the state handler first updates the state to ; subsequently, the local handler asks for the local binding .
Still, our type-and-effect system rejects it.
The reason is that T-Let requires both branches of the  expression to have the same latent effects.
This implies that the type of the  operation is , which violates the operation typing restriction discussed above.

By insisting that operations have no latent effects we thus restrict programs that contain inline handlers, such as the  program above.
This may come as a surprise, as inline handlers are widely used in, e.g., Koka <cit.> and Frank <cit.>.
However, in a system like , we can generally use a higher-order operation anywhere you would want to use an inline handler.
In fact, we argue that we should replace occurrences of inline handlers by higher-order operations, since inline handlers break down the distinction between the syntax and semantics of programs.
That is, the syntax of programs should be given by the operations that occur in them, while handlers should assign a semantics to those operations.
Programs implemented using inline handlers are not syntactic in this sense.

§.§ Operational Semantics

We specify the run-time behaviour of  by giving a reduction semantics à
la Felleisen's prompt-control <cit.>. The
rules are presented in <ref>. The operational
semantics is specified using three key components:

* Evaluation contexts (), that capture the decomposition of a term into
its leftmost-outermost redex, and the surrounding expression.

* A contraction relation (), that describes a single reduction
step for a redex.

* A reduction relation (), that describes the reduction of an
expression at its leftmost-outermost redex.

Together, these components specify evaluation for : we repeatedly reduce
the leftmost-outermost redex of a term until it cannot be further reduced (i.e.,
it's a value). This evaluation strategy is formally captured by the reflexive
transitive closure of , which we denote by . In
<ref>, we show that, per Milner's motto,
evaluating well-typed expressions using  cannot go wrong.

\begin{align*}
\ensuremath{\Conid{E}}   &::= \ensuremath{\mathbin{∙}\mathbin{∣}\Conid{E}\;\Varid{e}\mathbin{∣}\Varid{v}\;\Conid{E}\mathbin{∣}\mathbf{let}\;\Varid{x}\mathrel{=}\Conid{E}\;\mathbf{in}\;\Varid{e}\mathbin{∣}\Conid{E}\kw{!}\mathbin{∣}\kw{handle}^{\ell}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}\;\Conid{E}\;\Varid{e}} & \text{(Evaluation contexts)} \\
& \ \ \ensuremath{\mathbin{∣}}\ \ \ensuremath{\kw{handle}^{\ell}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}\;\Varid{v}\;\Conid{E}}  \\
\ensuremath{\Conid{E}^{\Varid{ℓ}}}  &::= \ensuremath{\mathbin{∙}\mathbin{∣}\Conid{E}^{\Varid{ℓ}}\;\Varid{e}\mathbin{∣}\Varid{v}\;\Conid{E}^{\Varid{ℓ}}\mathbin{∣}\mathbf{let}\;\Varid{x}\mathrel{=}\Conid{E}^{\Varid{ℓ}}\;\mathbf{in}\;\Varid{e}\mathbin{∣}\Conid{E}^{\Varid{ℓ}}\kw{!}\mathbin{∣}\kw{handle}^{\ell^\prime}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}\;\Conid{E}^{\Varid{ℓ}}\;\Varid{e}} \\
& \ \ \ensuremath{\mathbin{∣}}\ \ \ensuremath{\kw{handle}^{\ell^\prime}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}\;\Varid{v}\;\Conid{E}^{\Varid{ℓ}}\;(}\text{if}\ \ensuremath{\Varid{ℓ}\neq\Varid{ℓ}^{\prime})}
\end{align*}

[x,p/,k/.  ]

Operational semantics

Evaluation contexts describe expressions with a single hole () in
them. Their definition is carefully chosen to ensure that the hole always points
to the leftmost-outermost redex whenever we replace the hole with a contractible
expression. We define a variation, , that additionally ensures that the
context contains no handlers for the effect .

The , , and Let rules are the usual reduction rules for
call-by-value evaluation, where  is a partial function describing how to
evaluate fully-reduced applications of constants. Enact replaces
consecutive suspension and enactment with the original expression, and the
Return rule invokes the return clause of a handler, if both the handler
parameter and the handler argument have been evaluated to a value.

The Handle rule replaces operations with their semantics, assuming that
the handler parameter has been fully reduced. The handler's argument is a
decomposed expression, $\ensuremath{\Conid{E}^{\Varid{ℓ}}}[\ensuremath{(\op{op}^{\ell}\;\Varid{f}\;\overline{\Varid{v}})\kw{!}}]$, where the context
ensures that there are no closer handlers for . Reducing a handler means
replacing it with the corresponding clause for , appropriately
substituting the operation arguments, handler parameter, and continuation. In
the continuation, we install the same handler on the composite expression
$\ensuremath{\Conid{E}^{\Varid{ℓ}}}[\ensuremath{\Varid{y}\kw{!}}]$, giving the clause implementation an opportunity to discharge
any latent effects in sub-computations of , or the effect  itself, to
the context of . Importantly, the type-and-effect system statically
guarantees that the context  contains handlers for all latent effects, by
restricting the latent effect annotation of operations to the empty row.

§.§ Type Soundness

We prove soundness of our type system (<ref>) with respect to
the operational semantics (<ref>) via the syntactic
approach of <cit.>. The proof for the final
soundness theorem (<ref>) follows from subject reduction
(reducing expressions preserves their type, <ref>) and
progress (every expression is either a value or can be reduced,

We start by proving subject reduction. For this, we need three additional

Given an expression  such that
., such that $x \notin \text{dom}(Γ)$, then for every value  where , it follows that [x/v] provided that $\ \notin \text{ftv}(Γ)$.

Given a deduction of the form  and its sub-deduction
, we can replace this sub-deduction by another
sub-deduction  such that .

Values can be annotated with any effect. That is, for every value , if , then also  for every , .

Proofs for <ref> and <ref> are
straightforward adaptations of the corresponding proofs by
<cit.>. A proof for <ref>
follows from case analysis on . We will use these lemmas to prove subject
reduction. First, we prove subject reduction for the contraction relation .

For all expressions  and , if  and ,
it follows that .

The proof proceeds by rule induction over the derivation . See <ref> for a proof sketch.

Next, we extend subject reduction to the reduction relation :

For all expressions  and , if  and ,

The proof is an immediate consequence from replacement
(<ref>), subject reduction for the contraction relation
(<ref>), and the definition of

The next part of proving type soundness is to show that well-typed programs
will not get stuck, which we prove directly by rule induction over the typing

For every expression , if , then either there exists
some  such that , or  is a value, where  is an initial
context that contains bindings for the operations of all known effects in .

The proof is routine and proceeds by rule induction over the derivation for . See <ref> for a more detailed proof

Type Soundness

We now have all the necessary ingredients to state and show type soundness of
our type system. Let  denote a diverging computation; i.e., the
expression  has a never-ending reduction.

For every , if , then either , or there exists a
value  and rows , , such that , ,
and .

From <ref> it follows that if , either there
exists some  such that , or . If , then from
<ref> and the definition of  we conclude that .

§ A FORMAL CHARACTERIZATION OF HANDLERS WITH SEPARATE CONCERNS

As discussed in <ref>, many effect handlers can be defined and handled in a way that running handlers in different orders only changes how return results are packaged, but not the return results themselves.
We argue that handlers that have this property are well-behaved, because it is possible to seamlessly compose these handlers in any order, without surprising effect interactions.
But what, precisely, does it mean that running handlers in different orders only changes how return results are packaged, but not the return results themselves?  And which handlers have this property?
In this section we characterize what it means for handlers to have separate concerns.
In the next section we prove that common algebraic effect handlers have this property, and discuss counter-examples of handlers that do not have the property.

Notationally, we will use both the symbol  and horizontal inference lines for logical implication in this section.
The functions we define in this section are generally logical meta-level functions as opposed to  functions.

§.§ Separation of Concerns

We say that handlers have the separation of concerns (s.o.c.) property when the handlers can be applied in any order, to yield equivalent results.
As hinted at above, we will compare results up-to how they are “packaged”.
By packaging we mean the type  that handlers decorate their return results by (we will use both the term functor and answer type modifier to describe ).
For example, the answer type modifier of  is , since the type of the  handler is .
For handlers that have no answer type modifier, we assume that there is an implicit identity answer type modifier .
We introduce an equivalence for comparing results by “extracting” bags of answers from answer type modifier wrapped results.

§.§.§ Baggable Functor Equivalence

We say that a functor  is baggable when it has a function that extracts the bag (also known as a multiset) of elements of type  contained in a functor structure ; i.e.:

\begin{equation*}
\ensuremath{\Varid{toBag}_{\Conid{F}}\mathbin{:}\Conid{F}\;\Conid{A}\mathbin{→}\Conid{Bag}\;\Conid{A}}
\end{equation*}

The notion of equivalence we will use to define our s.o.c. property is the following.
For any two baggable functors  and , and for any type , we can compare results of type  and  by comparing their corresponding bags; i.e.:

\begin{align*}
\inferrule*
{    \ensuremath{\Varid{x}\mathbin{:}\Conid{F}\;\Conid{A}}
\and \ensuremath{\Varid{y}\mathbin{:}\Conid{G}\;\Conid{A}}
\and \ensuremath{\Varid{toBag}_{\Conid{F}}\;\Varid{x}\mathrel{=}\Varid{toBag}_{\Conid{G}}\;\Varid{y}}
{ \ensuremath{\Varid{x}\sim\Varid{y}} }
\end{align*}

To define the s.o.c. property, we will also make use of the fact that, for any two baggable functors  and , we get the following  function for free:

\begin{align*}
&\ensuremath{\Varid{toBag}_{\Conid{F}\mathbin{∘}\Conid{G}}} : \ensuremath{\Conid{F}\;(\Conid{G}\;\Conid{A})\mathbin{→}\Conid{Bag}\;\Conid{A}}
\\
&\ensuremath{\Varid{toBag}_{\Conid{F}\mathbin{∘}\Conid{G}}} = \ensuremath{\Varid{join}\mathbin{∘}\Varid{fmap}_{\Conid{Bag}}\;\Varid{toBag}_{\Conid{F}}\mathbin{∘}\Varid{fmap}_{\Conid{G}}}
\end{align*}

Here,  is a function that joins a bag of bags using bag union, and  maps a function over a bag to modify its elements.

§.§.§ The Separation of Concerns Property

We will define separation of concerns for handlers by assuming that a handler of effect  is given by a function , where  is the parameter type of the handler.
We will write  to represent an invocation of a handler  with parameter .
Now, for any two handlers

\begin{gather*}
\ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}} .\ \ensuremath{\Conid{P}_1\mathbin{→}\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\
\ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}} .\ \ensuremath{\Conid{P}_2\mathbin{→}\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{2},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\end{gather*}

where  and where  and  are baggable functors, we say that  and  have separate concerns when, for any ,

\begin{equation*}
\inferrule*
{    %|v₁₂ : F₁ X|
%\and |v₂₁ : F₂ X|
\ensuremath{(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e}))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\and \ensuremath{(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e}))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}} }
{ \ensuremath{\Varid{v}_{\mathrm{21}}\sim\Varid{v}_{\mathrm{12}}} }.
\end{equation*}

This says that  and  can be run in any order, when  only has residual effects that are handled by  and ; i.e.,  and .
More generally, we say that  and  have separate concerns under a handler context . , where  is a baggable functor, when for any ,

\begin{equation*}
\inferrule
{  \ensuremath{(\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e})))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{(\Varid{h}^{\Varid{h}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e})))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
{  \ensuremath{\Varid{v}_{\mathrm{21}}\sim\Varid{v}_{\mathrm{12}}} }
\end{equation*}

In the proposition above, the handler context  may be a nested stack of handlers.
Similarly,  may contain nested handlers.
Since we can compose and re-associate handlers using function composition, the proposition tells us that we can reorder any pair of handlers in a handler stack.
We thus say that two handlers  and  have separate concerns iff reordering them in a nested stack of handlers yields an equivalent bag of values.
And we say that a handler  has separate concerns iff we can reorder it with any different handler  in a handler context to yield an equivalent bag of values.
In the next section we provide a set of criteria for proving that a given handler has separate concerns.

§.§.§ Criteria for Separation of Concerns

A handler has separate concerns when it satisfies the handler return lemma (<ref>) and the handler op lemma (<ref>).

The return case of handler  . , where  is a baggable functor, yields a result that corresponds to a singleton bag.
That is, for any value  and parameter ,

\begin{equation*}
\ensuremath{\Varid{toBag}_{\Conid{F}}\;(\Varid{h}^{\Varid{p}}\;\susp{\Varid{v}})\kw{!}\mathrel{=}\{\mskip1.5mu \Varid{v}\mskip1.5mu\}}
\end{equation*}

A handler  .  has separate concerns when all of its handler clauses are handled in a way that provides separation of concerns.
That is, for any ,
any ,
any ,
and any ,
where , and where  and  satisfy <ref>, the following holds:

\begin{equation*}
\inferrule
{    \ensuremath{(\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[\op{op}^{\ell}\;\Varid{f}\;\overline{\Varid{v}}])))\kw{!} \longmapsto \Varid{e'}}
\and \ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\   \ensuremath{(\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Conid{E}[\op{op}^{\ell}\;\Varid{f}\;\overline{\Varid{v}}])))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\   \left(\ensuremath{\mathbin{∀}e_{0}\;\!.\!\;\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}(\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})))\kw{!} \Longrightarrow \Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{12}} \Longrightarrow \Varid{v}_{\mathrm{21}}\sim\Varid{v}_{\mathrm{12}}}\right)
{ \ensuremath{\Varid{v}_{\mathrm{21}}\sim\Varid{v}_{\mathrm{12}}}
\end{equation*}

The  relation in <ref> represents a sequence of zero or more  reduction steps.

<Ref> below shows that any handler that satisfies the handler return and op lemmas has separate concerns.

Any handler  .  that satisfies the handler return lemma (<ref>) and handler op lemma (<ref>) has separate concerns.
That is, for
where each handler in the handler context  satisfies the handler return lemma,
that also satisfies the handler return and the handler op lemma,
and any ,

\begin{equation*}
\inferrule
{  \ensuremath{(\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e})))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{(\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e})))\kw{!} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
{  \ensuremath{\Varid{v}_{\mathrm{21}}\sim\Varid{v}_{\mathrm{12}}} }
\end{equation*}

The proof is by rule induction on  in the premise of the goal.
The base case, where  represents zero steps, holds vacuously, because  is not a value.
The inductive case proceeds by inversion on the  and  relations, and the resulting goals follow from the handler return and handler op lemmas, since the induction hypothesis matches matches exactly the premise of the op handler lemma.

§.§ Discussion

We have given a formal characterization of handlers that have separate concerns.
While our formal characterization is defined in terms of the notion of handlers of higher-order effects that this paper introduces, the characterization is expected to apply to plain algebraic effect handlers, and (perhaps with some adjustments) to scoped effect handlers.

Our characterization is currently limited to talking about a class of handlers that handles a single effect and is polymorphic in both the remaining set of effects and in the return type of the computation being handled.
While this class of handlers is representative of many effects and effect handlers found in the literature, it does not contain effect handlers that handle multiple effects at once, nor effect handlers that assume that the input computation has a particular return type or a particular set of effects.
Our characterization of separate concerns readily generalizes to effect handlers that handle multiple effects at once, and to effect handlers that are non-polymorphic in the type of their input computation; e.g.,  for some specific type .
Handlers that are not polymorphic in  and  cannot be reordered as freely, as a specific row of handlers implies the presence of a particular set of effects—which may change when reordering handlers.
But it is still possible to prove a form of separation of concerns for such handlers, as we demonstrate below in <ref> where we prove a notion of separation of concerns for a handler for  abstraction which is non-polymorphic in its row of effects.

§ SEPARATION OF CONCERNS FOR HANDLERS OF COMMON EFFECTS

We show (in <Ref>) that the characterization of separate concerns from <ref> applies to handlers of common effects found in programming languages.
We also show (in <Ref>) how handlers of other common effects, such as non-determinism, do not have separable concerns.

Finally, in <ref> we discuss a general criterion for handlers, which we conjecture implies separation of concerns.
The examples in this section are defined for a calculus that extends the core calculus from <ref> with recursive bindings,  expressions, and with data values (i.e., terms that represent constructors of data types).

§.§ Separation of Concerns for Three Common Algebraic Effects

<Ref> shows the handlers of three common algebraic effects: a state effect, abort effect, and read-only effect.
We show that these handlers satisfy <ref> and <ref>, and thus have separate concerns.

[9]∀α r r^'. S→⟨St,r⟩*r^'α[E]

[B]hSt s_0 prog=[E]

[3]handle {1.5mu [E]

[5]get [13]
[13]s [16]
[19]↦k s s,[E]

[5]put s' [13]
[13]s [16]
[19]↦k s' (),[E]

[5]return x s[19]

[3]1.5mu} s_0 prog![E]

[12]∀α r r^'. ⟨Ab,r⟩*r^'α[E]

[12]r*⟨Ab,r^'⟩Maybe α[E]

[B]hAbort prog=[E]

[3]handle {1.5mu [E]

[5]abort [15]

[5]return x[15]
[15]↦Just x[E]

[3]1.5mu} prog![E]

[11]∀α r r^'. R→⟨Rd,r⟩*r^'α[E]

[B]hRead r prog=[E]

[3]handle {1.5mu [E]

[5]read r k[17]
[17]↦k r r,[E]

[5]return x [17]

[3]1.5mu} r prog![E]

Handlers for common algebraic effects defined using handlers of higher-order effects

Each of the handlers in <ref> satisfy the handler return lemma (<ref>), using the following baggable functor definitions:

\begin{align*}
\ensuremath{\Varid{toBag}_{(,)\;\Conid{S}}\ (\Varid{x},\Varid{s})} &= \ensuremath{\{\mskip1.5mu \Varid{x}\mskip1.5mu\}}
\end{align*}

\begin{align*}
\ensuremath{\Varid{toBag}_{\Conid{Maybe}}\ (\Conid{Just}\;\Varid{x})} &= \ensuremath{\{\mskip1.5mu \Varid{x}\mskip1.5mu\}}
\\
\ensuremath{\Varid{toBag}_{\Conid{Maybe}}\ \Conid{Nothing}}    &= \ensuremath{\{\mskip1.5mu \mskip1.5mu\}}
\end{align*}

\begin{align*}
\ensuremath{\Varid{toBag}_{\Conid{Id}}\ \Varid{x}} &= \ensuremath{\{\mskip1.5mu \Varid{x}\mskip1.5mu\}}
\end{align*}

Follows from the definition of the  clauses in <ref> and the $\textit{toBag}$ definitions above.

Each of the handlers in <ref> satisfy the handler op lemma (<ref>).

The proofs are by inversion on , , and .
The goals follow from the “induction step premise” of the op handler lemma (see <ref>), and/or from the fact that  and  satisfy the handler return lemmas (<ref>).

§.§ Separation of Concerns for Three Common Higher-Order Effects

<Ref> shows three handlers of higher-order effects: a local effect (akin to Haskell's  monad), an exception catching effect, and an effect with operations for the lambda abstraction effect discussed in <ref>.

[12]∀α r r^'. R→⟨Lo,r⟩*r^'α[E]

[B]hLocal r prog=[E]

[3]handle {1.5mu [E]

[5]ask [16]
[16]r k[21]
[21]↦k r r[E]

[5]local f m [16]
[16]r k[21]

[7]k r (hLocal (f r) m!)[E]

[5]return x [21]

[3]1.5mu} r prog![E]

[12]∀α r r^'. ⟨Ca,r⟩*r^'α[E]

[12]r*⟨Ca,r^'⟩Maybe α[E]

[B]hCatch prog=[E]

[3]handle {1.5mu [E]

[5]throw [18]

[5]catch m_1 m_2 [18]

[7]k () {1.5mu [15]
[15]match (hCatch m_1)![E]

[15]|Just x→x[30]

[5]return x↦Just x[E]

[3]1.5mu} prog![E]

[11]∀α r r^'. Env→⟨La,⟨Ab,r⟩⟩*r^'α[E]

[B]hLam r prog=[E]

[3]handle {1.5mu [E]

[5]abs x m [18]
[18]r k[23]
[23]↦k r Clo x m r,[E]

[5]app v_1 v_2 [18]
[18]r k[23]
[23]↦match v_1[E]

[7]|(Clo x m r^')[24]

[9]k (hLam ((x,v_2)::r^') m)[E]

[5]var x [18]
[18]r k[23]
[23]↦k r lookup x r,[E]

[5]return x r[23]

[3]1.5mu} r prog![E]

[12]String→⟨La,⟨Ab,r⟩⟩*r^'Val r r^'[E]

[12]Env→Val r r^'[E]

Handlers for common higher-order effects

Each of the handlers in <ref> satisfy the handler return lemma (<ref>), using the $\mathit{toBag}_{\mathit{Id}}$ and $\mathit{toBag}_{\mathit{Maybe}}$ definitions from <ref>.

Follows from the definition of the  clauses in <ref> and the $\mathit{toBag}$ definitions from <ref>.

Each of the handlers in <ref> satisfy the handler op lemma (<ref>).

The proof is by inversion on , , and .
The goals follow from the “induction step premise” of the op handler lemma (see <ref>), and/or from the fact that  and  satisfy the handler return lemmas (<ref>).

§.§ Handlers with Non-Separable Concerns: Non-Determinism, Revisited

As argued in <ref>, the non-determinism handler  does not treat the  operation in a way that it is a separate concern.
Here, we make that argument formal.
To do so, we need to provide a baggable functor instance for s.
A sensible choice is to translate a list into a bag, as follows:

\begin{align*}
\ensuremath{\Varid{toBag}_{\Conid{List}}\ [\mskip1.5mu \mskip1.5mu]} &= \ensuremath{\{\mskip1.5mu \mskip1.5mu\}} \\
\ensuremath{\Varid{toBag}_{\Conid{List}}\ (\Varid{x}\mathbin{::}\Varid{xs})} &= \ensuremath{\{\mskip1.5mu \Varid{x}\mskip1.5mu\}\cup\Varid{toBag}_{\Conid{List}}\ \Varid{xs}}
\end{align*}

It is also possible to define $\mathit{toBag}_{\mathit{List}}$ in a way chooses the first or an arbitrary element of a list, and returns a singleton bag with that element.
It is, however, not possible to define $\mathit{toBag}_{\mathit{List}}$ in a way that returns the empty bag, since the handler return lemma would be violated for the  handler.
From the $\mathit{toBag}_{\mathit{List}}$ definition above, the examples we considered in <ref> are counter-examples of the separate concerns property, since:

\begin{equation*}
\ensuremath{\Varid{toBag}_{\Conid{List}\mathbin{∘}\Conid{Maybe}}\ [\mskip1.5mu \Conid{Nothing},\Conid{Just}\;\mathrm{1}\mskip1.5mu]\mathrel{=}\{\mskip1.5mu \mathrm{1}\mskip1.5mu\}\neq\{\mskip1.5mu \mskip1.5mu\}\mathrel{=}\Varid{toBag}_{\Conid{Maybe}\mathbin{∘}\Conid{List}}\ \Conid{Nothing}}
\end{equation*}

§.§ Conjectured Criterion for Separation of Concerns

In this section we observed that many common handlers of higher-order effects have separate concerns, and also observed that others do not.
From the observed examples, we can see that the handlers that call their continuation argument  at most once—such as , , , , , and —have separate concerns.
We can also see that handlers that may call their continuation argument more than once—such as , or the “scoped” encodings  and —do not have separate concerns.

Based on these observations, we conjecture that handlers that make affine use of their continuation argument have separate concerns.
By affine use we mean that the continuation is either called once (like in the  clause in <ref>) or not at all (like in the  clause in <ref>).

§ RELATED WORK

Models of effectful computations Monads, originally by
<cit.> and later popularized in the functional
programming community by <cit.>, have long been the
dominant approach to modelling programs with side effects. They are, however,
famously hard to compose, thus monad
transformers <cit.> were proposed as a means to
build monads from individual definitions of effects. Algebraic
effects <cit.> provide a more structured
approach, by specifying effects in terms of operations whose behaviour is
characterized by a set of equations that specify when it is well-behaved. Later,
<cit.> extended the approach with handlers,
which define interpretations of effectful operations by defining a homomorphism
from a free model that trivially inhabits the equational theory (i.e.,
syntax) to a programmer-defined domain, making the approach attractive for
implementing effects as well. Perhaps the most well-known implementation of
algebraic effects and handlers is the free
monad <cit.>, and this implementation is often
taken as the semantic foundation of languages with support for effect
handlers. <cit.> showed that algebraic
effects implemented using the free monad correspond to a sub-class of

It is future work to give a denotational model of  in terms of the free monad.

The obvious approach is to interpret suspension types as the free monad of a
signature functor corresponding to its annotation. However, since continuations
receive a computation argument as well, the usual inductive definition would
necessarily have a contravariant recursive occurence, meaning it lacks a
functorial semantics.  While it is possible to define such a type in, e.g.,
Haskell, it would be wrong to market it as a denotational model for .

Models of effects with higher-order operations

A crucial difference between our approach and plain algebraic effects is the
built-in support for higher-order operations. Though it is possible to
encode such operations with algebraic effects, this usually introduces at least
some mixing of operations and handlers. For example,
<cit.> implement a  operation in terms of
the exception handler. Scoped Effects <cit.>
were proposed as an alternative flavor of algebraic effects that syntactically
supports higher-operations, recovering the separation between syntax
semantics. In subsequent work, <cit.> adapted the
categorical formulation of algebraic effects to Scoped Effects, giving them the
same formal underpinning.

Higher-order operations in scoped effects are not unlike operations with
suspension parameters in , although sub-computations must have the exact
same effects as their parent operation. In , suspension parameters may be
annotated with any effect. In scoped effects one can recover multiple different
interactions for effects by changing the order in which they are
handled. In , on the other hand, strives for separation of concern:
effects should interact as little as possible to make their semantics more
predictable. Consequently, interaction semantics have to be explicitly
defined. Another key difference between scoped effects and our approach is the
treatment of effects in sub-computations. In , the syntax of
suspended computations is left intact until they are enacted. In scoped effects,
handlers are eagerly applied to sub-computations, replacing operations with
their semantics. As a result, handlers for higher-order operations necessarily
have to mediate the answer type modifications of previously-applied handlers
when enacting a sub-computation. This works well for polymorphic operations like
, where the semantic traces of earlier handlers can be hidden in the
existentially quantified type of its branches, but operations with
sub-computations that return a known type—such as —are awkward to

Latent effects were developed by <cit.> as a
refinement of scoped effects that solves this issue by explicitly tracking such
semantic residues using a latent effect functor, allowing for a more
fine-grained specification of the types of sub-computations. With their
approach, it is possible to capture function abstraction as a higher-order
operation. The latent effect functor serves an equivalent purpose as our latent
effect annotations, though latent effects remembers a semantic imprint of the
already-handled effects while we remember their syntax.

Implementations of Algebraic Effects and Handlers

There is an abundance of languages with support for algebraic effects and
handlers. Perhaps closest to our work is Koka <cit.>,
whose core calculus features a similar Hindley/Milner-style row-polymorphic type
system as . While we maintain a
CBPV-inspired <cit.> distinction between computations and
values, Koka is purely call-by-value, equating computations to
functions. Frank <cit.>, on the other hand, does
maintain this distinction. Its type system, however, is quite different from
ours, relying on an ambient ability and implicit row polymorphism to type
effectful operations. Handlers are not first-class constructs in Frank. Instead,
functions may adjust the ambient ability of their arguments by specifying the
behaviour of operations. This provides some additional flexibility over
conventional handers, permitting for example multihandlers that handle
multiple effects at once.  Both Koka and Frank lack native support for higher
order effects, thus encoding higher-order operations requires a similar kind of
inlining of handlers as discussed in <ref>.

Eff <cit.> is a functional language with support for
algebraic effects and handlers, with the possibility to dynamically generate new
operations and effects. In later work, <cit.>
developed a type-and-effect system for Eff, together with an inference
algorithm <cit.>. The language
Links <cit.> employs row-typed algebraic effects in
the context of database programming. Their system is based on System-F extended
with effect rows and row polymorphism, and limits effectful computations to
functions similar to Koka. Importantly, their system tracks effects using
Rémy-style rows <cit.>, maintaining so-called
presence types that can additionally express an effect's absence from a
computation. <cit.> presented
Effekt as a more practical implementation of effects and handlers, using
capability based type system where effect types express a set of
capabilities that a computation requires from its context.

We have proposed  as an approach to handling higher-order effects.
The approach builds on what Lindley[<https://effect-handlers.org/>] and <cit.> calls the effect-handler oriented programming paradigm.
An important aspect of this paradigm (and any programming paradigm) is being able to run programs efficiently.
The question of how to execute effect handlers efficiently is an active area of research.
We summarize some of the main recent results in this area below.
In future work, we intend to explore how to efficiently implement  in practice, and the literature we summarize below will be valuable to that end.

Effect handlers evidently <cit.> shows obtain efficient run times of algebraic effect handlers, by translating effect handlers to multi-prompt delimited continuations <cit.>.
The translation of <cit.> restricts effect handlers to use scoped resumptions; i.e., continuation values should not escape their handlers.
They argue that the restriction is mild, and that it mainly rules out ill-behaved programs.

<cit.> show how to compile Eff code into OCaml code in a way that aggressively reduce handler applications.
Their approach is different, but orthogonal, to the capability-passing compilation strategy due to <cit.>.
The compilation approaches of <cit.> and <cit.> both demonstrate speedups that bring the run time efficiency effect handler oriented code very close to the run time of plain, direct style code.
OCaml has also recently been retrofitted <cit.> with built-in support effect handlers, with impressive performance numbers.

<cit.> demonstrate how to significantly improve the run time efficiency of free monad based algebraic effect handlers in Haskell by fusing handlers.
This efficient encoding of effect handler has been adopted in the  library with support for scope effects in Haskell.[<https://hackage.haskell.org/package/fused-effects>]

§ CONCLUSION

We have presented , a calculus with effect handlers for higher-order effects.
We have shown that it can be used to implement all algebraic effects, common higher-order effects such as exception catching, and even effects with advanced control-flow such as lambda abstraction.
Additionally,  enables a definition of handlers for effects with separation of concerns, meaning the order of applying effect handlers does not change the essential results of the computation.
We have formalized this property and proved it for a selection of handlers for common algebraic and higher-order effects.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Bauer and PretnarBauer and Pretnar2014]
authorpersonAndrej Bauer and personMatija
Pretnar. year2014.
An Effect System for Algebraic Effects and
journalLog. Methods Comput. Sci.
volume10, number4 (year2014).

[Bauer and PretnarBauer and Pretnar2015]
authorpersonAndrej Bauer and personMatija
Pretnar. year2015.
Programming with algebraic effects and handlers.
journalJ. Log. Algebraic Methods Program.
volume84, number1 (year2015),

[Brachthäuser, Schuster, and
OstermannBrachthäuser et al2020]
authorpersonJonathan Immanuel Brachthäuser,
personPhilipp Schuster, and personKlaus Ostermann.
Effects as capabilities: effect handlers and
lightweight effect polymorphism.
journalProc. ACM Program. Lang.
volume4, numberOOPSLA (year2020),

[Convent, Lindley, McBride, and
McLaughlinConvent et al2020]
authorpersonLukas Convent, personSam
Lindley, personConor McBride, and personCraig
McLaughlin. year2020.
Doo bee doo bee doo.
journalJ. Funct. Program.  volume30
(year2020), pagese9.

authorpersonMatthias Felleisen.
The Theory and Practice of First-Class Prompts. In
booktitleConference Record of the Fifteenth Annual ACM
Symposium on Principles of Programming Languages, San Diego, California, USA,
January 10-13, 1988, editorpersonJeanne Ferrante
and personPeter Mager (Eds.). publisherACM
Press, pages180–190.

[Gunter, Rémy, and RieckeGunter
et al1995]
authorpersonCarl A. Gunter, personDidier
Rémy, and personJon G. Riecke.
A Generalization of Exceptions and Control in
ML-like Languages. In booktitleProceedings of the seventh
international conference on Functional programming languages and computer
architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995,
editorpersonJohn Williams (Ed.).
publisherACM, pages12–23.

authorpersonDaniel Hillerström.
titleComposing UNIX with Effect Handlers: A Case Study in
Effect Handler Oriented Programming.

Extended abstract, presented at ML Family Workshop 2021.

[Kammar, Lindley, and OuryKammar
et al2013]
authorpersonOhad Kammar, personSam Lindley,
and personNicolas Oury. year2013.
Handlers in action. In
booktitleACM SIGPLAN International Conference on
Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27,
2013, editorpersonGreg Morrisett and
personTarmo Uustalu (Eds.). publisherACM,

[Karachalias, Koprivec, Pretnar, and
SchrijversKarachalias et al2021]
authorpersonGeorgios Karachalias,
personFilip Koprivec, personMatija Pretnar, and
personTom Schrijvers. year2021.
Efficient compilation of algebraic effect
journalProc. ACM Program. Lang.
volume5, numberOOPSLA (year2021),

authorpersonDaan Leijen.
Type directed compilation of row-typed algebraic
effects. In booktitleProceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages, POPL 2017,
Paris, France, January 18-20, 2017,
editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

authorpersonPaul Blain Levy.
booktitleCall-By-Push-Value: A
Functional/Imperative Synthesis. seriesSemantics Structures in
Computation, Vol. volume2.

[Liang, Hudak, and JonesLiang
et al1995]
authorpersonSheng Liang, personPaul Hudak,
and personMark P. Jones. year1995.
Monad Transformers and Modular Interpreters. In
booktitleConference Record of POPL'95: 22nd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San
Francisco, California, USA, January 23-25, 1995,
editorpersonRon K. Cytron and
personPeter Lee (Eds.). publisherACM Press,

[Lindley and CheneyLindley and
authorpersonSam Lindley and personJames
Cheney. year2012.
Row-based effect types for database integration.
In booktitleProceedings of TLDI 2012: The Seventh ACM
SIGPLAN Workshop on Types in Languages Design and Implementation,
Philadelphia, PA, USA, Saturday, January 28, 2012,
editorpersonBenjamin C. Pierce (Ed.).
publisherACM, pages91–102.

authorpersonRobin Milner.
A Theory of Type Polymorphism in Programming.
journalJ. Comput. Syst. Sci. volume17,
number3 (year1978), pages348–375.

authorpersonEugenio Moggi.
Notions of Computation and Monads.
journalInf. Comput. volume93,
number1 (year1991), pages55–92.

[Piróg, Schrijvers, Wu, and
JaskelioffPiróg et al2018]
authorpersonMaciej Piróg, personTom
Schrijvers, personNicolas Wu, and personMauro
Jaskelioff. year2018.
Syntax and Semantics for Operations with Scopes.
In booktitleProceedings of the 33rd Annual ACM/IEEE
Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12,
2018, editorpersonAnuj Dawar and
personErich Grädel (Eds.). publisherACM,

[Plotkin and PowerPlotkin and Power2003]
authorpersonGordon D. Plotkin and
personJohn Power. year2003.
Algebraic Operations and Generic Effects.
journalAppl. Categorical Struct.
volume11, number1 (year2003),

[Plotkin and PretnarPlotkin and
authorpersonGordon D. Plotkin and
personMatija Pretnar. year2009.
Handlers of Algebraic Effects. In
booktitleProgramming Languages and Systems, 18th European
Symposium on Programming, ESOP 2009, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March
22-29, 2009. Proceedings (seriesLecture Notes in Computer
Science), editorpersonGiuseppe Castagna (Ed.),
Vol. volume5502. publisherSpringer,

authorpersonMatija Pretnar.
Inferring Algebraic Effects.
journalLog. Methods Comput. Sci.
volume10, number3 (year2014).

authorpersonDidier Rémy.
Typechecking Records and Variants in a Natural
Extension of ML. In booktitleConference Record of the
Sixteenth Annual ACM Symposium on Principles of Programming Languages,
Austin, Texas, USA, January 11-13, 1989. publisherACM Press,

[Schrijvers, Piróg, Wu, and
JaskelioffSchrijvers et al2019]
authorpersonTom Schrijvers, personMaciej
Piróg, personNicolas Wu, and personMauro
Jaskelioff. year2019.
Monad transformers and modular algebraic effects:
what binds them together. In booktitleProceedings of the
12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019,
Berlin, Germany, August 18-23, 2019,
editorpersonRichard A. Eisenberg (Ed.).
publisherACM, pages98–113.

[Schuster, Brachthäuser, and
OstermannSchuster et al2020]
authorpersonPhilipp Schuster,
personJonathan Immanuel Brachthäuser, and
personKlaus Ostermann. year2020.
Compiling effect handlers in capability-passing
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

[Sivaramakrishnan, Dolan, White, Kelly, Jaffer,
and MadhavapeddySivaramakrishnan et al2021]
authorpersonK. C. Sivaramakrishnan,
personStephen Dolan, personLeo White,
personTom Kelly, personSadiq Jaffer, and
personAnil Madhavapeddy. year2021.
Retrofitting effect handlers onto OCaml. In
booktitlePLDI '21: 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, Virtual Event,
Canada, June 20-25, 2021, editorpersonStephen N.
Freund and personEran Yahav (Eds.).
publisherACM, pages206–221.

[van den Berg, Schrijvers, Poulsen, and
Wuvan den Berg et al2021]
authorpersonBirthe van den Berg, personTom
Schrijvers, personCasper Bach Poulsen, and
personNicolas Wu. year2021.
Latent Effects for Reusable Language Components.
In booktitleProgramming Languages and Systems - 19th Asian
Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings
(seriesLecture Notes in Computer Science),
editorpersonHakjoo Oh (Ed.),
Vol. volume13008. publisherSpringer,

authorpersonPhilip Wadler.
The Essence of Functional Programming. In
booktitleConference Record of the Nineteenth Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
Albuquerque, New Mexico, USA, January 19-22, 1992,
editorpersonRavi Sethi (Ed.).
publisherACM Press, pages1–14.

[Wright and FelleisenWright and
authorpersonAndrew K. Wright and
personMatthias Felleisen. year1994.
A Syntactic Approach to Type Soundness.
journalInf. Comput. volume115,
number1 (year1994), pages38–94.

[Wu and SchrijversWu and Schrijvers2015]
authorpersonNicolas Wu and personTom
Schrijvers. year2015.
Fusion for Free - Efficient Algebraic Effect
Handlers. In booktitleMathematics of Program Construction -
12th International Conference, MPC 2015, Königswinter, Germany, June
29 - July 1, 2015. Proceedings (seriesLecture Notes in
Computer Science), editorpersonRalf Hinze and
personJanis Voigtländer (Eds.),
Vol. volume9129. publisherSpringer,

[Wu, Schrijvers, and HinzeWu
et al2014]
authorpersonNicolas Wu, personTom
Schrijvers, and personRalf Hinze.
Effect handlers in scope. In
booktitleProceedings of the 2014 ACM SIGPLAN symposium
on Haskell, Gothenburg, Sweden, September 4-5, 2014,
editorpersonWouter Swierstra (Ed.).
publisherACM, pages1–12.

[Xie, Brachthäuser, Hillerström,
Schuster, and LeijenXie et al2020]
authorpersonNingning Xie,
personJonathan Immanuel Brachthäuser,
personDaniel Hillerström, personPhilipp
Schuster, and personDaan Leijen.
Effect handlers, evidently.
journalProc. ACM Program. Lang.
volume4, numberICFP (year2020),

§ PROOF SKETCH OF SUBJECT REDUCTION AND PROGRESS LEMMAS

§.§ Subject Reduction

For all expressions  and , if  and ,
it follows that .

The proof proceeds by rule induction over the derivation .

Impossible,  is empty.

$\ensuremath{e_{1}\mathbin{-->}e_{2}\mathrel{=}(\Varid{λ}\;\Varid{x}}.\ensuremath{\Varid{e})\;\Varid{v}}$. From the sub-derivations of T-App,
from which ends in T-Abs, we derive $\ensuremath{\Conid{Γ},\Varid{x}\mathbin{:}\Varid{τ}^{\prime}\mathbin{⊢}\Varid{e}\mathbin{:}\Varid{τ}\mathbin{∣}\Varid{ε}\mathbin{*}\epsilon_{l}}$
and $\ensuremath{\Conid{Γ}\mathbin{⊢}\Varid{v}\mathbin{:}\Varid{τ}^{\prime}\mathbin{∣}\Varid{ε}\mathbin{*}\epsilon_{l}}$. Consequently, from <ref> it
follows that $[x/\ensuremath{\Varid{v}}]\ $. The case for Let
uses similar reasoning.

Follow immediately from the induction hypothesis.

$\ensuremath{e_{1}\mathbin{-->}e_{2}\mathrel{=}}$ e$\ensuremath{\kw{!}\mathbin{-->}\Varid{e}}$, hence the sub-derivation of
T-Enact ends with T-Suspend, giving us

Case analysis on  gives us the following two sub-cases:

* $[x/\ensuremath{\Varid{v}},p/\ensuremath{\Varid{v}_{\Varid{p}}}]$
(Return). From the sub-derivations of T-Handle, we learn
that $\ensuremath{\Conid{Γ},\Varid{x}\mathbin{:}\Varid{τ}^{\prime},\Varid{p}\mathbin{:}\tau_{p}\mathbin{⊢}\Varid{e}\mathbin{:}}\ann{\ensuremath{\Varid{ε}\mathbin{*}\mathbin{⟨}\Varid{ℓ},\epsilon_{l}\mathbin{⟩}}}{\susp{\ensuremath{\tau_{2}}}}\ensuremath{\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$
(1), $\ensuremath{\Conid{Γ}\mathbin{⊢}\Varid{v}\mathbin{:}\tau_{1}\mathbin{∣}\mathbin{⟨}\Varid{ℓ},\Varid{ε}\mathbin{⟩}\mathbin{*}\epsilon_{l}}$ (2), and
$\ensuremath{\Conid{Γ}\mathbin{⊢}\Varid{v}_{\Varid{p}}\mathbin{:}\tau_{p}\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$ (3) hold. From <ref>,
(1), and (3) we then have
$[p/\ensuremath{\Varid{v}_{\Varid{p}}}]$  (4). Then, from <ref>,
<ref>, (2), and (4) we derive
$\ensuremath{\Conid{Γ}\mathbin{⊢}\Varid{e}}[x/\ensuremath{\Varid{v}},p/\ensuremath{\Varid{v}_{\Varid{p}}}]\ \ensuremath{\mathbin{:}}\ann{\ensuremath{\Varid{ε}\mathbin{*}\mathbin{⟨}\Varid{ℓ},\epsilon_{l}\mathbin{⟩}}}{\susp{\ensuremath{\tau_{2}}}}\ensuremath{\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$.

* $\ensuremath{e_{1}\mathbin{-->}e_{2}\mathrel{=}\kw{handle}^{\ell}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}\;\Conid{E}^{\Varid{ℓ}}}[\ensuremath{(\op{op}^{\ell}\;\Varid{f}\;\overline{\Varid{v}})\kw{!}}]\ \ensuremath{\Varid{v}_{\Varid{p}}\mathbin{-->}\Varid{e}}[\bsubst{x}{\ensuremath{\Varid{v}}},p/\ensuremath{\Varid{v}_{\Varid{p}}},k/\ensuremath{(\Varid{λ}\;\Varid{y}\;\Varid{q}}.\ensuremath{\kw{handle}^{\ell}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}}\ \\ \inE{\ensuremath{\Varid{y}\kw{!}}}\ \ensuremath{\Varid{q})}]$ (Handle). From the sub-derivations of
T-Handle, we learn that
$\ensuremath{\Conid{Γ},\overline{x_{i}},\Varid{p},\Varid{k}\mathbin{⊢}\Varid{e}\mathbin{:}}\ann{\ensuremath{\Varid{ε}\mathbin{*}\mathbin{⟨}\Varid{ℓ},\epsilon_{l}\mathbin{⟩}}}{\susp{\ensuremath{\tau_{2}}}}\ensuremath{\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$ (1), $[$$]\ $ (2),
$\ensuremath{\Conid{Γ}\mathbin{⊢}\Varid{v}_{\Varid{p}}\mathbin{:}\tau_{p}\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$ (3), and
$\ensuremath{\Conid{Γ}\mathbin{⊢}\op{op}^{ℓ}_{i}\mathbin{:}\mathbin{∀}\Varid{r}\;r_{l}\;\!.\!\;\overline{\tau_{i}}}[\ensuremath{\Varid{r}}/\ensuremath{\Varid{ε}},\ensuremath{r_{l}},\ensuremath{\epsilon_{l}}]\ensuremath{\to }\ann{\ensuremath{\Varid{ε}\mathbin{⊕}\epsilon_{l}\mathbin{⊕}\mathbin{⟨}\Varid{ℓ}\mathbin{⟩}\mathbin{*}\mathbin{⟨⟩}}}{\susp{\ensuremath{\tau_{i}}}}\
\ensuremath{\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$ (5).

We discharge , , and  from the context in (1) using
repeated applications of <ref>, concluding
$\ensuremath{\Conid{Γ}\mathbin{⊢}e_{2}\mathbin{:}\Varid{τ}\mathbin{∣}\Varid{ε}^{\prime}\mathbin{*}\epsilon_{l}^{\prime}}$.  We obtain the required derivations for the
substituted values as follows:

* For , we use the T-Abs and T-Handle rules,
together with <ref> and (2) to construct a
derivation that the expression $\ensuremath{(\Varid{λ}\;\Varid{y}\;\Varid{q}}.\ensuremath{\kw{handle}^{\ell}\;\{\mskip1.5mu \overline{\Conid{C}}\mskip1.5mu\}}\
\inE{\ensuremath{\Varid{y}\kw{!}}}\ \ensuremath{\Varid{q})}$ has the required type.

* For , we use (3).

* For , we use the sub-derivations we get from (2) by decomposing the
operation call and its context, removing the trailing occurrences of T-App.

§.§ Progress

For every expression , if , then either there exists
some  such that , or  is a value, where  is an initial
context that contains bindings for the operations of all known effects in .

We proceed by rule induction over the derivation for  .

[T-Var, T-Abs]
is a value.

, thus from the induction hypothesis for  we know that we can
either step , or  is a value, in which case it must be a
-abstraction and we can step using the -rule.

. The induction hypothesis for e₁ tells us that
is either a value, or it can be reduced. In the former case, we step using
the Let rule. Otherwise, we reduce .

[T-Inst, T-Gen, T-Resurface]
, follows from the induction hypothesis.

e, thus  is a value.

, thus from the induction hypothesis for  we know that either we
can step , or  is value. In the latter case  must of the form
$\susp{e}$ and we step with the Enact rule.

. The induction hypothesis for  tells us we
can either step , or  is a value. In the latter case, by the
induction hypothesis for  we can either step ,  enacts an operation
of the effect , or  is a value, in which case we step either
with Handle or Return.

§ PROVING SEPARATION OF CONCERNS

This appendix contains the proof that handling order is irrelevant for nested handlers with separate concerns; i.e.,

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Varid{e}\mathbin{:}\ann{\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε}\mathbin{⟩}\mathbin{⟩}\mathbin{*}\Varid{ε'}}{\susp{\Conid{X}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e})) \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{ex})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }.
\end{equation*}

To get a more useful induction hypothesis, we generalize  as follows, where  represents a sequence of zero or more  reductions:

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Varid{e}\mathbin{:}\ann{\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε}\mathbin{⟩}\mathbin{⟩}\mathbin{*}\Varid{ε'}}{\susp{\Conid{X}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}e_{0} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\and \ensuremath{\Conid{H0}^{\prime}\mathbin{:}e_{0} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e}))}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{ex})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }.
\end{equation*}

The proof assumes that the handler op lemma holds for each handler.
The rule below summarizes the handler op lemma proposition, which assumes that  and  satisfy the handler return lemma:

Each operation  of handler  .  provides separation of concerns.
That is,

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[\op{op}^{\ell}\;\Varid{f}\;\overline{\Varid{v}_{\Varid{v}}}\;\overline{\susp{e_{\Varid{m}}}}])) \longmapsto \Varid{e}^{\prime}}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Conid{E}[\op{op}^{\ell}\;\Varid{f}\;\overline{\Varid{v}_{\Varid{v}}}\;\overline{\{\mskip1.5mu e_{\Varid{m}}\mskip1.5mu\}}])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Furthermore, we assume that handler return lemma holds for each handler; i.e.,

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r}^{\prime}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Varid{ℓ},\Varid{r}^{\prime}\mathbin{⟩}}{\susp{\Conid{F}\;\Varid{α}}}}
\\ \ensuremath{\Varid{p}\mathbin{:}\Conid{P}}
\\ \ensuremath{\Varid{v}\mathbin{:}\Conid{X}}
{ \ensuremath{\Varid{toBag}_{\Conid{F}}\;(\Varid{h}^{\Varid{p}}\;\susp{\Varid{v}})\mathrel{=}\{\mskip1.5mu \Varid{v}\mskip1.5mu\}} }
\end{equation*}

Lastly, we assume the following definition of .

§.§ Proof that Handling Order is Irrelevant for Nested Handlers with Separate Concerns

Our goal is to prove

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Varid{e}\mathbin{:}\ann{\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε}\mathbin{⟩}\mathbin{⟩}\mathbin{*}\Varid{ε'}}{\susp{\Conid{X}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}e_{0} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\and \ensuremath{\Conid{H0}^{\prime}\mathbin{:}e_{0} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e}))}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }.
\end{equation*}

The proof is by rule induction on .

The base case of the induction proof holds vacuously, because a value  cannot  reduce to .

The proof obligation for the inductive case is

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Varid{e}\mathbin{:}\ann{\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε}\mathbin{⟩}\mathbin{⟩}\mathbin{*}\Varid{ε'}}{\susp{\Conid{X}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}e_{0} \longmapsto \Varid{e}^{\prime}}
\\ \ensuremath{\Conid{H0}^{\prime}\mathbin{:}e_{0} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e}))}
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inverting , there are two cases to consider.

The goal is

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Varid{e}\mathbin{:}\ann{\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε}\mathbin{⟩}\mathbin{⟩}\mathbin{*}\Varid{ε'}}{\susp{\Conid{X}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e})) \longmapsto \Varid{e}^{\prime}}
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inverting  using the definition of  and , the cases for  and  follow trivially from the induction hypothesis.
The Return case follows from the handler return lemmas of  and , and the Handle case follows from the handler op lemmas of  and .

The goal is

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_1\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{1},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_1\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_1\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\ell_{1},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Varid{e}\mathbin{:}\ann{\mathbin{⟨}\ell_{1},\mathbin{⟨}\ell_{2},\Varid{ε}\mathbin{⟩}\mathbin{⟩}\mathbin{*}\Varid{ε'}}{\susp{\Conid{X}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}e_{0} \longmapsto \Varid{e}^{\prime}}
\\ \ensuremath{\Conid{H0}^{\prime}\mathbin{:}e_{0} \longmapsto _{\beta}e_{0}^{\prime}}
\\ \ensuremath{\Conid{H0}^{\prime\prime}\mathbin{:}e_{0}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Varid{e}))}
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;\Varid{e})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_1^{\Varid{p}_{1}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }.
\end{equation*}

Because  is a deterministic relation, we get that , and that the goal follows from the induction hypothesis.

§.§ S.o.C. Lemmas for the State Handler

§.§.§ Handler Return Lemma for the State Handler

The goal is to prove that

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}_{\Conid{St}}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r}^{\prime}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{St},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{S}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r}^{\prime}\mathbin{⟩}}{\susp{(\Varid{α},\Conid{S})}}}
\\ \ensuremath{\Varid{s}\mathbin{:}\Conid{S}}
\\ \ensuremath{\Varid{v}\mathbin{:}\Conid{X}}
{ \ensuremath{\Varid{toBag}_{(,)\;\Conid{S}}\ (\Varid{h}_{\Conid{St}}^{\Varid{s}}\;\susp{\Varid{v}})\mathrel{=}\{\mskip1.5mu \Varid{v}\mskip1.5mu\}} }
\end{equation*}

The goal follows trivially from the definition of the return case of the state handler.

§.§.§ Handler Op Lemma for the State Handler

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{St},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{St},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_{\Conid{St}}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{St},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{S}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r'}\mathbin{⟩}}{\susp{(\Varid{α},\Varid{s})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[\op{put}\;\Varid{s}^{\prime}])) \longmapsto \Varid{e}^{\prime}}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;\Conid{E}[\op{put}\;\Varid{s}^{\prime}])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inversion on .

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{St},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{St},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_{\Conid{St}}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{St},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{S}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r'}\mathbin{⟩}}{\susp{(\Varid{α},\Varid{s})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
%  \\ |H0: (hdl h p) ((hdl hSt s) ((hdl h₂ p2) (decomp E (put s ′))))
%       >--> e ′|
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime}\mathbin{≡}\Varid{h}\;(((\Varid{λ}\;()\;\Varid{s}^{\prime\prime}\!.\!\;\Varid{h}_{\Conid{St}}^{\Varid{s}^{\prime\prime}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[()]))\;()\;\Varid{s}^{\prime})) \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;\Conid{E}[\op{put}\;\Varid{s}^{\prime}])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inversion on  and ; specialize , using .

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{St},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{St},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{h}_{\Conid{St}}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{St},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{S}\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r'}\mathbin{⟩}}{\susp{(\Varid{α},\Varid{s})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{St},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
%  \\ |H0: (hdl h p) ((hdl hSt s) ((hdl h₂ p2) (decomp E (put s ′))))
%       >--> e ′|
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{h}\;(\Varid{h}_{\Conid{St}}^{\Varid{s'}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[()])) \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;\Conid{E}[()])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}}
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{h}_{\Conid{St}}^{\Varid{s}}\;\Conid{E}[()])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Goal follows from  and .

Analogous to the case for .

§.§ S.o.C. Lemmas for the Catch Handler

§.§.§ Handler Return Lemma for the Catch Handler

The goal is to show that

\begin{equation*}
\inferrule
{ \ensuremath{\Varid{hCatch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\ \ensuremath{\ann{\mathbin{⟨}\Conid{Catch},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}()\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{(\Conid{Maybe}\;\Varid{α})}}}
\\
\ensuremath{\Varid{v}\mathbin{:}\Conid{X}} }
{ \ensuremath{\Varid{toBag}_{\Conid{Maybe}}\ (\Varid{hCatch}^{()}\;\susp{\Varid{v}})}
\end{equation*}

\begin{align*}
\ensuremath{\Varid{toBag}_{\Conid{Maybe}}\ (\Conid{Just}\;\Varid{x})} &= \ensuremath{\{\mskip1.5mu \Varid{x}\mskip1.5mu\}}
\\
\ensuremath{\Varid{toBag}_{\Conid{Maybe}}\ \Conid{Nothing}} &= \ensuremath{\{\mskip1.5mu \mskip1.5mu\}}
\end{align*}

The goal follows trivially from the definition of the return case of the catch handler.

§.§.§ Handler Op Lemma for the Catch Handler

Assumes that  and  satisfy the handler return lemma.

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{hCatch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{Catch},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}()\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{(\Conid{Maybe}\;\Varid{α})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{hCatch}^{()}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[\op{throw}])) \longmapsto \Varid{e}^{\prime}}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;\Conid{E}[\op{throw}])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{hCatch}^{()}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inversion on .

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{hCatch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{Catch},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}()\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{(\Conid{Maybe}\;\Varid{α})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{h}^{\Varid{p}}\;\susp{\Conid{Nothing}} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;\Conid{E}[\op{throw}])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{hCatch}^{()}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inversion on  using definition of  and .

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{hCatch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{Catch},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}()\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{(\Conid{Maybe}\;\Varid{α})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{h}^{\Varid{p}}\;\susp{\Conid{Nothing}} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{Nothing}) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{hCatch}^{()}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

The goal follows from the fact that  and  satisfy the handler return lemma.

The goal is

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{hCatch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{Catch},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}()\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{(\Conid{Maybe}\;\Varid{α})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H0}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{hCatch}^{()}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[(\op{catch}\;\Varid{m}_{1}\;\Varid{m}_{2})])) \longmapsto \Varid{e}^{\prime}}
\and \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime} \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;\Conid{E}[(\op{catch}\;\Varid{m}_{1}\;\Varid{m}_{2})])) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\
\ensuremath{\Varid{e}^{\prime} \longtwoheadmapsto _{\beta}^{*}\Varid{h}^{\Varid{p}}\;(\Varid{hCatch}^{()}\;(\Varid{h}_2^{\Varid{p}_{2}}\;e_{0})) \Longrightarrow }
\ensuremath{\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;(\Varid{hCatch}^{()}\;e_{0})) \longtwoheadmapsto \Varid{v}_{\mathrm{21}} \Longrightarrow }
\ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}}
\end{array}\right)}
{ \ensuremath{\Varid{v}_{\mathrm{12}}\sim\Varid{v}_{\mathrm{21}}} }
\end{equation*}

Inversion on  and .

\begin{equation*}
\inferrule*
{  \ensuremath{\Varid{h}\mathbin{:}\mathbin{∀}\Varid{α}}.\
\ensuremath{\ann{\Varid{ε}\mathbin{*}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩}\mathbin{⟩}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}\mathbin{→}\ann{\mathbin{⟨⟩}\mathbin{*}(\Varid{ε}\mathbin{⊕}\mathbin{⟨}\Conid{Catch},\mathbin{⟨}\ell_{2},\Varid{ε'}\mathbin{⟩⟩})}{\susp{\Conid{G}\;\Varid{α}}}}
\\ \ensuremath{\Varid{hCatch}\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\Conid{Catch},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}()\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{(\Conid{Maybe}\;\Varid{α})}}}
\\ \ensuremath{\Varid{h}_2\mathbin{:}\mathbin{∀}\Varid{α}\;\Varid{r}\;\Varid{r'}}.\
\ensuremath{\ann{\mathbin{⟨}\ell_{2},\Varid{r}\mathbin{⟩}\mathbin{*}\Varid{r'}}{\susp{\Varid{α}}}\mathbin{→}\Conid{P}_2\mathbin{→}\ann{\Varid{r}\mathbin{*}\mathbin{⟨}\Conid{Catch},\Varid{r'}\mathbin{⟩}}{\susp{\Conid{F}_2\;\Varid{α}}}}
\\ \ensuremath{\Conid{H1}\mathbin{:}\Varid{e}^{\prime}\mathbin{≡}\Varid{h}^{\Varid{p}}\;((\Varid{λ}\;\Varid{x}\;\Varid{q}\;\!.\!\;\Varid{hCatch}^{\Varid{q}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;\Conid{E}[\Varid{x}\mathbin{!}]))\;\susp{\begin{array}{l} \kw{match}(\Varid{hCatch}^{()}\;\Varid{m}_{1})\\\;\mid\Conid{Nothing}\mathbin{→}\Varid{m}_{2}\mathbin{!}\\\;\mid(\Conid{Just}\;\Varid{x})\mathbin{→}\Varid{x}\end{array}}\;()) \longtwoheadmapsto \Varid{v}_{\mathrm{12}}}
\\ \ensuremath{\Conid{H2}\mathbin{:}\Varid{h}^{\Varid{p}}\;(\Varid{h}_2^{\Varid{p}_{2}}\;((\Varid{λ}\;\Varid{x}\;\Varid{q}\;\!.\!\;(\Varid{hCatch}^{\Varid{q}}\;\Conid{E}[\Varid{x}\mathbin{!}]))\;\susp{\begin{array}{l} \kw{match}(\Varid{hCatch}^{()}\;\Varid{m}_{1})\\\;\mid\Conid{Nothing}\mathbin{→}\Varid{m}_{2}\mathbin{!}\\\;\mid(\Conid{Just}\;\Varid{x})\mathbin{→}\Varid{x}\end{array}})\;()) \longtwoheadmapsto \Varid{v}_{\mathrm{21}}}
\\ \ensuremath{\Conid{IH}\mathbin{:}} {\left(\begin{array}{l}
\ensuremath{\mathbin{∀}e_{0}}.\