# A Functional Abstraction of
Typed Invocation Contexts

Youyou Cong  Tokyo Institute of Technology, 2-12-1, Ookayama, Meguro-ku,
Tokyo, Japan<EMAIL_ADDRESS>,  Chiaki Ishio  Ochanomizu University,
2-1-1, Otsuka, Bunkyo-ku, Tokyo, Japan<EMAIL_ADDRESS>,  Kaho
Honda  Ochanomizu University, 2-1-1, Otsuka, Bunkyo-ku, Tokyo, Japan
<EMAIL_ADDRESS>and  Kenichi Asai  Ochanomizu University, 2-1-1,
Otsuka, Bunkyo-ku, Tokyo, Japan<EMAIL_ADDRESS>
###### Abstract.

In their paper “A Functional Abstraction of Typed Contexts”, Danvy and
Filinski show how to derive a type system of the shift and reset operators
from a CPS semantics. In this paper, we show how this method scales to
Felleisen’s control and prompt operators. Compared to shift and reset, control
and prompt exhibit a more dynamic behavior, in that they can manipulate a
_trail_ of contexts surrounding the invocation of previously captured
continuations. Our key observation is that, by adopting a functional
representation of trails in the CPS semantics, we can derive a type system
that encodes all and only constraints imposed by the CPS semantics.

###### Key words and phrases:

delimited continuations, control operators, control and prompt, CPS
translation, type system

###### keywords:

data

###### keywords:

data

###### keywords:

data

###### keywords:

where

###### keywords:

data

###### keywords:

where

###### keywords:

data

###### keywords:

data

###### keywords:

data

###### keywords:

where

###### keywords:

data

###### keywords:

where

###### keywords:

data

###### keywords:

where

Supported in part by JSPS KAKENHI under Grant No. JP19K24339.

Supported in part by JSPS KAKENHI under Grant No. JP18H03218.

##  1\. Introduction

Delimited continuations have been proven useful in diverse domains. Their
applications range from representation of monadic effects [25], to
formalization of partial evaluation [18], and to implementation of automatic
differentiation [53]. As a means to handle delimited continuations,
researchers have designed a variety of _control operators_ [24, 20, 28, 22,
42]. Among them, Danvy and Filinski’s [20] shift/reset operators have a solid
theoretical foundation: there exist a simple CPS translation [20], a general
type system [19], and a set of equational axioms [34]. A variation of
shift/reset, known as shift0/reset0, also have similar theoretical artifacts,
due to recent work by Materzok and Biernacki [42, 41]. Other variants,
however, are not as well-understood as the aforementioned ones, because of
their complex semantics.

Understanding the subtleties of control operators is important, especially
given the rapid adoption of _algebraic effects and handlers_ [47, 6] observed
in the past decade. Effect handlers can be thought of as a generalization of
exception handlers that provide access to the continuation surrounding an
exception. As suggested by the similarity in the functionality, effect
handlers have a close connection with control operators [26, 46], and in fact,
they are often implemented using control operators provided by the host
language [36, 39]. This means, a well-established theory of control operators
is crucial for safer and more efficient implementation of effect handlers.

In this paper, we formalize a typed calculus of control and prompt, a pair of
control operators proposed by Felleisen [24]. These operators bring an
interesting behavior into programs: when a captured continuation $k$ is
invoked, the subsequent computation may capture the context surrounding the
invocation of $k$. From a practical point of view, the ability to manipulate
invocation contexts is useful for implementing sophisticated algorithms, such
as list reversing [9] and breadth-first traversal [11]. From a theoretical
perspective, on the other hand, this ability makes it hard to type programs in
a way that fully reflects their runtime behavior.

We address the challenge with typing by rigorously following Danvy and
Fillinski’s [19] recipe for building a type system of a delimited control
calculus. The idea is to analyze the denotational semantics of the calculus —
essentially a CPS translation — and identify all the constraints that are
necessary for making the denotation well-typed. In fact, the recipe has been
applied to the control and prompt operators before [35], but the type system
obtained is not satisfactory for two reasons. First, the type system imposes
certain restrictions on the contexts in which a captured continuation may be
invoked. Second, the type system does not precisely describe the way contexts
compose and propagate during evaluation. We show that, by choosing a right
representation of invocation contexts in the CPS translation, we can build a
type system without such limitations.

Below is a summary of our specific contributions:

  * •

We present a type system of control and prompt that accounts for manipulation
of invocation contexts. The type system is the control/prompt-equivalent of
Danvy and Filinski’s [19] type system for shift/reset, in that it incorporates
all and only constraints that are imposed by the CPS translation.

  * •

We prove three properties of our calculus: type soundness, type preservation
of the CPS translation, and termination of well-typed programs. Among these
properties, termination relies on the precise typing of invocation contexts
available in our calculus; indeed, the property does not hold for the existing
type system of control and prompt [35].

  * •

We further design a more fine-grained type system that distinguishes between
pure and impure expressions, and define a selective CPS translation based on
the type system. The selective translation is crucial for practical
implementation of control and prompt, as it generates less administrative
redexes.

  * •

We formalize our calculi and CPS translations in the Agda proof assistant
[45]. The formalization serves as the mechanized proofs of many of the
theorems stated in the paper, and is available online at
https://github.com/YouyouCong/lmcs-artifact.

We begin with an informal account of control and prompt (Section 2),
highlighting the dynamic behavior of these operators. We next formalize an
untyped calculus of control/prompt (Section 3) and its CPS translation
(Section 4). Then, from the CPS translation, we derive a type system of our
calculus (Section 5), and prove its properties (Section 6). Having established
a basic typing principle, we refine the calculus with the notion of purity,
and define a selective CPS translation (Section 7). After that, we briefly
explain how we developed our Agda formalization. Lastly, we discuss related
work (Section 9) and conclude with future directions (Section 10).

#### Relation to Prior Work

This is an updated and extended version of our previous paper [16]. The
primary new contribution of this version is the fine-grained calculus and
selective CPS translation developed in Section 7. We also used the extra space
to describe our Agda formalization and expand various discussions.

##  2\. Control and Prompt

In this section, we familiarize the reader with control and prompt by walking
through two examples. These examples exhibit the dynamic behavior of control
and prompt, as well as the heterogeneous nature of captured contexts.

###  2.1. The Dynamic Behavior of Control

The control and prompt operators are control primitives for capturing and
delimiting continuations. To see how these operators behave, let us look at
the following program:

$\displaystyle\langle(\mathcal{F}k_{1}.\,2*(k_{1}\
5))+(\mathcal{F}k_{2}.\,3+(k_{2}\ 8))\rangle+13$ (1)

Throughout the paper, we write $\mathcal{F}$ to mean control and
$\langle\rangle$ to mean prompt. Under the call-by-value, left-to-right
evaluation strategy, the above program evaluates in the following way:

$\displaystyle\langle(\mathcal{F}k_{1}.\,2*(k_{1}\
5))+(\mathcal{F}k_{2}.\,3+(k_{2}\ 8))\rangle+13$ $\displaystyle=\langle
2*(k_{1}\ 5)\,[\lambda x.\,x+(\mathcal{F}k_{2}.\,3+(k_{2}\
8))/k_{1}]\rangle+13$ $\displaystyle=\langle
2*(5+(\mathcal{F}k_{2}.\,3+(k_{2}\ 8)))\rangle+13$ $\displaystyle=\langle
3+(k_{2}\ 8)\,[\lambda x.\,2*(5+x)/k_{2}]\rangle+13$ $\displaystyle=\langle
3+(2*(5+8))\rangle+13$ $\displaystyle=42$

The first control operator captures the delimited context up to the enclosing
prompt, namely $[.]+(\mathcal{F}k_{2}.\,3+(k_{2}\ 8))$ (where $[.]$ denotes a
hole). The captured context is then reified into a function $\lambda
x.\,x+(\mathcal{F}k_{2}.\,3+(k_{2}\ 8))$, and evaluation shifts to the body
$2*(k_{1}\ 5)$, where $k_{1}$ is the reified continuation. After
$\beta$-reducing the invocation of $k_{1}$, we obtain another control in the
evaluation position. This control captures the context $2*(5+[.])$, which is a
composition of _two_ contexts: the addition context originally surrounding the
control construct, and the multiplication context surrounding the invocation
of $k_{1}$. The context is then reified into a function $\lambda x.\,2*(5+x)$,
and evaluation shifts to the body $3+(k_{2}\ 8)$, where $k_{2}$ is the reified
continuation. By $\beta$-reducing the invocation of $k_{2}$, we obtain the
expression $3+(2*(5+8))$, where the original delimited context, the invocation
context of $k_{1}$, and the invocation context of $k_{2}$ are all composed
together. The expression returns the value $29$ to the enclosing prompt
clause, and the evaluation of the whole program finishes with $42$.

From this example, we observe that a control operator can capture the context
surrounding the invocation of a previously captured continuation. More
generally, control may capture a _trail_ of such invocation contexts. The
ability comes from the absence of the delimiter in the body of captured
continuations. Indeed, if we replace control with shift ($\mathcal{S}$) in the
above program, the second shift would have no access to the context $2*[.]$,
since the first shift would insert a reset into the continuation $k_{1}$. As a
consequence, the program yields a different result $45$.

$\displaystyle\langle(\mathcal{S}k_{1}.\,2*(k_{1}\
5))+(\mathcal{S}k_{2}.\,3+(k_{2}\ 8))\rangle+13$ $\displaystyle=\langle
2*(k_{1}\ 5)\,[\lambda x.\,\langle x+(\mathcal{S}k_{2}.\,3+(k_{2}\
8))\rangle/k_{1}]\rangle+13$ $\displaystyle=\langle 2*\langle
5+(\mathcal{S}k_{2}.\,3+(k_{2}\ 8))\rangle\rangle+13$ $\displaystyle=\langle
2*\langle 3+(k_{2}\ 8)\,[\lambda x.\,\langle
5+x\rangle/k_{2}]\rangle\rangle+13$ $\displaystyle=\langle 2*\langle 3+\langle
5+8\rangle\rangle\rangle+13$ $\displaystyle=45$

In the continuations literature, control/prompt are classified as _dynamic_ ,
because they require us to actually run a program in order to see what
continuation a control captures. In contrast, shift/reset are called _static_
, as they allow us to determine the extent of continuations from the lexical
information of a program.

###  2.2. The Heterogeneous Nature of Trails

In the example discussed above, we only had contexts whose input and output
types are both int. In practice, however, we may wish to deal with contexts
having different input and output types. Here is such an example:

$\displaystyle\langle(\mathcal{F}k_{1}.\,\texttt{is0}\ (k_{1}\
5))+(\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\ 8))\rangle$ (2)

We assume two primitive functions: is0, which tells us if a given integer is
zero or not, and b2s, which converts a boolean into a string "true" or
"false". Below is the reduction sequence of the above program:

$\displaystyle\langle(\mathcal{F}k_{1}.\,\texttt{is0}\ (k_{1}\
5))+(\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\ 8))\rangle$
$\displaystyle=\langle\texttt{is0}\ (k_{1}\ 5)\,[\lambda
x.\,x+(\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\ 8))/k_{1}]\rangle$
$\displaystyle=\langle\texttt{is0}\ (5+(\mathcal{F}k_{2}.\,\texttt{b2s}\
(k_{2}\ 8)))\rangle$ $\displaystyle=\langle\texttt{b2s}\ (k_{2}\ 8)\,[\lambda
x.\,\texttt{is0}\ (5+x)/k_{2}]\rangle$ $\displaystyle=\langle\texttt{b2s}\
(\texttt{is0}\ (5+8))\rangle$ $\displaystyle=\langle\texttt{b2s}\
(\texttt{is0}\ 13)\rangle$ $\displaystyle=\langle\texttt{b2s}\
\texttt{false}\rangle$ $\displaystyle=\langle\texttt{"{false}"}\rangle$
$\displaystyle=\texttt{"{false}"}$

The first control operator captures the delimited context
$[.]+(\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\ 8))$, and invokes it in the
context $\texttt{is0}\ [.]$. The second control captures the context
$\texttt{is0}\ (5+[.])$, and invokes it in the context $\texttt{b2s}\ [.]$. By
composing these contexts, and by plugging $8$ into the hole, we obtain
$\texttt{b2s}\ (\texttt{is0}\ (5+8))$, which evaluates to the string "false".

From this example, we observe that a trail of invocation contexts can be
_heterogeneous_. In particular, the input and output types of each context can
be different. Of course, the invocation contexts in a heterogeneous trail must
align in a way that makes their composition type-safe. The type safety holds
when the input type of an invocation context is equal to the output type of
the previous context. It is easy to see that example (2) meets this condition:
the original delimited context ($5+[.]$) is int-to-int, the first invocation
context ($\texttt{is0}\ [.]$) is int-to-bool, and the second invocation
context ($\texttt{b2s}\ [.]$) is bool-to-string. Therefore, the application
$\texttt{b2s}\ (k_{2}\ 8)$ is well-typed.

It turns out that example (2) is judged ill-typed by the existing type system
for control and prompt [35]. This is because the type system imposes the
following restrictions on the type of invocation contexts.

  * •

All invocation contexts within a prompt clause must have the same type.

  * •

