1

# Grokking the Sequent Calculus (Functional Pearl)

David Binder  0000-0003-1272-0972 Department of Computer ScienceUniversity of
TübingenSand 14Tübingen72076Germany<EMAIL_ADDRESS>,  Marco
Tzschentke  0009-0004-8834-2984 Department of Computer ScienceUniversity of
TübingenSand 14Tübingen72076Germany<EMAIL_ADDRESS>,
Marius Müller  0000-0002-0260-6298 Department of Computer ScienceUniversity of
TübingenSand 14Tübingen72076Germany<EMAIL_ADDRESS>and  Klaus
Ostermann  0000-0001-5294-5506 Department of Computer ScienceUniversity of
TübingenSand 14Tübingen72076Germany<EMAIL_ADDRESS>
###### Abstract.

The sequent calculus is a proof system which was designed as a more symmetric
alternative to natural deduction. The $\lambda\mu\tilde{\mu}$-calculus is a
term assignment system for the sequent calculus and a great foundation for
compiler intermediate languages due to its first-class representation of
evaluation contexts. Unfortunately, only experts of the sequent calculus can
appreciate its beauty. To remedy this, we present the first introduction to
the $\lambda\mu\tilde{\mu}$-calculus which is not directed at type theorists
or logicians but at compiler hackers and programming-language enthusiasts. We
do this by writing a compiler from a small but interesting surface language to
the $\lambda\mu\tilde{\mu}$-calculus as a compiler intermediate language.

Intermediate representations, continuations, codata types, control effects

††journal: PACMPL††journalvolume: 1††journalnumber: ICFP††article:
1††journalyear: 2024††publicationmonth: 1††copyright: none††ccs: Theory of
computation Lambda calculus††ccs: Software and its engineering Compilers††ccs:
Software and its engineering Control structures

##  1\. Introduction

Suppose you have just implemented your own small functional language. To test
it, you write the following function which multiplies all the numbers
contained in a list:

$\displaystyle\mathbf{def}\ \text{mult}(l)\coloneq\mathbf{case}\ l\
\mathbf{of}\ \\{\,\text{Nil}\Rightarrow 1,\text{Cons}(x,xs)\Rightarrow
x*\text{mult}(xs)\,\\}$

What bugs you about this implementation is that you know an obvious
optimization: The function should directly return zero if it encounters a zero
in the list. There are many ways to achieve this, but you choose to extend
your language with labeled expressions and a goto instruction. This allows you
to write the optimized version:

