fscd-term.tex

\documentclass[a4paper, 11pt,titlepage, openright, twoside]{report}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{silence}
\usepackage{amsmath,amsfonts,amssymb,amsthm}
\usepackage{mathtools}
\usepackage{enumitem}
\usepackage{newunicodechar}
\usepackage[margin=3cm,bindingoffset=1cm]{geometry}
\usepackage{stmaryrd}
\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n}
% https://tex.stackexchange.com/a/106719
\DeclareSymbolFont{sfletters}{OML}{cmbrm}{m}{it}
\DeclareMathSymbol{\slambda}{\mathord}{sfletters}{"15}
%https://tex.stackexchange.com/a/335857
\usepackage{microtype}
\usepackage[dvipsnames]{xcolor}
\usepackage{mathpartir}
\usepackage[style=alphabetic]{biblatex}
\usepackage{hyperref}
\usepackage{cleveref}
\usepackage{tikz}
\usepackage{listings}
\lstset{basicstyle= \footnotesize \ttfamily}
\lstset{language=ml}

\usepackage[nodisplayskipstretch]{setspace}
\setlength{\parskip}{0pt}

\addbibresource{refs.bib}


\title{\textbf{Normalization for algebraic effect handlers}}
\author{Wiktor Kuchta}

\date{29 czerwca 2022} %TODO

\usepackage{titling}

\renewcommand \maketitlehookb {
  \begin{center}\large
  Normalizacja dla handlerów efektów algebraicznych
  \end{center}
  \vfil
}

\renewcommand \maketitlehookc {
  \vfil
  \begin{center}
  \large Praca licencjacka \\[0.85em]
  \begin{tabular}[t]{rl}
  \textbf{Promotor:} & dr hab. Dariusz Biernacki
  \end{tabular}\end{center}
  \vfil\vfil\vfil\vfil
  \begin{center}Uniwersytet Wroc\l{}awski\\
  Wydzia\l{} Matematyki i Informatyki\\
  Instytut Informatyki
  \end{center}
}


\newunicodechar{λ}{\slambda}
\newcommand{\keyword}[1]{\textsf{\textup{#1}}}
\newcommand{\KwDo}{\keyword{do}}
\newcommand{\Do}{\KwDo\;}
\newcommand{\KwHandle}{\keyword{handle}}
\newcommand{\Handle}{\KwHandle\;}
\newcommand{\Lift}[1]{\boldsymbol{[}#1\boldsymbol{]}}
\newcommand{\subst}[2]{\{#1/#2\}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\K}{\mathcal{K}}
\renewcommand{\S}{\mathcal{S}}
\newcommand{\kT}{\mathsf{T}}
\newcommand{\kE}{\mathsf{E}}
\newcommand{\kR}{\mathsf{R}}
\newcommand{\Free}{\textrm{-}\mathrm{free}}
\newcommand{\Obs}{\mathrm{Obs}}
\newcommand{\N}{\mathbb{N}}
\DeclareMathOperator{\dom}{dom}
\newcommand{\+}{\enspace}

\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\newunicodechar{│}{\mid} % Digr vv
\newunicodechar{╱}{\mathbin{/}} % Digr FD
\newunicodechar{∷}{::} % Digr ::
\newunicodechar{□}{\square} % Digr OS
\newunicodechar{∅}{\emptyset} % Digr /0
\newunicodechar{α}{\alpha}
\newunicodechar{β}{\beta}
\newunicodechar{δ}{\delta} % Digr d*
\newunicodechar{ε}{\varepsilon}
\newunicodechar{γ}{\gamma} % Digr g*
\newunicodechar{ι}{\iota} % Digr i*
\newunicodechar{κ}{\kappa}
\newunicodechar{μ}{\mu}
\newunicodechar{ν}{\nu}
\newunicodechar{ρ}{\rho}
\newunicodechar{σ}{\sigma}
\newunicodechar{τ}{\tau}
\newunicodechar{η}{\eta} % Digr y*
\newunicodechar{Δ}{\Delta}
\newunicodechar{Γ}{\Gamma}
\newunicodechar{Ω}{\Omega} % digr W*
\newunicodechar{ℕ}{\N} % Digr NN 8469 nonstandard
\newunicodechar{⊆}{\subseteq} % Digr (_
\newunicodechar{∪}{\cup} % Digr )U
\newunicodechar{∈}{\in} % Digr (-
\newunicodechar{∃}{\exists} % Digr TE
\newunicodechar{∀}{\forall} % Digr FA
\newunicodechar{∧}{\wedge} % Digr AN
\newunicodechar{∨}{\vee} % Digr OR
\newunicodechar{⊥}{\bot} % Digr -T
\newunicodechar{⊢}{\vdash} % Digr \- 8866 nonstandard
\newunicodechar{⊨}{\models} % Digr \= 8872 nonstandard
\newunicodechar{⊤}{\top} % Digr TO 8868 nonstandard
\newunicodechar{⇒}{\implies} % Digr =>
\newunicodechar{⇔}{\iff} % Digr ==
\newunicodechar{↦}{\mapsto} % Digr T> 8614 nonstandard
\newunicodechar{⟦}{\llbracket} % Digr [[ 10214 nonstandard (needs pkg stmaryrd)
\newunicodechar{⟧}{\rrbracket} % Digr ]] 10215 nonstandard


% cursed
\WarningFilter{newunicodechar}{Redefining Unicode}
\newunicodechar{·}{\ifmmode\cdot\else\textperiodcentered\fi} % Digr .M
\newunicodechar{×}{\ifmmode\times\else\texttimes\fi} % Digr *X
\newunicodechar{→}{\ifmmode\rightarrow\else\textrightarrow\fi} % Digr ->
\newunicodechar{…}{\ifmmode\dots\else\textellipsis\fi} % Digr .,

\begin{document}

\maketitle


\thispagestyle{empty}
\cleardoublepage
\begin{abstract}
	Algebraic effects and handlers are gaining popularity in the theory and practice
	of programming languages as they provide unparalleled ability to define and combine computational effects.
	In this work,
	we demonstrate a novel proof of termination of evaluation and type soundness for
	a $λ$-calculus with deep effect handlers and a type-and-effect system that
	disallows recursive effects.
	The key idea is a fixed-point construction of logical relations for the language.

	\begin{center} \rule[3pt]{300pt}{1pt} \end{center}

	Efekty algebraiczne i ich handlery zyskują na popularności w teorii i praktyce
	języków programowania dzięki ich niezrównanym możliwościom definiowania i łączenia efektów obliczeniowych.
	W niniejszej pracy
	prezentujemy nowy dowód terminacji ewaluacji i poprawności typów
	dla rachunku $λ$ z głębokimi handlerami oraz systemem typów i efektów zabraniającym
	rekurencyjnych efektów.
	Kluczowym pomysłem jest stałopunktowa konstrukcja relacji logicznych dla języka.


\vfil
Wyniki badań powstały w ramach projektu „Szkoła Orłów” realizowanego na Uniwersytecie Wrocławskim
i współfinansowanego ze środków Unii Europejskiej z Europejskiego Funduszu Społecznego w ramach
Programu Operacyjnego Wiedza Edukacja Rozwój.
\end{abstract}


\thispagestyle{empty}
\cleardoublepage
\setcounter{page}{5}
\tableofcontents

\chapter{Introduction}
A programming language needs to be more than just a lambda calculus,
capable only of functional abstraction and evaluation of expressions.
Programs need to have an effect on the outside world and, thinking more locally,
in our programs we would like to have fragments that do not merely reduce to a value in isolation,
but also nontrivially affect the execution of surrounding code.
This is what we call computational effects, the typical examples of which are:
input/output, mutable state, exceptions, nondeterminism, and coroutines.


Today, we are at the mercy of programming language designers
and we can only hope they provide the
effects we would like to use and make sure that they all interact with
each other well.
A traditional way to remedy this is to (purely functionally) model effects using monads \cite{monads}.
This requires the use of monadic style, which among other things causes
stratification of code into two styles and does not always cooperate well with
the language's native facilities.
Moreover, monads do not compose in general, so modular programming with monads has some overheads.

\section{Algebraic effects}

In recent years, a new promising approach has emerged: \textit{algebraic effects and handlers} \cite{Plotkin_2013}.
A language featuring algebraic effects lets programmers express all common computational effects as library code
and use them in the usual direct style.
This is done by decoupling effects into purely syntactic {\em operations} with their type signatures % TODO? awkward
and giving them meaning separately, here by using {\em effect handlers}.

Effect handlers generalize exception handlers.
We can \textit{perform} an operation,
just as we can raise an exception in a typical high-level programming language.
The operation is then handled by the nearest enclosing \textit{handler} for the specific operation.
The handler receives the value given at perform-point and also,
unlike normal exception handlers,
a \textit{resumption} – a first-class functional value representing the rest
of the code to execute inside the handler from the perform-point.
By calling the resumption with a value we can resume at the perform-point
as if performing the operation evaluated to the value.
But more interestingly, we can resume multiple times, or never, or store the resumption for later use.

To prevent crashes because of unhandled operations and aid understanding of effectful code,
languages with algebraic effects typically have powerful
\textit{type-and-effect systems},\footnote{
We will often say just ``type'' when referring to both types and effects.}
not only tracking the type of value an expression might evaluate to, but also
what kind of effects it may perform along the way.
Type-and-effect systems allow us to deduce some basic information about programs,
for example that a pure expression cannot evaluate to two different values,
or, in some systems, that it will {\em always} evaluate to a value.

\section{Contributions}

In this work we demonstrate a (to our knowledge) novel proof of
termination of evaluation (also known as normalization) for a
language \cite{fscd19} equipped with algebraic effects.
We obtain type soundness as a corollary.
We also explain how the proof can carry over to other calculi.
Further, we present code that mirrors the computational content of the proof.

Termination of evaluation might be of interest for several reasons,
for example, it can simplify formal semantics and reasoning, just by virtue of
eliminating nontermination as a case to consider.
It can also be regarded as another safety property, just like ``never crashing''
(though in practice nonterminating programs are indistinguishable from {very long}-running ones).
Although most programming languages support recursion, loops, and other
features allowing for nontermination (e.g., recursive types),
it might be useful to know that fragments that do not use these features cannot be blamed
for it.

Nontermination is sometimes also viewed as a computational effect,
which however does not neatly fit the algebraic effect framework.
Despite that, it can still be added as a built-in effect to be tracked by
the effect system, provided that we have sufficiently identified possible sources
of nontermination.
This is done, for example, in the Koka programming language \cite{koka}.

Normalization also implies that the calculus is sound as a logic,
looking through the lens of the Curry-Howard isomorphism \cite{ch}.
However, it is hard to give logical interpretations to effect annotations \cite{oleg}
and it is unclear how useful it is to treat calculi with algebraic effects as logics.

The primary tool for proving normalization (and many other properties) of
typed formal calculi is {\em logical relations} \cite{lr}.\footnote{
	In the context of normalization, logical relations have many names, including:
	(Tait's) reducibility predicates, reducibility candidates, and saturated sets.
}
Logical relations are
type-indexed relations on terms that essentially help carry additional
information about {\em local} behavior of terms to make a type derivation-directed
proof of the {\em global} property (such as normalization)
have strong enough induction hypotheses and ultimately go through.

In this work we define direct-style logical relations
to prove termination
of evaluation in our language.
A novelty of our approach
is that the definition of the logical relations
is recursive, more concretely, it is a solution to a fixed-point equation.
%This is unlike any normalization proof we know of.
The fixed-point construction replaces the use of step-indexing
which appears in the logical relation construction we are most directly inspired by \cite{hwc}.

\section{Acknowledgements}
I would like to thank Dariusz Biernacki, Filip Sieczkowski, and Piotr Polesiuk
for their help with this work.

\chapter{The language}\label{chap:language}
We will study the deep handler calculus and type-and-effect system formulated
in \cite{fscd19}.
It is a refreshingly minimal language – the call-by-value lambda calculus with a few extensions
to be able to express the essence of algebraic effects.
There is only the universal operation, performed $\Do v$.
To be able to reach beyond the closest effect handler,
the \textit{lift} operator, written $\Lift{e}$, is introduced,
which makes operations in $e$ skip the nearest handler.
In contrast to much work on algebraic effects, the effect-tracking system here is structural –
signatures of effects do not have to be separately defined and named before their use.
Finally, the type system features polymorphic expressions and polymorphic operations.

%\section{Formal definition}
\section{Untyped syntax and semantics}

The syntax of the calculus is shown in \cref{syntax}.
We use metavariables $x$ and $r$ to refer to expression variables.
As is standard, we work modulo $α$-equivalence and distinguish separate instances
of metavariables by using subscripts, superscripts, or adding primes.
Capture-avoiding substitution of $v$ for $x$ in $e$ is denoted $e\subst{v}{x}$.

Evaluation contexts are expressions with a hole ($□$) and
encode a left-to-right evaluation order.
We use the standard notation $K[x]$ for substituting $x$ for the hole in $K$.
There is a concept of {\em freeness} of evaluation contexts (\cref{freeness}),
a quantity increased by lifts and decreased by handlers.
Intuitively, an evaluation context is $n\Free$
if an operation performed inside the context (in place of the hole) % in the place?
would be handled by the $n$-th handler outside of the context.

Naturally, freeness is used in the operational semantics (\cref{reduction}),
where we can see that effect handling occurs if there
is a $0\Free$ context between the operation and the handler.
The resumption $v_c$ wraps the context $K$
with the same handler, which is why the effect handlers are called {\em deep}
– all operations are handled, not just the first one (as in so-called {\em shallow} handlers).
The other rules are the standard $β$-reduction of the $λ$-calculus
and reductions in cases where an (effect-free) value is wrapped by an effect-related construct.
It is straightforward to see that reduction is deterministic
and compatible with respect to evaluation contexts.

\section{Type-and-effect system}

In \cref{types} the type system is introduced.
We have three kinds: types ($\kT$), effects ($\kE$), and rows ($\kR$).
We use $α$ to range over type variables and
$Δ$ to range over type contexts, which assign kinds to type variables.
Similarly, contexts $Γ$ assign types to term-level variables.
We furthermore have the concept of {\em type-level substitutions}:
we write $Δ ⊢ δ ∷ Δ'$ if $δ$ maps type variables in $Δ'$ to types of the corresponding kinds,
well-formed in $Δ$.

We assume that all types are well-formed (well-kinded) in the appropriate contexts in the sense of \cref{kinding}.
Types can be function types or universal types.
Effects consist of an operation argument type and return type,
possibly with variables bound by the type context.
Rows are lists of effects,
with $ι$ denoting the empty row.

Type-level substitutions are used only in the rule for $\KwDo$
to instantiate the polymorphic variables $Δ'$ of effect $Δ'.\,τ_1 \Rightarrow τ_2$.
Complementarily, the rule for $\KwHandle$ states that the effect handler clause $e_h$
has to be essentially parametric in $Δ'$.

We can intuitively understand effect rows as follows:
 if $e : τ ╱ ρ$ and effect $ε$ appears at position $n$ in $ρ$, then
subexpressions performing $ε$ are wrapped by $n$ lifts inside $e$.
Clearly, the order of effects in the row matters.
The type system enables {\em row polymorphism}
since we can have a row ending in a polymorphic type variable.
Such rows are usually called {\em open} (and {\em closed} otherwise).

In \cref{subtyping} the subtyping rules are introduced.
Their main purpose is to allow
effect rows to be subsumed by rows with more effects at the end.
For that to be of use in more places,
we also have subsumption rules for universal types and function types. % polymorphic?
In particular, closed rows are subsumed by open rows.

\begin{figure}
\begin{align*}
	%\textrm{Var} ∋ f,r,x,y,…    &                    \\%&\textrm{(variables)}\\
	v,u          &::= x │ λx.\,e &\textrm{(values)}\\
	e            &::=
		v │ e\;e │ \Lift{e} │ \Do v │ \Handle e\,\{x,r.\,e;\,x.\,e\}
		&\textrm{(expressions)}\\
	K            &::=
		□ │ K\;e │ v\;K │ \Lift{K} │ \Handle K\,\{x,r.\,e;\,x.\,e\}
		&\textrm{(evaluation contexts)}
\end{align*}
\caption{Syntax.}
\label{syntax}
\end{figure}

\begin{figure}
\begin{mathpar}
	\inferrule
		{ }
		{0\Free(□)}

	\inferrule
		{n\Free(K)}
		{n\Free(K\;e)}

	\inferrule
		{n\Free(K)}
		{n\Free(v\;K)}

	\inferrule
		{n\Free(K)}
		{{n+1}\Free(\Lift{K})}

	\inferrule
		{{n+1}\Free(K)}
		{n\Free(\Handle K\,\{x,r.\,e_h;\,x.\,e_r\})}
\end{mathpar}
\caption{Evaluation context freeness.}
\label{freeness}
\end{figure}

\begin{figure}
\begin{mathpar}
	\inferrule
		{e_1 ↦ e_2}
		{K[e_1] → K[e_2]}

	(λx.\,e)\;v ↦ e\subst{v}{x}

	\Lift{v} ↦ v

	\inferrule
		{0\Free(K) \\ v_c = λz.\,\Handle K[z]\,\{x,r.\,e_h;\,x.\,e_r\}}
		{\Handle K[\Do v]\,\{x, r.\,e_h;\,x.\,e_r\} ↦ e_h\subst{v}{x}\subst{v_c}{r}}

	\Handle v\,\{x,r.\,e_h;\,x.\,e_r\} ↦ e_r\subst{v}{x}
\end{mathpar}
\caption{Contraction ($↦$) and single-step reduction ($→$).}
\label{reduction}
\end{figure}

\clearpage

\begin{figure}
\begin{mathpar}
	κ ::= \kT │ \kE │ \kR

	%(type variables): α,β,…

	%Δ ::= · │ α::κ, Δ

	%Γ ::= · │ x:τ, Γ

	σ,τ,ε,ρ ::=
		α │ τ→_ρτ │ ∀α::κ.\,τ │ ι │ Δ.\,τ \Rightarrow τ │ ε · ρ \\

	\inferrule
		{x : τ ∈ Γ}
		{Δ;Γ ⊢ x : τ ╱ ι}

	\inferrule
		{Δ ⊢ τ_1 ∷ \kT \\ Δ;Γ, x:τ_1 ⊢ e : τ_2 ╱ ρ}
		{Δ;Γ ⊢ λx.\,e : τ_1 →_ρ τ_2 ╱ ι}

	\inferrule
		{Δ;Γ ⊢ e_1 : τ_1 →_ρ τ_2 ╱ ρ \\ Δ;Γ ⊢ e_2 : τ_1 ╱ ρ}
		{Δ;Γ ⊢ e_1\,e_2 : τ_2 ╱ ρ}

	\inferrule
		{Δ ⊢ ε ∷ \kE \\ Δ;Γ ⊢ e : τ ╱ ρ}
		{Δ;Γ ⊢ \Lift{e} : τ ╱ ε·ρ}

	\inferrule
		{Δ,α∷κ;Γ ⊢ e : τ ╱ ι}
		{Δ;Γ ⊢ e : ∀α∷κ.\,τ ╱ ι}

	\inferrule
		{Δ ⊢ σ ∷ κ \\ Δ;Γ ⊢ e : ∀α∷κ.\, τ ╱ ρ}
		{Δ;Γ ⊢ e : τ\subst{σ}{α} ╱ ρ}

	\inferrule
		{Δ;Γ ⊢ v : δ(τ_1) ╱ ι \\ Δ ⊢ δ ∷ Δ' \\ Δ ⊢ Δ'.\, τ_1 \Rightarrow τ_2 ∷ \kE}
		{Δ;Γ ⊢ \Do v : δ(τ_2) ╱ (Δ'.\, τ_1 \Rightarrow τ_2)}

	\inferrule
		{Δ;Γ ⊢ e : τ ╱ (Δ'.\,τ_1 \Rightarrow τ_2) · ρ \\
		Δ,Δ';Γ,x:τ_1,r:τ_2→_ρ τ_r ⊢ e_h : τ_r ╱ ρ \\
		Δ;Γ, x:τ ⊢ e_r : τ_r ╱ ρ}
		{Δ;Γ ⊢ \Handle e\;\{x,r.\,e_h;x.\,e_r\} : τ_r ╱ ρ}

	\inferrule
		{Δ ⊢ τ_1 <: τ_2 \\ Δ ⊢ ρ_1 <: ρ_2 \\ Δ;Γ ⊢ e : τ_1 ╱ ρ_1}
		{Δ;Γ ⊢ e : τ_2 ╱ ρ_2}

\end{mathpar}
\caption{Type system.}
\label{types}
\end{figure}

\begin{figure}
\begin{mathpar}
	\inferrule
		{α ∷ κ ∈ Δ}
		{Δ ⊢ α ∷ κ}

	\inferrule
		{Δ ⊢ τ_1 ∷ \kT \\ Δ ⊢ ρ ∷ \kR \\ Δ ⊢ τ_2 ∷ \kT}
		{Δ ⊢ τ_1 →_ρ τ_2 ∷ \kT}

	\inferrule
		{Δ, α :: κ ⊢ τ ∷ \kT}
		{Δ ⊢ ∀α::κ.\, τ ∷ \kT}

	\inferrule
		{Δ,Δ' ⊢ τ_1 ∷ \kT \\ Δ,Δ' ⊢ τ_2 ∷ \kT}
		{Δ ⊢ Δ'.\, τ_1 \Rightarrow τ_2 ∷ \kE}

	\inferrule
		{ }
		{Δ ⊢ ι ∷ \kR}

	\inferrule
		{Δ ⊢ ε ∷ \kE \\ Δ ⊢ ρ ∷ \kR}
		{Δ ⊢ ε · ρ ∷ \kR}

	%Δ ⊢ δ ∷ Δ' ⇔ \dom(δ) = \dom(Δ') ∧ ∀α∈\dom(δ).\, Δ ⊢ δ(α) ∷ Δ'(α)
\end{mathpar}
%\caption{Well-formedness of types, rows, and type substitution.}
\caption{Well-formedness of types and rows.}
\label{kinding}
\end{figure}
\begin{figure}
\begin{mathpar}
	\inferrule
		{ }
		{Δ ⊢ σ <: σ}
		%\textsc{(S-Refl)}

	\inferrule
		{Δ ⊢ ρ ∷ \kR}
		{Δ ⊢ ι <: ρ}
		%\textsc{(S-Empty)}

	\inferrule
		{Δ ⊢ ρ_1 <: ρ_2}
		{Δ ⊢ ε·ρ_1 <: ε·ρ_2}
		%\textsc{(S-Extend)}

	\inferrule
		{Δ ⊢ τ_2^1 <: τ_1^1 \\ Δ ⊢ ρ_1 <: ρ_2 \\ Δ ⊢ τ_1^2 <: τ_2^2}
		{Δ ⊢ τ_1^1 →_{ρ_1} τ_1^2 <: τ_2^1 →_{ρ_2} τ_2^2}
		%\textsc{(S-Arrow)}

	\inferrule
		{Δ, α ∷ κ ⊢ τ_1 <: τ_2}
		{Δ ⊢ ∀α∷κ.\, τ_1 <: ∀α∷κ. \,τ_2}
		%\textsc{(S-ForAll)}
\end{mathpar}
\caption{Subtyping.}
\label{subtyping}
\end{figure}

\chapter{The logical relation}
The logical relation is inspired by \cite{hwc}.
Some changes are due to language differences:
we have only one universal operation which simplifies the treatment of effects,
polymorphism does not manifest at the expression level (we do not have type lambdas),
and our operations can be polymorphic.
Instead of a binary step-indexed relation,
our goal is to build a unary relation without step-indexing.

\section{Definition}

We begin with defining the interpretations of kinds.
We call them the spaces of \textit{semantic types} or,
in the specific cases of $\kE$ and $\kR$, \textit{semantic effects}:
\begin{align*}
	⟦\kT⟧ &= \mathcal{P}(\textrm{CVal}) = \mathsf{Type}\\
	⟦\kE⟧ = ⟦\kR⟧ &= \mathcal{P}(\textrm{CExp}×ℕ×\mathsf{Type}) = \mathsf{Eff}
\end{align*}
We write $\textrm{CVal}$ and $\textrm{CExp}$ for the sets of closed values and closed expressions respectively, so
elements of $\mathsf{Type}$ are simply sets of closed values.
Semantic effects are sets of triples that aim to describe a situation
in which an expression tries to perform an effect but there is no handler for it – it gets {\em control-stuck}.
The components of such a triple are:
the operation with its argument,
the freeness of the enclosing context,
and the semantic type of values we could resume with – the return type of the operation.

Generalizing the preceding,
type contexts are interpreted as mappings from type variables to semantic types:%
$$⟦Δ⟧ = \{ η │ \dom(η) = \dom(Δ) ∧ ∀α∷κ∈Δ.\,η(α) ∈ ⟦κ⟧ \}$$

The logical relations, defined by (mutual) structural induction, appear in \cref{logrel}. % TODO: appear in? ;/
They are parameterized by a mapping $η$ from type variables to
semantic types.

The interpretation of a type variable
is directly retrieved from the environment $η$.
The treatment of function types is standard,
except effect annotations also have to be taken into account.
The definition may not look structurally recursive at first,
but we can consider $τ_2/ρ$ to be a subterm of $τ_1 →_ρ τ_2$,
just rearranged to a different notation.
A universal type is interpreted, as usual,
as the intersection of the interpretations
for all possible choices of the semantic type for the type variable.
\begin{figure}
\begin{align*}
	⟦α⟧_η &= η(α) \\
	%\\
	⟦τ_1 →_ρ τ_2⟧_η
	 &= \{ λx.\,e \mid ∀v∈⟦τ_1⟧_η.\, e\subst{v}{x} ∈ \E⟦τ_2/ρ⟧_η \} \\
	⟦∀α::κ.\,τ⟧_η
	&= \{ v \mid ∀μ∈⟦κ⟧.\, v ∈ ⟦τ⟧_{η[α↦μ]} \} \\
	⟦Δ.\,τ_1 \Rightarrow τ_2⟧_η &= \{(\Do v,0,⟦τ_2⟧_{ηη'}) \mid η'∈⟦Δ⟧ ∧ v∈⟦τ_1⟧_{ηη'} \} \\
	⟦ε · ρ⟧_η &= ⟦ε⟧_η ∪ \{(e, n+1, μ) \mid (e, n, μ)∈⟦ρ⟧_η \} \\
	⟦ι⟧_η &= ∅
\end{align*}
\begin{align*}
	\E⟦τ/ρ⟧_η &=
	\{ e \mid ∃v∈⟦τ⟧_η.\, e →^* v ∨ ∃e'∈\S⟦τ/ρ⟧_η.\, e →^* e' \} \\
	\S⟦τ/ρ⟧_η &= \{ K[e] \mid ∃n,μ.\, (e,n,μ)∈⟦ρ⟧_η  ∧ n\Free(K) ∧ ∀u∈μ.\, K[u]∈ \E⟦τ/ρ⟧_η \}
\end{align*}
\caption{
	Interpretation of types.
	Relations on expressions and stuck terms.%
	\protect\footnotemark
}
\label{logrel}
\end{figure}

Dually, we can see that a polymorphic effect is interpreted as the {\em union} of the interpretations
of the effect for all possible choices of the semantic types for the type variables.
The interpretation of a single operation is implicitly treated as if it were
at the beginning of a row, so the freeness is $0$.
When we prepend to a row, we increase this freeness for every element of its semantic effect
and combine with the interpretation of the prepended effect.
Naturally, the semantic effect for the empty row is empty.

\footnotetext{
	Technically, the terms in $\S⟦τ/ρ⟧_η$ do not have to be control-stuck, since
	the $(e,n,μ)$ could come from the interpretation of an effect or row variable,
	and the space of semantic effects allows for any $e$.
	Such a term {\em is} stuck if the triple comes from the interpretation of an operation.
	We leave it that way to make adding multiple operations easier later.
	An analogous definition appears in \cite{hwc}.
}

The definition of the set $\E⟦τ/ρ⟧_η$ is recursive and we interpret it inductively,
i.e., as the least solution to the equations (we will elaborate on that soon).
Note the similarity to the interpretation of function types in the definition of
$\S⟦τ/ρ⟧_η$.
The intuition is that an element of $\E⟦τ/ρ⟧_η$
evaluates to a value of type $τ$ while possibly performing an effect in $ρ$ and
getting control-stuck
finitely many times along the way.
When the term is control-stuck, we do not have a handler,
but we do know the return type of the operation,
so we resume with all possible values in parallel.

This is a very local view of effectful computations,
perhaps giving the false impression that all handlers immediately resume with a value and
do nothing more (this is called the {\em reader} effect and is equivalent to dynamically-scoped variables).
In reality, much can happen between
performing the operation and it finally returning.
Nevertheless, this local view suffices for our purposes and
accurately reflects how much of the computation remains in the scope of a handler
throughout evaluation.

\begin{figure}
\begin{tikzpicture}

	\node (e) at (0,0.5) {$\textit{times}\;(\Do ())\,\textit{tick}$};
	\node (e0) at (0,-1) {$\textit{times}\;0\,\textit{tick}$};
	\node (e1) at (4,-1) {$\textit{times}\;1\,\textit{tick}$};
	\node (e2) at (8,-1) {$\textit{times}\;2\,\textit{tick}$};
	\node (einf) at (12,-1) {$\hdots$};
	\draw[dashed,->] (e.south) -- (e0.north);
	\draw[dashed,->] (e.south) -- (e1.north);
	\draw[dashed,->] (e.south) -- (e2.north);
	\draw[dashed,->] (e.south) -- ([yshift=4] einf.north);

	\node (e0a) at (0,-2.5) {$()$};
	\node (e1a) at (4,-2.5) {$\Lift{\Do ()}; \textit{times}\;0\,\textit{tick}$};
	\node (e2a) at (8,-2.5) {$\Lift{\Do ()}; \textit{times}\;1\,\textit{tick}$};
	%\node (einfa) at (12,-1.85) {$\ddots$};

	\draw[->] (e0.south) -- (e0a.north) node[very near end,right=-3]{\textsubscript{*}};
	\draw[->] (e1.south) -- (e1a.north) node[very near end,right=-3]{\textsubscript{*}};
	\draw[->] (e2.south) -- (e2a.north) node[very near end,right=-3]{\textsubscript{*}};

	\node (e1b) at (4,-4) {$\Lift{()}; \textit{times}\;0\,\textit{tick}$};
	\node (e2b) at (8,-4) {$\Lift{()}; \textit{times}\;1\,\textit{tick}$};

	\draw[dashed,->] (e1a.south) -- (e1b.north);
	\draw[dashed,->] (e2a.south) -- (e2b.north);

	\node (e1c) at (4,-5.5) {$()$};
	\node (e2c) at (8,-5.5) {$\Lift{\Do ()}; \textit{times}\;0\,\textit{tick}$};

	\draw[->] (e1b.south) -- (e1c.north) node[very near end,right=-3]{\textsubscript{*}};
	\draw[->] (e2b.south) -- (e2c.north) node[very near end,right=-3]{\textsubscript{*}};

	\node (e2d) at (8,-7) {$\Lift{()}; \textit{times}\;0\,\textit{tick}$};

	\draw[dashed,->] (e2c.south) -- (e2d.north);

	\node (e2e) at (8,-8.5) {$()$};

	\draw[->] (e2d.south) -- (e2e.north) node[very near end,right=-3]{\textsubscript{*}};

	\node (einfa) at (12,-5.5) {$\vdots$};
	\node (einfb) at (12,-10) {$\ddots$};

\end{tikzpicture}
\caption{
	An illustration of the reduction trace for $\textit{times}\,({\Do ()})\,\textit{tick} ∈
	\E⟦\textsf{unit}/ \textsf{askNat} · \textsf{tick} · ι⟧$,
	where $\textsf{askNat} = \textsf{unit}\Rightarrow\textsf{nat}$
	and $\textsf{tick} = \textsf{unit}\Rightarrow\textsf{unit}$.
	For clarity, we assume the unit type, the inductive naturals, and a function \textit{times} for invoking a thunk $n$ times,
	but these can be realized using Church encodings.
	We set $\textit{tick} = λx.\,\Lift{\Do ()}$.
	Here, the \textsf{tick} effect does not seem to do much, but
	a handler for it could, for instance, increment an external counter.
	The semicolon is standard syntax sugar:
	$e_1;e_2$ is expanded to $(λx.\,e_2)\;e_1$ with $x$ not free in $e_2$.
	The solid arrow is the usual reduction, while the dashed one represents substituting
	a value for the operation in a stuck term
	in $\S⟦\textsf{unit}/ \textsf{askNat} · \textsf{tick} · ι⟧$.
	This tree is well-founded despite having infinite depth.
}
\label{trace}
\end{figure}

More graphically (see \cref{trace}),
we can associate with an element in $\E⟦τ/ρ⟧_η$ what we will call a {\em reduction trace}
– a tree where nodes are expressions in $\E⟦τ/ρ⟧_η$,
leaves are values in $⟦τ⟧_η$, and edges are either (maximal) multi-step reductions
or branches from $\S⟦τ/ρ⟧_η$ for each element of $μ$,
which substitute the value for the operation.%
\footnote{
	This is also how we could view the structure of values of the inductive type $\E⟦τ/ρ⟧_η$,
	had we formalized the definitions in a (dependent) type theory.
}
Different choices of values to resume with can
lead to getting stuck a different number of times,
so the depth of the tree is not uniform, and it can even be infinite.
Still, these trees are well-founded thanks to the choice of the inductive interpretation.

To describe the construction in more detail, we temporarily overload notation and define
operators $\S⟦τ/ρ⟧_η$ and $\E⟦τ/ρ⟧_η$ on sets of expressions (denoted by $X$).
\begin{align*}
	\E⟦τ/ρ⟧_η(X) &=
	\{ e \mid ∃v∈⟦τ⟧_η.\, e →^* v ∨ ∃e'∈\S⟦τ/ρ⟧_η(X).\, e →^* e' \} \\
	\S⟦τ/ρ⟧_η(X) &= \{ K[e] \mid ∃n,μ.\, (e,n,μ)∈⟦ρ⟧_η  ∧ n\Free(K) ∧ ∀u∈μ.\, K[u]∈X \}
\end{align*}%
They are clearly monotone,
so by the Knaster-Tarski theorem % citation
the fixed-point equation $\E⟦τ/ρ⟧_η(X) = X$ has a least solution.\footnote{
	The operators are not Scott-continuous because of potentially infinite semantic
	types $μ$.
	This is why the construction from the Kleene fixed-point theorem (union of
	iterations of the operator on the empty set)
	would fail to be a solution.
	With this definition the reduction traces have bounded depth.
	The application compatibility lemma would fail:
	it grafts different reduction traces to the leaves of a
	potentially infinitely branching reduction trace,
	so the bounded depth is not preserved.
}
Moreover, it can be characterized as the intersection of all
$\E⟦τ/ρ⟧_η$-closed sets:
\begin{align*}
	\E⟦τ/ρ⟧_η &= \bigcap \{ X │ \E⟦τ/ρ⟧_η(X) ⊆ X \} \\
	\S⟦τ/ρ⟧_η &= \S⟦τ/ρ⟧_η(\E⟦τ/ρ⟧_η)
\end{align*}
We immediately obtain the following principle:

\begin{lemma}[Tarski induction principle]\label{tarski-induction}
	If $\E⟦τ/ρ⟧_η(X) ⊆ X$, then $\E⟦τ/ρ⟧_η ⊆ X$.
\end{lemma}

By expanding out the definition of the function $\E⟦τ/ρ⟧_η$
and treating $X$ as a predicate $P$,
we get the more familiar principle of structural induction on $\E⟦τ/ρ⟧_η$.
\begin{lemma}[Induction principle]\label{induction}
	Assume $P$ is a predicate on closed expressions and
\begin{itemize}
	\item if $e$ evaluates to a value in $⟦τ⟧_η$, then $P(e)$ holds; and
	\item if $e$ reduces to some $K[e']$ such that there exist $(e',n,μ)∈⟦ρ⟧_η$ such that $n\Free(K)$
		and $P(K[u])$ holds for all $u∈μ$, then $P(e)$ holds.
\end{itemize}
	Then $P(e)$ holds for all $e ∈ \E⟦τ/ρ⟧_η$.
\end{lemma}

We also note some straightforward but useful properties of the relations.
\begin{lemma}[Value inclusion]\label{value-inclusion}
	For any $τ$ and $ρ$ we have $⟦τ⟧_η ⊆ \E⟦τ/ρ⟧_η$.
\end{lemma}

\begin{lemma}[Control-stuck inclusion]\label{stuck-inclusion}
For any $τ$ and $ρ$ we have $\S⟦τ/ρ⟧_η ⊆ \E⟦τ/ρ⟧_η$.
\end{lemma}

\begin{lemma}[Closedness under antireduction]\label{antireduction}
If $e →^* e' ∈ \E⟦τ/ρ⟧_η$, then $e∈\E⟦τ/ρ⟧_η$.
\end{lemma}

\begin{lemma}[Weakening]\label{weakening}
	If $η'$ extends $η$,
	then $\E⟦τ/ρ⟧_η = \E⟦τ/ρ⟧_{η'}$.
\end{lemma}

\begin{lemma}[Monotonicity in types]\label{mono}
	If $⟦τ_1⟧_η ⊆ ⟦τ_2⟧_η$ and $⟦ρ_1⟧_η ⊆ ⟦ρ_2⟧_η$,
	then $\S⟦τ_1/ρ_1⟧_η ⊆ \S⟦τ_2/ρ_2⟧_η$
	and $\E⟦τ_1/ρ_1⟧_η ⊆ \E⟦τ_2/ρ_2⟧_η$.
\end{lemma}
%\begin{proof}
%We will show by induction on $e ∈ \E⟦τ_1/ρ_1⟧_η$ that $e ∈ \E⟦τ_2/ρ_2⟧_η$.
%
%If $e →^* v ∈ ⟦τ_1⟧_η$, then $v ∈ ⟦τ_2⟧_η$ and by \cref{value-inclusion} we have $v ∈ \E⟦τ_2/ρ_2⟧_η$.
%By \cref{antireduction} we conclude $e ∈ \E⟦τ_2/ρ_2⟧_η$.
%
%If $e →^* K[e']$ such that there exist $(e', n, μ) ∈ ⟦ρ_1⟧_η$ such that
%$n\Free(K)$ and $K[u] ∈ \E⟦τ_2/ρ_2⟧_η$ for all $u$ in $μ$,
%then, since $⟦ρ_1⟧_η ⊆ ⟦ρ_2⟧_η$, by definition we have $K[e'] ∈ \S⟦τ_2/ρ_2⟧_η$.
%By \cref{stuck-inclusion} and \cref{antireduction} we have $e∈\E⟦τ_2/ρ_2⟧_η$.
%
%Finally, since the operator $\S⟦τ/ρ⟧_η$ ignores $τ$ and is monotone in $⟦ρ⟧_η$,
%\begin{align*}
%\S⟦τ_1/ρ_1⟧_η = \S⟦τ_1/ρ_1⟧_η(\E⟦τ_1/ρ_1⟧_η) &⊆ \S⟦τ_1/ρ_1⟧_η(\E⟦τ_2/ρ_2⟧_η)\\
%&⊆ \S⟦τ_2/ρ_1⟧_η(\E⟦τ_2/ρ_2⟧_η) = \S⟦τ_2/ρ_2⟧_η.
%\end{align*}
%\end{proof}

\section{Compatibility} % TODO only "Compatibility" or other word? Adequacy? Soundness?
We want to establish that $⊢ e : τ ╱ ι$ implies $e ∈ \E⟦τ/ι⟧$.
For this purpose we will prove a semantic counterpart of each typing rule.
First, we need to define a counterpart to the typing judgment.
Unlike typing judgments, our relations are on closed terms only,
so we get around that by using substitution.
We define semantic entailment as follows:
$$Δ;Γ ⊨ e : τ ╱ ρ ⇔ ∀η∈⟦Δ⟧.\, ∀γ∈⟦Γ⟧_η.\,γ(e) ∈ \E⟦τ/ρ⟧_η,$$
where $⟦Γ⟧_η = \{ γ │ \dom(γ) = \dom(Γ) ∧ ∀x:τ∈Γ.\,γ(x) ∈ ⟦τ⟧_η\}$ contains expression-level
variable substitutions.

\begin{lemma}[Variable compatibility]
	$$
	\inferrule
		{x : τ ∈ Γ}
		{Δ;Γ ⊨ x : τ ╱ ι}
	$$
\end{lemma}
\begin{proof}
Assume $x : τ ∈ Γ$.
We want to prove $Δ;Γ ⊨ x : τ ╱ ι$.
Take any $η∈⟦Δ⟧$ and $γ∈⟦Γ⟧_η$.
We want to show $γ(x) ∈ \E⟦τ/ι⟧_η$.
From the definition of $⟦Γ⟧_η$
we know that $γ(x) ∈ ⟦τ⟧_η$,
so by \cref{value-inclusion} we have $γ(x) ∈ \E⟦τ/ι⟧_η$.
\end{proof}

\begin{lemma}[Abstraction compatibility]
	$$
	\inferrule
		{Δ ⊢ τ_1 ∷ \kT \\ Δ;Γ, x:τ_1 ⊨ e : τ_2 ╱ ρ}
		{Δ;Γ ⊨ λx.\,e : τ_1 →_ρ τ_2 ╱ ι}
	$$
\end{lemma}
\begin{proof}
Assume $Δ ⊢ {τ_1 ∷ \kT}$ and $Δ;Γ,{x:τ_1} ⊨ e : τ_2 ╱ ρ$.
% Note: kind assumption necessary so that τ_1 →_ρ τ_2 well formed
We want to prove $Δ;Γ ⊨ λx.\,e : {τ_1 →_ρ τ_2} ╱ ι$.
Take any $η∈⟦Δ⟧$ and $γ∈⟦Γ⟧_η$.
By \cref{value-inclusion} it suffices to show
$γ(λx.\,e) = λx.\,γ(e) ∈ ⟦τ_1 →_ρ τ_2⟧_η$.
So take any $v ∈ ⟦τ_1⟧_η.$
We need to show $γ(e)\subst{v}{x} ∈ \E⟦τ_2/ρ⟧_η$.
Let $γ' = γ'[x↦v]$.
Then $γ' ∈ ⟦Γ,x:τ_1⟧_η$, so $γ(e)\subst{v}{x} = γ'(e) ∈ \E⟦τ_2/ρ⟧_η.$
\end{proof}

For clarity of presentation,
in the following we will assume $Γ$ empty.
The lemmas in full generality can then be proven simply by
substituting an interpretation of $Γ$.

\begin{lemma}[Lift compatibility]
	$$
	\inferrule
		{Δ ⊢ ε ∷ \kE \\ Δ; ⊨ e : τ ╱ ρ}
		{Δ; ⊨ \Lift{e} : τ ╱ ε·ρ}
	$$
\end{lemma}
\begin{proof}
Assume $Δ ⊢ τ ∷ \kT$, $Δ ⊢ ε ∷ \kE$, and $Δ ⊢ ρ ∷ \kR$.
Take any $η∈⟦Δ⟧$.
We will show by induction on $e∈\E⟦τ/ρ⟧_η$ that $\Lift{e} ∈ \E⟦τ/ε·ρ⟧_η$.

If $e →^* K[e']$ and there exists
$(e', n, μ) ∈ ⟦ρ⟧_η$ such that $n\Free(K)$ and
for all $u∈μ$ the induction hypothesis holds for $K[u]$,
then we have $(e', n+1, μ) ∈ ⟦ε·ρ⟧_η$, $n+1\Free(\Lift{K})$,
and $∀u∈μ.\, \Lift{K[u]} ∈ \E⟦τ/ε·ρ⟧_η$.
So $\Lift{K[e']} ∈ \S⟦τ/ε·ρ⟧_η$ and $\Lift{e} ∈ \E⟦τ/ε·ρ⟧_η$ by antireduction.

If $e →^* v ∈ ⟦τ⟧_η$, then
$\Lift{e} →^* \Lift{v} → v$,
so $\Lift{e} ∈ \E⟦τ/ε·ρ⟧_η$.
\end{proof}

\begin{lemma}[Application compatibility]
	$$
	\inferrule
		{Δ; ⊨ e_1 : τ_1 →_ρ τ_2 ╱ ρ \\ Δ; ⊨ e_2 : τ_1 ╱ ρ}
		{Δ; ⊨ e_1\,e_2 : τ_2 ╱ ρ}
	$$
\end{lemma}
\begin{proof}
%Assume $Δ;Γ ⊨ e_1 : τ_1 →_ρ τ_2 ╱ ρ$ and $Δ;Γ ⊨ e_2 : τ_1 ╱ ρ$.
Fix any well-formed $Δ$ and $τ_1 →_ρ τ_2$.
Take any $η∈⟦Δ⟧$ and $e_2 ∈ \E⟦τ_1/ρ⟧_η$.
We will show by induction on $e_1∈\E⟦τ_1→_ρ τ_2/ρ⟧_η$ that
$e_1\;e_2 ∈ \E⟦τ_2/ρ⟧_η$.

If $e_1 →^* K_1[e_1']$ and
there exists $(e_1',n,μ)∈⟦ρ⟧_η$ such that $n\Free(K_1)$ and for all $u∈μ$
the inductive hypothesis holds for $K_1[u]$,
then $K_1[e_1']\;e_2 ∈ \S⟦τ_2/ρ⟧_η$, since $n\Free(K_1\;e_2)$.
By antireduction $e_1\;e_2 ∈ \E⟦τ_2/ρ⟧_η$.

Now assume $e_1 →^* (λx.\,e) ∈ ⟦τ_1 →_ρ τ_2/ρ⟧_η$.
We will show by induction on $e_2 ∈ \E⟦τ_1/ρ⟧_η$ that $(λx.\,e)\;e_2 ∈ \E⟦τ_2/ρ⟧_η$
and the claim will follow by antireduction.

If $e_2 →^* K_2[e_2']$ and
there exists $(e_2',n,μ)∈⟦ρ⟧_η$ such that $n\Free(K_2)$ and for all $u∈μ$
the inductive hypothesis holds for $K_2[u]$,
then $(λx.\,e)\;K_2[e_2'] ∈ \S⟦τ_2/ρ⟧_η$, since $n\Free((λx.\,e)\;K_2)$.
By antireduction $(λx.\,e)\;e_2 ∈ \E⟦τ_2/ρ⟧_η$.

If $e_2 →^* v ∈ ⟦τ_1⟧_η$, then
$(λx.\,e)\;e_2 →^* (λx.\,e)\;v → e\subst{v}{x} ∈ \E⟦τ_2/ρ⟧_η$.
\end{proof}

\begin{lemma}[Handle compatibility]
	$$
	\inferrule
		{Δ; ⊨ e : τ ╱ (Δ'.\,τ_1 \Rightarrow τ_2) · ρ \\
		Δ,Δ';x:τ_1,r:τ_2→_ρ τ_r ⊨ e_h : τ_r ╱ ρ \\
		Δ; x:τ ⊨ e_r : τ_r ╱ ρ}
		{Δ; ⊨ \Handle e\;\{x,r.\,e_h;x.\,e_r\} : τ_r ╱ ρ}
	$$
\end{lemma}
\begin{proof}
Assume $Δ, Δ' ; x:τ_1, r:τ_2 →_ρ τ_r ⊨ e_h : τ_r ╱ ρ$ and
$Δ; x:τ ⊨ e_r : τ_r ╱ ρ$.
%We want to show
%$Δ;Γ ⊨ \Handle e\,\{x,r.\,e_h;\;x.\,e_r\} : τ_r ╱ ρ$.
Let $h$ stand for $\{x,r.\,e_h;\,x.\,e_r\}$.
Take any $η∈⟦Δ⟧$.
We will show by induction on $e∈\E⟦τ/(Δ'.\,τ_1 \Rightarrow τ_2) · ρ⟧_η$
that $\Handle e\,h ∈ \E⟦τ_r/ρ⟧_η$.
Note that only $τ_1$ and $τ_2$ require $Δ'$ to be in context.

If $e →^* v ∈ ⟦τ⟧_η$,
then $\Handle e\,h →^* e_r\subst{v}{x} ∈ \E⟦τ_r/ρ⟧_η$,
so the claim follows by antireduction.

Now assume $e →^* K[e']$ and
we have $(e',n,μ) ∈ ⟦(Δ'.\,τ_1 \Rightarrow τ_2) · ρ⟧_η$
such that $n\Free(K)$ and
for all $u∈μ$ the induction hypothesis holds for $K[u]$.

If $n=0$, then $(e',n,μ) ∈ ⟦τ_1 \Rightarrow τ_2⟧_{ηη'}$ for some $η'∈⟦Δ'⟧$.
More specifically, $e' = \Do v$, $v∈⟦τ_1⟧_{ηη'}$ and $μ = ⟦τ_2⟧_{ηη'}$.
We have $\Handle e\,h →^* \Handle K[\Do v]\,h → e_h\subst{v}{x}\subst{v_c}{r}$,
where $v_c=λz.\,\Handle K[z]\,h$.
To show $v_c ∈ ⟦τ_2 →_ρ τ_r⟧_{ηη'}$, take any $u ∈ ⟦τ_2⟧_{ηη'}$ and show
$\Handle K[u]\,h ∈ \E⟦τ_r/ρ⟧_{ηη'} = \E⟦τ_r/ρ⟧_η$.
Which holds by induction hypothesis.
Therefore, $e_h\subst{v}{x}\subst{v_c}{r}$ is in $\E⟦τ_r/ρ⟧_η$ and so is $\Handle e\;h$.

If $n>0$, then
$\Handle K[e']\,h ∈ \S⟦τ_r/ρ⟧_η$,
since $n-1\Free(\Handle K\,h)$, $(e',n-1,μ) ∈ ⟦ρ⟧_η$,
and $∀u∈μ.\,\Handle K[u]\,h ∈ \E⟦τ_r/ρ⟧_η$.
Again, the claim follows by antireduction.

\end{proof}


\begin{lemma} \label{subst-comp}
	Syntactic type substitutions are compatible with semantic type environments: If
	\begin{itemize}
	\item $Δ$ and $Δ'$ have disjoint domains; and
	\item $Δ,Δ' ⊢ τ ∷ κ$; and
	\item $η∈⟦Δ⟧$; and
	\item $Δ ⊢ δ ∷ Δ'$; and
	\item $η'$ extends $η$ by $α↦⟦δ(α)⟧_η$ for each $α$ in the domain of $Δ'$;
	\end{itemize}
	then $⟦τ⟧_{η'} = ⟦δ(τ)⟧_η$.
\end{lemma}
\begin{proof}
	By induction on the kinding rules.

	If $τ=α ∈ Δ$, then both sides are equal to $η(α)$.

	If $τ=α ∈ Δ'$, then equality follows from the definition of $η'$.

	If $τ=ι$, then both sides are empty.

	If $τ=τ_1 →_ρ τ_2$, then
	$⟦τ⟧_{η'} = \{λx.\,e │ ∀v ∈ ⟦τ_1⟧_{η'}.\,e\subst{v}{x} ∈ \E⟦τ_2/ρ⟧_{η'}\}$
	and
	$⟦δ(τ)⟧_η = \{λx.\,e │ ∀v ∈ ⟦δ(τ_1)⟧_η.\,e\subst{v}{x} ∈ \E⟦δ(τ_2)/δ(ρ)⟧_η\}$,
	which are equal by the inductive hypothesis and definition of $\E$.

	If $τ=∀α∷κ.\,τ'$, then
	$⟦τ⟧_{η'} = \bigcap \{⟦τ'⟧_{η'[α↦μ]} │ μ∈⟦κ⟧\}$
	and
	$⟦δ(τ)⟧_{η} = \bigcap \{⟦δ(τ')⟧_{η[α↦μ]} │ μ∈⟦κ⟧\}$,
	which are equal by the inductive hypothesis
	(taking $Δ, α∷κ$ as $Δ$ in the statement).

	If $τ=Δ''.\,τ_1 \Rightarrow τ_2$,
	then $⟦τ⟧_{η'} = \{(e,0,⟦τ_2⟧_{η'η''}) │ η'' ∈ ⟦Δ''⟧ ∧ v ∈ ⟦τ_1⟧_{η'η''} \}$
	and $⟦δ(τ)⟧_{η} = \{(e,0,⟦δ(τ_2)⟧_{ηη''}) │ η'' ∈ ⟦Δ''⟧ ∧ v ∈ ⟦δ(τ_1)⟧_{ηη''} \}$,
	which are equal by the inductive hypothesis (taking $Δ, Δ''$ as $Δ$ in the statement).

	If $τ=ε·ρ$,
	then $⟦τ⟧_{η'} = ⟦ε⟧_{η'} ∪ \{(e,n+1,μ) │ (e,n,μ) ∈ ⟦ρ⟧_{η'} \}$
	and $⟦δ(τ)⟧_{η} = ⟦δ(ε)⟧_{η} ∪ \{(e,n+1,μ) │ (e,n,μ) ∈ ⟦δ(ρ)⟧_{η} \}$,
	which are equal by the inductive hypothesis.
\end{proof}

\begin{lemma}[Do compatibility]
	$$
	\inferrule
		{Δ; ⊨ v : δ(τ_1) ╱ ι \\ Δ ⊢ δ ∷ Δ' \\ Δ ⊢ Δ'.\, τ_1 \Rightarrow τ_2 ∷ \kE}
		{Δ; ⊨ \Do v : δ(τ_2) ╱ (Δ'.\, τ_1 \Rightarrow τ_2)}
	$$
\end{lemma}
\begin{proof}
Assume $Δ ⊢ δ ∷ Δ'$, $Δ⊢Δ'.\,τ_1→τ_2 ∷ \kE$.
Take any $η ∈ ⟦Δ⟧$.
Assume $v ∈ \E⟦δ(τ_1)/ι⟧_η$.
Clearly, $v ∈ ⟦δ(τ_1)⟧_η$.
We want to show $\Do v ∈ \E⟦δ(τ_2)/(Δ'.\,τ_1 \Rightarrow τ_2)⟧_η$.

By \cref{stuck-inclusion} it suffices to show
$\Do v ∈ \S⟦δ(τ_2)/(Δ'.\,τ_1 \Rightarrow τ_2)⟧_η$.
By taking the empty context in the definition of $\S$ and \cref{value-inclusion},
it suffices to show $(\Do v,0,⟦δ(τ_2)⟧_η) ∈ ⟦Δ'.\,τ_1 \Rightarrow τ_2⟧_η$.
By the interpretation of polymorphic effects, it
would be enough to show $(\Do v,0,⟦δ(τ_2)⟧_η) ∈ ⟦τ_1 \Rightarrow τ_2⟧_{η'}$,
where $η'$ extends $η$ by mappings $α↦⟦δ(α)⟧_η$ for all $α∈Δ'$.
In other words, we need
$v ∈ ⟦τ_1⟧_{η'}$ and $⟦δ(τ_2)⟧_η = ⟦τ_2⟧_{η'}$,
which follows immediately from \cref{subst-comp}.
\end{proof}

\begin{lemma}[Subtyping compatibility]
	$$
	\inferrule
		{Δ ⊢ τ_1 <: τ_2 \\ Δ ⊢ ρ_1 <: ρ_2 \\ Δ; ⊨ e : τ_1 ╱ ρ_1}
		{Δ; ⊨ e : τ_2 ╱ ρ_2}
	$$
\end{lemma}
\begin{proof}
By induction on subtyping rules we will show that
if $Δ ⊢ σ_1 <: σ_2$, then $⟦σ_1⟧_η ⊆ ⟦σ_2⟧_η$ for all $η ∈ ⟦Δ⟧$.
Then, by \cref{mono}, from $Δ ⊢ τ_1 <: τ_2$, $Δ ⊢ ρ_1 <: ρ_2$ and $Δ; Γ ⊨ e : τ_1╱ρ_1$
we will be able to conclude
$Δ; Γ ⊨ e : τ_2╱ρ_2$.

For the case of the reflexivity rule,
we obviously have $⟦σ⟧_η ⊆ ⟦σ⟧_η$.

For the case of the function type rule,
assume $⟦τ_2^1⟧_η ⊆ ⟦τ_1^1⟧_η$, $⟦ρ_1⟧_η ⊆ ⟦ρ_2⟧_η$, and $⟦τ_1^2⟧_η ⊆ ⟦τ_2^2⟧_η$.
We want to show $⟦τ_1^1 →_{ρ_1} τ_1^2⟧_η ⊆ ⟦τ_2^1 →_{ρ_2} τ_2^2⟧_η$.
So take any $(λx.\,e)$ in the former and any $v ∈ ⟦τ_2^1⟧$.
Since $v ∈ ⟦τ_1^1⟧_η$, we have $e\subst{v}{x} ∈ \E⟦τ_1^2/ρ_1⟧_η$.
By \cref{mono} we obtain $e\subst{v}{x} ∈ \E⟦τ_2^2/ρ_2⟧_η$ as desired.

For the case of the universal quantifier rule,
assume $⟦τ_1⟧_{η[α↦μ]} ⊆ ⟦τ_2⟧_{η[α↦μ]}$ for all $μ ∈ ⟦κ⟧$.
The claim holds since
\begin{align*}
⟦∀α∷κ.\,τ_1⟧_η
&= \{ v \mid ∀μ∈⟦κ⟧.\, v ∈ ⟦τ_1⟧_{η[α↦μ]} \} \\
&⊆ \{ v \mid ∀μ∈⟦κ⟧.\, v ∈ ⟦τ_2⟧_{η[α↦μ]} \}
=
⟦∀α∷κ.\,τ_2⟧_η.
\end{align*}

The case of the empty row rule holds trivially, since $⟦ι⟧_η = ∅$.

For the case of the row extension rule, assume $⟦ρ_1⟧_η ⊆ ⟦ρ_2⟧_η$.
We clearly have
$$\{(e,n+1,μ) │ (e,n,μ) ∈ ⟦ρ_1⟧_η\} ⊆ \{(e,n+1,μ) │ (e,n,μ) ∈ ⟦ρ_2⟧_η\},$$
so $⟦ε·ρ_1⟧_η ⊆ ⟦ε·ρ_2⟧_η$ as well.

\end{proof}

\begin{lemma}[Polymorphism introduction compatibility]
	$$
	\inferrule
		{Δ,α∷κ; ⊨ e : τ ╱ ι}
		{Δ; ⊨ e : ∀α∷κ.\,τ ╱ ι}
	$$
\end{lemma}
\begin{proof}
Assume $Δ,α∷κ; ⊨ e : τ ╱ ι$.
Take $η∈⟦Δ⟧$.
We know $e$ evaluates to a value in $⟦τ⟧_{η[α↦μ]}$ for
any $μ∈⟦κ⟧$.
Therefore this value is in $⟦∀α∷κ.\,τ⟧_η$,
and by antireduction $e ∈ \E⟦∀α∷κ.\,τ/ι⟧_η$.
\end{proof}

\begin{lemma}[Polymorphism elimination compatibility]
	$$
	\inferrule
		{Δ ⊢ σ ∷ κ \\ Δ; ⊨ e : ∀α∷κ.\, τ ╱ ρ}
		{Δ; ⊨ e : τ\subst{σ}{α} ╱ ρ}
	$$
\end{lemma}
\begin{proof}
Assume $Δ ⊢ σ ∷ κ$ and $Δ; ⊨ e : ∀α∷κ.\,τ╱ρ$.
Take $η ∈ ⟦Δ⟧$.
By \cref{subst-comp} we have $⟦τ\subst{σ}{α}⟧_η = ⟦τ⟧_{η[α↦⟦σ⟧_η]}$,
which is a superset of $⟦∀α∷κ.\,τ⟧_η$.
So we have $Δ; ⊨ e : τ\subst{σ}{α} ╱ ρ$ by \cref{mono}.
\end{proof}

\begin{theorem}[Termination of evaluation]
	If $⊢ e : τ ╱ ι$, then evalution of $e$ terminates.
\end{theorem}
\begin{proof}
Take a derivation of $⊢ e : τ ╱ ι$.
After replacing each typing rule by the corresponding compatibility lemma,
we obtain $⊨ e : τ ╱ ι$, so $e ∈ \E⟦τ/ι⟧$.
Therefore $e$ has to terminate to a value, since
$⟦ι⟧$ is empty and hence $\S⟦τ/ι⟧$ is empty.
\end{proof}

This is also an alternative proof of soundness (``well-typed programs do not go wrong''),
which was already shown using
the technique of progress and preservation in \cite{fscd19}.

\section{Extensions}

The calculus considered so far is fairly simple.
We will discuss extensions that bring it closer to other calculi with algebraic effects.
Adapting the proofs to the changes poses no difficulty and is not interesting,
so we will omit that.

A simple extension we can make is analogous to multiple prompts for delimited continuations:
annotate each operation ($\keyword{do}_l \;v$), handler
($\keyword{handle}_l\;e\;h$), and lift ($\Lift{e}_l$) with a label $l$ from a
fixed set of labels $\mathcal{L}$.
As a result, we obtain sets of completely independent effectful operators for each label.
We would also need a notion of freeness per label,
which would naturally be reflected in the type system as having different rows of effects per label.\footnote{
	Alternatively: one row in which effects are tagged with labels and consecutive effects with different tags can be swapped using subsumption rules.
}
The typing rule for an effectful operation with label $l$ would only look at the row for $l$.
The numbers representing freeness in the logical relations would also have to be indexed by labels,
i.e., changed into
functions from labels to natural numbers.

Another common feature in languages with algebraic effects is grouping
multiple operations into one effect.
We argue that this is not a significant change and is not deeply related
to effects,
as it could be simulated if the language featured generalized algebraic data types (GADTs) with pattern matching.
If we want an effect $ε$ with operations $Δ'_i.\,op_i : τ_i \Rightarrow σ_i$,
we can define a GADT $e\;α$ with constructors $op_i : ∀Δ'_i.\,τ_i → e\;σ_i$
and set $ε = α::\kT.\, e\;α \Rightarrow α$.
A handler for this effect would have to pattern match on a value of type $e\;α$
to refine the type variable $α$.

Nevertheless, we can sketch how we could accommodate grouping operations into one effect natively.
We fix a set of operation names ranged over by $op$.
Effects are now sets of distinct operation names together with their types:
$$
	\inferrule
	{\textrm{for each }i ∈ \{1…n\} \\ Δ,Δ'_i ⊢ τ_i ∷ \kT \\ Δ,Δ'_i ⊢ σ_i ∷ \kT}
	{Δ ⊢ \{op_i : Δ'_i.\, τ_i \Rightarrow σ_i │ i ∈ \{1…n\}\} ∷ \kE }
$$
Handlers would take on the form $\Handle e\;\{op_1\;x\;r.\,e_1; …; op_n\;x\;r.\,e_n; x.\,e_r \}$
and $\Do v$ would be generalized to $op\;v$.
The typing rule for operations would also have to ``guess'' the other operations in an effect
(in the original rule it already guesses the types in the operation and a type-level substitution).
The rule for $\KwHandle$ would naturally need a suitable premise for each operation clause.

When we have both features and identify labels with effects (groups of operations),%
\footnote{
	Technically, effects are formed in type contexts. Therefore,
	we also forbid effects to have free type variables, so that they can be formed
	at the ``top-level'', where the set of labels is also fixed.
	This is similar to effects in \cite{hwc}.
	We also note that, with this restriction, effect rows could be represented
	simply as mappings from labels to natural numbers.
}
we arrive at a calculus very similar to the one in \cite{hwc}.
A crucial difference still remains: our effect types are structural.
In particular, effects cannot be recursive.
In the work cited it is conjectured that a restriction on recursive occurrences of effects would
make their calculus terminating.
Therefore, we claim that our method settles this conjecture positively.
The interpretations
of effects would be essentially the same as in the cited work (but unary)
and the definitions of $\E$ and $\S$ would be inductive as in this work.

We consider the language in \cite{hwc} to be a good representative
calculus for algebraic effects
– we want to stress that our normalization result is not just a
peculiarity of the calculus chosen.
In particular, it features polymorphism and allows duplicate instances of effects,
both of which are sometimes omitted in the literature.

\section{Related work}

One thing that was not mentioned about \cite{hwc}, where the interpretation of effects
and the relation on control-stuck terms come from,
is that their relation is {\em biorthogonal}
– there is an additional relation on (full program) evaluation contexts.
Their relation on expressions is defined extensionally:
an expression is ``good'' if it behaves ``well'' in all ``good'' contexts.
In our work, noticing that this is unnecessary led to simpler definitions and proofs.
More importantly, our intensional direct-style definition of good expressions leads to
better intuition, in particular, allows us to consider reduction traces.
However, opting for direct-style logical relations would possibly not simplify the work
in \cite{hwc} dramatically,
as the relations are binary.

A work which is eerily similar to ours, albeit in a very different setting, is \cite{marriage}.
To reason about program equivalence,
they define a relation $\E$ on expressions
and a relation $\S$ on stuck terms
by solving a recursive equation.
But the terms are ``stuck'' for a different reason:
they are applications to ``external'' functions about which we in a sense do not know enough,
a situation reminiscent of normal form bisimulations.
Furthermore, they interpret the recursive definition {\em coinductively},
i.e., as the greatest fixed point.

In our setting, a coinductive definition would theoretically allow
expressions in $\E⟦τ/ρ⟧_η$ to have reduction traces that are ill-founded,
i.e., contain infinite paths.
%i.e., some choices of operation return values would lead to nontermination.
The compatibility lemmas can be proven using strong coinduction\footnote{
	Strong coinduction is the principle that $X ⊆ F(X ∪ νF)$ implies $X ⊆ νF$,
	where $F$ is a monotone operator on a complete lattice and $νF$ is its greatest fixed point.
}
	at the type in the rule conclusion,
except for the one for $\KwHandle$.
The problem is that we substitute a resumption
(which contains a handler) for $r$,
but to show that it is in $⟦τ_2 →_ρ τ_r⟧_η$
we would need exactly the claim we are trying to prove in the first place.
The failure of $\KwHandle$ compatibility should not be very surprising,
as this is the rule responsible for eliminating effects –
in particular, it should be able to take
any expression in $\E⟦τ/τ_1 \Rightarrow τ_2 · ι⟧_η$ and show that wrapping it in a
suitable handler produces an expression in $\E⟦τ/ι⟧_η$, which cannot get
stuck and simply evaluates to a value of type $τ$.
This seems impossible,
as theoretically the expression's reduction trace could have no
leaves, so by definition of $\E$ the type $τ$ could be arbitrary.

We have found only sketches of normalization proofs for algebraic effects in the literature,
so we cannot be sure of how they work.
Such a mention appears in \cite{hia}.
We speculate that their proof might have
a combinatorial flavor, rather than use only logical relations.
This is because multiple such arguments appear in a paper they cite \cite{exrw} and
because of the mention that the handler is reapplied
on a strict subterm of the original computation during each handling reduction.
This is possible thanks to an unusual calculus,
where the operation carries a continuation alongside the argument
and there is a reduction that moves frames surrounding the expression to the continuation until
the operation is directly inside the handler.
It is feasible that such an argument could also work in our semantics by using
a suitable term size function.

A calculus with effect handlers appears with a mention of a termination proof in \cite{expressive}.
As it is even terser than the previous one, we cannot give any comment.

A mechanized proof of strong normalization for the calculus defined in \cite{expressive}
is reported in \cite{sol}.
A tool for proof search is used and the proof is not spelled out in detail,
but it also relies on combinatorial arguments and strikes us as more elaborate than ours.

We did not consider recursive effects, as they are known to introduce nontermination \cite{hwc}.
Likely, we could allow effects where all recursive occurrences are positive
– but note that
the left side of an effect arrow ($\Rightarrow$) is positive and the right is negative,
as opposed to function arrows ($→$).
Needless to say, a least fixed point construction would have to be used in the interpretation of effects.
This is discussed from the perspective of a translation into a System F-like calculus in
\cite{xie2020effect}.

The possibility of defining logical relations by solving fixed-point equations
has been known for a long time.
This is most natural when the language considered has features directly
concerning fixed points, such as (co)inductive types \cite{altenkirch, operfl}.
In different settings, this technique appears rare, and our work is one example.

% would the proof even work with biorthogonality?

\chapter{Implementation}

We will present an expository implementation of the language,
including a rewriting-based evaluator and an evaluator based on the proof in the previous chapter.
%and a type-checker.

One can see logical relations as interpreting the object language into a metalanguage.
Indeed, we have not been using the words ``interpretation'' and ``semantic'' baselessly.
In the previous chapter, our metalanguage was informal mathematics – set theory, we could say.
The proof was constructive and it should also be readily formalizable in a dependent type theory.
If we care only for the computational content of the proof, a simpler metalanguage will suffice –
we no longer have to consider proof terms with complex types but which are operationally unit types.
Here, we will use the OCaml language.

\section{Syntax and rewriting-based evaluator}

To be faithful to the presentation in \autoref{chap:language},
we use a representation with named variables (rather than de Bruijn indices
or higher-order abstract syntax).
For simplicity, we do not have a separate type for values.

\lstinputlisting[linerange={1-14}]{syntax.ml}

\lstinputlisting[linerange={16-25}]{syntax.ml}

We define evaluation contexts as lists of evaluation context frames
(the hole is at the front)
and define a function for calculating freeness:

\lstinputlisting[linerange={3-24}]{step.ml}

We implement decomposing terms into evaluation contexts and redexes:

\lstinputlisting[linerange={26-51}]{step.ml}

Finally, we can implement reductions and multi-step reductions:

\lstinputlisting[linerange={52-57}]{step.ml}

\lstinputlisting[linerange={59-67}]{step.ml}

\section{Evaluator based on the proof of termination}

Now, we demonstrate the computational content of the proof of termination.
The code may appear simpler than the code performing multi-step reductions,
in part because we leverage
the metalanguage's features to realize the object language's features.
For instance, functions are realized as OCaml functions and
we do not have to consider variable binding ourselves.

First, we define analogs of the interpretations
of values and the relation $\E$.
We can see that effect types do not play a role in computation.

\lstinputlisting[linerange={3-6}]{eval.ml}

Now, we define functions which closely follow the compatibility lemmas:

\lstinputlisting[linerange={8-33}]{eval.ml}

We finish by performing something akin to a fold on the syntax tree.

\lstinputlisting[linerange={35-45}]{eval.ml}

Because OCaml functions are opaque,
we cannot observe much using this function.
To test that it is adequate,
we could add integers to the language.
Then, we will have an integer constructor of \texttt{goodval},
and we can compare outputs with the rewriting-based evaluator.
We omit these straightforward modifications.

Our proof relied on the type system, yet here
types (of the object language) are nowhere to be seen.
This evaluator is only guaranteed to work if
the term is typeable.
It is not hard to find a term on which it disagrees with our
operational semantics:
$$\Handle (\Do v)\;Ω\;\{x,r.\,x;x.\,x\},$$
where $Ω$ is a nonterminating term, for instance $(λx.\,x\;x)\;(λx.\,x\;x)$.
(Such a term is untypeable, as we have proven.)
The semantics are left-to-right, so in this program an effect will be performed
and the handler will just return the value, ignoring the resumption.
Evaluation will never reach the $Ω$.

Contrarily,
the evaluator extracted from the proof will walk this term and try to recursively evaluate subterms.
In particular, it will try to evaluate $Ω$, where it will loop forever.

We leave it for future work to determine if this evaluator
can form part of a normalization by evaluation algorithm,
i.e., if there exists a function \texttt{reify : goodexp -> exp}
that can reconstruct a term in normal form given
its semantics.
%Such that \texttt{eval (reify x) = x}.

\hfuzz=1pt
\printbibliography[heading=bibintoc]

\end{document}