For each invocation context, the input and output types must be the same.

We claim that, a fully general type system of control and prompt should be
more flexible about the type of invocation contexts. Now the question is: Is
it possible to allow such flexibility? Our answer is “yes”. As we will see in
Section 5, we can build a type system that accommodates invocation contexts
having different types, and that accepts example (2) as a well-typed program.

##  3\. $\lambda_{\mathcal{F}}$: A Calculus of Control and Prompt

Syntax

$\displaystyle v$ $\displaystyle::=c\mid x\mid\lambda x.\,e$ Values
$\displaystyle e$ $\displaystyle::=v\mid e\ e\mid\mathcal{F}k.\,e\mid\langle
e\rangle$ Expressions

Evaluation Contexts

$\displaystyle E$ $\displaystyle::=[]\mid E\ e\mid v\ E\mid\langle E\rangle$
General Contexts $\displaystyle F$ $\displaystyle::=[]\mid F\ e\mid v\ F$ Pure
Contexts

Reduction Rules

$\displaystyle E[(\lambda x.\,e)\ v]$ $\displaystyle\leadsto E[e\,[v/x]]$
$\displaystyle(\textsc{$\beta$})$ $\displaystyle E[\langle
F[\mathcal{F}k.\,e]\rangle]$ $\displaystyle\leadsto E[\langle e\,[\lambda
x.\,F[x]/k]\rangle]$ $\displaystyle(\textsc{$\mathcal{F}$})$ $\displaystyle
E[\langle v\rangle]$ $\displaystyle\leadsto E[v]$
$\displaystyle(\textsc{$\mathcal{P}$})$

Figure 1. Syntax and Reduction of $\lambda_{\mathcal{F}}$

Having seen how control and prompt behave, we define a formal calculus of
these operators. In Figure 1, we present $\lambda_{\mathcal{F}}$, a (currently
untyped) $\lambda$-calculus extended with control and prompt. The calculus has
a separate syntactic category for values, which, in addition to variables and
abstractions, includes a set of constants $c$ (such as integers, booleans, and
string literals). Expressions consist of values, application, and delimited
control constructs control and prompt.

We equip $\lambda_{\mathcal{F}}$ with a call-by-value, left-to-right
evaluation strategy. As is usual with delimited control calculi, there are two
groups of evaluation contexts: general contexts ($E$) and pure contexts ($F$).
Their difference is that general contexts may contain prompt surrounding a
hole, while pure contexts can never have such prompt. The distinction is used
in the reduction rule ($\mathcal{F}$) of control, which says, control always
captures the context up to the nearest enclosing prompt. In the reduct, we see
that the body of a captured continuation is _not_ surrounded by prompt, as we
observed in the previous section. On the other hand, the body of control is
evaluated in a prompt clause. The reduction rule ($\mathcal{P}$) for prompt
simply removes a delimiter surrounding a value.

##  4\. CPS Translation

In the previous section, we defined the semantics of control and prompt
directly on $\lambda_{\mathcal{F}}$ expressions. Another way to define the
semantics is to convert $\lambda_{\mathcal{F}}$ expressions into the plain
$\lambda$-calculus, via a continuation-passing style (CPS) [19] translation.
In this section, we give a CPS translation of control and prompt.

When the source calculus has control and prompt, a CPS translation exposes
continuations and trails of invocation contexts. Among these, trails can be
represented either as a list of functions [9, 10] or as a composition of
functions [52]. Previous work [35] on typing control and prompt adopts the
list representation, because it is conceptually simpler. We, however, adopt
the functional representation, as it makes it easier to build a fully general
type system (see Section 5).

###  4.1. $\lambda_{C}$: Target Calculus of CPS Translation

Syntax

$\displaystyle v$ $\displaystyle::=c\mid x\mid\lambda x.\,e\mid()$ Values
$\displaystyle e$ $\displaystyle::=v\mid e\ e\mid(\texttt{case}\ t\
\texttt{of}\ ()\Rightarrow e\mid k\Rightarrow e)$ Expressions

Evaluation Contexts

$\displaystyle E$ $\displaystyle::=[]\mid E\ e\mid v\ E\mid(\texttt{case}\ E\
\texttt{of}\ ()\Rightarrow e\mid k\Rightarrow e)$

Reduction Rules

$\displaystyle E[(\lambda x.\,e)\ v]$ $\displaystyle\leadsto E[e\,[v/x]]$
$\displaystyle(\textsc{$\beta$})$ $\displaystyle E[\texttt{case}\ ()\
\texttt{of}\ ()\Rightarrow e_{1}\mid k\Rightarrow e_{2}]$
$\displaystyle\leadsto E[e_{1}]$ $\displaystyle(\textsc{case-$()$})$
$\displaystyle E[\texttt{case}\ v\ \texttt{of}\ ()\Rightarrow e_{1}\mid
k\Rightarrow e_{2}]$ $\displaystyle\leadsto E[e_{2}\,[v/k]]\quad\text{where
}v\neq()$ $\displaystyle(\textsc{case-$k$})$

Figure 2. Syntax and Reduction of $\lambda_{C}$

In Figure 2, we define the target calculus of the CPS translation, which we
call $\lambda_{C}$. The calculus is a pure, call-by-value $\lambda$-calculus
featuring the unit value $()$, which represents an empty trail, and a case
analysis construct, which allows inspection of trails. Note that a non-empty
trail is represented as a regular function.

As in $\lambda_{\mathcal{F}}$, we evaluate $\lambda_{C}$ programs under a
call-by-value, left-to-right strategy. The choice of evaluation strategy in
the target calculus is not important in our setting, but it matters if the
target calculus has computational effects (such as non-termination and I/O),
because the CPS image of control and prompt has non-tail calls.

###  4.2. The CPS Translation

$\displaystyle\llbracket c\rrbracket$ $\displaystyle=\lambda k.\,\lambda
t.\,k\ c\ t$ $\displaystyle\llbracket x\rrbracket$ $\displaystyle=\lambda
k.\,\lambda t.\,k\ x\ t$ $\displaystyle\llbracket\lambda x.\,e\rrbracket$
$\displaystyle=\lambda k.\,\lambda t.\,k\ (\lambda x.\,\lambda
k^{\prime}.\,\lambda t^{\prime}.\,\llbracket e\rrbracket\ k^{\prime}\
t^{\prime})\ t$ $\displaystyle\llbracket e_{1}\ e_{2}\rrbracket$
$\displaystyle=\lambda k.\,\lambda t.\,\llbracket e_{1}\rrbracket\ (\lambda
v_{1}.\,\lambda t_{1}.\,\llbracket e_{2}\rrbracket\ (\lambda v_{2}.\,\lambda
t_{2}.\,v_{1}\ v_{2}\ k\ t_{2})\ t_{1})\ t$
$\displaystyle\llbracket\mathcal{F}c.\,e\rrbracket$ $\displaystyle=\lambda
k.\,\lambda t.\,\llbracket e\rrbracket\,[\lambda x.\,\lambda
k^{\prime}.\,\lambda t^{\prime}.\,k\ x\ (t\,@\,(k^{\prime}::t^{\prime}))/c]\
k_{id}\ ()$ $\displaystyle\llbracket\langle e\rangle\rrbracket$
$\displaystyle=\lambda k.\,\lambda t.\,k\ (\llbracket e\rrbracket\ k_{id}\
())\ t$ $\displaystyle k_{id}$ $\displaystyle=\lambda v.\,\lambda
t.\,\texttt{case}\ t\ \texttt{of}\ ()\Rightarrow v\mid k\Rightarrow k\ v\ ()$
$\displaystyle\\_@\\_$ $\displaystyle=\lambda t.\,\lambda
t^{\prime}.\,\texttt{case}\ t\ \texttt{of}\ ()\Rightarrow t^{\prime}\mid
k\Rightarrow k::t^{\prime}$ $\displaystyle\\_\\!::\\!\\_$
$\displaystyle=\lambda k.\,\lambda t.\,\texttt{case}\ t\ \texttt{of}\
()\Rightarrow k\mid k^{\prime}\Rightarrow\lambda v.\,\lambda t^{\prime}.\,k\
v\ (k^{\prime}::t^{\prime})$ Figure 3. CPS Translation of
$\lambda_{\mathcal{F}}$ Expressions

In Figure 3, we present the CPS translation $\llbracket\\_\rrbracket$ from
$\lambda_{\mathcal{F}}$ to $\lambda_{C}$, which is equivalent to the
translation given by Shan [52]. The translation converts an expression into a
function that takes in a continuation $k$ and a trail $t$. The trail is the
composition of the invocation contexts encountered so far, and is used
together with a continuation to produce an answer. Below, we detail the
translation of three representative constructs: variables, prompt, and
control.

Variables. The translation of a variable is an $\eta$-expanded version of the
standard, call-by-value translation. The trivial use of the current trail $t$
communicates the fact that a variable can never change the trail during
evaluation. More generally, the CPS translation of a pure expression uniformly
calls the continuation with an unmodified trail.

Prompt. The translation of prompt has the same structure as the translation of
variables, because prompt forms a pure expression. The translated body
$\llbracket e\rrbracket$ is run with the identity continuation $k_{id}$ and an
empty trail $()$111The identity continuation $k_{id}$ and the empty trail $()$
correspond to the send function and the #f value of Shan [52], respectively.,
describing how prompt resets the context of evaluation. Note that, in this CPS
translation, the identity continuation is _not_ the identity function. It
receives a value $v$ and a trail $t$, and behaves differently depending on
whether $t$ is empty or not. When $t$ is empty, the identity continuation
simply returns $v$. When $t$ is non-empty, $t$ must be a function composed of
one or more invocation contexts, which looks like $\lambda
x.\,E_{n}[...\,E_{1}[x]\,...]$. In this case, the identity continuation builds
an expression $E_{n}[...\,E_{1}[v]\,...]$ by calling the trail with $v$ and
$()$.

Control. The translation of control shares the same pattern with the
translation of prompt, because its body is evaluated in a prompt clause (as
defined by the ($\mathcal{F}$) rule in Figure 1). The translated body
$\llbracket e\rrbracket$ is applied a substitution that replaces the variable
$c$ with the trail $t\,@\,(k^{\prime}::t^{\prime})$, describing how an
invocation of a captured continuation extends the trail222 There is a
superficial difference between our CPS translation and Shan’s original
translation [52]. In our translation rule for control, the continuation
variable $c$ is replaced by the function $\lambda x.\,\lambda
k^{\prime}.\,\lambda t^{\prime}.\,k\ x\ (t\,@\,(k^{\prime}::t^{\prime}))$. In
Shan’s translation, $c$ is replaced by $\lambda x.\,\lambda
k^{\prime}.\,\lambda t^{\prime}.\,(k::t)\ x\ (k^{\prime}::t^{\prime})$.
However, by expanding the definition of $@$ and $::$, we can easily see that
the two functions are equivalent. We prefer the one that uses $@$ because it
is closer to the abstract machine given by Biernacki et al. [10], as well as
the list-based CPS translation derived from it.. The extension is necessary
for correctly computing the continuations captured during the invocation of
$c$. In particular, it makes the invocation context $k^{\prime}$ of $c$
accessible to the control operators that are executed during the invocation of
$c$. Recall that, in this CPS translation, trails are represented as
functions. The $@$ and $::$ operators are thus defined as a function producing
a function333The $::$ function is equivalent to Shan’s compose function.. More
specifically, these operators compose contexts in a first-captured, first-
called manner (as we can see from the second clause of $::$). Notice that $::$
is defined as a _recursive_ function444 While recursive, the $::$ function is
guaranteed to terminate, as the types of the two arguments become smaller in
every three successive recursive calls (or they reach the base case in fewer
steps).. The reason is that, when extending a trail $t$ with a continuation
$k$, we need to produce a function that takes in a trail $t^{\prime}$, which
in turn must be composed with a continuation $k^{\prime}$.

The CPS translation is correct with respect to the definitional abstract
machine given by Biernacka et al. [7]. The statement is proved by Shan [52],
using the functional correspondence [1] between evaluators and abstract
machines. We are also developing a mechanized proof of correctness in Agda.
The goal is to show that, if two $\lambda_{\mathcal{F}}$ expressions are
related by reduction, their CPS images are related by $\beta$-equality. We
have proved all cases but the control reduction (rule ($\mathcal{F}$) in
Figure 1), which requires careful reasoning on the equivalence of trails.

As a last note, let us mention here that the alternative CPS translation of
control and prompt, where trails are represented as lists, can be obtained by
replacing $()$ with the empty list, and the two operations $@$ and $::$ with
ones that work on lists.

##  5\. Type System

The CPS translation defined in the previous section shows how control and
prompt manipulate continuations and trails. Guided by this behavior, we now
derive a type system of $\lambda_{\mathcal{F}}$. We proceed in three steps.
First, we specify the syntax of trail types (Section 5.1). Next, we identify
an appropriate form of typing judgment (Section 5.2). Lastly, we define the
typing rules of individual syntactic constructs (Section 5.3). In each step,
we contrast our outcome with its counterpart in Kameyama and Yonezawa’s [35]
type system, showing how different representations of trails in the CPS
translation lead to different typing principles.

###  5.1. Syntax of Trail Types