$\displaystyle\mathbf{def}\ \text{mult}(l)\coloneq\mathbf{label}\ \alpha\
\\{\,\text{mult'}(l;\alpha)\,\\}$ $\displaystyle\mathbf{def}\
\text{mult'}(l;\alpha)\coloneq\mathbf{case}\ l\ \mathbf{of}\
\\{\,\text{Nil}\Rightarrow
1,\text{Cons}(x,xs)\Rightarrow\mathbf{ifz}(x,\mathbf{goto}(0;\alpha),x*\text{mult'}(xs;\alpha))\,\\}$

You used $\mathbf{label}\ \alpha\ \\{\text{mult'}(l;\alpha)\\}$ to introduce a
label $\alpha$ around the call to the helper function mult’ which takes this
label as an additional argument (we use ; to separate the label argument from
the other arguments), and $\mathbf{goto}(0;\alpha)$ to jump to this label
$\alpha$ with the expression $0$ in the recursive helper function. But since
your language now has control effects, you need to reconsider how you want to
compile and optimize programs. In particular, you have to decide on an
appropriate intermediate language which can express these control effects. In
this paper, we introduce you to one such intermediate language: the sequent-
calculus-based $\lambda\mu\tilde{\mu}$-calculus. The result of compiling the
efficient multiplication function to the $\lambda\mu\tilde{\mu}$-calculus is:

$\displaystyle\mathbf{def}\
\text{mult}(l;\alpha)\coloneq\text{mult'}(l;\alpha,\alpha)$
$\displaystyle\mathbf{def}\ \text{mult'}(l;\alpha,\beta)\coloneq$
$\displaystyle\quad\langle l\mid\mathbf{case}\ \\{\text{Nil}\Rightarrow\langle
1\mid\beta\rangle,\text{Cons}(x,xs)\Rightarrow\mathbf{ifz}(x,\langle
0\mid\alpha\rangle,\text{mult'}(xs;\alpha,\tilde{\mu}z.*(x,z;\beta)))\\}\rangle$

Here is how you read this snippet: Besides the list argument $l$, the
definition $\mathbf{def}\ \text{mult}(l;\alpha)\coloneq\ldots$ takes an
argument $\alpha$ which indicates how the computation should continue once the
result of the multiplication is computed (we again use ; to separate these two
kinds of arguments). The helper function mult’ takes a list argument $l$ and
two arguments $\alpha$ and $\beta$; the argument $\beta$ indicates where the
function should return to on a normal recursive call while $\alpha$ indicates
the return point of a short-circuiting computation. In the body of mult’ we
use $\langle l\mid\mathbf{case}\
\\{\text{Nil}\Rightarrow\ldots,\text{Cons}(x,xs)\Rightarrow\ldots\\}\rangle$
to perform a case split on the list $l$. If the list is Nil, then we use
$\langle 1\mid\beta\rangle$ to return 1 to $\beta$, which is the return for a
normal recursive call. If the list has the form Cons$(x,xs)$ and $x$ is zero,
we return with $\langle 0\mid\alpha\rangle$, where $\alpha$ is the return
point which short-circuits the computation. If $x$ isn’t zero, then we have to
perform the recursive call
$\text{mult'}(xs;\alpha,\tilde{\mu}z.*(x,z;\beta))$, where we use
$\tilde{\mu}z.*(x,z;\beta)$ to bind the result of the recursive call to the
variable $z$ before multiplying it with $x$ and returning to $\beta$. Don’t be
discouraged if this looks complicated at the moment; the main part of this
paper will cover everything in much more detail.

Screenshot of the online evaluator.

Figure 1. Screenshot of the online evaluator.

The $\lambda\mu\tilde{\mu}$-calculus that you have just seen was first
introduced by Curien and Herbelin (2000) as a solution to a long-standing open
question: What should a term language for the sequent calculus look like? The
sequent calculus is one of two influential proof calculi introduced by Gentzen
(1935a, b) in a single paper, the other calculus being natural deduction. The
term language for natural deduction is the ordinary lambda calculus, but it
was difficult to find a good term language for the sequent calculus. After it
had been found, the $\lambda\mu\tilde{\mu}$-calculus was proposed as a better
foundation for compiler intermediate languages, for example by Downen et al.
(2016). Despite this, most language designers and compiler writers are still
unfamiliar with it. This is the situation that we hope to remedy with this
pearl.

We frequently discuss ideas which involve the $\lambda\mu\tilde{\mu}$-calculus
with students and colleagues and therefore have to introduce them to its
central ideas. But we usually cannot motivate the
$\lambda\mu\tilde{\mu}$-calculus as a term assignment system for the sequent
calculus, since most of them are not familiar with it. We instead explain the
$\lambda\mu\tilde{\mu}$-calculus on the whiteboard by compiling small
functional programs into it. Such an introduction is regrettably still missing
in the published literature; most existing presentations either presuppose
knowledge of the sequent calculus or otherwise spend a lot of space
introducing it first. We believe that if one can understand the lambda
calculus without first learning about natural deduction proofs, then one
should also be able to understand the $\lambda\mu\tilde{\mu}$-calculus without
knowing the sequent calculus111For the interested reader, we show in Appendix
A how the sequent calculus and the $\lambda\mu\tilde{\mu}$-calculus are
connected..

Why are we excited about the $\lambda\mu\tilde{\mu}$-calculus, and why do we
think that more people should become familiar with its central ideas and
concepts? The main feature which distinguishes the
$\lambda\mu\tilde{\mu}$-calculus from the lambda calculus is its first-class
treatment of evaluation contexts. An evaluation context is the remainder of
the program which runs after the current subexpression we are focused on
finishes evaluating.

This becomes clearer with an example: When we want to evaluate the expression
$(2+3)*5$, we first have to focus on the subexpression $2+3$ and evaluate it
to its result $5$. The remainder of the program, which will run after we have
finished the evaluation, can be represented with the evaluation context
$\square*5$. We cannot bind an evaluation context like $\square*5$ to a
variable in the lambda calculus, but in the $\lambda\mu\tilde{\mu}$-calculus
we can bind such evaluation contexts to covariables. Furthermore, the
$\mu$-operator gives direct access to the evaluation context in which the
expression is currently evaluated. Having such direct access to the evaluation
context is not always necessary for a programmer who wants to write an
application, but it is often important for compiler implementors who write
optimizations to make programs run faster. One solution that compiler writers
use to represent evaluation contexts in the lambda calculus is called
continuation-passing style. In continuation-passing style, an evaluation
context like $\square*5$ is represented as a function $\lambda x.x*5$. This
solution works, but the resulting types which are used to type a program in
this style are arguably hard to understand. Being able to easily inspect these
types can be very valuable, especially for intermediate representations, where
terms tend to look complex. The promise of the
$\lambda\mu\tilde{\mu}$-calculus is to provide the expressive power of
programs in continuation-passing style without having to deal with the type-
acrobatics that are usually associated with it.

The remainder of this paper is structured as follows:

  * •

In Section 2 we introduce the surface language Fun and show how we can
translate it into the sequent-calculus-based language Core. The surface
language is mostly an expression-oriented functional programming language, but
we have added some features such as codata types and control operators whose
translations provide important insights into how the
$\lambda\mu\tilde{\mu}$-calculus works. In this section, we also compare how
redexes are evaluated in both languages.

  * •

In Section 3 we discuss static and dynamic focusing, which are two closely
related techniques for lifting subexpressions which are not values into a
position where they can be evaluated.

  * •

Section 4 introduces the typing rules for Fun and Core and proves standard
results about typing and evaluation.

  * •

We show why we are excited about the $\lambda\mu\tilde{\mu}$-calculus in
Section 5. We present various programming language concepts which become much
clearer when we present them in the $\lambda\mu\tilde{\mu}$-calculus: We show
that let-bindings are precisely dual to control operators, that data and
codata types are two perfectly dual ways of specifying types, and that the
case-of-case transformation is nothing more than a $\mu$-reduction. These
insights are not novel for someone familiar with the
$\lambda\mu\tilde{\mu}$-calculus, but not yet as widely known as they should
be.

  * •

Finally, in Section 6 we discuss related work and provide pointers for further
reading. We conclude in Section 7.

This paper is accompanied by a Haskell implementation which we also make
available as an interactive website (cf. Figure 1). You can run the examples
presented in this paper in the online evaluator.

##  2\. Translating To Sequent Calculus

In this section, we introduce Fun, an expression-oriented functional
programming language, together with its translation into the sequent-calculus-
based intermediate language Core. We present both languages and the
translation function $\llbracket-\rrbracket$ in multiple steps, starting with
arithmetic expressions and adding more features in later subsections. We
postpone the typing rules for both languages until Section 4.

###  2.1. Arithmetic Expressions

We begin with arithmetic expressions which consist of variables, integer
literals, binary operators and $\mathbf{ifz}$, a conditional expression which
checks whether its first argument is equal to zero. The syntax of arithmetic
expressions for Fun and Core is given in 2.1.

######  Definition 2.1 (Arithmetic Expressions).

$x,y,z,\ldots\in\textsc{Variables}\quad\bigstar,\alpha,\beta,\gamma,\ldots\in\textsc{Covariables}\quad\odot\in\\{\ast,+,-\\}$

$\begin{array}[]{r
l}\lx<EMAIL_ADDRESS>t&\Coloneqq
x\mid\ulcorner n\urcorner\mid t\odot t\mid\mathbf{ifz}(t,t,t)\\\
&\phantom{\Coloneqq}\\\ &\phantom{\Coloneqq}\\\ \end{array}$

$\begin{array}[]{r l
r}\lx<EMAIL_ADDRESS>p&\Coloneqq
x\mid\ulcorner n\urcorner\mid\mu\alpha.s&\emph{Producer}\\\
c&\Coloneqq\alpha&\emph{Consumer}\\\
s&\Coloneqq\odot(p,p;c)\mid\mathbf{ifz}(p,s,s)\mid\langle p\mid
c\rangle&\emph{Statement}\end{array}$

$\displaystyle\llbracket x\rrbracket$ $\displaystyle\coloneq x$
$\displaystyle\llbracket t_{1}\odot t_{2}\rrbracket$
$\displaystyle\coloneq\mu\alpha.\odot(\llbracket t_{1}\rrbracket,\llbracket
t_{2}\rrbracket;\alpha)$ $\displaystyle(\alpha\text{ fresh})$
$\displaystyle\llbracket\ulcorner n\urcorner\rrbracket$
$\displaystyle\coloneq\ulcorner n\urcorner$
$\displaystyle\llbracket\mathbf{ifz}(t_{1},t_{2},t_{3})\rrbracket$
$\displaystyle\coloneq\mu\alpha.\mathbf{ifz}(\llbracket
t_{1}\rrbracket,\langle\llbracket
t_{2}\rrbracket\mid\alpha\rangle,\langle\llbracket
t_{3}\rrbracket\mid\alpha\rangle)$ $\displaystyle(\alpha\text{ fresh})$

In Fun there is only one syntactic category: terms $t$. These terms can either
be variables $x$, literals $\ulcorner n\urcorner$, binary operators $t+t$,
$t*t$ and $t-t$, or a conditional $\mathbf{ifz}(t,t_{0},t_{1})$. This
conditional evaluates to $t_{0}$ if $t$ evaluates to $\ulcorner 0\urcorner$,
or to $t_{1}$ otherwise. In contrast to this single category, Core uses three
different syntactic categories: producers $p$, consumers $c$ and statements
$s$. These categories are directly inherited from the
$\lambda\mu\tilde{\mu}$-calculus, and it is important to understand their
differences:

Producers:

All constructs in Core which _construct_ or _produce_ an element of some type
belong to the syntactic category of producers. In other words, producers
correspond to “introduction forms” or “proof terms”, and every term of the
language Fun is translated to a producer in Core.

Consumers:

Consumers are probably less intuitive than producers since they do not
correspond directly to any term of the language Fun. The basic idea is that if
some consumer $c$ has type $\tau$, then $c$ _consumes_ or _destructs_ a
producer of type $\tau$. If you have encountered evaluation contexts or
continuations before, then it is helpful to think of consumers of type $\tau$
as continuations or evaluation contexts for a producer of type $\tau$. And if
you are familiar with the Curry-Howard correspondence, then you can think of
consumers as refutations or direct evidence that a proposition is false.

Statements:

Statements are the ingredient which make computation _happen_ ; without
statements, we would only have static objects without any dynamic behavior.
Here is a non-exhaustive list of examples for statements: Every IO action
which reads from or prints to the console or a file should be represented as a
statement in Core. Computations on primitive types such as machine integers
should be statements. Finally, everything which is a redex in an expression-
based language should also correspond to a statement in Core. Since statements
themselves only compute and do not return anything they do not have a type.

After these general remarks, let us now look at how arithmetic expressions are
represented in the language Core. Variables $x$ and literals $\ulcorner
n\urcorner$ both belong to the category of producers, but binary operators are
represented as statements $\odot(p_{1},p_{2};c)$. First, let us explain why
they are represented as statements instead of producers. The idea is that a
binary operator on primitive integers has to be evaluated directly by the
arithmetic logic unit (ALU) of the underlying machine. And any operation which
directly invokes the machine should belong to the same syntactic category as a
print or other IO instruction: statements. The machine does not return a
result; rather, it reads inputs from registers and makes the result available
in a register for further computation. This is also reflected in the second
surprising aspect: the operator has three instead of two arguments. The two
producers $p_{1}$ and $p_{2}$ correspond to the usual arguments, but the third
consumer argument $c$ says what should happen to the result once the binary
operator has been evaluated. This is similar to the continuation argument of a
function in continuation-passing style. Binary operators
$\odot(p_{1},p_{2};c)$ also display a syntactic convention we use: whenever
some construct has arguments of different syntactic categories, we use a
semicolon instead of a comma to separate them.

We can immediately see that the result of $\llbracket p_{1}+p_{2}\rrbracket$
should contain the statement $+(\llbracket p_{1}\rrbracket,\llbracket
p_{2}\rrbracket;?)$, but we still have to figure out which consumer to plug in
at the third-argument place, and how to convert this statement into a
producer. We can do this with a $\mu$-abstraction in Core, which turns a
statement into a producer while binding a covariable $\alpha$:
$\mu\alpha.+(\llbracket p_{1}\rrbracket,\llbracket p_{2}\rrbracket;\alpha)$.

The statement $\mathbf{ifz}$ works similarly to binary operators: It is a
computation which checks if the producer $p$ is zero and then continues with
one of its two branches. These branches are also statements, indicating which
computation to run after the condition has been evaluated. In the language Fun
the two branches were terms, so we now have to find a way to transform two
producers into two statements. We can do this by using a cut $\langle p\mid
c\rangle$ which combines a producer and a consumer of the same type to obtain
a statement in each branch: $\mathbf{ifz}(\llbracket
t_{1}\rrbracket,\langle\llbracket
t_{2}\rrbracket\mid\,?\,\rangle,\langle\llbracket
t_{3}\rrbracket\mid\,?\,\rangle)$. We can then use the same covariable
$\alpha$ in both statements to represent the fact that the we want the result
in either branch to return to the same point in the program; we use a
surrounding $\mu$-binding again to bind this covariable:
$\mu\alpha.\mathbf{ifz}(\llbracket t_{1}\rrbracket,\langle\llbracket
t_{2}\rrbracket\mid\alpha\rangle,\langle\llbracket
t_{3}\rrbracket\mid\alpha\rangle)$.

Let us now see how arithmetic expressions are evaluated. 2.2 introduces the
syntax of values and covalues, and shows how to reduce immediate redexes. We
use a simple syntactic convention here: The metavariable for a value of terms
$t$ is $\mathfrak{t}$, the values of producers $p$ are written $\mathfrak{p}$
and the covalues which correspond to consumers $c$ are written $\mathfrak{c}$.
We use the symbol $\triangleright$ for reduction in both Fun and Core (and
write $\triangleright^{\ast}$ when multiple steps are performed at once).

######  Definition 2.2 (Evaluation for Arithmetic Expressions).

$\begin{array}[]{l c l
r}\lx<EMAIL_ADDRESS>\mathfrak{t}&\Coloneqq&\ulcorner n\urcorner&\emph{Values}\\\ &\phantom{X}&&\\\
\end{array}$ $\displaystyle\mathbf{ifz}(\ulcorner 0\urcorner,t_{1},t_{2})$
$\displaystyle\triangleright t_{1}$ $\displaystyle\mathbf{ifz}(\ulcorner
n\urcorner,t_{1},t_{2})$ $\displaystyle\triangleright t_{2}\quad\text{(if
$n\neq 0$)}$ $\displaystyle\ulcorner n\urcorner\odot\ulcorner m\urcorner$
$\displaystyle\triangleright\ulcorner n\odot m\urcorner$

$\begin{array}[]{l c l
r}\lx<EMAIL_ADDRESS>\mathfrak{p}&\Coloneqq&\ulcorner n\urcorner&\emph{Values}\\\
\mathfrak{c}&\Coloneqq&\alpha&\emph{Covalues}\end{array}$
$\displaystyle\mathbf{ifz}(\ulcorner 0\urcorner,s_{1},s_{2})$
$\displaystyle\triangleright s_{1}$ $\displaystyle\mathbf{ifz}(\ulcorner
n\urcorner,s_{1},s_{2})$ $\displaystyle\triangleright s_{2}\quad\text{(if
$n\neq 0$)}$ $\displaystyle\odot(\ulcorner n\urcorner,\ulcorner m\urcorner;c)$
$\displaystyle\triangleright\langle\ulcorner n\odot m\urcorner\mid c\rangle$
$\displaystyle\langle\mu\alpha.s\mid\mathfrak{c}\rangle$
$\displaystyle\triangleright s[\mathfrak{c}/\alpha]$

Values and the evaluation of redexes in Fun is straightforward, the only
noteworthy aspect is that the two rules for $\mathbf{ifz}(\cdot,t_{1},t_{2})$
do not require $t_{1}$ and $t_{2}$ to be values. Thus, let us proceed with the
discussion of the language Core.

The first interesting aspect of the language Core is that there are both
values and covalues. This can be explained by the role that values play in
operational semantics: they specify the subset of terms that we are allowed to
substitute for a variable. And since we have both variables which stand for
producers and covariables which stand for consumers, we need both values and
covalues as the respective subsets which we are allowed to substitute for a
variable or covariable.

The second interesting aspect of the language Core is that only statements are
reduced, not producers or consumers. This substantiates our remark from above
that it is statements that introduce dynamism into the language by driving
computation. It also contributes to the feeling that reduction in the language
is close to the evaluation of an abstract machine and that the statements of
Core correspond to the states of such an abstract machine.

We are still faced with a small problem when we want to show that a term of
Fun evaluates to the same result as its translation into Core: We have only
specified the reduction for statements but not for producers. We can easily
solve this problem by introducing a special covariable $\bigstar$ which acts
as the “top-level” consumer of an evaluation. Using $\bigstar$ we can then
evaluate the statement $\langle\llbracket t\rrbracket\mid\bigstar\rangle$
instead of the producer $\llbracket t\rrbracket$.

###### Example 2.1.

Consider the two terms $\ulcorner 2\urcorner*\ulcorner 3\urcorner$ and
$\mathbf{ifz}(\ulcorner 2\urcorner,\ulcorner 5\urcorner,\ulcorner
10\urcorner)$ of Fun. Their respective translations into Core are
$\mu\alpha.*(\ulcorner 2\urcorner,\ulcorner 3\urcorner;\alpha)$ and
$\mu\alpha.\mathbf{ifz}(\ulcorner 2\urcorner,\langle\ulcorner
5\urcorner\mid\alpha\rangle,\langle\ulcorner 10\urcorner\mid\alpha\rangle)$.
When we wrap them into a statement using the top-level continuation
$\bigstar$, we observe the following evaluation:

$\displaystyle\langle\mu\alpha.*(\ulcorner 2\urcorner,\ulcorner
3\urcorner;\alpha)\mid\bigstar\rangle\ \triangleright\ *(\ulcorner
2\urcorner,\ulcorner 3\urcorner;\bigstar)\ \triangleright\ \langle\ulcorner
6\urcorner\mid\bigstar\rangle$
$\displaystyle\langle\mu\alpha.\mathbf{ifz}(\ulcorner
2\urcorner,\langle\ulcorner 5\urcorner\mid\alpha\rangle,\langle\ulcorner
10\urcorner\mid\alpha\rangle)\mid\bigstar\rangle\ \triangleright\
\mathbf{ifz}(\ulcorner 2\urcorner,\langle\ulcorner
5\urcorner\mid\bigstar\rangle,\langle\ulcorner
10\urcorner\mid\bigstar\rangle)\ \triangleright\ \langle\ulcorner
10\urcorner\mid\bigstar\rangle$

We have successfully evaluated the first term to the result $\ulcorner
6\urcorner$ and the second term to the result $\ulcorner 10\urcorner$.

In the following, we will often leave out the first reduction step in
examples, thus silently replacing the covariable bound by the outermost
$\mu$-binding with the top-level consumer $\bigstar$.

Here is a bigger problem that we haven’t addressed yet. The evaluation rules
in the present section do not allow to evaluate nested expressions like
$(\ulcorner 2\urcorner*\ulcorner 4\urcorner)+\ulcorner 5\urcorner$ in Fun or
its translation $\mu\alpha.+(\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
4\urcorner;\beta),\ulcorner 5\urcorner;\alpha)$ in Core. We will discuss this
problem and its solution in more detail in Section 3.

###  2.2. Let Bindings

Let-bindings are important since we can use them to eliminate duplication and
make code more readable. In this section we introduce let-bindings to Fun for
an additional reason: they allow us to introduce the second construct which
gives the $\lambda\mu\tilde{\mu}$-calculus its name:
$\tilde{\mu}$-abstractions.

######  Definition 2.3 (Let-Bindings and $\tilde{\mu}$-abstractions).

$\begin{array}[]{l c
l}\lx<EMAIL_ADDRESS>t&\Coloneqq&\ldots\mid\mathbf{let}\ x=t\ \mathbf{in}\ t\\\
\phantom{\Coloneqq}\end{array}$ $\displaystyle\mathbf{let}\ x=\mathfrak{t}\
\mathbf{in}\ t\triangleright t[\mathfrak{t}/x]$

$\begin{array}[]{l c
l}\lx<EMAIL_ADDRESS>c&\Coloneqq&\ldots\mid\tilde{\mu}x.s\\\
\mathfrak{c}&\Coloneqq&\ldots\mid\tilde{\mu}x.s\\\ \end{array}$
$\displaystyle\langle\mathfrak{p}\mid\tilde{\mu}x.s\rangle\triangleright
s[\mathfrak{p}/x]$

$\displaystyle\llbracket\mathbf{let}\ x=t_{1}\ \mathbf{in}\
t_{2}\rrbracket\coloneq\mu\alpha.\langle\llbracket
t_{1}\rrbracket\mid\tilde{\mu}x.\langle\llbracket
t_{2}\rrbracket\mid\alpha\rangle\rangle$ $\displaystyle\quad(\alpha\text{
fresh})$

The let-bindings in Fun are standard and are evaluated by substituting the
_value_ $\mathfrak{t}$ for the variable $x$ in the body which is a term. The
analogue of a let-binding in Fun is a $\tilde{\mu}$-binding in Core which also
binds a variable, with the difference that the body of a $\tilde{\mu}$-binding
is a statement. It can easily be seen that $\tilde{\mu}$-bindings are the
precise dual of $\mu$-bindings that we have already introduced.

With both $\mu$\- and $\tilde{\mu}$-bindings in Core we have to face a
potential problem, namely statements of the form
$\langle\mu\alpha.s_{1}\mid\tilde{\mu}x.s_{2}\rangle$. Such a statement is
called a _critical pair_ since it can potentially be reduced to both
$s_{1}[\tilde{\mu}x.s_{2}/\alpha]$ and $s_{2}[\mu\alpha.s_{1}/x]$ which can be
a source of non-confluence. A closer inspection of the rules shows that we
avoid this pitfall and always evaluate the statement to
$s_{1}[\tilde{\mu}x.s_{2}/\alpha]$. We do not allow to reduce the statement to
$s_{2}[\mu\alpha.s_{1}/x]$ since only values $\mathfrak{p}$ can be substituted
for variables, and $\mu\alpha.s_{1}$ is not a value. This restriction
precisely mirrors the restriction on the evaluation of let-bindings in Fun. In
other words, we use call-by-value evaluation order. We will address the
critical pair and how it relates to different evaluation orders again in
Section 5.6.

###### Example 2.2.

Consider the term $\mathbf{let}\ x=\ulcorner 2\urcorner*\ulcorner 2\urcorner\
\mathbf{in}\ x*x$ whose translation into Core is the producer
$\mu\alpha.\underline{\langle\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
2\urcorner;\beta)\mid\tilde{\mu}x.\langle\mu\gamma.*(x,x;\gamma)\mid\alpha\rangle\rangle}$.
This producer contains a critical pair which we have underlined. Because we
are using call-by-value, we can observe how the following reduction steps
resolve the critical pair by evaluating the $\mu$-abstraction first.

$\displaystyle\langle\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
2\urcorner;\beta)\mid\tilde{\mu}x.\langle\mu\gamma.*(x,x;\gamma)\mid\bigstar\rangle\rangle\triangleright*(\ulcorner
2\urcorner,\ulcorner
2\urcorner;\tilde{\mu}x.\langle\mu\gamma.*(x,x;\gamma)\mid\bigstar\rangle)\triangleright$
$\displaystyle\langle\ulcorner
4\urcorner\mid\tilde{\mu}x.\langle\mu\gamma.*(x,x;\gamma)\mid\bigstar\rangle\rangle\triangleright\langle\mu\gamma.*(\ulcorner
4\urcorner,\ulcorner
4\urcorner;\gamma)\mid\bigstar\rangle\triangleright*(\ulcorner
4\urcorner,\ulcorner 4\urcorner;\bigstar)\triangleright\langle\ulcorner
16\urcorner\mid\bigstar\rangle$

We can observe that the arithmetic expression $2*2$ has been evaluated only
once, which is precisely what we expect from call-by-value.

###  2.3. Top-level Definitions

We introduce recursive top-level definitions to Fun and Core for two reasons.
They allow us to write more interesting examples and they illustrate a
difference in how recursive calls are handled. The extension is specified in
2.4.

######  Definition 2.4 (Top-level Definitions).

We assume for both languages that $f,g,h,\ldots\in\textsc{Names}$.

$\begin{array}[]{l c l
r}\lx<EMAIL_ADDRESS>F&\Coloneqq&\mathbf{def}\ f(\overline{x};\overline{\alpha})\coloneq
t&\emph{Definitions}\\\ P&\Coloneqq&\emptyset\ \mid\ F,P&\emph{Programs}\\\
t&\Coloneqq&\ldots\mid f(\overline{t};\overline{\alpha})&\emph{Terms}\\\
\end{array}$ $f(\overline{\mathfrak{t}};\overline{\alpha})\triangleright
t[\overline{\mathfrak{t}}/\overline{x},\overline{\alpha}/\overline{\beta}]\quad(\text{if
}f(\overline{x};\overline{\beta})\coloneq t\in P)$

$\begin{array}[]{l c l
r}\lx<EMAIL_ADDRESS>F&\Coloneqq&\mathbf{def}\ f(\overline{x};\overline{\alpha})\coloneq
s&\emph{Definitions}\\\ P&\Coloneqq&\emptyset\ \mid\ F,P&\emph{Programs}\\\
s&\Coloneqq&\ldots\ \mid\ f(\overline{p};\overline{c})&\emph{Statements}\\\
\end{array}$ $f(\overline{\mathfrak{p}};\overline{\mathfrak{c}})\triangleright
s[\overline{\mathfrak{p}}/\overline{x},\overline{\mathfrak{c}}/\overline{\alpha}]\quad(\text{if
}f(\overline{x};\overline{\alpha})\coloneq s\in P)$

$\begin{array}[]{ccc}\llbracket\mathbf{def}\
f(\overline{x};\overline{\alpha})\coloneq t\rrbracket\coloneq\mathbf{def}\
f(\overline{x};\overline{\alpha},\alpha)\coloneq\langle\llbracket
t\rrbracket\mid\alpha\rangle&(\alpha\text{ fresh})\\\ \llbracket
f(\overline{t};\overline{\alpha})\rrbracket\coloneq\mu\alpha.f(\overline{\llbracket
t\rrbracket};\overline{\alpha},\alpha)&(\alpha\text{ fresh})\end{array}$

Top-level definitions should not be confused with first-class functions which
will be introduced later, since they cannot be passed as an argument or
returned as a result. They are a part of a program that consists of a list of
such top-level definitions. The top-level definitions in Fun curiously also
take covariables as arguments even though the language does not contain
consumers; you can ignore that for now. If you remember the example from the
introduction, then you might recall that we use them for passing labels, but
we will only formally introduce that construct in Section 2.6.

We evaluate the call of a top-level definition by looking up the body in the
program and substituting the arguments of the call for the parameters in the
body of the definition. The body of a top-level definition is a term in Fun
and a statement in Core. This difference explains why we have to add an
additional parameter $\alpha$ to every top-level definition when we translate
it; this parameter $\alpha$ also corresponds to the additional continuation
argument when we ordinarily translate a function into continuation-passing
style. We could also have specified that the body of a top-level definition in
Core should be a producer. We don’t do that because when we eventually
translate Core to machine code we want every top-level definition to become
the target of a jump with arguments _without building up a function call
stack_. The following example shows how this works:

###### Example 2.3.

Using a top-level definition, we can represent the factorial function in Core.

$\displaystyle\mathbf{def}\
\text{fac}(n;\alpha)\coloneq\mathbf{ifz}(n,\langle\ulcorner
1\urcorner\mid\alpha\rangle,-(n,\ulcorner
1\urcorner;\tilde{\mu}x.\text{fac}(x;\tilde{\mu}r.*(n,r;\alpha))))$

For the argument $\ulcorner 1\urcorner$ this evaluates in the following way:

$\displaystyle\text{fac}(\ulcorner 1\urcorner,\bigstar)$
$\displaystyle\triangleright\mathbf{ifz}(\ulcorner 1\urcorner,\langle\ulcorner
1\urcorner\mid\bigstar\rangle,-(\ulcorner 1\urcorner,\ulcorner
1\urcorner;\tilde{\mu}x.\text{fac}(x;\tilde{\mu}r.*(\ulcorner
1\urcorner,r;\bigstar))))$ $\displaystyle\triangleright-(\ulcorner
1\urcorner,\ulcorner
1\urcorner;\tilde{\mu}x.\text{fac}(x;\tilde{\mu}r.*(\ulcorner
1\urcorner,r;\bigstar)))$ $\displaystyle\triangleright\langle\ulcorner
0\urcorner\mid\tilde{\mu}x.\text{fac}(x;\tilde{\mu}r.*(\ulcorner
1\urcorner,r;\bigstar))\rangle$ ($\ast$)
$\displaystyle\triangleright\text{fac}(\ulcorner
0\urcorner;\tilde{\mu}r.*(\ulcorner 1\urcorner,r;\bigstar))$
$\displaystyle\triangleright\mathbf{ifz}(\ulcorner 0\urcorner,\langle\ulcorner
1\urcorner\mid\tilde{\mu}r.*(\ulcorner 1\urcorner,r;\bigstar)\rangle,\ldots)$
$\displaystyle\triangleright\langle\ulcorner
1\urcorner\mid\tilde{\mu}r.*(\ulcorner 1\urcorner,r;\bigstar)\rangle$
$\displaystyle\triangleright*(\ulcorner 1\urcorner,\ulcorner
1\urcorner;\bigstar)\triangleright\langle\ulcorner
1\urcorner\mid\bigstar\rangle$

At the point ($\ast$) of the evaluation we can now see how the recursive call
is evaluated. In Fun this recursive call would have the form $1*\text{fac}(0)$
and require a function stack, but in Core we can jump to the definition of fac
with the consumer $\tilde{\mu}r.*(\ulcorner 1\urcorner,r;\bigstar)$ as an
additional argument which contains the information that the result of the
recursive call should be bound to the variable $r$ and then multiplied with
$\ulcorner 1\urcorner$. Note again that this consumer argument corresponds to
a continuation in continuation-passing style (in that sense it might be viewed
as a reified stack) and so the basic techniques used in CPS-based intermediate
representations and compilers can be applied for its implementation.

###  2.4. Algebraic Data and Codata Types

We now extend Fun and Core with two new features: algebraic data and codata
types. Algebraic data types are familiar from most typed functional
programming languages. Algebraic codata types (Hagino, 1989) are a little more
unusual; they are defined by a set of observations or methods called
destructors and are quite similar to interfaces in object-oriented programming
(Cook, 2009). We introduce them both in the same section because they help to
illustrate some of the deep theoretical dualities and symmetries of the
sequent calculus and the $\lambda\mu\tilde{\mu}$-calculus.

To get acquainted with our syntax, let us first briefly look at two short
examples in Fun. The following definition calculates the sum over a
$\mathtt{List}$ it receives as input.

$\displaystyle\mathbf{def}\ \text{sum}(x)\coloneq\mathbf{case}\ x\
\mathbf{of}\ \\{\mathtt{Nil}\Rightarrow\ulcorner
0\urcorner,\mathtt{Cons}(y,ys)\Rightarrow y+\text{sum}(ys)\\}$

It does so by pattern matching using the $\mathbf{case}\ ...\ \mathbf{of}\
\\{...\\}$ construct which is entirely standard. As an example of codata
types, consider this definition:

$\displaystyle\mathbf{def}\ \text{repeat}(x)\coloneq\mathbf{cocase}\
\\{\mathtt{hd}\Rightarrow x,\mathtt{tl}\Rightarrow\text{repeat}(x)\\}$

It constructs an infinite $\mathtt{Stream}$ whose elements are all the same as
the input $x$ of the function. A $\mathtt{Stream}$ is defined by two
destructors, $\mathtt{hd}$ yields the head of the stream and $\mathtt{tl}$
yields the remaining stream without the head. The stream is constructed by
copattern matching (Abel et al., 2013) using the $\mathbf{cocase}\ \\{...\\}$
construct.

######  Definition 2.5 (Algebraic Data and Codata Types).

$\begin{array}[]{rl}\lx<EMAIL_ADDRESS>t&\Coloneqq\ldots\mid K(\overline{t})\mid\mathbf{case}\ t\ \mathbf{of}\
\\{\overline{K(\overline{x})\Rightarrow t}\\}\\\ &\mid
t.D(\overline{t})\mid\mathbf{cocase}\ \\{\overline{D(\overline{x})\Rightarrow
t}\\}\\\ \mathfrak{t}&\Coloneqq\ldots\mid
K(\overline{\mathfrak{t}})\mid\mathbf{cocase}\
\\{\overline{D(\overline{x})\Rightarrow t}\\}\\\
\phantom{\Coloneqq}\end{array}$ $\displaystyle\mathbf{case}\
K(\overline{\mathfrak{t}})\ \mathbf{of}\ \\{K(\overline{x})\Rightarrow
t,\ldots\\}\triangleright t[\overline{\mathfrak{t}}/\overline{x}]$
$\displaystyle\mathbf{cocase}\ \\{D(\overline{x})\Rightarrow
t,\ldots\\}.D(\overline{\mathfrak{t}})\triangleright
t[\overline{\mathfrak{t}}/\overline{x}]$

$\begin{array}[]{rl}\lx<EMAIL_ADDRESS>p&\Coloneqq\ldots\mid K(\overline{p};\overline{c})\mid\mathbf{cocase}\
\\{\overline{D(\overline{x};\overline{\alpha})\Rightarrow s}\\}\\\
c&\Coloneqq\ldots\mid D(\overline{p};\overline{c})\mid\mathbf{case}\
\\{\overline{K(\overline{x};\overline{\alpha})\Rightarrow s}\\}\\\
\mathfrak{p}&\Coloneqq\ldots\mid
K(\overline{\mathfrak{p}};\overline{c})\mid\mathbf{cocase}\
\\{\overline{D(\overline{x};\overline{\alpha})\Rightarrow s}\\}\\\
\mathfrak{c}&\Coloneqq\ldots\mid
D(\overline{p};\overline{c})\mid\mathbf{case}\
\\{\overline{K(\overline{x};\overline{\alpha})\Rightarrow s}\\}\end{array}$
$\displaystyle\langle
K(\overline{\mathfrak{p}};\overline{\mathfrak{c}})\mid\mathbf{case}\
\\{K(\overline{x};\overline{\alpha})\Rightarrow
s,\ldots\\}\rangle\triangleright
s[\overline{\mathfrak{p}}/\overline{x};\overline{\mathfrak{c}}/\overline{\alpha}]$
$\displaystyle\langle\mathbf{cocase}\
\\{D(\overline{x};\overline{\alpha})\Rightarrow s,\ldots\\}\mid
D(\overline{\mathfrak{p}};\overline{\mathfrak{c}})\rangle\triangleright
s[\overline{\mathfrak{p}}/\overline{x};\overline{\mathfrak{c}}/\overline{\alpha}]$

$\displaystyle\llbracket K(t_{1},\ldots,t_{n})\rrbracket$
$\displaystyle\coloneq K(\llbracket t_{1}\rrbracket,\ldots,\llbracket
t_{n}\rrbracket)$ $\displaystyle\llbracket\mathbf{case}\ t\ \mathbf{of}\
\\{\overline{K_{i}(\overline{x_{i,j}})\Rightarrow t_{i}}\\}\rrbracket$
$\displaystyle\coloneq\mu\alpha.\langle\llbracket
t\rrbracket\mid\mathbf{case}\
\\{\overline{K_{i}(\overline{x_{i,j}})\Rightarrow\langle\llbracket
t_{i}\rrbracket\mid\alpha\rangle}\\}\rangle$ $\displaystyle(\alpha\text{
fresh})$ $\displaystyle\llbracket t.D(t_{1},\ldots,t_{n})\rrbracket$
$\displaystyle\coloneq\mu\alpha.\langle\llbracket t\rrbracket\mid D(\llbracket
t_{1}\rrbracket,\ldots,\llbracket t_{n}\rrbracket;\alpha)\rangle$
$\displaystyle(\alpha\text{ fresh})$ $\displaystyle\llbracket\mathbf{cocase}\
\\{\overline{D_{i}(\overline{x_{i,j}})\Rightarrow t_{i}}\\}\rrbracket$
$\displaystyle\coloneq\mathbf{cocase}\
\\{\overline{D_{i}(\overline{x_{i,j}};\alpha_{i})\Rightarrow\langle\llbracket
t_{i}\rrbracket\mid\alpha_{i}\rangle}\\}$
$\displaystyle(\overline{\alpha_{i}}\text{ fresh})$

The general syntax is given in 2.5. We assume fixed sets of constructors $K$
containing at least $\mathtt{Nil}$, $\mathtt{Cons}$ and $\mathtt{Tup}$ and
destructors $D$ containing at least $\mathtt{hd}$, $\mathtt{tl}$,
$\mathtt{fst}$ and $\mathtt{snd}$. In Fun we use constructors $K$ to define
both terms $K(\overline{t})$ and case expressions $\mathbf{case}\ t\
\mathbf{of}\ \\{\overline{K(\overline{x})\Rightarrow t}\\}$. Destructors $D$
of codata types are used in destructor terms $t.D(\overline{t})$ and cocase
expressions $\mathbf{cocase}\ \\{\overline{D(\overline{x})\Rightarrow t}\\}$.
The term $t$ in $\mathbf{case}\ t\ \mathbf{of}\
\\{\overline{K(\overline{x})\Rightarrow t}\\}$ and $t.D(\overline{t})$ is
called the _scrutinee_ in both cases.

####  2.4.1. Data Types

Let us consider another example to better understand the general syntax:

$\displaystyle\mathbf{def}\ \text{swap}(x)\coloneq\mathbf{case}\ x\
\mathbf{of}\ \\{\mathtt{Tup}(y,z)\Rightarrow\mathtt{Tup}(z,y)\\}$

The function swap takes a $\mathtt{Pair}$ and swaps its elements. To do so, it
pattern matches on its input using the $\mathbf{case}\ t\ \mathbf{of}\
\\{\overline{K(\overline{x})\Rightarrow t}\\}$ construct, and constructs a
tuple using a constructor $K(\overline{t})$, where $K$ is specialized to
$\mathtt{Tup}$. Our syntax is quite general, so it is easy to extend it with
new constructors; any such extension only requires that we also add
corresponding typing rules (Section 4).

In Core, algebraic data types are mostly handled in the same way as in Fun.
The main difference is that the scrutinee is no longer a part of a case
expression. Instead, the case expression is a consumer and the scrutinee is a
producer, which are then combined in a statement. This is exactly what is done
in the translation. When a case and a constructor meet, there is an
opportunity for computation, _consuming_ the constructed term and continuing
with the corresponding right-hand side of the case expression. This also
explains our terminology of _producers_ and _consumers_. Constructors create,
or in other words, _produce_ data structures while cases destroy, or _consume_
them.

There is another difference, however. Constructors in Core can now also take
consumers as arguments which is not the case in Fun. An example of this is the
negation type of a type $\tau$ which can be formulated as a data type with one
constructor taking a consumer of type $\tau$ as an argument. A program making
use of this type can be found in section 7.2 of Ostermann et al. (2022).

Fun is a call-by-value language which manifests itself in that a value of an
algebraic data type consists of a constructor applied to other values. A case
expression $\mathbf{case}\ t\ \mathbf{of}\ \\{\ldots\\}$ can only be evaluated
if the scrutinee $t$ is a value, so this means that it must be a constructor
whose arguments are all values in the evaluation rule.

Evaluation in Core is done the same way, only with the scrutinee term changed
to be the producer of a cut. Note that all consumers in Core are covalues
(which is why the arguments of destructors in the definition of covalues are
not in Fraktur font), so in order for a constructor term to be a value, only
its producer arguments need to be values. This also means that the requirement
for the consumer arguments of the constructor to be covalues is vacuously
satisfied in the evaluation rule in Core.

###### Example 2.4.

The translation of swap (including a simplification) is given by

$\displaystyle\mathbf{def}\ \text{swap}(x;\alpha)\coloneq\langle
x\mid\mathbf{case}\
\\{\mathtt{Tup}(y,z)\Rightarrow\langle\mathtt{Tup}(z,y)\mid\alpha\rangle\\}\rangle$

Evaluating with an argument $\mathtt{Tup}(\ulcorner 2\urcorner,\ulcorner
3\urcorner)$ and $\bigstar$ then proceeds as we would expect

$\displaystyle\langle\mathtt{Tup}(\ulcorner 2\urcorner,\ulcorner
3\urcorner)\mid\mathbf{case}\
\\{\mathtt{Tup}(y,z)\Rightarrow\langle\mathtt{Tup}(z,y)\mid\bigstar\rangle\\}\rangle\triangleright\langle\mathtt{Tup}(\ulcorner
3\urcorner,\ulcorner 2\urcorner)\mid\bigstar\rangle$

####  2.4.2. Codata Types

To illustrate the syntax for codata types further, consider the definition

$\displaystyle\mathbf{def}\ \text{swap_lazy}(x)\coloneq\mathbf{cocase}\
\\{\mathtt{fst}\Rightarrow x.\mathtt{snd},\mathtt{snd}\Rightarrow
x.\mathtt{fst}\\}$

swap_lazy takes a lazy pair ($\mathtt{LPair}$), which is defined by its
projections $\mathtt{fst}$ and $\mathtt{snd}$, and swaps its elements. It does
so with a copattern match $\mathbf{cocase}\
\\{\overline{D_{i}(\overline{x})\Rightarrow t_{i}}\\}$ which invokes the
opposite destructor on the original pair in each branch. With a destructor
invocation $t.D(\overline{t})$, where $D$ is specialized to $\mathtt{fst}$ or
$\mathtt{snd}$, we can then obtain the corresponding component of the new
pair.

For codata in Fun, the scrutinee is located in the destructor term instead of
the cocase, inverse to data types. So now destructors are the consumers and
cocases are the producers. This is mirrored in the translation which again
separates the scrutinee, since in Core codata types and copattern matching are
perfectly dual to data types and pattern matching.

All the destructors we have used here do not have producer parameters, but
this is just due to the selection of examples. In the next section, we will
see an example of a destructor with a producer parameter. Moreover, during the
translation each destructor is endowed with an additional consumer parameter
which again determines how execution continues after the destructor was
invoked (and is thus bound by a surrounding $\mu$). For constructors this is
not necessary, as we can use the same consumer variable directly in each
branch of a $\mathbf{case}$ (similar to $\mathbf{ifz}$222We could have
modelled $\mathbf{ifz}$ as a $\mathbf{case}$, too, by modeling numbers as a
data type. But since $\mathbf{ifz}$ corresponds to a machine instruction quite
directly, it is natural to make it a statement, as explained in Section 2.1.)
because the scrutinee and the $\mathbf{case}$ are in the same expression.
Destructors (and also constructors) in Core can even have more than one
consumer parameter. An example of this is given in Section 5.7.

Evaluation is done analogous to data types, with the roles of cases and
constructors reversed for cocases and destructors. Note, however, that for
evaluation in Core the producer arguments of the destructor also have to be
values, so it is not sufficient for the destructor to be a covalue (which it
always is). We will come back to this subtlety in Section 3.

###### Example 2.5.

Translating swap_lazy is done analogously to swap.

$\displaystyle\mathbf{def}\
\text{swap_lazy}(x;\alpha)\coloneq\langle\mathbf{cocase}\
\\{\mathtt{fst}(\beta)\Rightarrow\langle
x\mid\mathtt{snd}(\beta)\rangle,\mathtt{snd}(\beta)\Rightarrow\langle
x\mid\mathtt{fst}(\beta)\rangle\\}\mid\alpha\rangle$

Now take $p=\mathbf{cocase}\
\\{\mathtt{fst}(\alpha)\Rightarrow\langle\ulcorner
1\urcorner\mid\alpha\rangle,\mathtt{snd}(\alpha)\Rightarrow*(\ulcorner
2\urcorner,\ulcorner 3\urcorner;\alpha)\\}$ and evaluate swap_lazy with
$\mathtt{snd}$ to retrieve its first element:

$\displaystyle\text{swap_lazy}(p;\mathtt{snd}(\bigstar))\ \triangleright\ $
$\displaystyle\langle\mathbf{cocase}\ \\{\mathtt{fst}(\beta)\Rightarrow\langle
p\mid\mathtt{snd}(\beta)\rangle,\mathtt{snd}(\beta)\Rightarrow\langle
p\mid\mathtt{fst}(\beta)\rangle\\}\mid\mathtt{snd}(\bigstar)\rangle$
$\displaystyle\triangleright\ \langle p\mid\mathtt{fst}(\bigstar)\rangle\
\triangleright\ $ $\displaystyle\langle\ulcorner
1\urcorner\mid\bigstar\rangle$

Because $\mathbf{cocase}$s are values regardless of their right-hand sides (in
contrast to constructors), we can apply the destructor $\mathtt{snd}$ without
first evaluating the product $*(\ulcorner 2\urcorner,\ulcorner
3\urcorner;\alpha)$. For pairs, we could not do this, as
$\mathtt{Tup}(\ulcorner 1\urcorner,*(\ulcorner 2\urcorner,\ulcorner
3\urcorner;\alpha))$ is not a value, so its arguments have to be evaluated
first. This is why this codata type is called _lazy pair_ , as it allows to
not evaluate its contents in contrast to regular pairs.

This section showed an important property of Core which does not hold for Fun.
The data and codata types of Core are completely symmetric: the syntax for
cases is the same as the syntax for cocases and the same is true for
constructors and destructors. The reason for this deep symmetry is the same
reason that makes the sequent calculus more symmetric than natural deduction,
but in 2.5 we can observe it in a programming language.

###  2.5. First-Class Functions

A core feature that we have omitted until now are first-class functions which
are characterized by lambda abstractions $\lambda x.t$ and function
applications $t_{1}\ t_{2}$. But first-class functions do not add any
expressive power to a language with codata types, since codata types are a
more general concept which subsumes functions as a special case. We could
therefore implement lambda abstractions and function applications as syntactic
sugar in both Fun and Core. This is incidentally also what the developers of
Java did when they introduced lambdas to the language (Goetz et al., 2014). We
introduce lambda abstractions and function application to the syntax of Fun
and desugar them to cocases and destructors of a codata type with an
$\mathtt{ap}$ destructor during the translation to Core.

######  Definition 2.6 (First-Class Functions).

$\begin{array}[]{lcl}\lx<EMAIL_ADDRESS>t&\Coloneqq&\ldots\mid\lambda x.t\mid t\ t\\\
\mathfrak{t}&\Coloneqq&\ldots\mid\lambda x.t\\\\[5.69046pt]
\lx@intercol\hfil(\lambda x.t)\ \mathfrak{t}\triangleright
t[\mathfrak{t}/x]\hfil\lx@intercol\end{array}$

$\begin{array}[]{c}\textbf{Core}\\\\[5.69046pt]
D\in\\{\ldots,\mathtt{ap}\\}\phantom{v}\\\\[5.69046pt] \phantom{\lambda}\\\
\end{array}$

$\begin{array}[]{cc}\llbracket\lambda x.t\rrbracket\coloneq\mathbf{cocase}\
\\{\mathtt{ap}(x;\alpha)\Rightarrow\langle\llbracket
t\rrbracket\mid\alpha\rangle\\}&(\alpha\text{ fresh})\\\ \llbracket t_{1}\
t_{2}\rrbracket\coloneq\mu\alpha.\langle\llbracket
t_{1}\rrbracket\mid\mathtt{ap}(\llbracket
t_{2}\rrbracket;\alpha)\rangle&(\alpha\text{ fresh})\end{array}$

###### Example 2.6.

Consider the term $(\lambda x.x*x)\ \ulcorner 2\urcorner$ in Fun. We can
translate this term and evaluate it in Core as follows:

$\displaystyle\langle\mathbf{cocase}\
\\{\mathtt{ap}(x,\beta)\Rightarrow\langle\mu\gamma.*(x,x;\gamma)\mid\beta\rangle\\}\mid\mathtt{ap}(\ulcorner
2\urcorner;\bigstar)\rangle\triangleright\langle\mu\gamma.*(\ulcorner
2\urcorner,\ulcorner
2\urcorner;\gamma)\mid\bigstar\rangle\triangleright^{\ast}\langle\ulcorner
4\urcorner\mid\bigstar\rangle$

###  2.6. Control Operators

Finally, we add the feature that we used in the motivating example in the
introduction: labels and jumps. We have to extend Fun with $\mathbf{label}$
and $\mathbf{goto}$ constructs but since we can translate them locally to
$\mu$-bindings we don’t have to add anything to Core.

######  Definition 2.7 (Control Operators).

$\begin{array}[]{lcl}t&\Coloneqq&\ldots\mid\mathbf{label}\ \alpha\
\\{t\\}\mid\mathbf{goto}(t;\alpha)\end{array}$ $\llbracket\mathbf{label}\
\alpha\ \\{t\\}\rrbracket\coloneq\mu\alpha.\langle\llbracket
t\rrbracket\mid\alpha\rangle\qquad\llbracket\mathbf{goto}(t;\alpha)\rrbracket\coloneq\mu\beta.\langle\llbracket
t\rrbracket\mid\alpha\rangle\quad(\beta\text{ fresh})$

A term $\mathbf{label}\ \alpha\ \\{t\\}$ binds a covariable $\alpha$ in the
term $t$ and thereby provides a location to which a $\mathbf{goto}$ used
within $t$ can jump. Such a $\mathbf{goto}(t;\alpha)$ takes the location
$\alpha$ as an argument, as well as the term $t$ that should be used to
continue the computation at the location where $\alpha$ was bound. It is a bit
tricky to write down precisely how the evaluation of $\mathbf{label}$ and
$\mathbf{goto}$ works, but the following two rules are a good approximation,
where we assume that $\alpha$ does not occur free in $\mathfrak{t}$:

$\mathbf{label}\ \alpha\
\\{\mathfrak{t}\\}\triangleright\mathfrak{t}\qquad\qquad\mathbf{label}\
\alpha\
\\{\dots\mathbf{goto}(\mathfrak{t};\alpha)\dots\\}\triangleright\mathfrak{t}$

The left rule says that when the labeled term $t$ can be evaluated to a value
$\mathfrak{t}$ without ever using a $\mathbf{goto}$, then we can discard the
surrounding $\mathbf{label}$. The rule on the right says that if we do have a
$\mathbf{goto}$ which jumps to the $\mathbf{label}$ $\alpha$ with a value
$\mathfrak{t}$, then we discard everything between the $\mathbf{label}$ and
the $\mathbf{goto}$ and continue the computation with this value
$\mathfrak{t}$. In order to make this second rule precise, we have to make
explicit what we only indicate with the ellipses separating the label from the
jump; we will do so in Section 3.

###### Example 2.7.

In the introduction, we used the example of a fast multiplication function
which multiplies all the elements of a list and short-circuits the computation
if it encounters a zero. As we have allowed top-level definitions to pass
covariables as arguments, we can now write the example of the introduction.

$\displaystyle\mathbf{def}\ \text{mult}(l)\coloneq\mathbf{label}\ \alpha\
\\{\text{mult'}(l;\alpha)\\}$ $\displaystyle\mathbf{def}\
\text{mult'}(l;\alpha)\coloneq\mathbf{case}\ l\ \mathbf{of}\
\\{\text{Nil}\Rightarrow
1,\text{Cons}(x,xs)\Rightarrow\mathbf{ifz}(x,\mathbf{goto}(0;\alpha),x*\text{mult'}(xs;\alpha))\\}$

When we translate to Core and simplify the resulting term, we get the result:

$\displaystyle\mathbf{def}\
\text{mult}(l;\alpha)\coloneq\text{mult'}(l;\alpha,\alpha)$
$\displaystyle\mathbf{def}\ \text{mult'}(l;\alpha,\beta)\coloneq$
$\displaystyle\quad\langle l\mid\mathbf{case}\ \\{\text{Nil}\Rightarrow\langle
1\mid\beta\rangle,\text{Cons}(x,xs)\Rightarrow\mathbf{ifz}(x,\langle
0\mid\alpha\rangle,*(x,\mu\gamma.\text{mult'}(xs;\alpha,\gamma);\beta))\\}\rangle$

This is almost the result we have seen in the introduction. The only
difference is that the recursive call to mult’ is nested inside the
multiplication. This is the same problem we have seen with nested arithmetic
operations at the end of Section 2.1 and we will address it in the next
section.

The $\mathbf{label}/\mathbf{goto}$ control operator we have introduced in this
subsection is of course named after the goto instructions and labels which can
be found in many imperative programming languages. Our adaption to the context
of functional programming languages is similar to classical control operators
(see Section 5.3 for a more precise discussion) such as J (Landin, 1965) or
$\mathtt{let/cc}$ (also known as $\mathbf{escape}$) (Reynolds, 1972); the
programming language Scala also provides the closely related
$\mathtt{boundary}/\mathtt{break}$333See scala-
lang.org/api/3.3.0/scala/util/boundary$.html. where a boundary marks a block
of code to which the programmer can jump with a break instruction. One central
property of this control effect is that it is lexically scoped, since the
label names $\alpha$ are passed around lexically and can be shadowed. This
distinguishes them from dynamically scoped control operators like the
exception mechanisms found in many programming languages like Java or C++. (A
dynamically scoped variant of our control operator would omit the label names,
and the jump in $\mathbf{label}\ \\{\ldots\mathbf{goto}(t)\ldots\\}$ would
return to the nearest enclosing label at runtime.) We follow the more recent
reappraisal of lexically scoped control effects, for example by Zhang et al.
(2016) in the case of exceptions or by Brachthäuser et al. (2020) in the case
of effect handlers and delimited continuations.

##  3\. Evaluation Within a Context

At the end of Section 2.1 we ran into the problem that we cannot yet fully
evaluate the term $(\ulcorner 2\urcorner*\ulcorner 4\urcorner)+\ulcorner
5\urcorner$ in Fun or its translation $\mu\alpha.+(\mu\beta.*(\ulcorner
2\urcorner,\ulcorner 4\urcorner;\beta),\ulcorner 5\urcorner;\alpha)$ in Core
with the rules that are available to us: we are stuck. In this section, we
finally address this problem. We are going to show how we can evaluate
subexpressions of Fun in Section 3.1, but since we are ultimately more
interested in compiling programs into Core to optimize and reduce those
programs, we are spending more time on the problem for Core in Section 3.2.

###  3.1. Evaluation Contexts for Fun

The problem with evaluating the term $(\ulcorner 2\urcorner*\ulcorner
4\urcorner)+\ulcorner 5\urcorner$ is that the available rules only allow to
reduce direct redexes and not redexes that are nested somewhere within a term.
Evaluation contexts solve this problem by specifying the locations within a
term which are in evaluation position. In our example, the term $(\ulcorner
2\urcorner*\ulcorner 4\urcorner)+\ulcorner 5\urcorner$ can be factored into
the evaluation context $\square+\ulcorner 5\urcorner$ and the redex $\ulcorner
2\urcorner*\ulcorner 4\urcorner$. We can then use the old rules to reduce this
redex to $\ulcorner 8\urcorner$ and then plug this result back into the
evaluation context, which yields the new term $\ulcorner 8\urcorner+\ulcorner
5\urcorner$. The syntax of evaluation contexts is given in 3.1.

######  Definition 3.1 (Evaluation Contexts).

Evaluation contexts $E$ are defined as:

$\begin{array}[]{rcl}E&\Coloneqq&\square\mid E\odot t\mid\mathfrak{t}\odot
E\mid\mathbf{ifz}(E,t,t)\mid\mathbf{let}\ x=E\ \mathbf{in}\ t\mid
f(\overline{\mathfrak{t}},E,\overline{t})\mid
K(\overline{\mathfrak{t}},E,\overline{t})\\\ &\mid&\mathbf{case}\ E\
\mathbf{of}\ \\{\overline{K(\overline{x})\Rightarrow t}\\}\mid E\
t\mid\mathfrak{t}\ E\mid
E.D(\overline{t})\mid\mathfrak{t}.D(\overline{\mathfrak{t}},E,\overline{t})\mid\mathbf{label}\
\alpha\ \\{E\\}\mid\mathbf{goto}(E;\alpha)\end{array}$

These evaluation contexts also allow us to specify formally the second
approximate evaluation rule of the $\mathbf{label}$ and $\mathbf{goto}$
constructs from Section 2.6:

$E[\mathbf{label}\ \alpha\
\\{E^{\prime}[\mathbf{goto}(\mathfrak{t};\alpha)]\\}]\triangleright
E[\mathfrak{t}]$

Here we again assume that $\alpha$ does not occur free in $\mathfrak{t}$ and
moreover that the inner evaluation context $E^{\prime}$ does not contain
another $\mathbf{label}$ construct. For the full operational semantics of
$\mathbf{label}/\mathbf{goto}$ we also need to handle the cases where $\alpha$
can occur free in $\mathfrak{t}$ and where $E^{\prime}$ can contain other
$\mathbf{label}$s. Otherwise, we could get stuck during evaluation even for
closed and well-typed terms, i.e., the progress theorem (see Theorem 4.1 in
Section 4.3) would not hold. As the full semantics is in essence that of other
classical control operators (i.p., $\mathtt{let/cc}$; also see the discussion
in Section 5.3) and requires some more formalism, we do not give it here and
instead refer the interested reader to the brief discussion in Appendix C.

With evaluation contexts, we finally have a working and precise operational
semantics for Fun (apart from the approximate rules for $\mathbf{label}$ and
$\mathbf{goto}$) which we can use to reason about programs. Unfortunately, it
is wildly inefficient to implement an evaluator which uses evaluation contexts
in the way described above. The reason for this inefficiency is that we very
elegantly specified how a term can be factored into an evaluation context and
a redex, but the evaluator which implements this behavior has to search for
the next redex after every single evaluation step. We will see in the next
section that we have a better solution once our programs are compiled into
Core.

###  3.2. Focusing on Evaluation in Core

Let us now come back to the problem in Core and find a solution for the stuck
term $\mu\alpha.+(\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
4\urcorner;\beta),\ulcorner 5\urcorner;\alpha)$. We know that we have to
evaluate $\mu\beta.*(\ulcorner 2\urcorner,\ulcorner 4\urcorner;\beta)$ next
and then somehow plug the intermediate result into the hole $[\cdot]$ in the
producer $\mu\alpha.+([\cdot],\ulcorner 5\urcorner;\alpha)$. If we give the
intermediate result the name $x$ and play around with cuts, $\mu$-bindings and
$\tilde{\mu}$ bindings, we might discover that we can recombine all these
parts in the following way:

$\mu\alpha.\langle\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
4\urcorner;\beta)\mid\tilde{\mu}x.+(x,\ulcorner 5\urcorner;\alpha)\rangle$

This term looks a bit mysterious, but the transformation corresponds roughly
to what happens when we translate the term $\mathbf{let}\ x=2*4\ \mathbf{in}\
x+5$ instead of $(2*4)+5$ into Core. That is, we have lifted a subcomputation
to the outside of the term we are evaluating. This kind of transformation is
called _focusing_ (Andreoli, 1992; Curien and Munch-Maccagnoni, 2010) and we
use it to solve the problem with stuck terms in Core. We can see that it
worked in our example because the term now fully evaluates to its normal form.

###### Example 3.1.

The producer $\mu\alpha.\langle\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
4\urcorner;\beta)\mid\tilde{\mu}x.+(x,\ulcorner 5\urcorner;\alpha)\rangle$
reduces as follows:

$\displaystyle\langle\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
4\urcorner;\beta)\mid\tilde{\mu}x.+(x,\ulcorner 5\urcorner;\bigstar)\rangle$
$\displaystyle\triangleright*(\ulcorner 2\urcorner,\ulcorner
4\urcorner;\tilde{\mu}x.+(x,\ulcorner 5\urcorner;\bigstar))$
$\displaystyle\triangleright\langle\ulcorner
8\urcorner\mid\tilde{\mu}x.+(x,\ulcorner 5\urcorner;\bigstar)\rangle$
$\displaystyle\triangleright+(\ulcorner 8\urcorner,\ulcorner
5\urcorner;\bigstar)\triangleright\langle\ulcorner
13\urcorner\mid\bigstar\rangle$

Once we have settled on focusing, we have another choice to make: Do we want
to use this trick during the evaluation of a statement or as a preprocessing
step before we start with the evaluation? These two alternatives are called
dynamic and static focusing.

Dynamic Focusing:

With dynamic focusing (Wadler, 2003) we add additional evaluation rules,
usually called $\varsigma$-rules, to lift sub-computations to the outside of
the statement we are evaluating.

Static Focusing:

For static focusing (Curien and Herbelin, 2000) we perform a transformation on
the code before we start evaluating it. This results in a focused normal form
which is a subset of the syntax of Core that we have described so far.

Dynamic focusing is great for reasoning about the meaning of programs, but
static focusing is more efficient if we are interested in compiling and
running programs. For this reason, we only consider static focusing in what
follows.

######  Definition 3.2 (Static Focusing).

Static focusing is done using the following rules:

$\begin{array}[]{r c
l}\lx<EMAIL_ADDRESS>\mathcal{F}(\ulcorner n\urcorner)&\coloneq&\ulcorner n\urcorner\\\
\mathcal{F}(x)&\coloneq&x\\\
\mathcal{F}(\mu\alpha.s)&\coloneq&\mu\alpha.\mathcal{F}(s)\\\
\mathcal{F}(K(\overline{\mathfrak{p}},p,\overline{p};\overline{c}))&\coloneq&\mu\alpha.\langle\mathcal{F}(p)\mid\tilde{\mu}x.\langle\mathcal{F}(K(\overline{\mathfrak{p}},x,\overline{p},\overline{c}))\mid\alpha\rangle\rangle\quad(p\text{
not a value})\\\
\mathcal{F}(K(\overline{\mathfrak{p}};\overline{c}))&\coloneq&K(\overline{\mathcal{F}(\mathfrak{p})};\overline{\mathcal{F}(c)})\\\
\mathcal{F}(\mathbf{cocase}\
\\{\overline{D(\overline{x};\overline{\alpha})\Rightarrow
s}\\})&\coloneq&\mathbf{cocase}\
\\{\overline{D(\overline{x};\overline{\alpha})\Rightarrow\mathcal{F}(s)}\\}\\\\[2.84544pt]
\lx<EMAIL_ADDRESS>\mathcal{F}(\alpha)&\coloneq&\alpha\\\
\mathcal{F}(\tilde{\mu}x.s)&\coloneq&\tilde{\mu}x.\mathcal{F}(s)\\\
\mathcal{F}(\mathbf{case}\
\\{\overline{K(\overline{x};\overline{\alpha})\Rightarrow
s}\\})&\coloneq&\mathbf{case}\
\\{\overline{K(\overline{x};\overline{\alpha})\Rightarrow\mathcal{F}(s)}\\}\\\
\mathcal{F}(D(\overline{\mathfrak{p}},p,\overline{p},\overline{c}))&\coloneq&\tilde{\mu}y.\langle\mathcal{F}(p)\mid\tilde{\mu}x.\langle
y\mid\mathcal{F}(D(\overline{\mathfrak{p}},x,\overline{p};\overline{c}))\rangle\rangle\quad(p\text{
not a value})\\\
\mathcal{F}(D(\overline{\mathfrak{p}};\overline{c}))&\coloneq&D(\overline{\mathcal{F}(\mathfrak{p})};\overline{\mathcal{F}(c)})\\\\[2.84544pt]
\lx<EMAIL_ADDRESS>\mathcal{F}(\langle p\mid
c\rangle)&\coloneq&\langle\mathcal{F}(p)\mid\mathcal{F}(c)\rangle\\\
\mathcal{F}(\odot(p_{1},p_{2},c))&\coloneq&\langle\mathcal{F}(p_{1})\mid\tilde{\mu}x.\mathcal{F}(\odot(x,p_{2},c))\rangle\quad(p_{1}\text{
not a value})\\\
\mathcal{F}(\odot(\mathfrak{p},p,c))&\coloneq&\langle\mathcal{F}(p)\mid\tilde{\mu}x.\mathcal{F}(\odot(\mathfrak{p},x,c))\rangle\quad(p\text{
not a value})\\\
\mathcal{F}(\odot(\mathfrak{p}_{1},\mathfrak{p}_{2},c))&\coloneq&\odot(\mathcal{F}(\mathfrak{p}_{1}),\mathcal{F}(\mathfrak{p}_{2}),\mathcal{F}(c))\\\
\mathcal{F}(\mathbf{ifz}(p,s_{1},s_{2}))&\coloneq&\langle\mathcal{F}(p)\mid\tilde{\mu}x.\mathbf{ifz}(x,s_{1},s_{2})\rangle\quad(p\text{
not a value})\\\
\mathcal{F}(\mathbf{ifz}(\mathfrak{p},s_{1},s_{2}))&\coloneq&\mathbf{ifz}(\mathcal{F}(\mathfrak{p}),\mathcal{F}(s_{1}),\mathcal{F}(s_{2}))\\\
\mathcal{F}(\text{f}(\overline{\mathfrak{p}},p,\overline{p};\overline{c}))&\coloneq&\langle\mathcal{F}(p)\mid\tilde{\mu}x.\mathcal{F}(f(\overline{\mathfrak{p}},x,\overline{p};\overline{c}))\rangle\quad(p\text{
not a value})\\\
\mathcal{F}(\text{f}(\overline{\mathfrak{p}},\overline{c}))&\coloneq&\text{f}(\overline{\mathcal{F}(\mathfrak{p})},\overline{\mathcal{F}(c)})\end{array}$

The complete rules for static focusing are presented in 3.2. Most of these
rules are only concerned with performing the focusing transformation on all
subexpressions, but some of the clauses where something interesting happens
are the clauses for binary operators:

$\displaystyle\mathcal{F}(\odot(p_{1},p_{2},c))$
$\displaystyle\coloneq\langle\mathcal{F}(p_{1})\mid\tilde{\mu}x.\mathcal{F}(\odot(x,p_{2},c))\rangle\quad(p_{1}\text{
not a value})$ $\displaystyle\mathcal{F}(\odot(\mathfrak{p},p,c))$
$\displaystyle\coloneq\langle\mathcal{F}(p)\mid\tilde{\mu}x.\mathcal{F}(\odot(\mathfrak{p},x,c))\rangle\quad(p\text{
not a value})$
$\displaystyle\mathcal{F}(\odot(\mathfrak{p}_{1},\mathfrak{p}_{2},c))$
$\displaystyle\coloneq\odot(\mathcal{F}(\mathfrak{p}_{1}),\mathcal{F}(\mathfrak{p}_{2}),\mathcal{F}(c))$

The first two clauses look for the arguments of the binary operator $\odot$
which are not values and use the trick described above to lift them to the
outside. Focusing is invoked recursively until the binary operator is only
applied to values and the third clause comes into play. This third clause then
applies the focusing transformation to all arguments of the binary operator.
The clauses for constructors, destructors, $\mathbf{ifz}$ and calls to top-
level definitions work in precisely the same way as those for binary
operators. It is noteworthy that by focusing the producer arguments of
destructors we guarantee that the evaluation rule for codata types can fire.
If we had not required the producer arguments to be values in that rule (but
only that the destructor is a covalue), we could easily introduce an unfocused
term again by substituting a non-value for a variable.

The focusing transformation described in 3.2 is not ideal since it creates a
lot of administrative redexes. As an example, consider how the statement
defining mult’ from Example 2.7 is focused:

$\displaystyle\mathcal{F}(\langle l\mid\mathbf{case}\
\\{\text{Nil}\Rightarrow\langle
1\mid\beta\rangle,\text{Cons}(x,xs)\Rightarrow\mathbf{ifz}(x,\langle
0\mid\alpha\rangle,*(x,\mu\gamma.\text{mult'}(xs;\alpha,\gamma);\beta))\\}\rangle)$
$\displaystyle=\langle l\mid\mathbf{case}\ \\{\text{Nil}\Rightarrow\langle
1\mid\beta\rangle,\text{Cons}(x,xs)\Rightarrow\mathbf{ifz}(x,\langle
0\mid\alpha\rangle,\langle\mu\gamma.\text{mult'}(xs;\alpha,\gamma)\mid\tilde{\mu}z.*(x,z;\beta)\rangle)\\}\rangle$

Focusing has introduced the administrative redex
$\langle\mu\gamma.\text{mult'}(xs;\alpha,\gamma)\mid\tilde{\mu}z.*(x,z;\beta)\rangle$
in the second statement of the $\mathbf{ifz}$. After reducing this redex to
$\text{mult'}(xs;\alpha,\tilde{\mu}z.*(x,z;\beta))$, we finally arrive at the
result from the introduction. In the implementation, we solve this problem by
statically reducing administrative redexes in a simplification step, but it is
also possible to come up with a more elaborate definition of focusing which
does not create them in the first place. Such an optimized focusing
transformation is, however, much less transparent than the one we have
described.

##  4\. Typing Rules

In this section, we introduce the typing rules for Fun in Section 4.1 and for
Core in Section 4.2. In Section 4.3 we state type soundness for both languages
and prove that the translation from Fun to Core preserves the typeability of
programs. We use the same constructors, destructors, types and typing contexts
for both Fun and Core, which are summarized in 4.1. Note that we distinguish
between producer and consumer variables in the typing contexts, which we
indicate with the prd and cns annotations.

######  Definition 4.1 (Types and Typing Contexts).

$\begin{array}[]{l c l
r}K&\Coloneqq&\mathtt{Nil}\mid\mathtt{Cons}\mid\mathtt{Tup}&\emph{Constructors}\\\
D&\Coloneqq&\mathtt{hd}\mid\mathtt{tl}\mid\mathtt{fst}\mid\mathtt{snd}\mid\mathtt{ap}&\emph{Destructors}\\\
\tau&\Coloneqq&\mathbf{Int}\mid\mathtt{List}(\tau)\mid\mathtt{Pair}(\tau,\tau)\mid\mathtt{Stream}(\tau)\
\mid\ \mathtt{LPair}(\tau,\tau)\mid\tau\to\tau&\emph{Types}\\\
\Gamma&\Coloneqq&\emptyset\mid\Gamma,x:^{\text{\tiny
prd}}\tau\mid\Gamma,\alpha:^{\text{\tiny cns}}\tau&\emph{Typing
Contexts}\end{array}$

We specialize the rules for data types to the concrete types $\mathtt{Pair}$
and $\mathtt{List}$, and the rules for codata types to $\mathtt{LPair}$,
$\mathtt{Stream}$ and functions $\sigma\to\tau$. A realistic programming
language would use type declarations introduced by the programmer to typecheck
data and codata types instead of using these special cases. But the
formalization of such a general mechanism for specifying data and codata types
makes the typing rules less readable. This kind of mechanism for specifying
algebraic data and codata types in sequent-calculus-based languages can be
found in (Downen et al., 2015) or (Downen and Ariola, 2020, section 8). In all
of the typing rules below we assume that we have a program environment which
contains type declarations for all the definitions contained in the program,
but don’t explicitly thread this program environment through each of the
typing rules.

###  4.1. Typing Rules for Fun

We don’t discuss the typing rules for Fun in detail since they are mostly
standard. Instead, we provide the full rules in Appendix B. The language Fun
only has one syntactic category, terms, so we only need one typing judgment
$\Gamma\vdash t:\tau$. This typing judgment says that in the context $\Gamma$
(which contains type assignments for both variables and covariables) the term
$t$ has type $\tau$. The only two interesting rules concern the control
operators $\mathbf{label}$ and $\mathbf{goto}$:

$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash t:\tau$ Label
$\Gamma\vdash\mathbf{label}\ \alpha\ \\{t\\}:\tau$

$\Gamma\vdash t:\tau$ $\alpha:^{\text{\tiny cns}}\tau\in\Gamma$ Goto
$\Gamma\vdash\mathbf{goto}(t;\alpha):\tau^{\prime}$

In the rule Label we add the covariable $\alpha:^{\text{\tiny cns}}\tau$ to
the typing context which is used to typecheck the term $t$. The labeled
expression $\mathbf{label}\ \alpha\ \\{t\\}$ can return in only one of two
ways: either the term $t$ is evaluated to a value and returned, or a jump
instruction is used to jump to the label $\alpha$. For this reason, the term
$t$ and the label $\alpha$ must have the same type $\tau$, which is also the
type for the labeled expression itself.

In the rule Goto we require that the covariable $\alpha$ is in the context
with type $\tau$, and that the term $t$ can be typechecked with the same type.
The term $\mathbf{goto}(t;\alpha)$ itself can be used at any type
$\tau^{\prime}$ because it does not return to its immediately surrounding
context.

###  4.2. Typing Rules for Core

The complete typing rules for Core are given in Figure 2, but we will present
them step by step. We now have producers, consumers and statements as
different syntactic categories. For each of these categories, we use a
separate judgment form:

Producers:

The judgment $\Gamma\vdash p:^{\text{\tiny prd}}\tau$ says that the producer
$p$ has type $\tau$ in context $\Gamma$.

Consumers:

The judgment $\Gamma\vdash c:^{\text{\tiny cns}}\tau$ says that the consumer
$c$ has type $\tau$ in context $\Gamma$.

Statements:

The judgment $\Gamma\vdash s$ says that the statement $s$ is well-typed in
context $\Gamma$. In contrast to producers and consumers, statements do not
have a type.

All typing judgments are also implicitly indexed by the program $P$ containing
the top-level definitions. However, as these definitions are only needed when
typechecking their calls (rule Call), we usually omit the index from the
presentation.

$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash s$ $\mu$
$\Gamma\vdash\mu\alpha.s:^{\text{\tiny prd}}\tau$

$\Gamma,x:^{\text{\tiny prd}}\tau\vdash s$ $\tilde{\mu}$
$\Gamma\vdash\tilde{\mu}x.s:^{\text{\tiny cns}}\tau$

$x:^{\text{\tiny prd}}\tau\in\Gamma$ Var1 $\Gamma\vdash x:^{\text{\tiny
prd}}\tau$

$\alpha:^{\text{\tiny cns}}\tau\in\Gamma$ Var2
$\Gamma\vdash\alpha:^{\text{\tiny cns}}\tau$

$\Gamma\vdash p:^{\text{\tiny prd}}\tau$ $\Gamma\vdash c:^{\text{\tiny
cns}}\tau$ Cut $\Gamma\vdash\langle p\mid c\rangle$

$\Gamma\vdash p:^{\text{\tiny prd}}\mathbf{Int}$ $\Gamma\vdash s_{1}$
$\Gamma\vdash s_{2}$ IfZ $\Gamma\vdash\mathbf{ifz}(p,s_{1},s_{2})$

Lit $\Gamma\vdash\ulcorner n\urcorner:^{\text{\tiny prd}}\mathbf{Int}$

$\Gamma\vdash p_{1}:^{\text{\tiny prd}}\mathbf{Int}$ $\Gamma\vdash
p_{2}:^{\text{\tiny prd}}\mathbf{Int}$ $\Gamma\vdash c:^{\text{\tiny
cns}}\mathbf{Int}$ binop $\Gamma\vdash\odot(p_{1},p_{2};c)$

$\mathbf{def}\ f(\overline{x_{i}:^{\text{\tiny
prd}}\tau_{i}};\overline{\alpha_{j}:^{\text{\tiny cns}}\tau_{j}})\in P$
$\overline{\Gamma\vdash p_{i}:^{\text{\tiny prd}}\tau_{i}}$
$\overline{\Gamma\vdash c_{j}:^{\text{\tiny cns}}\tau_{j}}$ Call
$\Gamma\vdash_{P}f(\overline{p_{i}};\overline{c_{j}})$

$\Gamma\vdash s_{1}$ $\Gamma,x:^{\text{\tiny prd}}\tau,xs:^{\text{\tiny
prd}}\mathtt{List}(\tau)\vdash s_{2}$ Case-List $\Gamma\vdash\mathbf{case}\
\\{\mathtt{Nil}\Rightarrow s_{1},\mathtt{Cons}(x,xs)\Rightarrow
s_{2}\\}:^{\text{\tiny cns}}\mathtt{List}(\tau)$

Nil $\Gamma\vdash\mathtt{Nil}:^{\text{\tiny prd}}\mathtt{List}(\tau)$

$\Gamma\vdash t_{1}:^{\text{\tiny prd}}\tau$ $\Gamma\vdash t_{2}:^{\text{\tiny
prd}}\mathtt{List}(\tau)$ Cons
$\Gamma\vdash\mathtt{Cons}(t_{1},t_{2}):^{\text{\tiny
prd}}\mathtt{List}(\tau)$

$\Gamma\vdash t_{1}:^{\text{\tiny prd}}\tau_{1}$ $\Gamma\vdash
t_{2}:^{\text{\tiny prd}}\tau_{2}$ Tup
$\Gamma\vdash\mathtt{Tup}(t_{1},t_{2}):^{\text{\tiny
prd}}\mathtt{Pair}(\tau_{1},\tau_{2})$

$\Gamma,x:^{\text{\tiny prd}}\tau_{1},y:^{\text{\tiny prd}}\tau_{2}\vdash s$
Case-Pair $\Gamma\vdash\mathbf{case}\ \\{\mathtt{Tup}(x,y)\Rightarrow
s\\}:^{\text{\tiny cns}}\mathtt{Pair}(\tau_{1},\tau_{2})$

$\Gamma\vdash k:^{\text{\tiny cns}}\tau$ Hd
$\Gamma\vdash\mathtt{hd}(k):^{\text{\tiny cns}}\mathtt{Stream}(\tau)$

$\Gamma\vdash k:^{\text{\tiny cns}}\mathtt{Stream}(\tau)$ Tl
$\Gamma\vdash\mathtt{tl}(k):^{\text{\tiny cns}}\mathtt{Stream}(\tau)$

$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash s_{1}$
$\Gamma,\beta:^{\text{\tiny cns}}\mathtt{Stream}(\tau)\vdash s_{2}$ Cocase-
Stream $\Gamma\vdash\mathbf{cocase}\ \\{\mathtt{hd}(\alpha)\Rightarrow
s_{1},\mathtt{tl}(\beta)\Rightarrow s_{2}\\}:^{\text{\tiny
prd}}\mathtt{Stream}(\tau)$

$\Gamma\vdash k:^{\text{\tiny cns}}\tau_{1}$ Fst
$\Gamma\vdash\mathtt{fst}(k):^{\text{\tiny
cns}}\mathtt{LPair}(\tau_{1},\tau_{2})$

$\Gamma\vdash k:^{\text{\tiny cns}}\tau_{2}$ Snd
$\Gamma\vdash\mathtt{snd}(k):^{\text{\tiny
cns}}\mathtt{LPair}(\tau_{1},\tau_{2})$

$\Gamma,\alpha:^{\text{\tiny cns}}\tau_{1}\vdash s_{1}$
$\Gamma,\beta:^{\text{\tiny cns}}\tau_{2}\vdash s_{2}$ Cocase-LPair
$\Gamma\vdash\mathbf{cocase}\ \\{\mathtt{fst}(\alpha)\Rightarrow
s_{1},\mathtt{snd}(\beta)\Rightarrow s_{2}\\}:^{\text{\tiny
prd}}\mathtt{LPair}(\tau_{1},\tau_{2})$

$\Gamma\vdash p:^{\text{\tiny prd}}\sigma$ $\Gamma\vdash c:^{\text{\tiny
cns}}\tau$ Ap $\Gamma\vdash\mathtt{ap}(p,c):^{\text{\tiny cns}}\sigma\to\tau$

$\Gamma,x:^{\text{\tiny prd}}\sigma,\alpha:^{\text{\tiny cns}}\tau\vdash s$
Cocase-Fun $\Gamma\vdash\mathbf{cocase}\ \\{\mathtt{ap}(x,\alpha)\Rightarrow
s\\}:^{\text{\tiny prd}}\sigma\to\tau$

Wf-Empty $\vdash\emptyset\ \textsc{Ok}$

$\vdash P\ \textsc{Ok}$ $\overline{x:^{\text{\tiny
prd}}\tau_{i}},\overline{\alpha:^{\text{\tiny
cns}}\tau_{j}}\vdash_{P,\mathbf{def}\ \text{f}(\overline{x_{i}:^{\text{\tiny
prd}}\tau_{i}};\overline{\alpha_{j}:^{\text{\tiny cns}}\tau_{j}})\coloneq s}s$
Wf-Cons $\vdash P,\mathbf{def}\ \text{f}(\overline{x_{i}:^{\text{\tiny
prd}}\tau_{i}},\overline{\alpha_{j}:^{\text{\tiny cns}}\tau_{j}})\coloneq s\
\textsc{Ok}$

Figure 2. Typing rules of Core.

The three different judgments can be illustrated by the rules for variables,
covariables and cuts. In the rules Var1 and Var2 we check that a variable or
covariable is contained in the typing context $\Gamma$ and then type the
variable as a producer or the covariable as a consumer. The rule Cut combines
a producer $p$ and consumer $c$ of the same type $\tau$ into the statement
$\langle p\mid c\rangle$ which does not have a type.

$x:^{\text{\tiny prd}}\tau\in\Gamma$ Var1 $\Gamma\vdash x:^{\text{\tiny
prd}}\tau$

$\alpha:^{\text{\tiny cns}}\tau\in\Gamma$ Var2
$\Gamma\vdash\alpha:^{\text{\tiny cns}}\tau$

$\Gamma\vdash p:^{\text{\tiny prd}}\tau$ $\Gamma\vdash c:^{\text{\tiny
cns}}\tau$ Cut $\Gamma\vdash\langle p\mid c\rangle$

The two unusual constructs which are central to Core and give the
$\lambda\mu\tilde{\mu}$-calculus its name are the $\mu$\- and
$\tilde{\mu}$-abstractions. A $\mu$-abstraction $\mu\alpha.s$ abstracts over a
consumer $\alpha$ of type $\tau$ in the statement $s$ and is typed as a
producer of type $\tau$. A $\tilde{\mu}$-abstraction $\tilde{\mu}x.s$
abstracts over a producer $x$ of type $\tau$ and is typed as a consumer of
type $\tau$, which can be seen in the following two rules.

$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash s$ $\mu$
$\Gamma\vdash\mu\alpha.s:^{\text{\tiny prd}}\tau$

$\Gamma,x:^{\text{\tiny prd}}\tau\vdash s$ $\tilde{\mu}$
$\Gamma\vdash\tilde{\mu}x.s:^{\text{\tiny cns}}\tau$

####  4.2.1. Data and Codata Types

Figure 2 contains the typing rules for both $\mathtt{Pair}$ and
$\mathtt{List}$; since their rules are so similar we only discuss those of
$\mathtt{Pair}$ explicitly:

$\Gamma\vdash t_{1}:^{\text{\tiny prd}}\tau_{1}$ $\Gamma\vdash
t_{2}:^{\text{\tiny prd}}\tau_{2}$ Tup
$\Gamma\vdash\mathtt{Tup}(t_{1},t_{2}):^{\text{\tiny
prd}}\mathtt{Pair}(\tau_{1},\tau_{2})$

$\Gamma,x:^{\text{\tiny prd}}\tau_{1},y:^{\text{\tiny prd}}\tau_{2}\vdash s$
Case-Pair $\Gamma\vdash\mathbf{case}\ \\{\mathtt{Tup}(x,y)\Rightarrow
s\\}:^{\text{\tiny cns}}\mathtt{Pair}(\tau_{1},\tau_{2})$

In the rule Tup we type a pair constructor $\mathtt{Tup}$ applied to two
arguments as a producer, and in the rule Case-Pair we type the case, which
pattern-matches on this constructor and brings two variables into scope, as a
consumer.

The typing rules for codata types look exactly the same, only the roles of
producers and consumers are swapped.

$\Gamma\vdash k:^{\text{\tiny cns}}\tau$ Hd
$\Gamma\vdash\mathtt{hd}(k):^{\text{\tiny cns}}\mathtt{Stream}(\tau)$

$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash s_{1}$
$\Gamma,\beta:^{\text{\tiny cns}}\mathtt{Stream}(\tau)\vdash s_{2}$ Cc-Str
$\Gamma\vdash\mathbf{cocase}\ \\{\mathtt{hd}(\alpha)\Rightarrow
s_{1},\mathtt{tl}(\beta)\Rightarrow s_{2}\\}:^{\text{\tiny
prd}}\mathtt{Stream}(\tau)$

Most of the other rules directly correspond to a similar rule for Fun. When
typing arithmetic expressions, for example, we only have to make sure all
subterms have type $\mathbf{Int}$.

We typecheck programs using the two rules Wf-Empty and Wf-Cons. The former is
used to typecheck an empty program, and the rule Wf-Cons extends a typechecked
program with a new top-level definition. When we typecheck the body of this
top-level definition that we are about to add, we extend the program with this
definition so that it can refer to itself recursively.

###  4.3. Type Soundness

In this section, we discuss the soundness of the type systems for both Fun and
Core and show that the translation $\llbracket-\rrbracket$ preserves the
typeability of terms. We follow Wright and Felleisen (1994) in presenting type
soundness as the combination of a progress and a preservation theorem.

###### Theorem 4.1 (Progress, Fun).

Let $t$ be a closed term in Fun, such that $\vdash t:\tau$ for some type
$\tau$. Then either $t$ is a value or there is some term $t^{\prime}$ such
that $t\triangleright t^{\prime}$.

This can easily be proved with an induction on typing derivations. Due to the
presence of the $\mathbf{label}/\mathbf{goto}$ construct, the standard
formulation of the (strong) preservation theorem does not immediately hold for
Fun (also see the discussion in Appendix C). The following weak form of
preservation can again be easily proved by induction.

###### Theorem 4.2 ((Weak) Preservation, Fun).

Let $t,t^{\prime}$ be terms in Fun such that $t\triangleright t^{\prime}$,
$\Gamma$ an environment and $P$ a program such that $\Gamma\vdash_{P}t:\tau$.
Then there is a type $\tau^{\prime}$ such that
$\Gamma\vdash_{P}t^{\prime}:\tau^{\prime}$.

The usual strong preservation theorem requires $\tau^{\prime}=\tau$. But in
fact, a slight variation of this strong form can be proved for Fun by adapting
the technique found in Section 6 in (Wright and Felleisen, 1994). Thus, strong
type soundness still does hold.

Before we can state the analogous theorems for Core, we will need an
additional definition as a termination condition for evaluation.

###### Definition 4.3 (Terminal statement).

If $\mathfrak{p}$ is a producer value in Core and $\bigstar$ a covariable
which does not appear free in $\mathfrak{p}$, then
$\langle\mathfrak{p}\mid\bigstar\rangle$ is called a _terminal statement_.

Terminal statements in Core have the same role as values in Fun. Some sequent-
calculus-based languages use a special statement $\mathbf{Done}$ instead of
terminal statements for this purpose.

###### Theorem 4.4 (Progress, Core).

Let $s$ be a focused statement in Core such that $\vdash s$. Then either $s$
is a terminal statement, or there is some $s^{\prime}$ such that
$s\triangleright s^{\prime}$.

For this theorem, we require $s$ to be focused, in contrast to Fun, where
progress holds for any (well-typed) term. This is because we have used static
focusing for full evaluation in Core. If we used dynamic focusing instead,
this requirement could be dropped, corresponding to using evaluation contexts
(dynamic) in Fun, instead of a translation to normal form (static).

The Preservation theorem for Core is analogous to Fun.

###### Theorem 4.5 (Preservation, Core).

Let $s,s^{\prime}$ be statements in Core with $s\triangleright s^{\prime}$,
$\Gamma$ an environment and $P$ a program. If $\Gamma\vdash_{P}s$, then
$\Gamma\vdash_{P}s^{\prime}$.

This theorem can also be proven with a straightforward induction on typing
derivations. Of course, this preservation theorem does not make any assertion
about result types, as statements do not return anything that could be typed.
However, if evaluation starts with a statement $\langle p\mid\bigstar\rangle$
where $\bigstar$ does not occur free in $p$ and ends in a terminal statement
$s$, then $s=\langle\mathfrak{p}\mid\bigstar\rangle$ for some producer value
$\mathfrak{p}$. This is because no reduction step can introduce a free
variable, so the final one must be the same as the initial one. Hence, by
well-typedness, if $p:^{\text{\tiny prd}}\tau$, then also
$\mathfrak{p}:^{\text{\tiny prd}}\tau$, because $\bigstar:^{\text{\tiny
cns}}\tau$.

Lastly, we come to an important property of the translation between these
languages:

###### Theorem 4.6 (Type Preservation of Translation).

Let $t$ be a term in Fun, $\Gamma$ an environment and $P$ a program. If
$\Gamma\vdash_{P}t:\tau$ for some type $\tau$, then $\Gamma\vdash_{\llbracket
P\rrbracket}\llbracket t\rrbracket:^{\text{\tiny prd}}\tau$ where $\llbracket
P\rrbracket$ denotes the translation of all definitions in $P$.

###### Proof.

Most cases are straightforward in the proof which proceeds by a structural
induction on the typing derivation. The interesting cases are when the typing
derivation types a control operator. The only rule in Fun with
$\mathbf{label}\ \alpha\ \\{t_{1}\\}$ in the conclusion is Label. This rule
has the premise $\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash t_{1}:\tau$, and
applying the induction hypothesis gives $\Gamma,\alpha:^{\text{\tiny
cns}}\tau\vdash\llbracket t_{1}\rrbracket:^{\text{\tiny prd}}\tau$. Then we
can derive $\llbracket t\rrbracket=\mu\alpha.\langle\llbracket
t_{1}\rrbracket\mid\alpha\rangle:^{\text{\tiny prd}}\tau$:

(Induction Hypothesis) $\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash\llbracket
t_{1}\rrbracket:^{\text{\tiny prd}}\tau$ Var2 $\Gamma,\alpha:^{\text{\tiny
cns}}\tau\vdash\alpha:^{\text{\tiny cns}}\tau$ Cut
$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash\langle\llbracket
t_{1}\rrbracket\mid\alpha\rangle$ $\mu$
$\Gamma\vdash\mu\alpha.\langle\llbracket
t_{1}\rrbracket\mid\alpha\rangle:^{\text{\tiny prd}}\tau$

The only rule with $\mathbf{goto}(t_{1};\alpha)$ in the conclusion is Goto,
which has premises $\Gamma\vdash t_{1}:\tau$ and $\alpha:^{\text{\tiny
cns}}\tau\in\Gamma$. Applying the induction hypothesis gives
$\Gamma\vdash\llbracket t_{1}\rrbracket:^{\text{\tiny prd}}\tau$, and we can
therefore type the translation of the translation as follows (where we
implicitly use weakening, which is allowed since $\beta$ is fresh)

(Induction Hypothesis) $\Gamma,\beta:^{\text{\tiny cns}}\sigma\vdash\llbracket
t_{1}\rrbracket:^{\text{\tiny prd}}\tau$ $\alpha:^{\text{\tiny
cns}}\tau\in\Gamma,\beta:^{\text{\tiny cns}}\sigma$ Var2
$\Gamma,\beta:^{\text{\tiny cns}}\sigma\vdash\alpha:^{\text{\tiny cns}}\tau$
Cut $\Gamma,\beta:^{\text{\tiny cns}}\sigma\vdash\langle\llbracket
t_{1}\rrbracket\mid\alpha\rangle$ $\mu$
$\Gamma\vdash\mu\beta.\langle\llbracket
t_{1}\rrbracket\mid\alpha\rangle:^{\text{\tiny prd}}\tau$

∎

##  5\. Insights

In the previous section, we have explained _what_ the
$\lambda\mu\tilde{\mu}$-calculus is, and _how_ it works. Now that we know the
what and how we can explain _why_ this calculus is so interesting. This
section is therefore a small collection of independent insights. To be clear,
these insights are obvious to those who are deeply familiar with the
$\lambda\mu\tilde{\mu}$-calculus, but we can still recall how surprising they
were for us when we first learned about them.

###  5.1. Evaluation Contexts are First Class

A central feature of the $\lambda\mu\tilde{\mu}$-calculus is the treatment of
evaluation contexts as first-class objects, as we have mentioned before. For
example, consider the term $(\ulcorner 2\urcorner*\ulcorner
3\urcorner)*\ulcorner 4\urcorner$ in Fun. When we want to evaluate this, we
have to use the evaluation context $\square*\ulcorner 4\urcorner$ to evaluate
the subterm $(\ulcorner 2\urcorner*\ulcorner 3\urcorner)$ and get $\ulcorner
6\urcorner*\ulcorner 4\urcorner$ which we can then evaluate to $\ulcorner
24\urcorner$. Translating this term into Core gives
$\mu\alpha.*(\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
3\urcorner;\beta),\ulcorner 4\urcorner;\alpha)$. To evaluate this term, we
first need to focus it giving

$\displaystyle\mu\alpha.\langle\mu\beta.*(\ulcorner 2\urcorner,\ulcorner
3\urcorner;\beta)\mid\tilde{\mu}x.*(x,\ulcorner 4\urcorner;\alpha)\rangle$

When we now start evaluating with $\bigstar$, the steps are the same as in
Fun. Using call-by-value, the $\mu$-abstraction is evaluated first, giving
$*(\ulcorner 2\urcorner,\ulcorner 3\urcorner;*(\tilde{\mu}x.*(x,\ulcorner
4\urcorner;\bigstar))$. This now has the form where the product can be
evaluated to $\langle\ulcorner 6\urcorner\mid\tilde{\mu}x.*(x,\ulcorner
4\urcorner;\bigstar)\rangle$, after which $\ulcorner 6\urcorner$ is
substituted for $x$. The term $*(\ulcorner 6\urcorner,\ulcorner
4\urcorner;\bigstar)$ can then be directly evaluated to $\ulcorner
24\urcorner$.

After focusing, we can see how $\beta$ is a variable that stands for the
evaluation context in Fun. The term $\tilde{\mu}x.*(x,\ulcorner
4\urcorner;\alpha)$ is the first-class representation of the evaluation
context $\square*\ulcorner 4\urcorner$. We first evaluate the subexpression
$*(\ulcorner 2\urcorner,\ulcorner 3\urcorner;\beta)$ and then insert the
result into $*(x,\ulcorner 4\urcorner;\bigstar)$ to finish the evaluation, as
we did in Fun. In other words, the $\square$ of an evaluation context in Fun,
corresponds to a continuation $\beta$ in Core, and similarly determines in
which order subexpressions are evaluated.

###  5.2. Data is Dual to Codata

The sequent calculus clarifies the relation between data and codata as being
exactly dual to each other. When looking at the typing rules in Figure 2, we
can see that data and codata types are completely symmetric. The two are not
symmetric in languages based on natural deduction: A pattern match on data
types includes the scrutinee but there is no corresponding object in the
construction of codata. Similarly, invoking a destructor $D$ of a codata type
always includes the codata object $x$ to be destructed, e.g., $x.D(\ldots)$,
whereas the invocation of the constructor of a data type has no corresponding
object.

This asymmetry is fixed in the sequent calculus. Destructors (such as
$\mathtt{fst}$) are first-class and don’t require a scrutinee, which repairs
the symmetry to constructors. Similarly, pattern matches ($\mathbf{case}\
\\{\ldots\\}$) do not require an object to destruct, which makes them
completely symmetrical to copattern matches. This duality reduces the
conceptual complexity and opens the door towards shared design and
implementation of features of data and codata types.

###  5.3. Let-Bindings are Dual to Control Operators

The $\mathbf{label}$ construct in Fun is translated to a $\mu$-binding in
Core. Also, when considering the typing rule for $\mathbf{label}\ \alpha\
\\{t\\}$ in Section 4.1, we can see that it directly corresponds to typing a
$\mu$-binding with the label $\alpha$ being the bound covariable. Similarly, a
$\mathbf{let}$-binding is translated to a $\tilde{\mu}$-binding and typing a
$\mathbf{let}$-binding in Fun closely corresponds to typing a
$\tilde{\mu}$-term in Core. This way, $\mathbf{label}$s and
$\mathbf{let}$-bindings are dual to each other, the same way $\mu$ and
$\tilde{\mu}$ are. The duality can be extended to other control operators such
as $\mathtt{call/cc}$.

As it turns out, the $\mathbf{label}$ construct is very closely related to
$\mathtt{call/cc}$. There are in fact only two differences. First,
$\mathbf{label}\ \alpha\ \\{t\\}$ has the binder $\alpha$ for the continuation
built into the construct, just as the variation of $\mathtt{call/cc}$ named
$\mathtt{let/cc}$ (which Reynolds (1972) called $\mathbf{escape}$). The
second, and more important difference is that the invocation of the
continuation captured by $\mathbf{label}\ \alpha\ \\{t\\}$ happens through an
explicit language construct $\mathbf{goto}(t;\alpha)$. This makes it easy to
give a translation to Core as we can simply insert another $\mu$-binding to
discard the remaining continuation at exactly the place where the captured
continuation is invoked. In contrast, with $\mathtt{call/cc}$ and
$\mathtt{let/cc}$ the continuation is applied in the same way as a normal
function, making it necessary to redefine the variable the captured
continuation is bound to when translating to Core. This obscures the duality
to $\mathbf{let}$-bindings which is so evident for $\mathbf{label}$ and
$\mathbf{goto}$.

To see this, here is a translation of $\mathtt{let/cc}~{}k~{}t$ to Core

$\displaystyle\llbracket\mathtt{let/cc}~{}k~{}t\rrbracket$
$\displaystyle\coloneq\mu\alpha.\langle\mathbf{cocase}\
\\{\mathtt{ap}(x,\beta)\Rightarrow\langle
x\mid\alpha\rangle\\}\mid\tilde{\mu}k.\langle\llbracket
t\rrbracket\mid\alpha\rangle\rangle$

The essence of the translation still is that the current continuation is
captured by the outer $\mu$ and bound to $\alpha$. But now we also have to
transform this $\alpha$ into a function (the $\mathbf{cocase}$ here) which
discards its context (here bound to $\beta$) and bind this function to $k$,
which is done using $\tilde{\mu}$. For $\mathtt{call/cc}$, the duality is even
more obscured, as there the binder for the continuation is hidden in the
function which $\mathtt{call/cc}$ is applied to. For the translation, this
function must then be applied to the above $\mathbf{cocase}$ and the captured
continuation $\alpha$, resulting in the following term (cf. also (Miquey,
2019)).

$\displaystyle\llbracket\mathtt{call/cc}~{}f\rrbracket$
$\displaystyle\coloneq\mu\alpha.\langle\llbracket
f\rrbracket\mid\mathtt{ap}(\mathbf{cocase}\
\\{\mathtt{ap}(x,\beta)\Rightarrow\langle
x\mid\alpha\rangle\\},\alpha)\rangle$

Other control operators for undelimited continuations can be translated in a
similar way. For example, consider Felleisen’s $\mathcal{C}$ (Felleisen et
al., 1987). The difference to $\mathtt{call/cc}$ is that $\mathcal{C}$
discards the current continuation if it is not invoked somewhere in the term
$\mathcal{C}$ is applied to, whereas $\mathtt{call/cc}$ leaves it in place and
thus behaves as a no-op if the captured continuation is never invoked. The
only change that needs to be made in the translation to Core is that the top-
level continuation $\bigstar$ has to be used for the outer cut instead of
using the captured continuation. This is most easily seen for a variation of
$\mathcal{C}$ which has the binder for the continuation built into the
operator and where the invocation of the continuation is explicit, similar to
$\mathbf{label}/\mathbf{goto}$. Calling this variation
$\mathbf{label}_{\mathcal{C}}$, we obtain the following translation

$\displaystyle\llbracket\mathbf{label}_{\mathcal{C}}\ \alpha\
\\{t\\}\rrbracket$ $\displaystyle\coloneq\mu\alpha.\langle\llbracket
t\rrbracket\mid\bigstar\rangle$

Here the duality to $\mathbf{let}$-bindings is evident again. The translation
for $\mathcal{C}$ itself is then obtained in the same way as for
$\mathtt{call/cc}$

$\displaystyle\llbracket\mathcal{C}~{}f\rrbracket$
$\displaystyle\coloneq\mu\alpha.\langle\llbracket
f\rrbracket\mid\mathtt{ap}(\mathbf{cocase}\
\\{\mathtt{ap}(x,\beta)\Rightarrow\langle
x\mid\alpha\rangle\\},\bigstar)\rangle$

###  5.4. The Case-of-Case Transformation

One important transformation in functional compilers is the case-of-case
transformation. Maurer et al. (2017) give the following example of this
transformation. The term

$\mathbf{if}\ (\mathbf{if}\ e_{1}\ \mathbf{then}\ e_{2}\ \mathbf{else}\
e_{3})\ \mathbf{then}\ e_{4}\ \mathbf{else}\ e_{5}$

can be replaced by the term

$\mathbf{if}\ e_{1}\ \mathbf{then}\ (\mathbf{if}\ e_{2}\ \mathbf{then}\ e_{4}\
\mathbf{else}\ e_{5})\ \mathbf{else}\ (\mathbf{if}\ e_{3}\ \mathbf{then}\
e_{4}\ \mathbf{else}\ e_{5}).$

Logicians call these kinds of transformations _commutative conversions_ , and
they play an important role in the study of the sequent calculus. But as
Maurer et al. (2017) show, they are also important for compiler writers who
want to generate efficient code.

In the $\lambda\mu\tilde{\mu}$-calculus, commuting conversions don’t have to
be implemented as a special compiler pass. They fall out _for free_ as a
special instance of $\mu$-reductions! Let us illustrate this point by
translating Maurer et al.’s example into the $\lambda\mu\tilde{\mu}$-calculus.
First, let us translate the two examples using pattern-matching syntax:

$\displaystyle\mathbf{case}\ (\mathbf{case}\ e_{1}\ \mathbf{of}\
\\{\mathtt{T}\Rightarrow e_{2};\mathtt{F}\Rightarrow e_{3}\\})\ \mathbf{of}\
\\{\mathtt{T}\Rightarrow e_{4};\mathtt{F}\Rightarrow e_{5}\\}$
$\displaystyle\mathbf{case}\ e_{1}\ \mathbf{of}\
\\{\mathtt{T}\Rightarrow\mathbf{case}\ e_{2}\ \mathbf{of}\
\\{\mathtt{T}\Rightarrow e_{4};\mathtt{F}\Rightarrow
e_{5}\\};\mathtt{F}\Rightarrow\mathbf{case}\ e_{3}\ \mathbf{of}\
\\{\mathtt{T}\Rightarrow e_{4};\mathtt{F}\Rightarrow e_{5}\\}\\}$

Let us now translate these two terms into the
$\lambda\mu\tilde{\mu}$-calculus:

$\displaystyle\mu\alpha.\underline{\langle\mu\beta.\langle\llbracket
e_{1}\rrbracket\mid\mathbf{case}\ \\{\mathtt{T}\Rightarrow\langle\llbracket
e_{2}\rrbracket\mid\beta\rangle;\mathtt{F}\Rightarrow\langle
e_{3}\mid\beta\rangle\\}\rangle\mid\mathbf{case}\
\\{\mathtt{T}\Rightarrow\langle\llbracket
e_{4}\rrbracket\mid\alpha\rangle,\mathtt{F}\Rightarrow\langle\llbracket
e_{5}\rrbracket\mid\alpha\rangle\\}\rangle}$
$\displaystyle\mu\alpha.\langle\llbracket e_{1}\rrbracket|\mathbf{case}\ \\{$
$\displaystyle\qquad\mathtt{T}\Rightarrow\underline{\langle\mu\beta.\langle\llbracket
e_{2}\rrbracket\mid\mathbf{case}\ \\{\mathtt{T}\Rightarrow\langle\llbracket
e_{4}\rrbracket\mid\beta\rangle,\mathtt{F}\Rightarrow\langle\llbracket
e_{5}\rrbracket\mid\beta\rangle\\}\rangle\mid\alpha\rangle}$
$\displaystyle\qquad\mathtt{F}\Rightarrow\underline{\langle\mu\beta.\langle\llbracket
e_{3}\rrbracket\mid\mathbf{case}\ \\{\mathtt{T}\Rightarrow\langle\llbracket
e_{4}\rrbracket\mid\beta\rangle,\mathtt{F}\Rightarrow\langle\llbracket
e_{5}\rrbracket\mid\beta\rangle\\}\rangle\mid\alpha\rangle}\\}\rangle$

We can see that just by reducing all of the underlined redexes we reduce both
of these examples to the same term.

###  5.5. Direct and Indirect Consumers

As mentioned in the introduction, a natural competitor of sequent calculus as
an intermediate representation is continuation-passing style (CPS). In CPS,
reified evaluation contexts are represented by functions. This makes the
resulting types of programs in CPS arguably harder to understand. There is,
however, another advantage of sequent calculus over CPS as described by Downen
et al. (2016). The first-class representation of consumers in sequent calculus
allows us to distinguish between two different kinds of consumers: direct
consumers, i.e., destructors, and indirect consumers. In particular, this
allows to chain direct consumers in Core in a similar way as in Fun.

Suppose we have a codata type with destructors $\mathtt{get}$ and
$\mathtt{set}$ for getting and setting the value of a reference. Now consider
the following chain of destructor calls on a reference $r$ in Fun

$\displaystyle r.\mathtt{set}(3).\mathtt{set}(4).\mathtt{get}()$

A compiler could use a user-defined custom rewrite rule for rewriting two
subsequent calls to $\mathtt{set}$ into only the second call. In Core the
above example looks as follows:

$\displaystyle\mu\alpha.\langle
r\mid\mathtt{set}(3;\mathtt{set}(4;\mathtt{get}(\alpha)\rangle$

We still can immediately see the direct chaining of destructors and thus apply
essentially the same rewrite rule. In CPS, however, the example would rather
become

$\displaystyle\lambda k.\ r.\mathtt{set}(3;\lambda s.\
s.\mathtt{set}(4;\lambda t.\ t.\mathtt{get}(k)))$

The chaining of the destructors becomes obfuscated by the indirections
introduced by representing the continuations for each destructor as a
function. To apply the custom rewrite rule mentioned above, it is necessary to
see through the lambdas, i.e. the custom rewrite rule has to be transformed to
be applicable.

###  5.6. Call-By-Value, Call-By-Name and Eta-Laws

In Section 2.2 we already pointed out the existence of statements
$\langle\mu\alpha.s_{1}\mid\tilde{\mu}x.s_{2}\rangle$ which are called
_critical pairs_ because they can a priori be reduced to either
$s_{1}[\tilde{\mu}x.s_{2}/\alpha]$ or $s_{2}[\mu\alpha.s_{1}/x]$. These
critical pairs were already discussed by Curien and Herbelin (2000) when they
introduced the $\lambda\mu\tilde{\mu}$-calculus. One solution is to pick an
evaluation order, either call-by-value (cbv) or call-by-name (cbn), that
determines to which of the two statements we should evaluate, and in this
paper we chose to always use the call-by-value evaluation order. The
difference between these two choices has also been discussed by Wadler (2003).
Note that this freedom for the evaluation strategy is another advantage of
sequent calculus over continuation-passing style, as the latter always fixes
an evaluation strategy.

Which evaluation order we choose has an important consequence for the
optimizations we are allowed to perform in the compiler. If we choose call-by-
value, then we are not allowed to use all $\eta$-equalities for codata types,
and if we use call-by-name, then we are not allowed to use all
$\eta$-equalities for data types. Let us illustrate the problem in the case of
codata types with the following example:

$\langle\mathbf{cocase}\
\\{\mathtt{ap}(x;\alpha)\Rightarrow\langle\mu\beta.s_{1}\mid\mathtt{ap}(x;\alpha)\rangle\\}\mid\tilde{\mu}x.s_{2}\rangle\equiv_{\eta}\langle\mu\beta.s_{1}\mid\tilde{\mu}x.s_{2}\rangle$

We assume that $x$ and $\alpha$ do not appear free in $s_{1}$. The
$\eta$-transformation is just the ordinary $\eta$-law for functions but
applied to the representation of functions as codata types. The statement on
the left-hand side reduces the $\tilde{\mu}$ first under both call-by-value
and call-by-name evaluation order, i.e.

$\langle\mathbf{cocase}\
\\{\mathtt{ap}(x;\alpha)\Rightarrow\langle\mu\beta.s_{1}\mid\mathtt{ap}(x;\alpha)\rangle\\}\mid\tilde{\mu}x.s_{2}\rangle\begin{array}[]{l
r}\triangleright_{\text{cbv}}&s_{2}[\mathbf{cocase}\ \\{\dots\\}/x]\\\
\triangleright_{\text{cbn}}&s_{2}[\mathbf{cocase}\ \\{\dots\\}/x]\end{array}$

The right-hand side of the $\eta$-equality, however, reduces the $\mu$ first
under call-by-value evaluation order, i.e.

$\langle\mu\beta.s_{1}\mid\tilde{\mu}x.s_{2}\rangle\begin{array}[]{l
r}\triangleright_{\text{cbv}}&s_{1}[\tilde{\mu}x.s_{2}/\beta]\\\
\triangleright_{\text{cbn}}&s_{2}[\mu\beta.s_{1}/x]\end{array}$

Therefore, the $\eta$-equality is only valid under call-by-name evaluation
order. This example shows that the validity of applying this $\eta$-rule as an
optimization depends on whether the language uses call-by-value or call-by-
name. If we instead used a data type such as $\mathtt{Pair}$, a similar
$\eta$-reduction would only give the same result as the original statement
when using call-by-value.

###  5.7. Linear Logic and the Duality of Exceptions

We have introduced the data type $\mathtt{Pair}(\sigma,\tau)$ and the codata
type $\mathtt{LPair}(\sigma,\tau)$ as two different ways to formalize tuples.
The data type $\mathtt{Pair}(\sigma,\tau)$ is defined by the constructor
$\mathtt{Tup}$ whose arguments are evaluated eagerly, so this type corresponds
to strict tuples in languages like ML or OCaml. The codata type
$\mathtt{LPair}(\sigma,\tau)$ is a lazy pair which is defined by its two
projections fst and snd, and only when we invoke the first or second
projection do we start to compute its contents. This is closer to how tuples
behave in a lazy language like Haskell.

Linear logic (Girard, 1987; Wadler, 1990) adds another difference to these
types. In linear logic we consider arguments as resources which cannot be
arbitrarily duplicated or discarded; every argument to a function has to be
used exactly once. If we follow this stricter discipline, then we have to
distinguish between two different types of pairs: In order to use a pair
$\sigma\otimes\tau$ (pronounced “times” or “tensor”), we have to use both the
$\sigma$ and the $\tau$, but if we want to use a pair $\sigma\with\tau$
(pronounced “with”), we must choose to either use the $\sigma$ or the $\tau$.
It is now easy to see that the type $\sigma\otimes\tau$ from linear logic
corresponds to the data type $\mathtt{Pair}(\sigma,\tau)$, since when we
pattern match on this type we get _two_ variables in the context, one for
$\sigma$ and one for $\tau$. The type $\sigma\with\tau$ similarly corresponds
to the type $\mathtt{LPair}(\sigma,\tau)$ which we use by invoking either the
first or the second projection, consuming the whole pair.

In addition to these two different kinds of conjunction, we also have two
different kinds of disjunction. These two disjunctions are written
$\sigma\oplus\tau$ (pronounced “plus”) and $\sigma\parr\tau$ (pronounced
“par”) and correspond to two different ways to handle errors in programming
languages. Their typing rules in Core are:

$\Gamma\vdash t:^{\text{\tiny prd}}\sigma$
$\Gamma\vdash\text{Inl}(t):^{\text{\tiny prd}}\sigma\oplus\tau$

$\Gamma\vdash t:^{\text{\tiny prd}}\tau$
$\Gamma\vdash\text{Inr}(t):^{\text{\tiny prd}}\sigma\oplus\tau$

$\Gamma,x:^{\text{\tiny prd}}\sigma\vdash s_{1}$ $\Gamma,y:^{\text{\tiny
prd}}\tau\vdash s_{2}$ $\Gamma\vdash\mathbf{case}\ \\{\text{Inl}(x)\Rightarrow
s_{1},\text{Inr}(y)\Rightarrow s_{2}\\}:^{\text{\tiny cns}}\sigma\oplus\tau$

$\Gamma\vdash c_{1}:^{\text{\tiny cns}}\sigma$ $\Gamma\vdash
c_{2}:^{\text{\tiny cns}}\tau$ $\Gamma\vdash\text{Par}(c1,c2):^{\text{\tiny
cns}}\sigma\parr\tau$

$\Gamma,\alpha:^{\text{\tiny cns}}\sigma,\beta:^{\text{\tiny cns}}\tau\vdash
s$ $\Gamma\vdash\mathbf{cocase}\ \\{\text{Par}(\alpha,\beta)\Rightarrow
s\\}:^{\text{\tiny prd}}\sigma\parr\tau$

Languages like Rust and Haskell use $\sigma\oplus\tau$ for error handling,
which corresponds to the “Either” and “Result” types in those languages. This
corresponds to the calling convention that the function returns a tagged
result which indicates whether an error has occurred or not, and the caller of
the function has to check this tag. The type $\sigma\parr\tau$ behaves
differently: A function which returns a value of type $\sigma\parr\tau$ has to
be called with two continuations, one for the possibility that the function
returns successfully and one for the possibility that the function throws an
error. And the function itself decides which continuation to call, so there is
no overhead for checking the result of a function call. This is quite similar
to how some functions in Javascript are called with an “onSuccess”
continuation and an “onFailure” continuation and different to the exception
model of, e.g., Java, where the exception handler is dynamically scoped
instead of lexically passed as an argument. This duality between the two
different ways of handling exceptions can be seen most clearly in the sequent
calculus; more details on this duality can be found in section 3.4 of
(Spiwack, 2014) or in section 7.1 of (Ostermann et al., 2022).

##  6\. Related Work

The central ideas of the calculi that we have presented in this pearl are not
novel: the $\lambda\mu\tilde{\mu}$-calculus is by now over 20 years old. We
chose a variant of this calculus that can be used as a starting point to
explore all the variants that have been described in the literature. This
related work section is therefore intended to provide suggestions for further
reading and the chance to dive deeper into specific topics that we have only
touched upon.

###  6.1. The Sequent Calculus

The basis of our language Core is a term assignment system for the sequent
calculus, an alternative logical system to natural deduction. The sequent
calculus was originally introduced by Gentzen in the articles Gentzen (1935a,
b, 1969). For a more thorough introduction to the sequent calculus as a
logical system, we can recommend the books by Negri and Von Plato (2001) and
Troelstra and Schwichtenberg (2000) which introduce the sequent calculus and
show how it differs from the natural deduction systems that are more commonly
taught.

###  6.2. Term Assignment for the Sequent Calculus

The original article which introduced the $\lambda\mu\tilde{\mu}$-calculus as
a term assignment system for the sequent calculus was by Curien and Herbelin
(2000). Before we list some of the other articles, we should preface them with
the following remark on notation:

######  Remark 1 (Alternative Notation).

Our notation for producers, consumers and statements follows the established
conventions in the literature. However, we diverge in the way that we write
typing judgments from the example of Curien and Herbelin (2000) which is
followed by most other authors. We use one typing context $\Gamma$ which binds
both variables $x:^{\text{\tiny prd}}\tau$ and covariables
$\alpha:^{\text{\tiny cns}}\tau$, whereas Curien and Herbelin (2000) use two
contexts; a context $\Gamma$ which contains bindings for all variables and a
context $\Delta$ which contains the bindings for all covariables. The
following table summarizes the difference between their notation and the
notation used in our paper.

Judgment Form | Our notation | Curien and Herbelin (2000)
---|---|---
Typing Producers | $\Gamma\vdash p:^{\text{\tiny prd}}\tau$ | $\Gamma\vdash p:\tau\mid\Delta$
Typing Consumers | $\Gamma\vdash c:^{\text{\tiny cns}}\tau$ | $\Gamma\mid c:\tau\vdash\Delta$
Typing Statements | $\Gamma\vdash s$ | $s:(\Gamma\vdash\Delta)$

The reasons for this divergence are easily explained. The notation of Curien
and Herbelin (2000) with its two contexts $\Gamma$ and $\Delta$ perfectly
illustrates the correspondence to the sequent calculus which operates with
sequents $\Gamma\vdash\Delta$ which contain multiple formulas on the left- and
right-hand side of the turnstile. This close correspondence to the sequent
calculus is less important for us. We found that splitting the context in this
way often makes it more difficult to write down rules in their full generality
when we extend the language with other features. Features which introduce a
dependency of later bindings on earlier bindings within a typing context, for
example when we add parametric polymorphism, don’t fit easily into the format
of Curien and Herbelin (2000).

With these remarks out of the way, we can recommend the articles by Zeilberger
(2008), Downen and Ariola (2014, 2018b, 2020), Munch-Maccagnoni (2009) and
Spiwack (2014) which were very helpful to us when we learned about the
$\lambda\mu\tilde{\mu}$-calculus.

###  6.3. Codata Types

Codata types were originally invented by Hagino (1989). They had the most
success in proof assistants such as Agda where they help circumvent certain
technical problems that arise when we try to model coinductive types.
Copattern matching as a way to create producers of codata types was
popularized by Abel et al. (2013), although the basic idea of the concept had
been around before that, see, e.g., (Zeilberger, 2008). But probably the best
starting point to learn more about codata types is an article written by
Downen et al. (2019).

###  6.4. Control Operators and Classical Logic

The $\mathbf{label}/\mathbf{goto}$ construct that we are using in Fun is an
example of a control operator, of which Landin’s operator J (Thielecke, 1998;
Felleisen, 1987; Landin, 1965) likely is the oldest. Their translation into
Core uses $\mu$-abstractions, which are also a form of control operator that
was originally introduced by Parigot (1992) before it became a part of the
$\lambda\mu\tilde{\mu}$-calculus of Curien and Herbelin (2000). Control
operators have an important relationship to classical logic via the Curry-
Howard isomorphism. This relationship was discovered by Griffin (1989); a more
thorough introduction can be found in Sørensen and Urzyczyn (2006).

###  6.5. Different Evaluation Orders

We have already talked about the evaluation strategies call-by-value and call-
by-name, and how their difference can be explained by different choices of how
a critical pair should be evaluated. This duality between call-by-value and
call-by-name has already been observed by Filinski (1989) and has been
explored in more detail by Wadler (2003, 2005). We have also seen in Section
5.6 how $\eta$-reduction only works with data types in call-by-value and with
codata types in call-by-name. A lot of people therefore conclude that the
choice of an evaluation order should maybe not be a global decision, but
should instead depend on the type. This approach requires tracking the
polarity of types and providing additional shift connectives which help
mediate between the different evaluation orders; the article by Downen and
Ariola (2018a) is a good entry point for pursuing these kinds of questions
which are discussed in detail in (Zeilberger, 2009) and (Munch-Maccagnoni,
2013). A well-known example of mixing evaluation orders is the call-by-push-
value paradigm (Levy, 1999) which distinguishes value types and computation
types and subsumes both call-by-value and call-by-name.

##  7\. Conclusion

In this functional pearl, we have presented the
$\lambda\mu\tilde{\mu}$-calculus in the way we introduce it to our colleagues
and students on the whiteboard; by compiling small examples of functional
programs. We think this is a better way to introduce programming-language
enthusiasts and compiler writers to the $\lambda\mu\tilde{\mu}$-calculus,
since it doesn’t require prior knowledge of the sequent calculus. We have also
shown _why_ we are excited about this calculus, by giving examples of how it
allows us to express aspects like strict vs. lazy evaluation or compiler
optimizations like case-of-case in an extremely clear way. We want to share
our enthusiasm for the sequent calculus and languages built on it with more
people, and with this pearl, we hope that others will start to write their own
little compilers to the sequent calculus and explore the exciting
possibilities it offers.

## Data Availability Statement

This paper is accompanied by an implementation in Haskell. Upon acceptance and
publication of this article, the implementation will be made available
permanently using Zenodo.

## Acknowledgments

We would like to thank the anonymous reviewers and Paul Downen for their
feedback which helped us greatly in improving the final presentation of the
paper.

##  Appendix A The Relationship to the Sequent Calculus

In the main part of the paper we introduced the
$\lambda\mu\tilde{\mu}$-calculus without any references to the sequent
calculus, because we think it is not essential to understand the latter in
order to understand the former. In this appendix, we provide the details which
help make the connection between the logical calculus and the term system
clear. We only discuss a very simple sequent calculus which contains two
logical connectives: the two conjunctions $A\otimes B$ and $A\with B$ which
correspond to the strict and lazy pairs that we have seen in Core. We use $X$
for propositional variables.

$A,B\Coloneqq X\mid A\otimes B\mid A\with B$

In the (classical) sequent calculus both the premisses and the conclusion of a
derivation rule consist of _sequents_ $\Gamma\vdash\Delta$. Both $\Gamma$ and
$\Delta$ are multisets of formulas; that is, it is important how often a
formula occurs on the left or the right, but not in which order the formulas
occur. In the sequent calculus, we only have _introduction rules_. This means
that the logically complex formula $A\otimes B$ or $A\with B$ only occurs in
the conclusion of the rules that define it, and not in one of the premises.
Every connective comes with a set of rules which introduce the connective on
the left and the right of the turnstile. In our case, the rules look like
this:

Axiom $A\vdash A$

$\Gamma_{1}\vdash\Delta_{1},A$ $A,\Gamma_{2}\vdash\Delta_{2}$ Cut
$\Gamma_{1},\Gamma_{2}\vdash\Delta_{1},\Delta_{2}$

$\Gamma,A_{1},A_{2}\vdash\Delta$ $\otimes$-L $\Gamma,A_{1}\otimes
A_{2}\vdash\Delta$

$\Gamma_{1}\vdash A_{1},\Delta_{1}$ $\Gamma_{2}\vdash A_{2},\Delta_{2}$
$\otimes$-R $\Gamma_{1},\Gamma_{2}\vdash A_{1}\otimes
A_{2},\Delta_{1},\Delta_{2}$

$\Gamma,A_{1}\vdash\Delta$ $\with$-L1 $\Gamma,A_{1}\with A_{2}\vdash\Delta$

$\Gamma,A_{2}\vdash\Delta$ $\with$-L2 $\Gamma,A_{1}\with A_{2}\vdash\Delta$

$\Gamma\vdash A_{1},\Delta$ $\Gamma\vdash A_{2},\Delta$ $\with$-R2
$\Gamma\vdash A_{1}\with A_{2},\Delta$

The rule Cut is the only rule which destroys the so-called _subformula
property_. This property says that every formula which occurs anywhere in a
derivation is a subformula of a formula occurring in the conclusion of the
derivation. Proof theorists therefore try to show that we can _eliminate the
cuts_ ; if every sequent which can be derived using the Cut rule can also be
derived without using it, we say that the calculus enjoys the _cut-elimination
property_. The Curry-Howard correspondence for the sequent calculus relates
this cut-elimination procedure to the computations that we have seen in the
paper.

The first step from the sequent calculus towards the
$\lambda\mu\tilde{\mu}$-calculus consists in marking at most one of the
formulas in each of the sequents as _active_. We mark a formula as active by
enclosing it in a pair of brackets. This yields two versions of the rule
Axiom, one where we mark the formula on the left and one where we mark the
formula on the right. If we want to translate every derivation using the
original rules to a derivation in the new variant we also have to add special
rules which _activate_ and _deactivate_ formulas both on the left and on the
right. This yields the following new set of rules:

Axiom-L $[A]\vdash A$

Axiom-R $A\vdash[A]$

$\Gamma_{1}\vdash\Delta_{1},[A]$ $[A],\Gamma_{2}\vdash\Delta_{2}$ Cut
$\Gamma_{1},\Gamma_{2}\vdash\Delta_{1},\Delta_{2}$

$\Gamma_{,}A_{1},A_{2}\vdash\Delta$ $\otimes$-L $\Gamma_{,}[A_{1}\otimes
A_{2}]\vdash\Delta$

$\Gamma_{1}\vdash[A_{1}],\Delta_{1}$ $\Gamma_{2}\vdash[A_{2}],\Delta_{2}$
$\otimes$-R $\Gamma_{1},\Gamma_{2}\vdash[A_{1}\otimes
A_{2}],\Delta_{1},\Delta_{2}$

$\Gamma,[A_{1}]\vdash\Delta$ $\with$-L1 $\Gamma,[A_{1}\with
A_{2}]\vdash\Delta$

$\Gamma,[A_{2}]\vdash\Delta$ $\with$-L2 $\Gamma,[A_{1}\with
A_{2}]\vdash\Delta$

$\Gamma\vdash A_{1},\Delta$ $\Gamma\vdash A_{2},\Delta$ $\with$-R2
$\Gamma\vdash[A_{1}\with A_{2}],\Delta$

$\Gamma,A\vdash\Delta$ Act-L $\Gamma,[A]\vdash\Delta$

$\Gamma,[A]\vdash\Delta$ Deact-L $\Gamma,A\vdash\Delta$

$\Gamma\vdash A,\Delta$ Act-R $\Gamma\vdash[A],\Delta$

$\Gamma\vdash[A],\Delta$ Deact-R $\Gamma\vdash A,\Delta$

We can now begin to assign terms to derivations in this calculus by
associating every non-active formula $A$ in the _left_ side of the turnstile
with a producer variable $x:^{\text{\tiny prd}}A$, and every non-active
formula $B$ on the _right_ side of the turnstile with a consumer variable
$\alpha:^{\text{\tiny cns}}B$. As discussed in Section 6.2 we write both
producer and consumer variables in a joint context $\Gamma$ on the left-hand
side of typing rules. We have to distinguish three different sequents,
depending on whether a formula is active, and if so, on which side the active
formula occurs. If there is no active formula, then we assign a _statement_ to
the sequent, if the formula on the right is active, we assign a _producer_ ,
and if the formula on the left is active, we assign a _consumer_. For most
rules the correspondence is clear: The rule Axiom-R corresponds to the typing
rule Var1 (and Axiom-L to Var2). The rule Tup corresponds to the rule
$\otimes$-R, and Case-Pair to $\otimes$-L. The rules Fst and Snd correspond to
the rules $\with$-L1 and $\with$-L2, and Cocase-LPair to $\with$-R. The
activation rules correspond to the rules $\mu$ and $\tilde{\mu}$, and
deactivation can be expressed as a cut with a variable.

##  Appendix B Typing Rules for Fun

Given a term $t$, an environment $\Gamma$ and a program $P$, if $t$ has type
$\tau$ in environment $\Gamma$ and program $P$, we write
$\Gamma\vdash_{P}t:\tau$. As $P$ is only used for typing calls to top-level
definitions (rule Call), we usually leave it implicit in the typing rules. To
make sure programs $P$ are well-formed, we have additional checking rules for
programs $\emptyset$-ok and P-Ok. If a program is well-formed, we write
$\vdash P\textsc{ Ok}$.
$x:^{\text{\tiny prd}}\tau\in\Gamma$ Var $\Gamma\vdash x:\tau$
$x:\tau\in\Gamma$ Lit $\Gamma\vdash\ulcorner n\urcorner:\mathbf{Int}$
$\Gamma\vdash t_{1}:\mathbf{Int}\quad\Gamma\vdash t_{2}:\mathbf{Int}$ Op
$\Gamma\vdash t_{1}\odot t_{2}:\mathbf{Int}$ $\Gamma\vdash n:\mathbf{Int}$
$\Gamma\vdash t_{1}:\tau$ $\Gamma\vdash t_{2}:\tau$ Ifz
$\Gamma\vdash\mathbf{ifz}(n,t_{1},t_{2}):\tau$ $\Gamma\vdash t_{1}:\tau_{1}$
$\Gamma,x:^{\text{\tiny prd}}\tau_{1}\vdash t_{2}:\tau_{2}$ Let
$\Gamma\vdash\mathbf{let}\ x=t_{1}\ \mathbf{in}\ t_{2}:\tau_{2}$
$\mathbf{def}\ f(\overline{x_{i}:^{\text{\tiny
prd}}\tau_{i}};\overline{\alpha_{j}:^{\text{\tiny cns}}\tau_{j}}):\tau\in P$
$\overline{\Gamma\vdash t_{i}:\tau_{i}}$
$\overline{\Gamma\vdash\alpha_{j}:^{\text{\tiny cns}}\tau_{j}}$ Call
$\Gamma\vdash_{P}f(\overline{t_{i}};\overline{\alpha_{j}}):\tau$ $\Gamma\vdash
t:\mathtt{List}(\tau^{\prime})$ $\Gamma\vdash t_{1}:\tau$
$\Gamma,y:^{\text{\tiny prd}}\tau^{\prime},z:^{\text{\tiny
prd}}\mathtt{List}(\tau^{\prime})\vdash t_{2}:\tau$ Case-List
$\Gamma\vdash\mathbf{case}\ t\ \mathbf{of}\ \\{\mathtt{Nil}\Rightarrow
t_{1},\mathtt{Cons}(y,z)\Rightarrow t_{2}\\}:\tau$ $\Gamma\vdash t_{1}:\tau$
$\Gamma\vdash t_{2}:\mathtt{List}(\tau)$ Cons
$\Gamma\vdash\mathtt{Cons}(t_{1},t_{2}):\mathtt{List}(\tau)$ $\Gamma\vdash
t_{1}:\tau$ Nil $\Gamma\vdash\mathtt{Nil}:\mathtt{List}(\tau)$ $\Gamma\vdash
t:\mathtt{Pair}(\tau_{1},\tau_{2})\quad\Gamma,x:^{\text{\tiny
prd}}\tau_{1},y:^{\text{\tiny prd}}\tau_{2}\vdash t:\tau$ Case-Pair
$\Gamma\vdash\mathbf{case}\ t\ \mathbf{of}\ \\{\mathtt{Tup}(x,y)\Rightarrow
t\\}:\tau$ $\Gamma\vdash t_{1}:\tau_{1}\quad\Gamma\vdash t_{2}:\tau_{2}$ Tup
$\Gamma\vdash\mathtt{Tup}(t_{1},t_{2}):\mathtt{Pair}(\tau_{1},\tau_{2})$
$\Gamma\vdash t:\mathtt{Stream}(\tau)$ Hd $\Gamma\vdash t.\mathtt{hd}:\tau$
$\Gamma\vdash t:\mathtt{Stream}(\tau)$ Tl $\Gamma\vdash
t.\mathtt{tl}:\mathtt{Stream}(\tau)$ $\Gamma\vdash t_{1}:\tau$ $\Gamma\vdash
t_{2}:\mathtt{Stream}(\tau)$ Stream $\Gamma\vdash\mathbf{cocase}\
\\{\mathtt{hd}\Rightarrow t_{1},\mathtt{tl}\Rightarrow
t_{2}\\}:\mathtt{Stream}(\tau)$ $\Gamma\vdash
t:\mathtt{LPair}(\tau_{1},\tau_{2})$ fst $\Gamma\vdash
t.\mathtt{fst}:\tau_{1}$ $\Gamma\vdash t:\mathtt{LPair}(\tau_{1},\tau_{2})$
snd $\Gamma\vdash t.\mathtt{snd}:\tau_{2}$ $\Gamma\vdash t_{1}:\tau_{1}$
$\Gamma\vdash t_{2}:\tau_{2}$ LPair $\Gamma\vdash\mathbf{cocase}\
\\{\mathtt{fst}\Rightarrow t_{1},\mathtt{snd}\Rightarrow
t_{2}\\}:\mathtt{LPair}(\tau_{1},\tau_{2})$ $\Gamma\vdash
t_{1}:\tau_{1}\rightarrow\tau_{2}\quad\Gamma\vdash t_{2}:\tau_{1}$ App
$\Gamma\vdash t_{1}\ t_{2}:\tau_{2}$ $\Gamma,x:^{\text{\tiny
prd}}\tau_{1}\vdash t:\tau_{2}$ Lam $\Gamma\vdash\lambda
x.t:\tau_{1}\rightarrow\tau_{2}$ $\Gamma\vdash t:\tau$ $\alpha:^{\text{\tiny
cns}}\tau\in\Gamma$ Goto $\Gamma\vdash\mathbf{goto}(t;\alpha):\tau^{\prime}$
$\Gamma,\alpha:^{\text{\tiny cns}}\tau\vdash t:\tau$ Label
$\Gamma\vdash\mathbf{label}\ \alpha\ \\{t\\}:\tau$

To check a program, we start with the empty program, which we know is well-
formed (Wf-Empty), and then add one definition at a time. A definition is then
well-typed if there are types $\overline{\tau_{i}}$ and $\overline{\tau_{j}}$
for its arguments such that its body is well-typed. Because we explicitly
allow recursive definitions, the body $t$ might contain the name f as well.
Thus, while we typecheck $t$, we add the definition of f to the program and
assume it is well-typed. After finding
$\overline{\tau_{i}},\overline{\tau_{j}}$ and $\tau$, these are added to the
program as well, that is, well-formed programs contain type annotations while
definitions on their own do not. This way, these types can be used while
checking types of calls (in rule Call).
Wf-Empty $\vdash\emptyset\ \textsc{Ok}$ $\vdash P\ \textsc{Ok}$
$\overline{x:^{\text{\tiny prd}}\tau_{i}},\overline{\alpha:^{\text{\tiny
cns}}\tau_{j}}\vdash_{P,\mathbf{def}\
\text{f}(\overline{x_{i}:\tau_{i}},\overline{\alpha_{j}:^{\text{\tiny
cns}}\tau_{j}}):\tau\coloneq t}t:\tau$ Wf-Cons $\vdash P,\mathbf{def}\
\text{f}(\overline{x_{i}:\tau_{i}},\overline{\alpha_{j}:^{\text{\tiny
cns}}\tau_{j}}):\tau\coloneq t\ \textsc{Ok}$

##  Appendix C Operational Semantics of $\mathbf{label}/\mathbf{goto}$

The full operational semantics for the $\mathbf{label}/\mathbf{goto}$
construct is in essence the same as for $\mathtt{let/cc}$. To make it precise,
we promote evaluation contexts to runtime values.

We first repeat 3.1 of evaluation contexts with one change: $\mathbf{label}\
\alpha\ \\{E\\}$ is not an evaluation context. We reduce a $\mathbf{label}$ as
soon as it comes into evaluation position.

$\begin{array}[]{rcl}E&\Coloneqq&\square\mid E\odot t\mid\mathfrak{t}\odot
E\mid\mathbf{ifz}(E,t,t)\mid\mathbf{let}\ x=E\ \mathbf{in}\ t\mid
f(\overline{\mathfrak{t}},E,\overline{t})\mid
K(\overline{\mathfrak{t}},E,\overline{t})\\\ &\mid&\mathbf{case}\ E\
\mathbf{of}\ \\{\overline{K(\overline{x})\Rightarrow t}\\}\mid E\
t\mid\mathfrak{t}\ E\mid
E.D(\overline{t})\mid\mathfrak{t}.D(\overline{\mathfrak{t}},E,\overline{t})\mid\mathbf{goto}(E;\alpha)\end{array}$

Now we add them as another form of value

$\mathfrak{t}\Coloneqq\ldots\mid E$

Note that these values only exist at runtime, that is, they cannot appear in
expressions before evaluation has started. They are typed as consumers, which
means that they are the only values with a consumer type. This makes sure that
we can substitute them for covariables. Their typing can be captured by the
following rule.

$x:^{\text{\tiny prd}}\tau\vdash E[x]:\tau_{0}$ Ctx $\vdash E:^{\text{\tiny
cns}}\tau$

The rule means that if the hole of a context $E$ expects an expression of type
$\tau$ to be plugged in, then we have $E:^{\text{\tiny cns}}\tau$.

Now we can give the evaluation rules for $\mathbf{label}$ and $\mathbf{goto}$:

$E[\mathbf{label}\ \alpha\ \\{t\\}]\triangleright E[t[E/\alpha]]\qquad\qquad
E^{\prime}[\mathbf{goto}(\mathfrak{t};E)]\triangleright E[\mathfrak{t}]$

In the rule for $\mathbf{label}$, the surrounding evaluation context $E$ is
reified as a value and then substituted for the covariable $\alpha$ in the
body $t$. Note that $E$ is not removed, i.e., evaluation continues in this
context. In particular, if $\alpha$ does not occur free in $t$, then the
$\mathbf{label}$ is effectively a no-op. We can also see that the types are
correct: If $t$ has type $\tau$, then so does $\mathbf{label}\ \alpha\
\\{t\\}$ and consequently we have $E:^{\text{\tiny cns}}\tau$ which is the
same type as that of $\alpha$. In the rule for $\mathbf{goto}$ the covariable
must have already been replaced by an evaluation context, which is ensured if
the evaluated term was closed and well-typed, because the only way to
introduce a covariable is through a $\mathbf{label}$. The evaluation step then
removes and discards the surrounding context $E^{\prime}$ and continues
evaluation by plugging the value $\mathfrak{t}$ into the previously reified
context $E$. Note that $E^{\prime}$ cannot contain $\mathbf{label}$s, as they
are not evaluation contexts. This ensures that there is no risk of removing a
binder for a free variable in $\mathfrak{t}$. Together these two rules also
allow us to simulate the approximate rule from Section 3.1:

$E[\mathbf{label}\ \alpha\
\\{E^{\prime}[\mathbf{goto}(\mathfrak{t};\alpha)]\\}]\triangleright
E[E^{\prime}[\mathbf{goto}(\mathfrak{t};E)]]\triangleright E[\mathfrak{t}]$

The rule for $\mathbf{goto}$ also is the reason why the theorem of strong
preservation does not immediately hold (see the discussion in Section 4.3).
The problem is that from this rule and the given typing rules for Fun it is
not immediate that the evaluation contexts $E^{\prime}$ and $E$ yield a term
of the same type when filling their holes, so that the overall type of the
term may not be preserved. But this cannot actually happen, because all other
reduction rules preserve the overall type and hence all evaluation contexts
that are reified by the rule for $\mathbf{label}$ must yield a term of that
same overall type when their holes are filled. Therefore, also the rule for
$\mathbf{goto}$ is type-preserving. This can be made precise by explicitly
tracking the overall type in the type system (see, e.g., Section 6 in (Wright
and Felleisen, 1994)).

## References

  * (1)
  * Abel et al. (2013) Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013.  Copatterns: Programming Infinite Structures by Observations. In _Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Rome, Italy) _(POPL ’13)_. Association for Computing Machinery, New York, NY, USA, 27–38.  https://doi.org/10.1145/2480359.2429075
  * Andreoli (1992) Jean-Marc Andreoli. 1992\.  Logic Programming with Focusing Proofs in Linear Logic.  _Journal of Logic and Computation_ 2 (1992), 297–347.  Issue 3. https://doi.org/10.1093/logcom/2.3.297
  * Brachthäuser et al. (2020) Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020\.  Effects as capabilities: effect handlers and lightweight effect polymorphism.  _Proc. ACM Program. Lang._ 4, OOPSLA, Article 126 (nov 2020), 30 pages.  https://doi.org/10.1145/3428194
  * Cook (2009) William R. Cook. 2009\.  On Understanding Data Abstraction, Revisited. In _Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications: Onward! Essays_ (Orlando). Association for Computing Machinery, New York, NY, USA, 557–572.  https://doi.org/10.1145/1640089.1640133
  * Curien and Herbelin (2000) Pierre-Louis Curien and Hugo Herbelin. 2000.  The Duality of Computation. In _Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming_ _(ICFP ’00)_. Association for Computing Machinery, New York, NY, USA, 233–243.  https://doi.org/10.1145/357766.351262