Recall from Section 4.1 that, in $\lambda_{C}$, trails have two possible
forms: $()$ or a function. Correspondingly, in $\lambda_{\mathcal{F}}$, trail
types $\mu$ are defined by a two-clause grammar:
$\bullet\mid\tau\rightarrow\,\langle\mu\rangle\,\,\tau^{\prime}$. The latter
type is interpreted in the following way.

  * •

The trail accepts a value of type $\tau$.

  * •

The trail is to be composed with a context of type $\mu$.

  * •

After the composition, the trail produces a value of type $\tau^{\prime}$.

Put differently, $\tau$ is the input type of the innermost invocation context,
$\tau^{\prime}$ is the output type of the context to be composed in the
future, and $\mu$ is the type of this future context.

To get some intuition about trail typing, let us revisit example (2) from
Section 2.2.

$\displaystyle\langle(\mathcal{F}k_{1}.\,\texttt{is0}\ (k_{1}\
5))+(\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\ 8))\rangle$
$\displaystyle=\langle\texttt{is0}\ (k_{1}\ 5)\,[\lambda
x.\,x+(\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\ 8))/k_{1}]\rangle$
$\displaystyle=\langle\texttt{is0}\ (5+(\mathcal{F}k_{2}.\,\texttt{b2s}\
(k_{2}\ 8)))\rangle$ $\displaystyle=\langle\texttt{b2s}\ (k_{2}\ 8)\,[\lambda
x.\,\texttt{is0}\ (5+x)/k_{2}]\rangle$ $\displaystyle=\langle\texttt{b2s}\
(\texttt{is0}\ (5+8))\rangle$ $\displaystyle=\texttt{"{false}"}$

When evaluation goes inside of prompt, the trail is initialized to an empty
one $()$. Such a trail is naturally given type $\bullet$.

When the continuation $k_{1}$ is invoked, the trail is extended with the
context $\texttt{is0}\ [.]$. This context will be composed with the invocation
context $\texttt{b2s}\ [.]$ of $k_{2}$ later in the reduction sequence.
Therefore, the trail at this point is given type
$\texttt{int}\rightarrow\,\langle\texttt{bool}\rightarrow\,\langle\bullet\rangle\,\,\texttt{string}\rangle\,\,\texttt{string}$,
consisting of the input type of is0, the type of b2s, and the output type of
b2s.

When the continuation $k_{2}$ is invoked, the trail is extended with the
context $\texttt{b2s}\ [.]$ (hence the whole trail looks like $\texttt{b2s}\
(\texttt{is0}\ [.])$). This context will not be composed with any further
contexts in the subsequent steps of reduction. Therefore, the trail at this
point is given type
$\texttt{int}\rightarrow\,\langle\bullet\rangle\,\,\texttt{string}$,
consisting of the input type of is0, the type of an empty trail, and the
output type of b2s.

Observe that our trail types can be inhabited by heterogeneous trails (e.g.,
$\texttt{b2s}\ (\texttt{is0}\ [.])$), where the input and output types of each
invocation context are different. The flexibility is exactly what we expect a
general type system of control and prompt to have, as we stated in Section
2.2.

#### Comparison with Previous Work

In the CPS translation of Kameyama and Yonezawa [35], a trail is treated as a
list of invocation contexts. Such a list is given a recursive type
$\texttt{Trail}(\rho)$ defined as follows:

$\texttt{Trail}(\rho)=\mu X.\,\texttt{list}(\rho\rightarrow X\rightarrow\rho)$

We can easily see that the definition restricts the type of invocation
contexts in two ways. First, all invocation contexts in a trail must have the
same type. This is because lists are homogeneous by definition. Second, each
invocation context must have equal input and output types. This is a direct
consequence of the first restriction. The two restrictions prevent one from
invoking a continuation in a context such as $\texttt{is0}\ [.]$ or
$\texttt{b2s}\ [.]$. Moreover, the use of the list type makes empty and non-
empty trails indistinguishable at the level of types, and extension of trails
undetectable in types. On the other hand, the limited expressiveness allows
one to use an ordinary expression type (such as int, instead of a type
designed specifically for trails) to encode the information of trails in the
control/prompt calculus. That is, if a trail has type $\texttt{Trail}(\rho)$
in the CPS world, it has type $\rho$ in the direct-style world.

###  5.2. Typing Judgment

Recall from Section 4.2 that a $\lambda_{\mathcal{F}}$ expression $e$ is CPS-
translated into a function $\lambda k.\,\lambda t.\,e^{\prime}$. Assuming $e$
has type $\tau$, the translated function can be typed in the following way:

$\llbracket e^{\tau}\rrbracket=\lambda
k^{\tau\rightarrow\mu_{\alpha}\rightarrow\alpha}.\,\lambda
t^{\mu_{\beta}}.\,{e^{\prime}}^{\beta}$

Here, $\alpha$ and $\beta$ are answer types, representing the return type of
the enclosing prompt before and after evaluation of $e$. It is well-known that
delimited control can make the two answer types distinct [19], and since
answer types are needed to decide typability of programs, they must be
integrated into the typing judgment. The other pair of types, $\mu_{\beta}$
and $\mu_{\alpha}$, are trail types, representing the composition of
invocation contexts encountered before and after evaluation of $e$. We have
seen that an invocation of a captured continuation can change the type of the
trail, and since trail types are also relevant to typability of programs, they
have to be integrated into the typing judgment.

Summing up the above discussion, we conclude that a fully general typing
judgment for control and prompt must carry five types, as follows:

$\Gamma\vdash
e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$

We place the types in the same order as their appearance in the annotated CPS
expression. That is, the first three types $\tau$, $\mu_{\alpha}$, and
$\alpha$ correspond to the continuation of $e$, the next one $\mu_{\beta}$
represents the trail required by $e$, and the last one $\beta$ stands for the
eventual value returned by $e$. We will hereafter call $\alpha$ and $\beta$
initial and final answer types, and $\mu_{\beta}$ and $\mu_{\alpha}$ initial
and final trail types — be careful of the direction in which answer types and
trail types change.

With the typing judgment specified, we can define the syntax of expression
types of $\lambda_{\mathcal{F}}$ (Figure 4). Expression types are formed with
base types $\iota$ (such as int and bool) and arrow types
$\tau_{1}\rightarrow\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$.
Notice that the codomain of arrow types carries five components. These types
represent the control effect of a function’s body, and correspond exactly to
the five types that appear in a typing judgment.

#### Comparison with Previous Work

In the type system developed by Kameyama and Yonezawa [35], a CPS-translated
expression is typed in the following way:

$\lambda k^{\tau\rightarrow\texttt{Trail}(\rho)\rightarrow\alpha}.\,\lambda
t^{\texttt{Trail}(\rho)}.\,{e^{\prime}}^{\beta}$

The typing is obviously not as general as ours, because the two trail types
are equal. This constraint is imposed by the list representation of trails:
even if an expression extends the trail during evaluation, the type of the
trail stays the same. Thus, Kameyama and Yonezawa arrive at a typing judgment
carrying four types, with the last one ($\rho$) representing the information
of trails:

$\Gamma\vdash e:\tau,\alpha,\beta/\rho$

Correspondingly, they assign direct-style functions an arrow type of the form
$\tau_{1}\rightarrow\tau_{2},\alpha,\beta/\rho$.

###  5.3. Typing Rules

Syntax of Types

$\displaystyle\tau,\alpha,\beta$
$\displaystyle::=\iota\mid\tau\rightarrow\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$
Expression Types $\displaystyle\mu,\mu_{\alpha},\mu_{\beta}$
$\displaystyle::=\bullet\mid\tau\rightarrow\,\langle\mu\rangle\,\,\tau$ Trail
Types

Typing Rules

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
26.35197pt\hbox{$\penalty 31415926c:\iota\in\Sigma$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=88.34843pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash
c:\iota\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\alpha}\rangle\,\alpha$}}}}\
(\textsc{Const})\hskip 28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 26.83809pt\hbox{$\penalty
31415926x:\tau\in\Gamma$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=90.56831pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash
x:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\alpha}\rangle\,\alpha$}}}}\
(\textsc{Var})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
33.68538pt\hbox{$\penalty 31415926\Gamma,\,x:\tau_{1}\vdash
e:\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=181.96674pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash\lambda
x.\,e:(\tau_{1}\rightarrow\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta)\,\langle\mu_{\gamma}\rangle\,\gamma\,\langle\mu_{\gamma}\rangle\,\gamma$}}}}\
(\textsc{Abs})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty 31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma\vdash
e_{1}:(\tau_{1}\rightarrow\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta)\,\langle\mu_{\gamma}\rangle\,\gamma\,\langle\mu_{\delta}\rangle\,\delta\cr\Gamma\vdash
e_{2}:\tau_{1}\,\langle\mu_{\beta}\rangle\,\beta\,\langle\mu_{\gamma}\rangle\,\gamma\crcr}}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=163.18608pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 30.7221pt\hbox{$\Gamma\vdash e_{1}\
e_{2}:\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\delta}\rangle\,\delta$}}}}\
(\textsc{App})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty
31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma,\,k:\tau\rightarrow\tau_{1}\,\langle\mu_{1}\rangle\,{\tau_{1}}^{\prime}\,\langle\mu_{2}\rangle\,\alpha\vdash
e:\gamma\,\langle\mu_{i}\rangle\,\gamma^{\prime}\,\langle\bullet\rangle\,\beta\cr\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\gamma,\mu_{i},\gamma^{\prime})\cr\mathsf{compatible}((\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}),\mu_{2},\mu_{0})\cr\mathsf{compatible}(\mu_{\beta},\mu_{0},\mu_{\alpha})\crcr}}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=179.56787pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern
37.91608pt\hbox{$\Gamma\vdash\mathcal{F}k.\,e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$}}}}\
(\textsc{Control})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.73996pt\hbox{$\penalty
31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma\vdash
e:\beta\,\langle\mu_{i}\rangle\,\beta^{\prime}\,\langle\bullet\rangle\,\tau\cr\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\beta,\mu_{i},\beta^{\prime})\crcr}}$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=91.73169pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash\langle
e\rangle:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\alpha}\rangle\,\alpha$}}}}\
(\textsc{Prompt})$

Figure 4. Type System of $\lambda_{\mathcal{F}}$
$\displaystyle\mathsf{id\mathchar 45\relax cont\mathchar 45\relax
type}(\tau,\bullet,\tau^{\prime})$ $\displaystyle=\tau\equiv\tau^{\prime}$
(first branch of $k_{id}$ in Figure 3) $\displaystyle\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\tau,(\tau_{1}\rightarrow\,\langle\mu\rangle\,\,\tau_{1}^{\prime}),\tau^{\prime})$
$\displaystyle=(\tau\equiv\tau_{1})\wedge(\tau^{\prime}\equiv\tau_{1}^{\prime})\wedge(\mu\equiv\bullet)$
(second branch of $k_{id}$ in Figure 3)
$\displaystyle\mathsf{compatible}(\bullet,\mu_{2},\mu_{3})$
$\displaystyle=\mu_{2}\equiv\mu_{3}$ (first branch of $@$ in Figure 3)
$\displaystyle\mathsf{compatible}(\mu_{1},\bullet,\mu_{3})$
$\displaystyle=\mu_{1}\equiv\mu_{3}$ (first branch of $::$ in Figure 3)
$\displaystyle\mathsf{compatible}((\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,\tau_{1}^{\prime}),\mu_{2},\bullet)$
$\displaystyle=\bot$ (no counterpart in Figure 3)
$\displaystyle\mathsf{compatible}((\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,\tau_{1}^{\prime}),\mu_{2},(\tau_{3}\rightarrow\,\langle\mu_{3}\rangle\,\,\tau_{3}^{\prime}))$
$\displaystyle=(\tau_{1}\equiv\tau_{3})\wedge(\tau_{1}^{\prime}\equiv\tau_{3}^{\prime})\,\wedge$
$\displaystyle\hskip 14.22636pt(\mathsf{compatible}(\mu_{2},\mu_{3},\mu_{1}))$
(second branch of $::$ in Figure 3) Figure 5. Auxiliary Relations

Using the trail types and typing judgment from the previous subsections, we
define the typing rules of $\lambda_{\mathcal{F}}$ (Figure 4). We assume a
global signature $\Sigma$ mapping constants to their types, which we leave
implicit in all rules but (Const). As in the previous section, we elaborate
the typing rules of variables, prompt, and control.

#### Variables

Recall that the CPS translation of variables is an $\eta$-expanded version of
the standard translation. If we annotate the types of each subexpression, a
translated variable would look like:

$\lambda k^{\tau\rightarrow\mu_{\alpha}\rightarrow\alpha}.\,\lambda
t^{\mu_{\alpha}}.\,(k\ x\ t)^{\alpha}$

We see duplicate occurrences of the answer type $\alpha$ and the trail type
$\mu_{\alpha}$. The duplication arises from the application $k\ x\ t$, and
reflects the fact that a variable cannot change the answer type or the trail
type. By a straightforward conversion from the annotated expression into a
typing judgment, we obtain rule (Var) in Figure 4. In general, when the
subject of a typing judgment is a pure expression, the answer types and trail
types both coincide.

#### Prompt

We next analyze the CPS translation of prompt, again with type annotations.

$\lambda k^{\tau\rightarrow\mu_{\alpha}\rightarrow\alpha}.\,\lambda
t^{\mu_{\alpha}}.\,(k\ (\llbracket
e\rrbracket^{(\beta\rightarrow\mu_{i}\rightarrow\beta^{\prime})\rightarrow\bullet\rightarrow\tau}\
k_{id}\ ())\ t)^{\alpha}$

As $\langle e\rangle$ is a pure expression, we again have equal answer types
$\alpha$ and trail types $\mu_{\alpha}$ for the whole expression. The initial
trail type $\bullet$ and final answer type $\tau$ of $e$ are determined by the
application $\llbracket e\rrbracket\ k_{id}\ ()$ and $k\ (\llbracket
e\rrbracket\ k_{id}\ ())$, respectively. What is left is to ensure that the
application of $\llbracket e\rrbracket$ to the identity continuation $k_{id}$
is type-safe. In our type system, we use a relation $\mathsf{id\mathchar
45\relax cont\mathchar 45\relax type}(\tau,\mu,\tau^{\prime})$ to ensure this
type safety. The relation holds when the type
$\tau\rightarrow\mu\rightarrow\tau^{\prime}$ can be assigned to the identity
continuation. The valid combination of $\tau$, $\mu$, and $\tau^{\prime}$ is
derived from the definition of the identity continuation, repeated below.

$\lambda v^{\tau}.\,\lambda t^{\mu}.\,\texttt{case}\ t\ \texttt{of}\
()\Rightarrow v^{\tau^{\prime}}\mid k\Rightarrow(k\ v\ ())^{\tau^{\prime}}$

When $t$ is an empty trail $()$ of type $\bullet$, the return value of
$k_{id}$ is $v$, which has type $\tau$. Since the expected return type of
$k_{id}$ is $\tau^{\prime}$, we need the equality $\tau\equiv\tau^{\prime}$.

When $t$ is a non-empty trail $k$ of type
$\tau_{1}\rightarrow\mu\rightarrow{\tau_{1}}^{\prime}$, the return value of
$k_{id}$ is the result of the application $k\ v\ ()$, which has type
${\tau_{1}}^{\prime}$. Since the expected return type of $k_{id}$ is
$\tau^{\prime}$, we need the equality
$\tau^{\prime}\equiv{\tau_{1}}^{\prime}$. Furthermore, since $k$ must accept
$v$ and $()$ as arguments, we need the equalities $\tau\equiv\tau_{1}$ and
$\mu\equiv\bullet$.

We define id-cont-type as an encoding of these constraints, and in the rule
(Prompt), we use the premise $\mathsf{id\mathchar 45\relax cont\mathchar
45\relax type}(\beta,\mu_{i},\beta^{\prime})$ to constrain the type of the
continuation of $e$. Now, it is statically guaranteed that $e$ will be safely
evaluated in an empty context.

#### Control

Lastly, we apply the same method to control. Here is the annotated CPS
translation:

$\lambda k^{\tau\rightarrow\mu_{\alpha}\rightarrow\alpha}.\,\lambda
t^{\mu_{\beta}}.\,\llbracket
e\rrbracket^{(\gamma\rightarrow\mu_{i}\rightarrow\gamma^{\prime})\rightarrow\bullet\rightarrow\beta}\,[\lambda
x^{\tau}.\,\lambda{k^{\prime}}^{\tau_{1}\rightarrow\mu_{1}\rightarrow{\tau_{1}}^{\prime}}.\,\lambda{t^{\prime}}^{\mu_{2}}.\,k\
x\ (t\,@\,(k^{\prime}::t^{\prime})^{\mu_{0}})/c]\ k_{id}\ ()$

As the body $e$ of control is evaluated in a prompt clause, we again have an
empty initial trail type for $e$, and we know that the types $\gamma$,
$\mu_{i}$, and $\gamma^{\prime}$ must satisfy the id-cont-type relation. What
is left is to ensure that the composition of contexts in
$t\,@\,(k^{\prime}::t^{\prime})$ is type-safe. In our type system, we use a
relation $\mathsf{compatible}(\mu_{1},\mu_{2},\mu_{3})$ to ensure this type
safety. The relation holds when composing a context of type $\mu_{1}$ and
another context of type $\mu_{2}$ results in a context of type $\mu_{3}$.
Intuitively, the relation can be thought of as an addition over trail types.
The valid combination of $\mu_{1}$, $\mu_{2}$, and $\mu_{3}$ is derived from
the definition of the $@$ and $::$ functions.

$\displaystyle t^{\mu_{1}}\,@\,{t^{\prime}}^{\mu_{2}}$
$\displaystyle=\texttt{case}\ t\ \texttt{of}\
()\Rightarrow{t^{\prime}}^{\mu_{3}}\mid k\Rightarrow(k::t^{\prime})^{\mu_{3}}$
$\displaystyle
k^{\tau_{1}\rightarrow\mu_{1}\rightarrow{\tau_{1}}^{\prime}}::t^{\mu_{2}}$
$\displaystyle=\texttt{case}\ t\ \texttt{of}\ ()\Rightarrow
k^{\tau_{3}\rightarrow\mu_{3}\rightarrow{\tau_{3}}^{\prime}}\mid
k^{\prime}\Rightarrow(\lambda v.\,\lambda t^{\prime}.\,k\ v\
(k^{\prime}::t^{\prime}))^{\tau_{3}\rightarrow\mu_{3}\rightarrow{\tau_{3}}^{\prime}}$

The first clause of $@$ and that of $::$ are straightforward: they tell us
that the empty trail type $\bullet$ serves as the left and right identity of
the addition.

The second clause of $::$ requires more careful reasoning. The return value of
this case is the result of the application $k\ v\ (k^{\prime}::t^{\prime})$,
which has type ${\tau_{1}}^{\prime}$. Since the expected return type of $::$
is ${\tau_{3}}^{\prime}$, we need the equality
${\tau_{1}}^{\prime}\equiv{\tau_{3}}^{\prime}$. Moreover, since $k$ must
accept $v$ and $k^{\prime}::t^{\prime}$ as arguments, we need the equality
$\tau_{1}\equiv\tau_{3}$, as well as the compatibility of $\mu_{2}$ (type of
$k^{\prime}$), $\mu_{3}$ (type of $t^{\prime}$), and $\mu_{1}$ (type of the
trail expected by $k$).

We define compatible as an encoding of these constraints, and in the (Control)
rule, we use two instances of this relation to constrain the type of contexts
appearing in $t\,@\,(k^{\prime}::t^{\prime})$. Among the two instances, the
first one
$\mathsf{compatible}((\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}),\mu_{2},\mu_{0})$
states that consing $k^{\prime}$ to $t^{\prime}$ is type-safe, and the result
has type $\mu_{0}$. The second one
$\mathsf{compatible}(\mu_{\beta},\mu_{0},\mu_{\alpha})$ states that appending
$t$ to $k^{\prime}::t^{\prime}$ is type-safe, and the result has type
$\mu_{\alpha}$, which is required by the continuation $k$ of the whole control
expression.

By designing (Control) and (Prompt) in this way, we have achieved the goal of
this work: a type system that encodes all and only restrictions that arise
from the CPS semantics of control and prompt. More precisely, we use the id-
cont-type and compatible relations to enforce type-safe manipulation of
contexts, while allowing the full flexibility in the type of contexts being
manipulated.

#### Comparison with Previous Work

In the type system of Kameyama and Yonezawa [35], the typing rules for control
and prompt are defined as follows:

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty
31415926\Gamma,\,k:\tau\rightarrow\rho,\rho,\alpha/\rho\vdash
e:\gamma,\gamma,\beta/\gamma$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=144.44896pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern
29.3942pt\hbox{$\Gamma\vdash\mathcal{F}k.\,e:\tau,\alpha,\beta/\rho$}}}}\
(\textsc{Control})\hskip 28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 2.33226pt\hbox{$\penalty
31415926\Gamma\vdash e:\rho,\rho,\tau/\rho$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=73.78572pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash\langle e\rangle:\tau,\alpha,\alpha/\sigma$}}}}\
(\textsc{Prompt})$

The rules are simpler than the corresponding rules in our type system. In
particular, there is no equivalent of id-cont-type or compatible, since the
homogeneous nature of trails makes those relations trivial.

A closer look at rule (Prompt) further reveals how prompt determines the trail
type of its body. To spell out, the first and third occurrences of $\rho$ in
the premise mean that, if an expression $e$ is surrounded by a prompt whose
body is of type $\rho$, then the invocation contexts in the trail of $e$ all
have the shared input and output types $\rho$.

###  5.4. Typing Heterogeneous Trails

We now show that example (2) from Section 2.2 is judged well-typed in
$\lambda_{\mathcal{F}}$ 555An implementation exp4 of this example is included
in lambdaf.agda in the artifact repository.. The well-typedness of the whole
program largely relies on the well-typedness of the two control constructs, so
let us look at the typing of these constructs:

$\vdash\mathcal{F}k_{1}.\,\texttt{is0}\ (k_{1}\
5):\texttt{int}\,\langle\mu_{1}\rangle\,\texttt{string}\,\langle\bullet\rangle\,\texttt{string}$

$\vdash\mathcal{F}k_{2}.\,\texttt{b2s}\ (k_{2}\
8):\texttt{int}\,\langle\mu_{2}\rangle\,\texttt{string}\,\langle\mu_{1}\rangle\,\texttt{string}$

For brevity, we write $\mu_{1}$ to mean
$\texttt{int}\rightarrow\,\langle\texttt{bool}\rightarrow\,\langle\bullet\rangle\,\,\texttt{string}\rangle\,\,\texttt{string}$,
and $\mu_{2}$ to mean
$\texttt{int}\rightarrow\,\langle\bullet\rangle\,\,\texttt{string}$. We can
see how the trail type changes from empty ($\bullet$), to one that refers to a
future context ($\mu_{1}$), and to one that mentions no further context
($\mu_{2}$). In particular, $\mu_{2}$ is the result of “adding” $\mu_{1}$ and
the type of $\texttt{b2s}\ [.]$; that is, the invocation of $k_{2}$
_discharges_ the future context awaited by $\texttt{is0}\ [.]$. The trail type
$\mu_{2}$ serves as the final trail type of the body of the enclosing prompt,
and as it allows us to establish the id-cont-type relation required by
(Prompt), we can conclude that the whole program is well-typed.

##  6\. Properties

The type system of $\lambda_{\mathcal{F}}$ enjoys various pleasant properties.
In this section, we sketch the proof of three properties.

###  6.1. Type Soundness

First, the type system is sound, that is, well-typed programs do not go wrong
[43]. Following Wright and Felleisen [54], we prove type soundness via the
preservation and progress theorems.

######  Theorem 1 (Preservation).

If $\Gamma\vdash
e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$
and $e\leadsto e^{\prime}$, then $\Gamma\vdash
e^{\prime}:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$.

###### Proof.

The proof is by induction on the typing derivation666The proof is implemented
as the Reduce relation in lambdaf-red.agda.. Note that, to prove this
property, we need to define a set of typing rules for evaluation contexts. ∎

######  Theorem 2 (Progress).

If $\bullet\vdash
e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$,
then either (i) $e$ is a value, (ii) $e$ takes a step, or (iii) $e$ is a stuck
term of the form $F[\mathcal{F}k.\,e^{\prime}]$.

###### Proof.

The proof is by induction on the typing derivation. The third alternative is
commonly found in the progress property of effectful calculi [3, 55], meaning
the presence of unhandled effects. ∎

######  Theorem 3 (Type Soundness).

If $\bullet\vdash
e:\tau\,\langle\bullet\rangle\,\alpha\,\langle\bullet\rangle\,\alpha$, then
evaluation of $e$ does not get stuck.

###### Proof.

The statement is a direct implication of preservation and progress. Note that
the empty final trail type means $e$ does not have control effects. This is
justified by the fact that the final trail type $\mu_{\alpha}$ in the typing
rule (Control) must be non-empty, as the trail is composed of a non-empty
trail of type
$\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}$. ∎

Syntax of Types

$\displaystyle\tau$ $\displaystyle=\iota\mid\tau\rightarrow\tau\mid\bullet$

Typing Rules

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty 31415926c:\iota\in\Sigma$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=35.64447pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern 0.07004pt\hbox{$\Gamma\vdash
x:\iota$}}}}\ (\textsc{Const})\hskip 28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 0.0pt\hbox{$\penalty
31415926x:\tau\in\Gamma$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=36.89214pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.27779pt\hbox{$\Gamma\vdash x:\tau$}}}}\
(\textsc{Var})\hskip 28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 4.58334pt\hbox{$\penalty
31415926\Gamma,\,x:\tau_{1}\vdash e:\tau_{2}$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=70.6865pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash\lambda x.\,e:\tau_{1}\rightarrow\tau_{2}$}}}}\
(\textsc{Abs})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
18.12492pt\hbox{$\penalty 31415926$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=36.24986pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash():\bullet$}}}}\
(\textsc{Unit})\hskip 28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 0.0pt\hbox{$\penalty
31415926\Gamma\vdash e_{1}:\tau_{1}\rightarrow\tau_{2}\hskip
8.53581pt\Gamma\vdash e_{2}:\tau_{1}$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=99.68478pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 24.56433pt\hbox{$\Gamma\vdash e_{1}\
e_{2}:\tau_{2}$}}}}\ (\textsc{App})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty 31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma\vdash
t:\mu^{\ast}\hskip 8.53581pt\Gamma,\,\mu\equiv\bullet\vdash
e_{1}:\tau\cr\forall\tau_{1},\mu_{1},{\tau_{1}}^{\prime}.\
\Gamma,\,k:\mu^{\ast},\,\mu\equiv\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}\vdash
e_{2}:\tau\crcr}}$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=179.53267pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 23.10014pt\hbox{$\Gamma\vdash\texttt{case}\ t\
\texttt{of}\ ()\Rightarrow e_{1}\mid k\Rightarrow e_{2}:\tau$}}}}\
(\textsc{Case})$

Figure 6. Type System of $\lambda_{C}$

Translation of Expression Types

$\displaystyle\iota^{\ast}$ $\displaystyle=\iota$
$\displaystyle(\tau_{1}\rightarrow\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta)^{\ast}$
$\displaystyle=\tau_{1}^{\ast}\rightarrow(\tau_{2}^{\ast}\rightarrow\mu_{\alpha}^{\ast}\rightarrow\alpha^{\ast})\rightarrow\mu_{\beta}^{\ast}\rightarrow\beta^{\ast}$

Translation of Trail Types

$\displaystyle\bullet^{\ast}$ $\displaystyle=\bullet$
$\displaystyle(\tau\rightarrow\,\langle\mu\rangle\,\,\tau^{\prime})^{\ast}$
$\displaystyle=\tau^{\ast}\rightarrow\mu^{\ast}\rightarrow{\tau^{\prime}}^{\ast}$

Figure 7. CPS Translation of $\lambda_{\mathcal{F}}$ Types

###  6.2. Type Preservation of CPS Translation

Secondly, our CPS translation preserves typing, i.e., it converts a well-typed
$\lambda_{\mathcal{F}}$ expression into a well-typed $\lambda_{C}$ expression.
To establish this theorem, we define the type system of $\lambda_{C}$ (Figure
6) and the CPS translation ∗ on $\lambda_{\mathcal{F}}$ types (Figure 7).

Let us elaborate on rule (Case) in Figure 6, which is the only non-trivial
typing rule. This rule is used to type the case analysis construct in the
three auxiliary functions of the CPS translation, namely $k_{id}$, $@$, and
$::$. Compared to the standard typing rule for case analysis, rule (Case) uses
extra equality assumptions $\mu\equiv\bullet$ and
$\mu\equiv\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}$
to type the two branches777The use of equality assumptions in (Case) is
inspired by _dependent pattern matching_ [17] available in dependently typed
languages. Our case analysis is weaker than the dependent variant, in that the
return type only depends on the _type_ of the scrutinee, not on the scrutinee
itself.. These assumptions, together with the id-cont-type and compatible
relations, fill in the gap between the expected and actual return types. As an
illustration, let us elaborate the typing of $k_{id}$:

$\lambda v^{\tau}.\,\lambda t^{\mu}.\,\texttt{case}\ t\ \texttt{of}\
()\Rightarrow v^{\tau^{\prime}}\mid k\Rightarrow(k\ v\ ())^{\tau^{\prime}}$

In the first branch, we see an inconsistency between the expected return type
$\tau^{\prime}$ and the actual return type $\tau$. However, by the typing
rules defined in Figure 4, we know that $k_{id}$ is used only when the
relation $\mathsf{id\mathchar 45\relax cont\mathchar 45\relax
type}(\tau,\mu,\tau^{\prime})$ holds. Moreover, by the definition of id-cont-
type, if $\mu\equiv\bullet$, we have $\tau\equiv\tau^{\prime}$. The equality
assumption $\mu\equiv\bullet$ made available by rule (Case) allows us to
derive $\tau\equiv\tau^{\prime}$ and conclude that the first branch has the
correct type. Similarly, in the second branch, we use the equality assumption
$\mu\equiv\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,\tau_{1}^{\prime}$ to
derive $\tau\equiv\tau_{1}$, $\tau^{\prime}\equiv\tau_{1}^{\prime}$, and
$\mu_{1}\equiv\bullet$, which imply the well-typedness of the application $k\
v\ ()$. The $@$ and $::$ functions can be typed in an analogous way.

Now we state the type preservation theorem.

######  Theorem 4 (Type Preservation of CPS Translation).

If $\Gamma\vdash
e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta$
in $\lambda_{\mathcal{F}}$, then $\Gamma^{\ast}\vdash\llbracket
e\rrbracket:(\tau^{\ast}\rightarrow\mu_{\alpha}^{\ast}\rightarrow\alpha^{\ast})\rightarrow\mu_{\beta}^{\ast}\rightarrow\beta^{\ast}$
in $\lambda_{C}$.

###### Proof.

The proof is by induction on the typing derivation888The proof is implemented
as function cpse in cps.agda.. With the carefully designed rule for case
analysis, we can prove the statement in a straightforward manner, as our type
system is directly derived from the CPS translation. ∎

###  6.3. Termination of Evaluation

Thirdly, and most interestingly, our type system ensures termination of pure
programs.

######  Theorem 5 (Termination).

If $\bullet\vdash
e:\tau\,\langle\bullet\rangle\,\alpha\,\langle\bullet\rangle\,\alpha$, then
there exists some value $v$ such that $e\leadsto^{\ast}v$, where
$\leadsto^{\ast}$ is the reflexive, transitive closure of $\leadsto$ defined
in Figure 1.

###### Proof.

The statement is witnessed by a CPS interpreter of $\lambda_{\mathcal{F}}$
implemented in Agda999The interpreter is implemented as function go in
lambdaf.agda.. Since every well-typed Agda program terminates, and since our
interpreter is judged well-typed, we know that evaluation of
$\lambda_{\mathcal{F}}$ expressions must terminate. ∎

The termination property is unique to our type system. In the existing type
system by Kameyama and Yonezawa [35], it is possible to write a well-typed
program that does not evaluate to a value. Here is a non-terminating program
adapted from Kameyama and Yonezawa’s example (we write $e_{1};e_{2}$ as an
abbreviation of $(\lambda\\_.\,e_{2})\ e_{1}$):

$\displaystyle\langle(\mathcal{F}k_{1}.\,k_{1}\ 1;k_{1}\
1);(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\ 1)\rangle$ $\displaystyle=\langle
k_{1}\ 1;k_{1}\ 1\,[\lambda x.\,x;(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\
1)/k_{1}]\rangle$ $\displaystyle=\langle(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\
1);((\lambda x.\,x;(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\ 1))\ 1)\rangle$
$\displaystyle=\langle k_{2}\ 1;k_{2}\ 1\,[\lambda y.\,y;(\lambda
x.\,x;(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\ 1))\ 1/k_{2}]\rangle$
$\displaystyle=\langle(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\ 1);(\lambda
y.\,y;(\lambda x.\,x;(\mathcal{F}k_{2}.\,k_{2}\ 1;k_{2}\ 1))\ 1)\ 1\rangle$
$\displaystyle=...$

We see that the two succeeding invocations of captured continuations result in
duplication of control, leading to a looping behavior.

The well-typedness of the above program in Kameyama and Yonezawa’s type system
is due to the limited expressiveness of trail types. More precisely, their
trail types are mere expression types, which carry no information about the
type of contexts to be composed in the future. In our type system, on the
other hand, trail types explicitly mention the type of future contexts. This
prevents us from duplicating control infinitely, and allows us to statically
reject the above looping program101010An incomplete implementation exp5 of the
non-terminating example is included in lambdaf.agda.

##  7\. Selective CPS Translation and Fine-grained Type System

In the CPS translation defined in Section 4, we converted every expression
into a function that receives a continuation and a trail. When used as an
implementation technique, such a whole-program translation would blow up the
size of programs and lead to poor performance. A popular solution to this
problem is to make the CPS translation _selective_ [44, 37, 49, 4], that is,
we only convert impure expressions into CPS, and keep pure expressions in
direct style.

In this section, we present a selective CPS translation for control and
prompt, as well as a corresponding type system. Unlike in the previous
sections, here we first define the type system (Section 7.1) _and then_ derive
the CPS translation (Section 7.2). This is because defining a selective CPS
translation requires a purity analysis, which in turn requires a type system.
We show that, with the distinction between pure and impure expressions, we can
still prove desired properties (Section 7.3). In addition to that, we can
macro-express Danvy and Filinski’s [20] shift operator using control and
prompt (Section 7.4).

###  7.1. Fine-grained Type System

Syntax of Expression Types

$\displaystyle\tau,\alpha,\beta$ $\displaystyle::=...\mid\tau\rightarrow\tau$

Typing Rules and Selective CPS Translation

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
10.32854pt\hbox{$\penalty 31415926c:\iota\in\Sigma$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=56.30156pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash_{p}c:\iota\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}c$}$}}}}\ (\textsc{Const})\hskip
28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 11.5085pt\hbox{$\penalty
31415926x:\tau\in\Gamma$}}\kern 0.0pt\hbox{\kern 0.0pt\vrule
width=59.90915pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash_{p}x:\tau\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}x$}$}}}}\ (\textsc{Var})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
13.41318pt\hbox{$\penalty 31415926\Gamma,\,x:\tau_{1}\vdash_{p}e:\tau_{2}\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}e^{\prime}$}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=112.39973pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash_{p}\lambda
x.\,e:\tau_{1}\rightarrow\tau_{2}\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}\lambda x.\,e^{\prime}$}$}}}}\
(\textsc{PAbs})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
48.99821pt\hbox{$\penalty 31415926\Gamma,\,x:\tau_{1}\vdash
e:\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto e^{\prime}$}$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=236.56639pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash_{p}\lambda
x.\,e:(\tau_{1}\rightarrow\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta)\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}\lambda x.\,\lambda
k^{\prime}.\,\lambda t^{\prime}.\,e^{\prime}\ k^{\prime}\ t^{\prime}\ $}$}}}}\
(\textsc{IAbs})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty
31415926\Gamma\vdash_{p}e_{1}:\tau_{1}\rightarrow\tau_{2}\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}{e_{1}}^{\prime}$}\quad\Gamma\vdash_{p}e_{2}:\tau_{1}\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}{e_{2}}^{\prime}$}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=152.07843pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 30.33623pt\hbox{$\Gamma\vdash_{p}e_{1}\
e_{2}:\tau_{2}\ \hbox{\pagecolor{mylightgray}$\leadsto_{p}{e_{1}}^{\prime}\
{e_{2}}^{\prime}$}$}}}}\ (\textsc{PApp})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty 31415926\Gamma\vdash
e_{1}:(\tau_{1}\rightarrow\tau_{2})\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto{e_{1}}^{\prime}$}\quad\Gamma\vdash
e_{2}:\tau_{1}\,\langle\mu_{\gamma}\rangle\,\gamma\,\langle\mu_{\alpha}\rangle\,\alpha\
\hbox{\pagecolor{mylightgray}$\leadsto{e_{2}}^{\prime}$}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=262.32452pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 1.29619pt\hbox{$\Gamma\vdash e_{1}\
e_{2}:\tau_{2}\,\langle\mu_{\gamma}\rangle\,\gamma\,\langle\mu_{\beta}\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto\lambda k.\,{e_{1}}^{\prime}\ (\lambda
v_{1}.\,{e_{2}}^{\prime}\ (\lambda v_{2}.\,k\ (v_{1}\ v_{2})))$}$}}}}\
(\textsc{PIApp})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
32.39214pt\hbox{$\penalty
31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma\vdash
e_{1}:(\tau_{1}\rightarrow\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta)\,\langle\mu_{\gamma}\rangle\,\gamma\,\langle\mu_{\delta}\rangle\,\delta\
\hbox{\pagecolor{mylightgray}$\leadsto{e_{1}}^{\prime}$}\cr\Gamma\vdash
e_{2}:\tau_{1}\,\langle\mu_{\beta}\rangle\,\beta\,\langle\mu_{\gamma}\rangle\,\gamma\
\hbox{\pagecolor{mylightgray}$\leadsto{e_{2}}^{\prime}$}\crcr}}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=251.96663pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash e_{1}\
e_{2}:\tau_{2}\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\delta}\rangle\,\delta\
\hbox{\pagecolor{mylightgray}$\leadsto\lambda k.\,{e_{1}}^{\prime}\ (\lambda
v_{1}.\,{e_{2}}^{\prime}\ (\lambda v_{2}.\,v_{1}\ v_{2}\ k))$}$}}}}\
(\textsc{IApp})$

Figure 8. Fine-grained Type System and Selective CPS Translation of
$\lambda_{\mathcal{F}}$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
52.50159pt\hbox{$\penalty
31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma,\,c:\tau\rightarrow\alpha\vdash
e:\gamma\,\langle\mu_{i}\rangle\,\gamma^{\prime}\,\langle\bullet\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto e^{\prime}$}\cr\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\gamma,\mu_{i},\gamma^{\prime})\crcr}}$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=251.59561pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash\mathcal{F}c.\,e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\alpha}\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto\lambda k.\,\lambda
t.\,e^{\prime}\,[\lambda x.\,k\ x\ t/c]\ k_{id}\ ()$}$}}}}\
(\textsc{PControl})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
66.07242pt\hbox{$\penalty
31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma,\,c:\tau\rightarrow\tau_{1}\,\langle\mu_{1}\rangle\,{\tau_{1}}^{\prime}\,\langle\mu_{2}\rangle\,\alpha\vdash
e:\gamma\,\langle\mu_{i}\rangle\,\gamma^{\prime}\,\langle\bullet\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto e^{\prime}$}\cr\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\gamma,\mu_{i},\gamma^{\prime})\cr\mathsf{compatible}((\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}),\mu_{2},\mu_{0})\cr\mathsf{compatible}(\mu_{\beta},\mu_{0},\mu_{\alpha})\crcr}}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=334.49342pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash\mathcal{F}c.\,e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta\
\hbox{\pagecolor{mylightgray}$\leadsto\lambda k.\,\lambda
t.\,e^{\prime}\,[\lambda x.\,\lambda k^{\prime}.\,\lambda t^{\prime}.\,k\ x\
(t\,@\,(k^{\prime}::t^{\prime}))/c]\ k_{id}\ ()$}$}}}}\ (\textsc{IControl})$

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.0pt\hbox{$\penalty 31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma\vdash
e:\beta\,\langle\mu_{i}\rangle\,\beta^{\prime}\,\langle\bullet\rangle\,\tau\
\hbox{\pagecolor{mylightgray}$\leadsto e^{\prime}$}\cr\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\beta,\mu_{i},\beta^{\prime})\crcr}}$}}\kern 0.0pt\hbox{\kern
0.0pt\vrule width=107.28091pt,height=0.0pt,depth=0.0pt\vbox{\kern
0.0pt\hbox{}\kern 0.0pt}}}}\kern 0.0pt\hbox{\kern
7.40352pt\hbox{$\Gamma\vdash_{p}\langle e\rangle:\tau\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}e^{\prime}\ k_{id}\ ()$}$}}}}\
(\textsc{Prompt})\hskip 28.45274pt\mathinner{\raise
0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern 53.15244pt\hbox{$\penalty
31415926\Gamma\vdash_{p}e:\tau\
\hbox{\pagecolor{mylightgray}$\leadsto_{p}e^{\prime}$}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=165.636pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern 0.0pt\hbox{$\Gamma\vdash
e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\alpha}\rangle\,\alpha\
\hbox{\pagecolor{mylightgray}$\leadsto\lambda k.\,\lambda t.\,k\ e^{\prime}\
t$}$}}}}\ (\textsc{Exp})$

Figure 9. Fine-grained Type System and Selective CPS Translation of
$\lambda_{\mathcal{F}}$ (continued)

We start by building a fine-grained type system (Figures 8 and 9, ignoring the
shaded parts) that is suitable for defining a selective CPS translation. As we
wish to use the type system to decide whether or not to CPS-translate an
expression, we make a rigorous distinction between pure and impure
expressions. We do this by introducing a special judgment
$\Gamma\vdash_{p}e:\tau$ for pure expressions, which does not carry answer
types or trail types. This design is borrowed from earlier work on typed
control operators [3, 35], and reflects the fact that a pure expression can be
evaluated independent of its surrounding context. As a corresponding change,
we extend the syntax of expression types with a new arrow type
$\tau\rightarrow\tau$, which we assign to functions having a pure body.

Using the pure judgment and function types, we define the typing rules. There
are several possible strategies for designing a fine-grained type system:

  * •

Define one rule for each combination of the purity of subexpressions [15].
This allows us to design the most optimized CPS translation, but results in a
large number of typing rules (for instance, we would need $2^{3}=8$ rules for
application).

  * •

Define one rule for each syntactic construct, and in each rule, perform a
sophisticated computation over the effects of subexpressions [49, 33]. This
allows us to keep the type system concise, but makes it hard to see how each
construct manipulates the answer type and trail type.

  * •

Define one or more rules for each syntactic construct depending on the
granularity one wish to achieve, and include a rule for converting a pure
expression into an impure one [42]. This allows us to have a reasonably
concise type system, at the cost of losing some optimization opportunities in
the CPS translation.

Here we take the third approach to balance conciseness and efficiency.

Among different constructs, values and prompt are syntactically classified as
pure. Notice that we have two rules for abstractions, differing in the purity
of the body expression. In particular, the (PAbs) rule is necessary for
judging certain applications as pure ones. As we will see shortly, having pure
applications allows us to eliminate multiple administrative redexes in the CPS
translation. For prompt, on the other hand, we only have one rule where the
body is an impure expression. This does not affect typability, as we can
always cast a pure expression into an impure one via (Exp). The casting
introduces some extra redexes in the CPS translation, but here we prioritize
conciseness over efficiency.

An application is pure when the function $e_{1}$, the argument $e_{2}$, and
the body of the function are all pure (PApp). The three rules for application,
together with (Exp), give us the same expressiveness as having $8$ rules as in
the first approach mentioned above. Note that, without (PIApp), we would not
be able to directly call a function that has a pure body but is itself an
impure expression.

A control construct is always judged impure, but it has two rules differing in
the purity of the captured continuation. The impure rule (IControl) is
identical to the (Control) rule from Section 5. The pure rule (PControl) is
simpler than the original rule in that it imposes no compatibility
requirements. To see why we do not need those requirements, recall that the
non-selective CPS translation of $\mathcal{F}c.\,e$ extends the given trail.
This is necessary for allowing the invocation context of $c$ to be accessed by
the control operators that reside in $c$. However, if $c$ is pure, we know
that its invocation does not involve any execution of control. This means, for
a control operator that captures a pure continuation, we do _not_ need to
extend the trail. The absence of the compatibility requirements communicates
the fact that no trail extension happens in this case. The equal initial and
final trail types in the conclusion also reflect the stability of the trail.
Having (PControl) could potentially be beneficial for optimizations, because
extending a trail is done by recursively calling the cons function in the CPS
translation.

###  7.2. Selective CPS Translation

Guided by the fine-grained type system, we define a selective CPS translation
from $\lambda_{\mathcal{F}}$ to $\lambda_{C}$ (shaded parts of Figures 8 and
9). The translation keeps pure expressions in direct-style, and turns impure
expressions into a continuation- and trail-taking function. Unlike the
translation defined in Section 4, the selective translation is defined on the
typing derivation, because the information about purity is not generally
available at the level of syntax. Therefore, we have one translation rule for
each typing rule.

Let us take a closer look at the interesting cases. First, observe the three
translation rules for application. In (PApp), we obtain a direct-style
application ${e_{1}}^{\prime}\ {e_{2}}^{\prime}$. In (PIApp) and (IApp), we
obtain a CPS function that uses the continuation $k$ in a way that is
consistent with the purity of the function body.

Second, compare the translation rules for control. In (PControl), we do _not_
extend the trail as we do in (IControl), since we know the captured
continuation is pure and thus cannot manipulate its invocation context. From
an implementation perspective, this means the selective translation not only
produces fewer applications involving continuations and trails, but also
introduces fewer extensions of trails via consing and appending.

Thirdly and lastly, if a pure expression $e$ is judged as impure via (Exp), it
is translated to a CPS function that immediately calls the continuation $k$
with the direct-style translation of $e$ and the given trail $t$.

###  7.3. Properties

The fine-grained formulation of $\lambda_{\mathcal{F}}$ enjoys similar
properties to the original $\lambda_{\mathcal{F}}$. Specifically, the type
system is sound, the selective CPS translation is type-preserving, and well-
typed programs are terminating.

######  Theorem 6 (Type Soundness).

If $\bullet\vdash_{p}e:\tau$, then evaluation of $e$ does not get stuck.

###### Proof.

As in the original $\lambda_{\mathcal{F}}$, we prove type soundness via
preservation and progress111111The preservation theorem is implemented as the
Reduce relation in lambdaf-fg-red.agda.. ∎

######  Theorem 7 (Type Preservation of Selective CPS Translation).

  1.   2. (1)

If $\Gamma\vdash_{p}e:\tau\leadsto_{p}e^{\prime}$ in $\lambda_{\mathcal{F}}$,
then $\Gamma^{\ast}\vdash e^{\prime}:\tau^{\ast}$ in $\lambda_{C}$.

  3. (2)

If $\Gamma\vdash
e:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\beta}\rangle\,\beta\leadsto
e^{\prime}$ in $\lambda_{\mathcal{F}}$, then $\Gamma^{\ast}\vdash
e^{\prime}:(\tau^{\ast}\rightarrow\mu_{\alpha}^{\ast}\rightarrow\alpha^{\ast})\rightarrow\mu_{\beta}^{\ast}\rightarrow\beta^{\ast}$
in $\lambda_{C}$.

###### Proof.

As before, we prove type preservation by induction on the typing
derivation121212The proof is implemented as functions cpsp and cpsi in cps-
selective.agda.. Note that we need to extend the type translation with a
clause for pure function types:

$\displaystyle(\tau_{1}\rightarrow\tau_{2})^{\ast}$
$\displaystyle=\tau_{1}^{\ast}\rightarrow\tau_{2}^{\ast}$

Notice also that the translation on pure expressions does not introduce new
arrow types, meaning that pure expressions are kept in direct style. ∎

######  Theorem 8 (Termination).

If $\Gamma\vdash_{p}e:\tau$, then there exists some value $v$ such that
$e\leadsto^{\ast}v$, where $\leadsto^{\ast}$ is the reflexive, transitive
closure of $\leadsto$ defined in Figure 1.

###### Proof.

The statement is again witnessed by a CPS interpreter of the fine-grained
$\lambda_{\mathcal{F}}$ implemented in Agda131313The interpreter is
implemented as function go in lambdaf-fg.agda.. ∎

###  7.4. Encoding of shift

Kameyama and Yonezawa [35] show that their type system allows a typed encoding
of shift in terms of control and prompt. We show that this is possible in our
fine-grained calculus as well.

Let us begin by comparing the reduction rules of shift and control:

$\displaystyle E[\langle F[\mathcal{S}k.\,e]\rangle]$ $\displaystyle\leadsto
E[\langle e\,[\lambda x.\,\langle F[x]\rangle/k]\rangle]$ $\displaystyle
E[\langle F[\mathcal{F}k.\,e]\rangle]$ $\displaystyle\leadsto E[\langle
e\,[\lambda x.\,F[x]/k]\rangle]$

We see that the two rules differ in the presence of the delimiter surrounding
the captured continuation. In other words, a continuation captured by shift is
always pure, while a continuation captured by control may be impure.

There is a straightforward encoding of shift by control and prompt [8]: we
simply wrap the continuation captured by control around prompt.

$\displaystyle\mathcal{S}k.\,e$
$\displaystyle=\mathcal{F}k^{\prime}.\,e\,[\lambda x.\,\langle k^{\prime}\
x\rangle/k]$

The encoding is well-typed in the fine-grained $\lambda_{\mathcal{F}}$
141414The encoding is implemented as shift in lambdaf-fg.agda.. Specifically,
the control construct can be typed by (PControl), because the captured
continuation is a pure function. The absence of compatibility requirements, as
well as the equal initial and final trail types, are consistent with the
semantics of the shift operator: it does not modify the trail as general
control may do.

Note that the encoding is _not_ well-typed in the original
$\lambda_{\mathcal{F}}$. The reason is that rule (Control) requires a
compatibility relation that can never hold. Let us look at the derivation of
the control construct:

$\mathinner{\raise 0.0pt\vtop{\offinterlineskip\hbox{\vbox{\hbox{\kern
0.63956pt\hbox{$\penalty
31415926\vbox{\halign{\hfil{\m@th$#$}\hfil\cr\Gamma,\,k^{\prime}:\tau\rightarrow\alpha\,\langle\bullet\rangle\,\alpha\,\langle\bullet\rangle\,\alpha\vdash
e:\gamma\,\langle\mu_{i}\rangle\,\gamma^{\prime}\,\langle\bullet\rangle\,\beta\cr\mathsf{id\mathchar
45\relax cont\mathchar 45\relax
type}(\gamma,\mu_{i},\gamma^{\prime})\cr\mathsf{compatible}((\alpha\rightarrow\,\langle\bullet\rangle\,\,\alpha),\bullet,\mu_{0})\cr\mathsf{compatible}(\mu_{\alpha},\mu_{0},\mu_{\alpha})\crcr}}$}}\kern
0.0pt\hbox{\kern 0.0pt\vrule
width=168.86931pt,height=0.0pt,depth=0.0pt\vbox{\kern 0.0pt\hbox{}\kern
0.0pt}}}}\kern 0.0pt\hbox{\kern
0.0pt\hbox{$\Gamma\vdash\mathcal{F}k^{\prime}.\,e\,[\lambda x.\,\langle
k^{\prime}\
x\rangle/k]:\tau\,\langle\mu_{\alpha}\rangle\,\alpha\,\langle\mu_{\alpha}\rangle\,\beta$}}}}\
(\textsc{Control})$

The instantiation of answer types and trail types is drawn from the typing
constraints of control and prompt. By the definition of compatible, we know
the trail type $\mu_{0}$ in the first compatibility relation must be
$\alpha\rightarrow\,\langle\bullet\rangle\,\,\alpha$. By substituting this
trail type for the $\mu_{0}$ in the second compatibility relation, we obtain
$\mathsf{compatible}(\mu_{\alpha},(\alpha\rightarrow\,\langle\bullet\rangle\,\,\alpha),\mu_{\alpha})$.
This relation does not hold, as we prove in our Agda formalization151515 The
impossibility proof c is included in lambdaf.agda.. As a consequence, we
cannot close the above derivation.

In the fine-grained $\lambda_{\mathcal{F}}$, we can in fact simplify the
encoding as follows:

$\displaystyle\mathcal{S}k.\,e$
$\displaystyle=\mathcal{F}k.\,e\quad\text{where $k$ is pure}$

The simplified encoding says: a control operator that captures a pure
continuation behaves the same as a shift operator. This can be proved by using
the fact that the prompt operator is no-op when its body is a pure expression.
Specifically, if $e$ is pure, the expression $\langle e\rangle$ eventually
evaluates to $\langle v\rangle$ by the termination theorem, and then to $v$ by
the reduction rule ($\mathcal{P}$). Using this fact, we can rewrite the
original encoding to $\mathcal{F}k^{\prime}.\,e\,[\lambda x.\,k^{\prime}\
x/k]$, and then to $\mathcal{S}k.\,e$ by $\eta$-reduction and renaming.

##  8\. Formalization in Agda

We have formalized $\lambda_{\mathcal{F}}$, $\lambda_{C}$, and the CPS
translations in the Agda proof assistant. In this section, we give the reader
a high-level idea of how we formalized these artifacts. For the full
formalization, we invite the reader to visit the following GitHub repository:

https://github.com/YouyouCong/lmcs-artifact

#### Defining Syntax and Typing Rules

Let us begin with the formalization of (original) $\lambda_{\mathcal{F}}$.
Following the recipe of Altenkirch and Reus [2], we define
$\lambda_{\mathcal{F}}$ as an _intrinsically-typed_ language. That is, we
define the syntax and typing at once, and thus guarantee that we can only
construct well-typed expressions.

Before defining expressions, we define expression types and trail types as
datatypes Ty and Tr.

     Ty : Set
     Tr : Set

     Ty
      Nat         : Ty
      Bool        : Ty
      Str         : Ty
      _ $\Rightarrow$ _ $\langle$ _ $\rangle$ _ $\langle$ _ $\rangle$ _ : Ty $\rightarrow$ Ty $\rightarrow$ Tr $\rightarrow$ Ty $\rightarrow$ Tr $\rightarrow$ Ty $\rightarrow$ Ty

     Tr
      $\bullet$      : Tr
      _ $\Rightarrow\!\langle$ _ $\rangle$ _ : Ty $\rightarrow$ Tr $\rightarrow$ Ty $\rightarrow$ Tr

The two datatypes Ty and Tr are declared as an inhabitant of Set, which
represents the type of types. The separation between datatype and constructor
signatures indicates that Ty and Tr are defined by mutual induction. In Ty, we
include three instances of base types, which are necessary for expressing the
two examples from Section 2.

Using Ty and Tr, we define values and expressions.

     Val[ _ ] _  (var : Ty $\rightarrow$ Set) : Ty $\rightarrow$ Set
     Exp[ _ ] _ $\langle$ _ $\rangle$ _ $\langle$ _ $\rangle$ _  (var : Ty $\rightarrow$ Set) : Ty $\rightarrow$ Tr $\rightarrow$ Ty $\rightarrow$ Tr $\rightarrow$ Ty $\rightarrow$ Set

     Val[ _ ] _
      Var : {$\tau$ : Ty} $\rightarrow$ var $\tau$ $\rightarrow$ Val[ var ] $\tau$
      ...

     Exp[ _ ] _ $\langle$ _ $\rangle$ _ $\langle$ _ $\rangle$ _
      Val    : {$\tau$ $\alpha$ : Ty} {$\mu\alpha$ : Tr} $\rightarrow$
               Val[ var ] $\tau$ $\rightarrow$ Exp[ var ] $\tau$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$
      App    : {$\tau_{1}$ $\tau_{2}$ $\alpha$ $\beta$ $\gamma$ $\delta$ : Ty} {$\mu\alpha$ $\mu\beta$ $\mu\gamma$ $\mu\delta$ : Tr} $\rightarrow$
               Exp[ var ] ($\tau_{1}$ $\Rightarrow$ $\tau_{2}$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\beta$ $\rangle$ $\beta$) $\langle$ $\mu\gamma$ $\rangle$ $\gamma$ $\langle$ $\mu\delta$ $\rangle$ $\delta$ $\rightarrow$
               Exp[ var ] $\tau_{1}$ $\langle$ $\mu\beta$ $\rangle$ $\beta$ $\langle$ $\mu\gamma$ $\rangle$ $\gamma$ $\rightarrow$
               Exp[ var ] $\tau_{2}$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\delta$ $\rangle$ $\delta$
      ...
      Prompt : {$\tau$ $\alpha$ $\beta$ $\beta^{\prime}$ : Ty} {$\mu_{i}$ $\mu\alpha$ : Tr} $\rightarrow$
               id-cont-type $\beta$ $\mu_{i}$ $\beta^{\prime}$ $\rightarrow$
               Exp[ var ] $\beta$ $\langle$ $\mu_{i}$ $\rangle$ $\beta^{\prime}$ $\langle$ $\bullet$ $\rangle$ $\tau$ $\rightarrow$
               Exp[ var ] $\tau$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$

The type of expressions can be read as an encoding of the typing judgment used
in the typing rules. The only gap between the two lies in the treatment of
variables. In our formalization, we adopt _parametric higher-order abstract
syntax (PHOAS)_ [14]. The technique allows us to use meta language binders to
manage object language bindings, without breaking the positivity of the
datatype. In our case, we parameterize Val and Exp over var, which is a
function from $\lambda_{\mathcal{F}}$ types to Agda types161616The var
argument is shared among all constructors of Val and Exp. For this reason, we
declare var as a _parameter_ (by writing it before the colon), and thus avoid
introducing it for every constructor signature. In contrast, the type and
trail type arguments vary across constructors. Therefore, we declare them as
_indices_ (by writing them after the colon), and introduce them for every
constructor signature as implicit arguments (by enclosing them in curly
brackets)..

The constructors of Val and Exp represent the typing rules of
$\lambda_{\mathcal{F}}$. For example, the App constructor takes in two
arguments corresponding to the two premises in the typing rule (App). As a
different example, the Prompt constructor demands a proof of the id-cont-type
relation, which is defined as an Agda function returning a type.

#### Defining Reduction Rules

Having defined the syntax and typing rules, we define the reduction rules.

     Reduce {var : Ty $\rightarrow$ Set} :
                {$\tau$ $\alpha$ $\beta$ : Ty} {$\mu\alpha$ $\mu\beta$ : Tr} $\rightarrow$
                Exp[ var ] $\tau$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\beta$ $\rangle$ $\beta$ $\rightarrow$
                Exp[ var ] $\tau$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\beta$ $\rangle$ $\beta$ $\rightarrow$ Set
      ...
      RPrompt : {$\tau$ : Ty} {v : Val[ var ] $\tau$} $\rightarrow$
                Reduce (Prompt (Val v)) (Val v)

The type Reduce e e’ means $e\leadsto e^{\prime}$, and has one constructor for
each reduction rule in Figure 1. For instance, RPrompt represents the rule
$\langle v\rangle\leadsto v$. Notice that the two arguments to Reduce have the
same type. This means, if we can define all the reduction rules as a
constructor of Reduce, then we can be sure that reducing a well-typed
expression produces an expression of the same type. Therefore, the definition
of Reduce is essentially the proof of the preservation theorem (Theorem 1).

#### Defining CPS Translation

Now we proceed to the CPS translation. We formalize the target calculus
$\lambda_{C}$ in a similar way to $\lambda_{\mathcal{F}}$, and define the CPS
translation of types and expressions.

    $\llbracket$ _ $\rrbracket\tau$ : Ty $\rightarrow$ CTy
    $\llbracket$ _ $\rrbracket\mu$ : Tr $\rightarrow$ CTy

    cpsv : {var : CTy $\rightarrow$ Set} {$\tau$ : Ty} $\rightarrow$
           Val[ var $\circ$ $\llbracket$ _ $\rrbracket\tau$ ] $\tau$ $\rightarrow$
           CVal[ var ] $\llbracket$ $\tau$ $\rrbracket\tau$
    cpse : {var : CTy $\rightarrow$ Set} {$\tau$ $\alpha$ $\beta$ : Ty} {$\mu\alpha$ $\mu\beta$ : Tr} $\rightarrow$
           Exp[ var $\circ$ $\llbracket$ _ $\rrbracket\tau$ ] $\tau$ $\langle$ $\mu\alpha$ $\rangle$ $\alpha$ $\langle$ $\mu\beta$ $\rangle$ $\beta$ $\rightarrow$
           CVal[ var ] (($\llbracket$ $\tau$ $\rrbracket\tau$ $\Rightarrow$ $\llbracket$ $\mu\alpha$ $\rrbracket\mu$ $\Rightarrow$ $\llbracket$ $\alpha$ $\rrbracket\tau$) $\Rightarrow$ $\llbracket$ $\beta$ $\rrbracket\mu$ $\Rightarrow$ $\llbracket$ $\beta$ $\rrbracket\tau$)

In the above definition, CTy is the type of $\lambda_{C}$ types, and CVal is
the type of $\lambda_{C}$ values. As we can see, the signature of cpse is
exactly the statement of the type preservation theorem (Theorem 4). Thus, the
definition of cpse serves as a proof of type preservation.

##  9\. Related Work

#### Variations of Control Operators

There are four variants of delimited control operators in the style of
control, differing in whether the operator keeps the surrounding delimiter,
and whether it inserts a delimiter into the captured continuation [22]. We
have seen that the absence of the latter delimiter makes it possible to
capture invocation contexts. The lack of the former delimiter, on the other
hand, gives us access to _metacontexts_ , i.e., contexts outside of the
innermost delimiter. In the CPS translation, metacontexts are represented
using a stack-like data structure, which is also called a trail in the
literature [42].

As an orthogonal variation, some implementations of control operators provide
_prompt tags_ [28, 38], allowing the programmer to specify the association
between the control operator and the delimiter. Since tagged control operators
make it possible to skip intervening delimiters, their CPS translation also
involves a form of trails, containing the delimited contexts within individual
delimiters.

#### Type Systems for Control Operators

The CPS-based approach to designing type systems has been applied to three
variants of delimited control operators, namely shift/reset [19, 3],
control/prompt [35], and shift0/reset0 [42]. Among them, shift0 can capture
metacontexts, hence its type system maintains a list of answer types,
representing the return types of nesting delimiters [42].

The CPS approach gives us by default a type system where every expression is
effectful, as in the original $\lambda_{\mathcal{F}}$. Such a type system is
however impractical, as it rejects many programs that are in fact type-safe.
For instance, we showed that the encoding of shift by control/prompt is ill-
typed if control can only ever capture an impure continuation. It is also
known that implementing the list prefix function using shift/reset requires
continuations to be _answer-type polymorphic_ [3], which basically means
“pure”. For this reason, many type systems for control operators employ a
purity distinction as in the fine-grained $\lambda_{\mathcal{F}}$ [3, 35, 42].

Selective CPS Translations. The idea of selectively CPS-translating programs
has long been studied as a compilation technique for effectful languages. For
example, Kim et al. [37] use a selective CPS translation to reduce the
overhead of ML exceptions. As a different example, Asai and Uehara [4]
implement the shift and reset operators via a selective CPS translation. A
particularly interesting result of the latter work is that, by treating shift-
captured continuations as pure functions, we can significantly speed-up non-
deterministic programs (such as the N-Queen puzzle). In the case of control,
the impact of pure continuations may be even more remarkable, because they not
only reduce continuation parameters, but also eliminate consing and appending
of trails.

Algebraic Effects and Handlers. In the past decade, algebraic effects and
handlers [6, 47] have become a popular tool for handling delimited
continuations. A prominent feature of effect handlers is that a captured
continuation is used at the delimiter site. This makes it unnecessary to keep
track of answer types in the type system, as we can decide within a handler
whether the use of a continuation is consistent with the actual context. The
irrelevance of answer types in turn makes the connection between the type
system and CPS translation looser. Indeed, type systems of effect handlers [5,
36] existed before their CPS semantics [40, 32, 31]. Also, type-preserving CPS
translation of effect handlers is still an open problem in the community [31].

##  10\. Conclusion and Future Work

In this paper, we show how to derive a general type system for the control and
prompt operators. The main idea is to identify all the typing constraints by
analyzing a CPS translation, where trails are represented as a composition of
functions.

The present study is part of a long-term project on formalizing delimited
control facilities whose theory is not yet fully developed. In the rest of
this section, we describe several directions for future work.

#### Polymorphism and Type Inference/Checking

Having established a principle for monomorphic typing, a natural next step is
to extend the calculus with polymorphism. The combination of polymorphism and
effects is a delicate issue, and often requires a value or purity restriction
to restore type soundness [29, 3]. In the presence of control/prompt, we must
further support abstraction over trail types, because otherwise we would not
be able to call a function or continuation in different contexts.

After adding polymorphism, we would like to design an algorithm for type
inference and type checking. We conjecture that answer types can be left
implicit in the user program, because it is the case in a calculus featuring
shift and reset [3]. On the other hand, we anticipate that some of the trail
types need to be explicitly given by the user, as it does not seem always
possible to synthesize the intermediate trail types ($\mu_{0}$,
$\tau_{1}\rightarrow\,\langle\mu_{1}\rangle\,\,{\tau_{1}}^{\prime}$, and
$\mu_{2}$) in the (Control) rule.

#### Implementation

With polymorphism and a type checking/inference algorithm, we are ready to
develop a practical implementation of our control/prompt calculus. There are
several approaches to implementing the dynamic behavior of the control
operators. One way is to use the CPS translation defined in this paper, which
eliminates the need for special runtime support. A more direct approach is to
implement Fujii and Asai’s [27] compiler, which is derived from a CPS
interpreter by applying various program transformations. Once we have a
language that we can play with, we will assess the usability of our language
from the viewpoints of expressiveness and efficiency.

#### Equational Theory and Reflection

So far, the semantics of control and prompt has been given as a CPS
translation and an abstract machine [52, 10]. In future work, we intend to
develop an alternative semantics in the form of an _equational theory_. Such a
semantics exists for shift/reset [34] and shift0/reset0 [41], and is
especially useful for compilation. For instance, it enables converting an
optimization in a CPS compiler into a rewrite in a direct-style program [50].

An equational theory can further be refined into a _reflection_ [51], where
direct-style and CPS expressions are related by reduction rather than
equation. Given the recent advance in the reflection for delimited control
operators [12, 13], we would naturally ask whether it is possible to extend
the results to control/prompt. To answer this question, we need to first
define a version of CPS translation that does not yield administrative redexes
[48, 21], including the applications arising from consing and appending of
trails.

#### Control0/Prompt0 and Shallow Effect Handlers

There is a variation of control and prompt, called control0 and prompt0, that
remove the matching delimiter upon capturing of a continuation. We are
currently formalizing a typed calculus of control0/prompt0, by combining the
insights from the present work and previous study on shift0/reset0 [42]. As
shown by Piróg et al. [46], there exists a pair of macro translations [23]
between control0/prompt0 and _shallow effect handlers_ [30]. Therefore, a good
understanding of control0/prompt0 would serve as a stepping stone to a better
implementation of shallow handlers, which has not yet been fully explored [55,
56].

## References

  * [1] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard.  A functional correspondence between evaluators and abstract machines.  In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, PPDP ’03, pages 8–19, New York, NY, USA, 2003. ACM.  doi:10.1145/888251.888254.
  * [2] Thorsten Altenkirch and Bernhard Reus.  Monadic presentations of lambda terms using generalized inductive types.  In International Workshop on Computer Science Logic, pages 453–468. Springer, 1999.
  * [3] Kenichi Asai and Yukiyoshi Kameyama.  Polymorphic delimited continuations.  In Proceedings of the 5th Asian Conference on Programming Languages and Systems, APLAS ’07, pages 239–254, Berlin, Heidelberg, 2007. Springer-Verlag.
  * [4] Kenichi Asai and Chihiro Uehara.  Selective CPS transformation for shift and reset.  In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’18, pages 40–52, New York, NY, USA, dec 2017\. ACM.  doi:10.1145/3162069.
  * [5] Andrej Bauer and Matija Pretnar.  An effect system for algebraic effects and handlers.  In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, pages 1–16, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
  * [6] Andrej Bauer and Matija Pretnar.  Programming with algebraic effects and handlers.  Journal of Logical and Algebraic Methods in Programming, 84(1):108–123, 2015.
  * [7] Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy.  An operational foundation for delimited continuations in the CPS hierarchy.  Logical Methods in Computer Science, 1, 2005.
  * [8] Dariusz Biernacki and Olivier Danvy.  A simple proof of a folklore theorem about delimited control.  BRICS Report Series, 12(25), 2005.
  * [9] Dariusz Biernacki, Olivier Danvy, and Kevin Millikin.  A dynamic continuation-passing style for dynamic delimited continuations.  BRICS Report Series, 13(15), 2006.
  * [10] Dariusz Biernacki, Olivier Danvy, and Kevin Millikin.  A dynamic continuation-passing style for dynamic delimited continuations.  ACM Trans. Program. Lang. Syst., 38(1), October 2015.  doi:10.1145/2794078.
  * [11] Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan.  On the static and dynamic extents of delimited continuations.  Science of Computer Programming, 60(3):274–297, 2006.
  * [12] Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski.  A reflection on continuation-composing style.  In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, FSCD ’20. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2020.
  * [13] Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski.  Reflecting stacked continuations in a fine-grained direct-style reduction theory.  In Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming, PPDP ’21. ACM, 2021.
  * [14] Adam Chlipala.  Parametric higher-order abstract syntax for mechanized semantics.  In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP ’08, page 143–156, New York, NY, USA, 2008\. Association for Computing Machinery.  URL: https://doi.org/10.1145/1411204.1411226, doi:10.1145/1411204.1411226.
  * [15] Youyou Cong and Kenichi Asai.  Handling delimited continuations with dependent types.  Proc. ACM Program. Lang., 2(ICFP):69:1–69:31, July 2018.  doi:10.1145/3236764.
  * [16] Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai.  A Functional Abstraction of Typed Invocation Contexts.  In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2021/14250, doi:10.4230/LIPIcs.FSCD.2021.12.
  * [17] Thierry Coquand.  Pattern matching with dependent types.  In Proceedings of the Third Workshop on Logical Frameworks, 1992\.
  * [18] Olivier Danvy.  Type-directed partial evaluation.  In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’96, pages 242–257. ACM, 1996.
  * [19] Olivier Danvy and Andrzej Filinski.  A functional abstraction of typed contexts.  BRICS 89/12, August 1989.
  * [20] Olivier Danvy and Andrzej Filinski.  Abstracting control.  In Proceedings of the 1990 ACM conference on LISP and functional programming, pages 151–160. ACM, 1990.
  * [21] Olivier Danvy and Lasse R Nielsen.  A first-order one-pass cps transformation.  Theoretical Computer Science, 308(1-3):239–257, 2003.
  * [22] R. Kent Dyvbig, Simon Peyton Jones, and Amr Sabry.  A monadic framework for delimited continuations.  J. Funct. Program., 17(6):687–730, November 2007.  doi:10.1017/S0956796807006259.
  * [23] Matthias Felleisen.  On the expressive power of programming languages.  In Selected Papers from the Symposium on 3rd European Symposium on Programming, ESOP ’90, pages 35–75, New York, NY, USA, 1991. Elsevier North-Holland, Inc.
  * [24] Mattias Felleisen.  The theory and practice of first-class prompts.  In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’88, pages 180–190, New York, NY, USA, 1988. ACM.  doi:10.1145/73560.73576.
  * [25] Andrzej Filinski.  Representing monads.  In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’94, pages 446–457, New York, NY, USA, 1994. ACM.  doi:10.1145/174675.178047.
  * [26] Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar.  On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control.  Proc. ACM Program. Lang., 1(ICFP):13:1–13:29, August 2017.  doi:10.1145/3110257.
  * [27] Maika Fujii and Kenichi Asai.  Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators.  In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1–16:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2021/14254, doi:10.4230/LIPIcs.FSCD.2021.16.
  * [28] Carl A. Gunter, Didier Rémy, and Jon G. Riecke.  A generalization of exceptions and control in ML-like languages.  In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA ’95, pages 12–23, New York, NY, USA, 1995. ACM.  doi:10.1145/224164.224173.
  * [29] Robert Harper and Mark Lillibridge.  Polymorphic type assignment and cps conversion.  LISP and Symbolic Computation, 6(3):361–379, 1993.
  * [30] Daniel Hillerström and Sam Lindley.  Shallow effect handlers.  In Asian Symposium on Programming Languages and Systems, APLAS ’18, pages 415–435. Springer, 2018.
  * [31] Daniel Hillerström, Sam Lindley, and Robert Atkey.  Effect handlers via generalised continuations.  Journal of Functional Programming, 30, 2020.  doi:10.1017/S0956796820000040.
  * [32] Daniel Hillerström, Sam Lindley, Robert Atkey, and KC Sivaramakrishnan.  Continuation passing style for effect handlers.  In Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction, FSCD ’17, pages 18:1–18:19. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017.
  * [33] Chiaki Ishio and Kenichi Asai.  Verifying selective cps transformation for shift and reset.  In William Bowman and Ronald Garcia, editors, International Symposium on Trends in Functional Programming, volume 12053 of Lecture Notes in Computer Science (LNCS), pages 38–57. Springer, 2019.
  * [34] Yukiyoshi Kameyama and Masahito Hasegawa.  A sound and complete axiomatization of delimited continuations.  In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, ICFP ’03, pages 177–188. ACM, 2003.
  * [35] Yukiyoshi Kameyama and Takuo Yonezawa.  Typed dynamic control operators for delimited continuations.  In International Symposium on Functional and Logic Programming, FLOPS ’08, pages 239–254. Springer, 2008.
  * [36] Ohad Kammar, Sam Lindley, and Nicolas Oury.  Handlers in action.  In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP ’13, pages 145–158, New York, NY, USA, 2013\. ACM.  doi:10.1145/2500365.2500590.
  * [37] Jung-taek Kim, Kwangkeun Yi, and Olivier Danvy.  Assessing the overhead of ML exceptions by selective CPS.  In Proceedings of the 1998 ACM SIGPLAN Workshop on ML, 1998.
  * [38] Oleg Kiselyov.  Delimited control in ocaml, abstractly and concretely.  Theor. Comput. Sci., 435:56–76, June 2012.  URL: https://doi.org/10.1016/j.tcs.2012.02.025, doi:10.1016/j.tcs.2012.02.025.
  * [39] Oleg Kiselyov and K. C. Sivaramakrishnan.  Eff directly in ocaml.  In ML Workshop, 2016.
  * [40] Daan Leijen.  Type directed compilation of row-typed algebraic effects.  In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL ’17, pages 486–499, New York, NY, USA, 2017. ACM.  doi:10.1145/3009837.3009872.
  * [41] Marek Materzok.  Axiomatizing subtyped delimited continuations.  In Computer Science Logic 2013, CSL 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013.
  * [42] Marek Materzok and Dariusz Biernacki.  Subtyping delimited continuations.  In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP ’11, pages 81–93, New York, NY, USA, 2011. ACM.  doi:10.1145/2034773.2034786.
  * [43] Robin Milner.  A theory of type polymorphism in programming.  Journal of computer and system sciences, 17(3):348–375, 1978.
  * [44] Lasse R Nielsen.  A selective CPS transformation.  Electronic Notes in Theoretical Computer Science, 45:311–331, 2001\.
  * [45] Ulf Norell.  Towards a practical programming language based on dependent type theory.  PhD thesis, Chalmers University of Technology, 2007.
  * [46] Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.  Typed equivalence of effect handlers and delimited control.  In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
  * [47] Gordon Plotkin and Matija Pretnar.  Handlers of algebraic effects.  In European Symposium on Programming, ESOP ’09, pages 80–94. Springer, 2009.
  * [48] Gordon D. Plotkin.  Call-by-name, call-by-value and the $\lambda$-calculus.  Theoretical computer science, 1(2):125–159, 1975.
  * [49] Tiark Rompf, Ingo Maier, and Martin Odersky.  Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform.  In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP ’09, pages 317–328, New York, NY, USA, 2009\. ACM.  doi:10.1145/1596550.1596596.
  * [50] Amr Sabry and Matthias Felleisen.  Reasoning about programs in continuation-passing style.  Lisp and symbolic computation, 6(3):289–360, 1993.
  * [51] Amr Sabry and Philip Wadler.  A reflection on call-by-value.  ACM transactions on programming languages and systems (TOPLAS), 19(6):916–941, 1997.
  * [52] Chung-chieh Shan.  A static simulation of dynamic delimited control.  Higher-Order and Symbolic Computation, 20(4):371–401, 2007.
  * [53] Fei Wang, Daniel Zheng, James Decker, Xilun Wu, Grégory M Essertel, and Tiark Rompf.  Demystifying differentiable programming: Shift/reset the penultimate backpropagator.  Proceedings of the ACM on Programming Languages, 3(ICFP):1–31, 2019\.
  * [54] Andrew K. Wright and Matthias Felleisen.  A syntactic approach to type soundness.  Information and computation, 115(1):38–94, 1994.
  * [55] Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen.  Effect handlers, evidently.  Proceedings of the ACM on Programming Languages, 4(ICFP):1–29, 2020\.  doi:10.1145/3408981.
  * [56] Ningning Xie and Daan Leijen.  Generalized evidence passing for effect handlers: Efficient compilation of effect handlers to C.  Proc. ACM Program. Lang., 5(ICFP):1–30, August 2021.  URL: https://doi.org/10.1145/3473576, doi:10.1145/3473576.