Gradual Typing for Effect Handlers
Max S. New

Computer Science and Engineering
University of Michigan

Eric Giovannini

Computer Science and Engineering
University of Michigan

Daniel R. Licata

Mathematics and Computer Science
Wesleyan University

We present a gradually typed language, GrEff, with effects and
handlers that supports migration from unchecked to checked effect
typing. This serves as a simple model of the integration of an
effect typing discipline with an existing effectful typed language
that does not track fine-grained effect information. Our language
supports a simple module system to model the programming model of
gradual migration from unchecked to checked effect typing in the
style of Typed Racket.

The surface language GrEff is given semantics by elaboration to a
core language Core GrEff. We equip Core GrEff with an inequational
theory for reasoning about the semantic error ordering and desired
program equivalences for programming with effects and handlers. We
derive an operational semantics for the language from the equations
provable in the theory. We then show that the theory is sound by
constructing an operational logical relations model to prove the
graduality theorem. This extends prior work on embedding-projection
pair models of gradual typing to handle effect typing and subtyping.

§ INTRODUCTION

Gradually typed programming languages are designed to support smooth
migration from a lax to a strict static type
discipline <cit.>. Most commonly, gradually
typed languages add a static type system to an existing dynamically
typed language and allow for (1) safe interoperability between the
languages and (2) semantic guarantees that adding types to existing
programs only results in stricter type enforcement, and no other
behavioral change. More generally, gradual typing has been
applied to provide a spectrum of precision in other kinds of typing
disciplines such as refinement typing or effect
typing <cit.>, where the “dynamic”
side is a statically typed language itself.

One particular presentation of effects and effect typing that is
gaining popularity is effect
handlers <cit.>. Operationally, effect
handlers are resumable exceptions, code can "raise" an effect
operation, which will then be handled by the closest enclosing
handler, which in addition to the exception data will also receive the
continuation for the raising code that can be invoked to resume at the
original point where the effect was raised. Effect handlers provide an
intuitive typed interface to delimited continuations, and can
similarly be used to conveniently implement backtracking search,
non-determinism, mutable state, and as a convenient interface to
external system calls.
Effect handlers have been implemented in a number of libraries and
experimental languages, and more recently have been incorporated as a
built-in feature into OCaml 5, and have been proposed as an extension
to WASM

Designers of languages supporting effect handlers, much like designers
of languages with exceptions, are left with a choice of whether the
type system should merely validate that the input and output types of
effect operations are respected, or if an effect typing system
should be employed to determine that a particular effect can only be
raised when the context is known to implement a handler for it.  On
the one hand, checked effects allow programmers to easily reason about
which effects can be raised by subprocedures and ensure they are
handled appropriately, rather than being caught by the runtime system
and causing the program to crash.
On the other hand, strict checking may necessitate large code changes
when code is extended to raise new operations, and even in languages
such as Java that support both checked and unchecked exceptions,
unchecked exceptions are preferred in many scenarios.
Furthermore, when adding effect typing to a language that does not
already support it, even correct existing libraries may not typically
pass the necessarily conservative static type checker. It may be
infeasible to rewrite large amounts of existing library code to
precisely track effect usage.
Gradual typing provides a linguistic framework for designing languages
where a programmer is not entirely locked in to one system or another:
they might use unchecked exceptions in one module and checked
exceptions in another, while supporting well-defined interoperability
with useful error messages at runtime if there is an effect raised in
a context where it is not expected. Further, a gradually typed
language provides a path for gradually migrating code from
less precise to more precise static type checking.
This potential for gradual typing to be used in this way to
incorporate effect typing disciplines into existing languages has been
eloquently pdiscussed in prior work by Phil Wadler <cit.>.

In this work we present the design and semantics of GrEff, a gradual
language with effect handlers that supports gradual migration from
unchecked effects to precise effect typing.

The untracked sublanguage of GrEff is designed to be similar to SML
and Java's treatment of exceptions: new effect operations are declared
with specified input and output types, and these can be imported and
used to raise and handle those operations in other modules, but which
effects are raised by a function is not tracked by the type system.

In addition, GrEff supports tracked function types $A \effto \sigma
B$ where the input values must be of type $A$, output values will be
of type $B$, and the function may raise any of and only the effects in the
set $\sigma$.

The untracked function type is modeled then as a type $A \to_{\dyn} B$
which has a “dynamic” effect type, in the sense that it may raise
any effect, possibly including unknown effect operations declared in
some independent module of the program.

Since our main focus in this work is on providing a foundation for
extending existing statically typed languages such as OCaml 5 with
effect types, we have chosen not to support full dynamic typing in the
design of GrEff. However, the design should easily accomodate
supporting fully dynamic value typing in addition to the dynamic
effect typing using standard gradual typing techniques.
We note that

In GrEff, new effect operations can be declared in each module, just
as new exceptions can be declared in Java and ML-style languages.

When an effect is declared in a module, it is given an
associated request and response type.

For instance, an effect for reading a boolean state would
be , the user provides a trivial value
as the request and receives a boolean value as the
response, while an effect for writing to boolean state would
be .

Similar to ML and Java, GrEff takes a nominal approach to
effect operations: each effect operation has an associated request and
response type that are used to determine when an effect is properly
raised or handled.

However, having a single, global assignment from effect names to
request/response types is problematic from the perspective
of gradual migration from untracked to tracked effects.

In a completely nominal form of effect typing, if an effect operation
is used in many different modules with imprecise typing, and one
module is migrated to use a more precise version of the effect's
request/response type, then we would need to migrate all modules to
use the more precise type.

Instead, gradual migration should allow for this to be done a single
module at a time.

To achieve this, in GrEff, we take a locally nominal but
globally structural approach to the typing of effect operations.

That is, locally, within each module, the request and response
type for an effect are fixed, and all
and  constructs are checked with the same typing.

On the other hand, globally, different modules across the
program can associate different types to the same effect operation.
At module boundaries, i.e., imports and exports, modules are
statically allowed to interoperate if they agree on the precisely
typed portion of the effects they share. If one module is more precise
than the other, then dynamic runtime monitoring is inserted in the
implementation to ensure that the runtime behavior agrees with the
static typing, raising an error if the dynamically typed code violates
the imposed runtime type discipline.

There are two aspects in designing a sound gradually typed
language: designing the syntax and gradual type checking of the
surface language and designing the corresponding core language and
semantics. The syntax should support a simple process for migrating
from an imprecise to a precise style, satisfying the
static gradual guarantee <cit.>.

We designed the surface language with the goal of modeling program
migration from static to dynamic typing. For this reason we include a
simple module system in the style of Typed
Racket <cit.> so that we can express that different
portions of the program have different views on how the effect
operations are typed. Once the base language is designed, the gradual
type checking is based on prior work on defining gradual type systems
that satisfy the static gradual guarantee<cit.>.

Next, the core language provides a definition for
the runtime semantics. The semantics should admit useful type-based
reasoning principles for precisely typed code, even in the presence of
interaction with imprecisely typed components. Further, the
aforementioned migration process should have a predictable impact on
program semantics: migrating from to more precise checking may result
in new errors being identified (statically or dynamically), but
otherwise should not impact program behavior, a property known as
the dynamic gradual guarantee
or graduality <cit.>.

To design the core language and runtime semantics, we follow the prior
work (<cit.>) which established a recipe
for designing a new gradual core language to satisfy the graduality
theorem and validate strong type-based equational reasoning

Their approach is to axiomatize the type-based reasoning
principles as equations and the graduality theorem as inequalities,
where casts are defined not by specifying their operational
behavior a priori but instead by assuming they are given by
least upper bounds/greatest lower bounds.

Then the operational behavior of the casts can be derived from
the inequational theory.

An operational or denotational model must then be constructed to prove
the theory is consistent, which implies the graduality theorem.

But since the operational semantics is derived from the
inequational theory, this also establishes a stronger theorem that the
observable behavior of the casts is uniquely determined by the
desired type-based reasoning and graduality, showing that any
observably different cast semantics must violate one or more of the

For designing our core language, called Core GrEff, we extend this
recipe, which previously has only been demonstrated on simple types, to
apply also to effect casts and subtyping of value and effect

We then show that every rule of an operational semantics is derivable
from the least upper bound/greatest lower bound specifications of
casts as well as congruence rules and an effect forwarding
principle for handlers.

The effect forwarding principle states that a handler clause that
simply re-raises the effect it handles with the same continuation can
be removed without changing the observable behavior of the system, an
intuitive principle as well as a highly desirable compiler

In this work, we extend prior step-indexed logical relations models
for proving graduality to handle effects and subtyping, by showing
that the runtime casts satisfy the properties of
being embedding-projection pairs <cit.>. In doing
so, we show how to combine effect and value embedding-projection pairs
within the same system, and how they interact. Additionally, we
identify new semantic principles for the interaction between subtyping
and runtime casts.

The contributions of the paper are as follows:

* We define a gradually typed language GrEff supporting migration from
unchecked to checked effects and handlers.

* We prove this language satisfies the static gradual guarantee and the
dynamic gradual guarantee (graduality).

* We give the language a semantics by elaboration into a core
language, core GrEff.

* We axiomatize the desired graduality and program equivalence
properties of the core language by giving an inequational theory. We
then derive from this an operational semantics by orienting certain
equations in the theory, showing that the operational behavior is
derivable from the graduality and extensionality principles.

* We prove type soundness and graduality by constructing a logical
relations model, extending prior work on embedding-projection pair
semantics to effects and subtyping.

§ OVERVIEW OF GREFF

Before discussing the syntax and semantics of GrEff, we provide an
informal introduction to its features and how it supports a gradual
migration from unchecked to checked effect handlers.

As an example, consider the implementation of a simple threading
library using effect handlers. We start with a system using unchecked
effect types in an ASCII syntax in Figure <ref>.

We split this program across three modules: first, a module
defines the effects we will be using in our other
modules. These are the effects that the threads use:  for
displaying output so that we can observe the interleaving of threads,
, which yields back control to the scheduler, and most
importantly, , which allows for a thread to spawn new
threads. Each effect declaration  is
annotated with two types: the type of requests to the ambient
handler, and the type of expected responses from the ambient
handler. For instance, the request type for print is a ing
to be printed, and the response is unit. In a more realistic setting,
the response type might be a boolean to say if the printing succeeded,
or an unsigned integer to say how many bytes were succesfully
printed. For yield, the request and response are both unit. For fork,
the response type is again unit and the request type is a thunk
where the $\dyn$ is the type of effects the
function may raise when called. In this case, $\dyn$ indicates the
thunk might raise any effect.

GrEff Threading Program with Imprecise Types

GrEff Threading Program with Precise Typing

Next, module  defines a round-robin scheduler as a
handler for the provided effects. For simplicity the implementation
relies on some built-in queue implementation, and shallow handlers, a
simple extension to our formalism which uses the more complex deep

Finally, we have the  module, which uses the scheduler
defined in the  module with a thunk that uses the
effects defined in the  to implement a program that
prints a simple message using threads whose output will depend on the
scheduler's behavior.

The imprecision of the effect typing in this program means that
programmers have to rely on documentation or understanding of the code
to understand what effects might be raised when they import a function
from another module. With effect typing, this information can be
expressed precisely using effect annotations on the functions

For instance, in the declaration of the  operation, the
request is a thunk that when launched as a thread itself may raise
further effects such as manipulating shared state, ing
to other threads, or ing additional threads. However with
imprecise effect tracking, the  procedure has the
uninformative type  so we cannot specify
in the type which operations the scheduler will handle and which it
will propagate forward.

GrEff allows as well for the introduction of precise effect
types to express these choices in the type structure.

In figure <ref>, we show a fully precisely typed
version of the same threading program (with implementations, which are
unchanged, now elided).

This allows us to specify in the  module that the
scheduler expects threads that can (1)  a string, (2)
to the other threads and (3)  further
threads with the same effects. To express this, the scheduler module
changes the type to
expressing that the scheduler will be passed a thunk that may ,
or , but will itself return a string without raising any
effects. Additionally, we can express that forked threads
should only raise these three effects as well. This is expressed by
annotating the import statement, which defines fork as a
recursive[though recursive effect types are natural here, we
do not support them in our core language and leave this extension to
future work] effect type whose response type is trivial and whose
request type is that of thunks that can raise the three provided

This typing will then be used by all occurrence of the fork effect, in
raise or handlers, within this module.

The types are also changed in the main module, where the
thunk can be given a type expressing it only prints
and yields, whereas  thunk only forks and prints.

These are compatible with the types in scheduler using an effect
subtyping that allows functions that use fewer effects to be used in a
context that can handle more.

Since GrEff is a gradual effect language, a programmer who
started with the imprecise program does not need to fully type the
entire program before running it. Instead, the programmer can
gradually migrate from the imprecise style to the more precise
style, for example one module at a time. In fact, any of the $2^3=8$
combinations of the imprecise versions and precise versions of the
three modules presented here will pass the GrEff gradual
type-and-effect checker.

For instance, we might start with adding precise effect typing to the
module to specify the effects that a forked thread
can have.

Whereas in a non-gradual type system, this would require changing the
consumer modules to use the more precise typing, in GrEff, the import
statements allow for the uses within the module to continue to use the
imprecise typing, and at the module boundary it is checked that the
precise components of the declared type for the  effect
match the precise components of the declaration in the defining

On the other hand, we can keep the  module
imprecisely typed, and instead add typing to the
module first. This is again unusual compared to a conventional typed
language, we have declared a nominal data type in one module, but use
it at a different type in a client module. The import statements allow
for the gradual migration of the client code without changing the
original library.

The module system plays a crucial role in allowing for the programmer
to independently choose between migrating the declaration site of the
nominal datatype and its uses. If we were in a purely
expression-oriented language, then any change to the module
declaration, even in a gradual language, would change the typing of
the uses of the operation. Here we use the module boundaries in the
style of Typed Racket as a way to formally specify different
expectations of what the type of the nominal effect operations should
be in different portions of the codebase.

§ SURFACE AND CORE GREFF

In this section, we introduce the syntax and typing of GrEff along
with its elaboration into a core language, Core GrEff.

GrEff includes a module system and nominal effect operations, as well
as a gradual type checking algorithm that allows for a mix of dynamic
and static effect tracking.

Core GrEff, on the other hand, is a simpler expression language with a
declarative type system where all gradual type casts (but not
subtyping) are explicit in the term.

The high-level features of GrEff are elaborated away into core GrEff.

Because Core GrEff is simpler, we describe its syntax and typing
first, and then describe GrEff and its type-checking/elaboration

§.§ Syntax and Typing of Core GrEff

We give an overview of the Core GrEff syntax in
Figure <ref>.

Core GrEff expression syntax include typical lambda calculus syntax
for variables, let-bindings, functions and booleans.

Additionally, there is a term $\err$ that represents a runtime error produced by a failed cast

Next, it includes forms for raising an effect operation $\raiseOpwithM
\effname M$ and handling effect operations $\hndl M x N \phi$. The
handler includes a clause $\kw{ret} x. N$ to handle a return value for
$M$ as well as clauses for handling effects $\phi$. Abstracting from
syntactic details, $\phi$ is modeled as a finitely supported partial
function (written $\parfin$) from effect names to terms, which all
have two free variables $x$ and $k$ for the payload of the effect
raised and its continuation. That is, if syntactically a handler has a
clause $\effname(x, k) \mapsto N_\effname$, we model this by having
$\phi(\effname) = N_\effname$.

Next, Core GrEff includes four explicit gradual type cast forms:
downcasts ($\dncast A B M$) and upcasts ($\upcast A B M$) for value
types, as well as analogous casts for effect types ($\dncast \sigma
\tau M$ and $\upcast \sigma \tau M$).

Finally, we include a term $\err$ that represents a runtime cast

The value types $A, B, C$ classify runtime values: in this simple
calculus, just booleans and functions, where functions are typed with
respect to a domain, codomain as well as an effect type $\sigma$ which
classifies what effects the function may raise when it is called.

The effect types are either $\dyn$ to indicate dynamically tracked
effects, or a concrete effect type. A concrete effect type says which
effect names $\effname$ can be raised, and when they are raised, what
is the type of the request $A$ the raising party provides and what is
the type of responses $B$ with which the handling party can
resume. Abstracting from syntactic details, this is defined to be a
finitely supported partial mapping from names to pairs of value types
(i.e., an element of the cartesian product $\text{ValueType}^2 =
\text{ValueType}\times\text{ValueType}$). To model that an effect
$\effname$ can be raised with request type $A$ and response type $B$
we would define $\sigma_c(\effname) = (A, B)$, which we will notate
more suggestively as $\effarr \effname A B \in \sigma_c$.

As shown in Section <ref>, programs declare which effect names
can be used, and with which associated request and response types.

To track this information in typing core GrEff expressions, we type
check all GrEff expressions against a Signature $\Sigma$ which
associates a pair of non-tracking types to each name. By a
non-tracking type, we mean a value types that only use $\dyn$
effect types.

Additionally, expressions are type-checked with respect to an ordinary
typing context $\Gamma$.

Finally, we define typical notions of value and evaluation context to
encode a call-by-value, left-to-right evaluation order.

Most notably, all casts are evaluation contexts, and function casts
are values, i.e. “proxies” that delay type enforcement until an
application is performed.

The use of non-tracking types in the signature is a design decision in
the semantics of GrEff: it means that when an effect is declared in a
module, it fully specifies only the non-effect typing portions of the
request and response types.

When a module imports an effect, it is only checked that the new
request and response type are consistent with the exporting
module. Since effect types can be re-exported and the consistency
relation is not transitive, this means that in general the types used
in one module will not be consistent with those of the module where it
was originally declared.

However, transitive closure of consistency does ensure that the
types have the same non-tracking portion, and so it is sensible to
define the valid instances of the effect type to be any that agree on
this non-tracking portion of the type.

An alternative would be for the signature to have a fully specified
type and limit all uses of the effect to be at least as precise as the
original declaration. However we argue that this is not in the spirit
of gradual typing: for instance it might be the case that module $P$
provides an effect declaration, module $I$ is an
intermediate that re-exports the effect and module $C$ is a
client of $I$ that uses the effect but does not directly
interact with $P$.

Say $P,I,C$ all initially use untracked effects, but then $C$ becomes
typed and so specifies precise effect typing for the effect.

The program functions properly and eventually $P$ is additionally made
more precise but in such a way that the effect implementation is
incompatible with the usage in $C$. In GrEff this does not lead to a
static error, because $C$ and $P$ are not directly communicating along
a precisely typed interface, but rather through an intermediary $I$
that uses imprecise typing. Indeed, it may be the case that $I$ uses
the effect differently between $C$ and $P$ and there is no runtime
type error. However, if $I$ becomes precisely typed, it must specify
its interpretation of the effect and will result in a static error
with either $C$ or $P$.

Terms  M,N    ::=    x λx. M M  M' M N N

M x N  M M x N ϕ

A B M A B M στ M σ τ M

Handler clause  ϕ    ∈    Name ⇀_fin Term

Value Types  A,B,C    ::=    A σB

Effect Types  σ,τ   ::=    σ_c

Concrete Effect Types  σ_c    ∈    Name⇀_fin ValueType^2

Signature     ∈    Name⇀_fin NonTrackingType^2

Non-tracking Types  A_   ::=    A_→_ A_

Typing Contexts  Γ    ::=     ·Γ, x : A

Values  V    ::=    x λx:A. M

A' σ' B'A σ BV A' σ' B'A σBV

Evaluation Context  E     ::=     ∙A B E A B E στ E σ τ E

E E x N ϕE M V E

E N_t N_f E x N

Core GrEff Syntax

Next, we present declarative term typing rules in
Figure <ref>.

The main judgment $\Tmhasty M A$ says that under the assumptions
$\Gamma$, $M$ can raise effects drawn from $\sigma$, and produce a
final value of type $A$.

We follow the convention that whenever we form the judgment $\Tmhasty
M A$ we must already have established that the types in $\Gamma, A,
\sigma$ are well-formed under the signature $\sig$.

First, we include a subsumption rule for value and effect
subtyping, which we will soon define.

The rules for value forms (variable, booleans, and lambdas) all have
an arbitrary effect type $\sigma$ because they do not raise any effects

The runtime cast error $\err$ can be given any value or effect type.

The let, application and if rules simply require that all the
sub-terms use the same effect type, though subsumption can be used to
combine effects.

The raise rule says that the effect being raised needs to be in the
current effect type and the payload of the request must also have the
same effect type.

Next, the rule for typing a handler works as follows. First, the
output value type is $B$ and output effect type is $\tau$, while for
the scrutinee $M$ the corresponding types are $A$ and $\sigma$. First,
we check that the return clause $N$ has the same output types as the
handler overall, when its input $x$ has the type of the output of
$M$. Next, for each effect operation $\effarr \effname
{A_\effname}{B_\effname}$ raised by $M$, either the effect is not
handled by $\phi$, in which case it must be included in the final
effect type, or it is handled by $\phi$. If it is handled by $\phi$,
then the clause $\phi(\effname)$ must be well typed with a request
value $x: A_\effname$ and a continuation that takes responses and has
output effect and value types that match the term overall $k :
B_\effname \effto \tau B$.

Lastly, we include the rules for type and effect upcasts and
downcasts. Whenever a type precision relationship $A \ltdyn B$
holds (to be defined), we get an upcast from the more precise
type $A$ to the more imprecise type $B$ and a corresponding downcast
from $B$ to $A$.

σMA ⊢A B ⊢στ

Γ(x) = A
x A

Γ, x : AτMB
Γσλx . MA τB

M A

Γ, x : AσNB
M x N B

σMA →_σB

σM  NB

σN_tB σN_fB
M N_tN_f B
σMA ϵ@ A B ∈σ
σ(ϵ@ A B) M B

σM A

Γ, x : A τN B

(∀(A_B_) ∈σ.
(∉(ϕ) ∧(A_B_) ∈τ)

∨(Γ, x:A_, k:B_τB τϕ() B))

τM x N ϕ B

M A A B
A B M B

M B A B
A B M A
σ M A σσ'
σ' σσ' M A
σ' M A σσ'
σ σσ' M A

Core Greff Typing

Finally, finishing out the syntax, in Figure <ref>,
we define three judgments on types: well-formedness, subtyping and type precision.

Well-formedness $\sig \vdash A$ and $\sig \vdash \sigma$ checks that
the types used in effect operations erase to the types associated in
the signature. Here we use the notation $\lceil A\rceil$ to mean the
erasure of effect typing information in that we replace any effect
type subterms $\sigma$ with dynamic $\dyn$.

Subtyping works as usual for booleans and functions, contravariant in
domain of the function type, but covariant in the codomain and effect.

Subtyping for effect types includes both a width subtyping
aspect: a smaller type can raise fewer operations, as well as a
depth aspect that is covariant in the request type and
contravariant in the response type. This variance makes sense
from the perspective of the party producing the request, to
match the function type subtyping.

Finally, type precision $A \ltdyn B$ tracks instead how “dynamic” or
“imprecise” a type is.

For functions it is covariant in every argument, and for effect types,
the dynamic effect is the most imprecise and for two concrete effect
sets, it has a depth rule that that is covariant in request and
response positions. In a more standard gradual language with full
dynamic typing, in addition to the dynamic effect type we would have a
dynamic value type $\dyn_v$ that is similarly maximally imprecise
among value types.

⊢⊢A ⊢σ⊢B
⊢A σB⊢∀A B ∈σ_c.

(|A||B| ∈). ∧⊢A∧⊢B)

A' A σσ' B B'
A →_σ B A' →_σ' B'
∀A_σ B_σ ∈σ_c. ∃A_τB_τ ∈τ_c.

σ_c τ_c

A A' σσ' B B'
A σB A' σ' B'

σ (σ_c) = (σ_c')

∀A B ∈σ_c. ∃A'B' ∈σ_c'.

A A' ∧B B'

σ_c σ_c'

Well formed types and effects, Type and Effect Precision

§.§ Syntax and Elaboration of GrEff

Programs  P     ::=     L; ⋯  L_main

Value Types  A,B,C    ::=    A σB

Effect Types  σ,τ   ::=    σ_s

Operation Set  σ_s,τ_s    ∈    𝒫_fin(Name)

Values  V    ::=    x λx:A. M

Terms  M,N    ::=    x ε M C σ M x N ϕ

λx. M M  M' M N N

M :: A M :: σ

Handler clauses  ϕ    ∈    Name ⇀_finTerm

Modules  L     ::=     module m   { b }

Module Body  b     ::=     ·D; b

Main Module  L_main     ::=     main { b; M }

Module reference  r     ::=     m.x m.

Declaration  D     ::=
r A B A B

x V r x A

Program Typing Contexts  Δ    ::=     ·Δ, x ↦Γ_s

Module  Typing Contexts  Γ_s     ::=     ·Γ_s , ε: A B Γ_s, x : A

GrEff Syntax

We present the syntax for the surface language GrEff in
Figure <ref>.

A GrEff program $P$ consists of a sequence of modules ending in a
single “main” module.

Each module $m$ consists of two parts: first, the effect definitions
and then the value definitions, whose types annotations may use the
effects previously defined in that module.

An effect definition is either a declaration of a new effect operation
$\neweffEofReqtoResp \effname A B$ or an import of an existing effect
operation $\importeffXatYtoZ {m.\effname} A B$. In either case, the
declaration includes the request type $A$ and the response type $B$ of
the effect.

An effect import brings an effect defined in another module into the
current scope, but with a possibly different request and response
type. To support gradual migration, these types are allowed to
have a different level of precision than the original, but where both
are precise they must match.

After the effect declarations are the value definitions which are also
either a definition of a new value $\defXtobeY x V$ or an import
of a value declared in a different module at a possibly different type
$\importvalXasYatZ r x A$.

For simplicity, all effects and values are public and can be imported
by later modules.

Finally a program ends with a main module, which consists of the
same kind of effect and value declarations, followed by a final main

Δ·b ' γΓ

ΓM_s M σA
Δmain b  M_s ' γΓ M σA
Δ·b ' γΓ

,' Δ,m↦Γ P ” M σA
Δmodule m b;  P ',” γΓ M σA

ε∉ΓA_s AΓB_s B

ΔΓεA_s B_s (ε@ ⌈A⌉⌈B⌉) ·ε@ A B

ΔΓD ' γ'Γ'

,'Δ Γ,Γ' b ”γ”Γ”

ΔΓD; b ',” γ',γ” Γ',Γ”
Δ(m) ∋ε@ A' B'ΓA_s AΓB_s B

A ∼A'B ∼B'

ΔΓm.ε A_s B_s ··ε@ AB

ΓV_s V ∅A
ΔΓx V_s ·V/x x:A
Δ(m) ∋x:A'ΓA_s AA' A

ΔΓm.x y A_s ·AA'x/y y:A

GrEff Typing/Elaboration, Module Language

A B M = A⌈A⌉B⌈B ⌉MστM = στ M

Γx x ∅A

ΓM_s M σA'ΓA_s AA' A

ΓM_s :: A_s AA' M σA
ΓM_s M σ' AΓσ_s σσ' σ
ΓM_s :: σ_s σσ' M σA

ΓM_s M σ_m ΓN_s N σ_n BΓN_s'N'σ_n' B'

C = B B'σ= σ_m σ_nσ_n'
ΓM_s N_sN_s' σσ_mM σσ_nC B Nσσ_n'C B' N' σ

ΓA_s AΓ, x:A M_s M σB

Γλx:A_s. M_s λx. M ∅A →_σ B
ΓM_s M σ_m A →_σ_o BΓN_s N σ_n A'

A' Aσ= σ_m σ_n σ_o

ΓM_s N_s (σσ_mM)(AA'σσ_n N) σB

ΓM_s M σ_m A'Γ∋ε@ A BA' Aσ= σ_m {ε@ A B }

ΓεM_s σσ_m M x σ{ε@ A B }εA A' x σB

ΓC_s CΓσ_s σΓM_s M σ_m A_m

Γ,x:A N_s N σ_n C_n σ_n σC_n C

(ϕ_⇐) = (ϕ_s) Γσ_mσ(ϕ_s) σ_m'

(∀∈(ϕ_s).  ∃(@ A_B_) ∈Γ.

Γ, x : A_, k : B_σ C ϕ_s() N_ σ_C_

σ_σC_C ϕ_⇐() = σσ_CC_N_)

Γσ_sC_s M_s x N_s ϕ_s
σ_m' σ_m M x σσ_n CC_nN ϕ_⇐

(σ_c) ⊆(τ_c) ∪σ_s
Γσ_cτ_c σ_s τ_c ∪Γ(σ_s)

Γτ_c σ_s τ_c ∪Γ(σ_s)

Γσ_c  σ_s σ_c|_σ_s ⊎⌈Γ((σ_c) - σ_s)⌉

GrEff Typing/Elaboration, Expression Language

Next, we present the elaborator from GrEff into core GrEff, which also
serves as the type checker.

We view GrEff programs as essentially a description of an effect
signature $\sig$ and a closed expression well-typed under that

The module system is a way to manage the declaration of new effect
operations in the signature and a way to manage the typing of effect
operations by giving nominal associations to request and response
types rather than solely the structural typing in core GrEff.

We describe the elaboration of the module language in
Figure <ref>.

The top-level judgment $\elabprog \sig \Delta P {\sig'} M \sigma A$
says that under the starting signature $\sig$ and previously defined
modules $\Delta$, we can elaborate $P$ to a term $M$ with effect type
$\sigma$ and value type $A$ that is well-typed under the extension of
the signature by $\sig'$. To elaborate a complete program, we
initialize this with empty signature and module typing ($\elabprog
\cdot \cdot P \sig M \sigma A$).

This expresses that not only does a program denote a core GrEff
program, but it also has a “side effect” of allocating new effect
names $\sig'$.

A module is elaborated with the judgment $\elabmod \sig \Delta \Gamma
b {\sig'} {\gamma'} {\Gamma'}$. The outputs of this judgment are the
newly allocated effects of the module $\sig'$, the names of effect
operations and types for values the module defines $\Gamma'$ and the
definitions of all the values the module defines, given as a
substitution $\gamma'$ from names in $\Gamma'$ to terms of their
associated types.

Then to elaborate a program consisting of several modules, first you
elaborate the modules and then elaborate the remainder of the program
and finally combine the two by let-binding all of the names declared
in the module, which we write as a shorthand $\letXbeboundtoYinZ
\gamma {\Gamma} M$. Note that though $\Gamma$ contains both variables
and effect declarations, the effect declarations are unused in this
part of the elaboration.

A module is elaborated by combining the results of elaborating each

A new effect declaration checks that the name is not previously
declared, and then recursively elaborates the syntactic types declared
for request and response and then adds these to the allocated effects
as well as the local effect names declared in the module.

When adding to the signature, we take erasure of the types
because signatures use untracked types.

Next, to import an effect from a different module, the types given for
the effect are checked to be compatible with the types declared in the
other module. Note that for simplicity of presentation, all effects
must be used with the same name in all modules. More flexible renaming
mechanisms can easily be supported in a realistic implementation.

Here the compatibility judgment $A \sim A'$ is defined as the
conjunction of gradual subtyping in both directions, $A \gsubty A'$
and $A' \gsubty A$, to be defined soon.

This ensures that any imports from that module using this effect name
will succeed. We check gradual subtyping in both directions, as the
effect may be used in both postive and negative positions in a later

This effect name is added to the local names only, and not the
signature, because it is using an already allocated effect name.

Next, defining a value simply elaborates the value and adds its type
to the output typing and associates the value to that name.

Importing a value is similar, except that we check that the declared
type is a gradual subtype, and so can be coerced by the cast
$\obliqueCast {A} {A'}$, whose definition will be described shortly.

Next, we define the elaboration of the expression language in
Figure <ref>.

The judgment $\elabtm \Gamma {M_s} M \sigma A$ says that under the
typing of names given by $\Gamma$, the GrEff expression $M_s$
elaborates to the core GrEff function $M$, which will be well-typed
with inferred effect type $\sigma$ and value type $A$.

All forms essentially elaborate to similar forms in core GrEff, but
with suitable casts inserted.

First, we define the translation of value type casts $\obliqueCast
{A}{B} M$ and effect type casts $\obliqueCast \sigma \tau M$ as an
upcast followed by a downcast.

For the effect cast, these casts go through the dynamic effect type,
but for two value types there is no single most dynamic effect type so
we again use the erasure operation.

Note that this will only be well-typed in case $\lceil B\rceil =
\lceil A\rceil$, which is ensured whenever $A \gsubty B$, which is a
precondition for inserting a cast.

This is not necessarily the most efficient implementation of the cast,
we discuss optimizations in Section <ref>

Next, variables, boolean values and function values elaborate to
themselves with an empty effect type $\emptyset$.

The let-binding form shows how different effect types are combined:
the effect types of $M$ and $N$ are combined using a gradual join
$\gjoin$, and casts are inserted into $M$ and
$N$ to give them this effect type.

The gradual join acts as the join on precise parts of the type, but
extended such that $\sigma \gjoin \dyn = \sigma$.

The ascription forms simply check that the appropriate kind of type
satisfies a gradual subtyping judgment and inserts a cast.

This uses the elaboration of types $\elabty \Gamma {A_s} A$, defined

The if rule checks that the condition has boolean type and gives the
output value type as the gradual join of the branches, and the output
effect type as the gradual join with the condition expression as well,
matching prior work <cit.>.

The application rule is similar except that the argument is cast to
have the type of the domain of the function and the effect type of the
function is joined with the effect types of the terms.

Next, we have the raise form, which elaborates to a raise but first
let-binds the request term and casts the raise term to have an effect
type that is the join of the request term's effect type and the
operation's type.

Finally, we have the most complex case, the handle form.

The handle form elaborates to a handle form in the core language with
casts inserted in each case to make them agree with the ascribed value
type $C$ and effect type $\sigma$.

The request variables and input to the continuations are given by
looking up the effect in $\Gamma$, while the output is given by the

The most complex part of this elaboration is the cast needed for the
scrutinee $M$. In the core language, we need that all of the effects
that $M$ raises but are not caught by the handle are in the
output type $\sigma$.

But when $\sigma$ is dynamic and $M$ has concrete effect type or
vice-versa, this is not necessarily true, so in these cases a cast
must be inserted that effectively handles all of the “other” effects.

This definition is given below in a special elaboration of handle
scrutinees $(\elabHandleType \Gamma {\sigma} {\tau} {\sigma_s}
{\sigma_o})$. Here, the type $\sigma$ is the elaborated type of the
scrutinee, $\tau$ is the elaborated type of the result of the handle
expression, and $\sigma_s$ is the set of effects caught by the
handler, where we write $\Gamma(\sigma_s)$ for the map that looks up
the currently associated types for each operation in
$\sigma_s$. First, if $\sigma$ and $\tau$ are both precise collections
of effects, then we check that all of the effects it raises are either
caught or still occur in the output type, and we insert a subtyping
cast. Second, if $\sigma$, the type of the scrutinee is imprecise,
then we downcast it to include only the union of the output effects
and the caught effects, otherwise erroring. Third, if the scrutinee is
precise but the result $\tau = \dyn$ is dynamic, then then we need to
upcast all of the unhandled effect operations to their dynamic
versions. This is expressed by having the result type be the
combination $(\uplus)$ of the effects who are handled as is, written
$\sigma_c|_{\sigma_s}$ with the most dynamic version of any other
effects that are not handled $\lceil \Gamma(\dom(\sigma_c) -
\sigma_s)\rceil$. Here $\sigma_c|_{\sigma_s}$ means the restriction of
the partial function $\sigma_s$ to only be defined on the set
Finally, if the scrutinee and the goal are both imprecise then we put
a trivial identity cast to $\dyn$ on the scrutinee.

ΓΓA_s AΓB_s B

Γσ_s σ
ΓA_s σ_s B_s A σB
Γ(σ_c) = σ_s

∀∈σ_c.  σ_c() = Γ()
Γσ_s σ_c

A' A' σσ' B B'
A σB A' σ' B'
σ  ∀A_σ B_σ ∈σ_c. ∃A_τB_τ ∈τ_c.

σ_c τ_c

Gradual Subtyping and Type Elaboration

Finally, Figure <ref> describes the elaboration
of types and gradual subtyping.

Value and effect type elaboration $\elabty \Gamma A B$ is mostly
structural except that the rule for concrete effect sets resolves the
request and response types of the effect operation based on the
context $\Gamma$.

Next, we describe the mostly standard gradual subtyping of
value types $A \gsubty B$ and effect types $\sigma \gsubty \tau$ to
determine when a dynamic cast $\obliqueCast {B} A$ or $\obliqueCast
\tau \sigma$ would reduce to subtyping on the precise portions of the

Note that we define gradual subtyping of types in the core language
i.e., after elaboration, so that we can compare effect types across
module boundaries that use different typings for the effect names.

With this intuition, the definition is like that of subtyping, except
that the dynamic effect type is a gradual subtype and supertype than
all other effect types. We conclude by noting the following syntactic
properties of elabortation, which follow by structural induction.

If $\elabprog \cdot \cdot P \sig M \sigma A$ and $\elabprog \cdot \cdot P
{\sig'}{M'}{\sigma'}{A'}$ then $\sig=\sig'$ and $M = M'$ and $\sigma
= \sigma'$ and $A = A'$.

If $\elabprog \cdot \cdot P \sig M \sigma A$, then $\sig \pipe\cdot \vdash_\sigma M : A$.

§ AXIOMATICS AND OPERATIONAL SEMANTICS

Next we turn to the semantic aspects of GrEff: how expressions are
evaluated, what simplifications/optimizations are correct to perform,
and that the graduality principle holds for the language.

We formalize these three aspects axiomatically in the form of an
inequational theory for reasoning about Core GrEff programs.

That is, we define a notion of inequality $M \ltdyn N$ between
expressions called term precision, which is a kind of extension
of the notion of type precision to expressions.

The semantic interpretation of this inequality is that $M$ has the
same behavior as $N$ with respect to output and termination, except in
that it may raise a dynamic type error when $N$ does not.

From this notion inequality we get an induced equivalence relation $M
\equiv N$ that specifies when $M$ and $N$ have the same behavior.

Term precision and the induced equivalence are used to model our
desired semantic ideas: an expression $M$ can be evaluated to a value
$V$ when the equivalence $M \equiv V$ holds, $M$ can be
simplified/optimized to $N$ when $M \equiv N$ holds, and the
graduality principle states that when $M$ is rewritten in the surface
language to some $M'$ that has more precise typing information, than a
corresponding relationship $M' \ltdyn M$ should hold: adding more
precise type information results in more precise dynamic type

With this in mind, we axiomatize the valid optimizations known from
effect handlers as well as desired inequalities from prior work on
graduality in our inequational theory.

Axioms are only useful if we can construct models in which they are
satisfied. For GrEff, we do this by constructing an operational
semantics that specifies more precisely how to evaluate programs and
then define notions of observational equivalence and an error ordering
to model $\equiv$ and $\ltdyn$ and prove that all of the axioms are
valid in this operational model.

We will construct this operational semantics, based on the axiomatics:
we show in Section <ref> that every reduction $M
\stepsin {} N$ is justified by a provable equivalence $M \equiv N$ in
the inequational theory. For many rules this is very straightforward,
e.g., $\beta$ reduction of functions is justified by a corresponding
$\beta$ equation. The most utility we get from the axioms in this case
is for the cast reductions: cast reductions for handlers are justified
not by a direct corresponding rule in the axioms, but instead by
extensionality ($\eta$) principles for handlers combined with a least
upper bound/greatest lower bound property of casts identified in prior
work as being key to the graduality property
<cit.>. This shows that the operational behavior we
define has a canonical status: if certain optimizations for
handlers are to be valid, and the graduality property is desired, then
the cast reductions we define must be used.

§.§ Axiomatics

We present a selection of the rules of the inequational theory of term
precision in Figure <ref>.

The full rules are provided in the appendix.

The form of the inequality judgment is $\Gamma^\ltdyn \vdash_{\sigma \ltdyn \tau} M \ltdyn
N : A \ltdyn B$, which says that $M$ is more precise, or, roughly,
“errors more” than $N$.

This is a kind of heterogeneous inequality relation in that $M$
and $N$ are not required to have the same type: $M$ must have value
type $A$ and effect type $\sigma$ and $N$ must have value type $B$ and
effect type $\tau$ under the context $\Gamma^\ltdyn$ and $A \ltdyn B$
and $\sigma \ltdyn \tau$ must hold.

We allow for $M$ and $N$ to be open terms, typed with respect to the
typing context $\Gamma^\ltdyn$.

The typing context $\Gamma^\ltdyn$ is like an ordinary typing context
$\Gamma$, except that variables are typed $x : A \ltdyn B$ where the
left type $A$ is the type $x$ has in the left term $M$ and $B$ is the
type for $N$. For the context to be well formed, each of the $A \ltdyn
B$ must be provable.

First, we add an axiom that $\err$ is the least term of any type, to
model the graduality property.  Next, we add an axiom that $\ltdyn$ is
transitive, where both the value and effect type are allowed to vary
simultaneously. The relation is reflexive as well, but this is
admissible from congruence rules.

Secondly, we give the congruence rules for functions and application,
and the full system includes such a congruence rule for all term

Next we have computation ($\beta$) and reasoning ($\eta$) rules for
each type. For functions and if, these are standard call-by-value
$\beta\eta$ rules, so we instead show only the handle rules. There are
two $\beta$ rules for handle. If the term being handled is a value,
then the return clause is used. If the term being handled is a raise
of an effect $\effname$, it is equivalent to the handler clause
$\phi(\effname)$ where the continuation is the captured continuation
surrounding the original handler term. We require this to be a let,
but note that we have additional rules that imply that any evaluation
context that doesn't handle can be re-written as a let.

We then have two reasoning ($\eta$) rules for handle. First, if $M$ is
handled by a handler with no effect clauses, then the handler is
equivalent to a let-binding. This can be combined with standard rules
for let binding to show that any term is equivalent to a handler with
no clauses $M \equiv \hndl M x x \emptyset$. We call this the
non-handling principle.

Second, we have a rule that says that any clause that simply re-raises
its operation with the same continuation it was passed can be dropped
from the handler, as this is the same behavior as not catching the
term at all. We call this the effect forwarding principle, as
it says that forwarding an effect to the ambient context is equivalent
to not handling it explicitly at all. Combined with the non-handling
principle, any term $M$ with effect type $\sigma$ can be shown
equivalent to $\hndl M x x {\phi_\sigma}$ where $\phi_\sigma$ simply
forwards all the effects in $\sigma$.

We next show rules describing the interaction of subtyping with value
type casts, the full system includes analogous rules for effect types.

The first says that an upcast followed by a subtyping coercion is less
than a subtyping coercion followed by an upcast, and the downcast rule
is similar.

Finally, we have rules specifying the behavior of value and effect
casts. These rules characterize upcasts as least upper bounds and
downcasts as greatest lower bounds. The first rule shows that the
downcast is a lower bound and the second that it is the greatest. The
upcasts have similar rules, and we include analogous rules for effect
casts as well.

These lub/glb properties are adapted from prior work on axiomatics for
gradual typing <cit.>, but now incorporate the
ordering on both effect and value typing.

We found that this general form of the rule, where the effect is
allowed to differ ($\sigma \ltdyn \sigma'$) while performing a value
cast, is essential for proving the commutativity of value and effect
casts, which is used in the derivation of the operational semantics
and also valid in our logical relations model.

Γ⊢_σ M : A
Γ⊢_σσ M : A A

Γ^⊢_σ_1 σ_2 M_1 M_2 : A_1 A_2Γ'^⊢_σ_2 σ_3 M_2 M_3 : A_2 A_3

rhs(Γ^) = lhs(Γ'^)  lhs(Γ^) = lhs(Γ”^)  rhs(Γ'^) = rhs(Γ”^)

Γ”^⊢_σ_1 σ_3 M_1 M_3 : A_1 A_3

Γ^, x:AA' ⊢_ττ' M M' : B B'
Γ^⊢_σσ' λx. M λx. M' : AτB A' τ' B'

Γ^⊢_σσ' M M' : A σB A' σ' B'

Γ^⊢_σσ' N N' : A A'
Γ^⊢_σσ' M N M' N' : B B'

V y M ϕ≡M[y/v]

(x o N_k) y M ϕ

≡ϕ()[λo. N_k y M ϕ/k]

M x N ∅ ≡M x N

∀∈(ϕ).  ψ() = ϕ()

∀∈(ψ). ∉(ϕ) ⇒ψ() = k(x)

M y N ϕ≡M y N ψ: σB

A A' B B'

Γ^⊢_σσ' M N : A

A B M A' B' N : B' B'

A A' B B'

Γ^⊢_σσ' M N : B B

A' B' M A B N : A' A'

Γ^⊢_σσ' M N : B B
Γ^⊢_σσ' A B M N : A B

Γ^⊢_σσ' M N : A B
Γ^⊢_σσ' M A B N : A A

Inequational Theory

§.§ Operational Semantics

Next, we show a selection of the rules of the operational semantics $M
\stepsin {} M'$ in Figure <ref>, eliding the
standard call-by-value rules for booleans, functions and let-bindings.

We capture the left-to-right, call-by-value evaluation order by using
evaluation contexts defined in Section <ref>.

First, we have the $\beta$ rules for handlers: when handling a value,
execute the return clause. Next, when a raise occurs, we search for
the closest enclosing handler that handles the raised effect and
capture the intermediate evaluation context in the continuation passed
to the appropriate handler..

We capture this with the relation $E' \apart \effname$ which says that
the evaluation context does not handle the given

The next rules concern the behavior of effect casts.

First, all effect casts are the identity on values. Next, when
upcasting a raise, we re-raise the effect, but upcast the
request and downcast the response according to the types in the
output effect type.

An effect downcast works dually if the effect occurs in the result
effect type.

However, if the effect does not occur in the output effect type (which
can only occur if the input effect type is $\dyn$), then an error is

Finally, we have the function downcast. Recall that a function cast
applied to a value itself is a value, and only reduces when applied to
a value.

When this occurs in a downcast, as shown, the result reduces
to applying the original function to an upcasted version of
the input and downcast of the output, where this time we cast
both value and effect types.

Note the order of the value and effect casts on the output is
arbitrarily chosen: because value casts only affect values and effect
casts only affect effect operations, the two possible orders are

The elided cast for function upcasts is precisely dual, and finally
there is a trivial cast rule for the identity cast on booleans.

E[V x N ϕ]

∈(ϕ) E'
E[E'[ V] x N ϕ]

(E'[y]) x N ϕ

E[(λx. M) V]  E[M[V/x]]

E[VxM]  E[M[V/x]]

E[ σσ' V ]

E[ V ]

∈σ' E'
E[ σσ' E'[
V] ]

E[ B B' A A' V
σ σ' E'[x] ]

E[ σσ' V ]

E[ V ]

E[ σσ' E'[
V] ]

E[ B B' A A' V
σ σ' E'[x] ]

E[ σ E'[
V] ]

E[ ((A σB) (A' σ' B') V_f)  V ]

E [B B' σσ' (V_f A A' V) ]

Operational semantics of Core GrEff

We conclude the operational semantics with the following theorem,
which establishes that the operational rules are all valid equational
reasoning principles in any system that models the inequational theory.

If $\cdot \vdash_{\emptyset} M, N : A$ and $M \stepsin{} N$ then $M
\equiv N$ is provable in the axiomatic semantics.

The full proof is in the appendix, but we give an overview of how the
behavior of effect casts $\dncast {\sigma}{\sigma'} M$ is derived in
particular. The core of the argument is to show that the downcast is
equivalent to a particular handler, and then derive the operational
reductions from the $\beta$ reductions for handlers. The handler is \( \dncast \sigma {\sigma'} M \equiv \hndl M x x {\phi_{\dncast \sigma {\sigma'}}} \)
where the $\phi_{\dncast \sigma {\sigma'}}$ handles precisely the effects in $\sigma'$ and for each such $\effname @ A_\sigma' \leadsto B_\sigma' \in \sigma'$, the clause is defined as

\[
\phi_{\dncast\sigma\sigma'}(\effname) =
\begin{cases}
\err & \effname \not\in\dom(\sigma)\\
k(\upcast{B_\sigma}{B_\sigma'}\raiseOpwithM \effname {\dncast {A_\sigma}{A_\sigma'} x}) & \effname @ A_\sigma \leadsto B_\sigma \in\sigma
\end{cases}
\]

That is, if the effect is not present in $\sigma$, the handler errors,
and otherwise it re-raises the effect to its context, but first
downcasting the request, and upcasting the received
response, before passing this back to the original continuation.

Then we show that $\dncast \sigma {\sigma'} M \equiv \hndl M x x
{\phi_{\dncast \sigma {\sigma'}}}$ by showing an ordering each

For the $\dncast \sigma {\sigma'} M \equiv \hndl M x x {\phi_{\dncast
\sigma {\sigma'}}}$ case, we apply the effect forwarding principle
to transform the left-hand side to $\hndl {\dncast\sigma{\sigma'} M} x
x {\phi_{\sigma}}$. Then we apply congruence for handlers, with the
cases of the right-hand side that handle effects not in $\sigma$ being
irrelevant. Then the remaining clauses are all of the same syntactic
structure except for upcasts and downcasts, and so the proof follows
by congruence and the upcast/downcast rules.

To show $\hndl M x x {\phi_{\dncast \sigma {\sigma'}}} \ltdyn
\dncast{\sigma}{\sigma'} M$, we first apply the downcast right rule to
eliminate the cast on the right. Then to show $\hndl M x x
{\phi_{\dncast \sigma {\sigma'}}} \ltdyn M$ we again use the effect
forwarding principle to rewrite the right-hand side as $\hndl M x x
{\phi_{\sigma'}}$. We again apply handler congruence, with the cases
where $\effname\in \sigma$ analogous to the prior argument. In the
remaining remaining cases $\phi_{\dncast{\sigma}{\sigma'}}(\effname)
\ltdyn \phi_{\sigma'}(\effname)$ where $\effname \not\in\sigma$, we
have the left hand side is an error, and so the argument follows by
the fact that the error is the minimum in the ordering.

§.§ Subtyping, Gradual Subtyping and Coercions

The elaboration defined in Section <ref> inserts casts of the
form $\dncast{A}{\lceil A\rceil}\upcast{B}{\lceil B \rceil}M$ when a
gradual subtyping $A\gsubty B$ is used in the type-checker.

If we think of $\lceil A \rceil$ as the type of programs in the
untracked language, this says to cast a program from one type to
another, we should cast it to an untracked type and then to the other
effect-tracking type, similar to prior work on cast calculi based on
upcasts and downcasts <cit.>. This is a reasonable cast if
we think of the untracked language as our “operational ground
truth”, and so we should prove that any other translation is
extensionally equivalent to this one.

However, operationally, this can be quite a wasteful translation, as a
cast can result in proxying at runtime, while subtyping
coercions have no runtime behavior, and so are zero cost.

For instance, if $A \gsubty B$ is true because in fact $A \subty B$,
then there need not be any runtime cast at all.

For this reason, we would prefer to optimize the cast based on the
subtyping information in the proof of $A\gsubty B$.

Since $A$ may be more imprecise than $B$ in some subterms and
vice-versa, the structure of the cast should still be an upcast
followed by a downcast, but with the possibility that we use implicit
subtyping coercions at some points.

There are three places we might insert the implicit subtyping
coercion: before the upcast, between the upcast and downcast and after
the downcast.

From the proof of $A \gsubty A'$, we can extract types and
subtyping/precision derivations as in
Figure <ref>.

A_h     D_h     B

A     D_l     B_l
["⊑"description, draw=none, from=2-1, to=2-2]
["⊒"description, draw=none, from=2-2, to=2-3]
["⊑"description, draw=none, from=1-1, to=1-2]
["⊒"description, draw=none, from=1-2, to=1-3]
[""description, draw=none, from=2-1, to=1-1]
[""description, draw=none, from=2-3, to=1-3]
[""description, draw=none, from=2-2, to=1-2]

Situation derivable from $A \gsubty B$

On the left we have a “pure subtyping” component of the gradual
subtpying proof coming from $A$, and on the right we we have the pure
subtyping component coming from $B$. In the middle we have two
“dynamic” types also related by subtyping.

There are then three paths from $A$ to $A'$ in this diagram, which
generate three different potential casts with implicit subtyping
coercions ensuring they are well-typed as taking $A$ to $A'$:
(1) Up and then right twice $\dncast{B}{D_h}\upcast{A_h}{D_h}$
(2) Right, up and then right: $\dncast{B}{D_h}\upcast{A}{D_l}$
(3) Right twice and then up:  $\dncast{B_l}{D_l}\upcast{A}{D_l}$

Fortunately we can choose whichever is operationally preferable: each
of these casts is equivalent as a function from $A$ to $B$ and they
are all equivalent to the ground truth cast $\dncast{A'}{\lceil A
\rceil}\upcast{A}{\lceil A\rceil}$.

The above discussion applies equally well to effect casts, which are
even simpler in that the “ground-truth” always factors through the
single most imprecise effect type: the dynamic effect type.

§ SOUNDNESS AND GRADUALITY

In this section we establish that the axiomatic semantics of core
GrEff has a sound model in terms of its operational semantics. This
establishes two key properties: equivalent terms ($M \equiv N$) are
contextually equivalent in the operational semantics, and the
graduality property holds. First, we review the definition of the
graduality property, and then we give a logical relations model and
prove that any provable inequality $M \ltdyn N$ implies that the terms
are related in the logical relation.

§.§ Static and Dynamic Gradual Guarantees

GrEff is designed to support a smooth migration from imprecise
to precise typing. The static gradual guarantee <cit.>
formalizes a syntactic element of this idea of a smooth migration. The
static gradual guarantee informally says that increasing the precision
of type annotations on a program can only make it harder to
satisfy the static type checker, or viewed the other way around,
decreasing the precision of type annotations can only make it
easier to satisfy the static type checker.

Then the dynamic gradual guarantee, also known as graduality,
establishes the semantic counterpart: increasing the precision of type
annotations on a program should only make it harder to
terminate without a dynamic type error, and furthermore except
where there are dynamic type errors, the behavior of the program
should match the original.

These properties can be formalized as a form of monotonicity of
the elaboration of the syntactic programs of surface GrEff into the
semantically meaningful core GrEff programs as follows.

First, we define a syntactic term precision ordering
$\mathrel{\ltdyn^\textrm{syn}}$ on untyped GrEff programs as the
congruence closure of the type precision ordering. Then the static
gradual guarantee says that this is a monotone partial function
from the syntactic term precision ordering to the axiomatic inequality
on core GrEff terms:

If $P \mathrel{\ltdyn^{\textrm{syn}}} P'$, then if $\elabprog \cdot
\cdot P \sig M \sigma A$, then there exist $M', \sigma', A'$ such
that $\elabprog \cdot \cdot {P'} \sig {M'} {\sigma'} {A'}$ such that
$\cdot \vdash_{\sigma \ltdyn \sigma'} M \ltdyn M' : A \ltdyn A'$.

Then the dynamic gradual guarantee says that this extends to
monotonicity in the following semantic ordering on core GrEff

Given $\cdot \vdash_{\emptyset} M, M' : \boolty$, define
$M \mathrel{\ltdyn^\textrm{sem}} M'$ to
hold when one of the following is satisfied (1) $M \stepstar \mho$,
(2) $M \Uparrow$ and $M' \Uparrow$, (3) $M \stepstar \tru$ and $M'
\stepstar \tru$ (4) $M \stepstar \fls$ and $M' \stepstar \fls$.

If $\sig\pipe\cdot \vdash_{\emptyset\ltdyn\emptyset} M \ltdyn M' : \boolty$,
then $M \mathrel{\ltdyn^\textrm{sem}} M'$.

This theorem is stated in terms of closed terms of a fixed type, but
to prove it we need a stronger inductive hypothesis, i.e., the logical
relation for open terms.

The resulting theorem that any inequation provable in the theory
implies the semantic ordering is called graduality, as it is
analogous in structure to the parametricity theorem in
parametric polymorphism.

Then the dynamic gradual guarantee follows as a corollary.

§.§ Logical Relation

In Figure <ref>, we present the definition of the step-indexed logical
relation for graduality.

Following prior work on logical relations for graduality, the relation
is indexed not by types, but by derivations of type precision
facts, i.e., proof terms for $c : A \ltdyn B$ or $d_\sigma : \sigma
\ltdyn \sigma'$.

We present the definition of these proof terms in the appendix.

For a type precision derivation $d$, define $d^l$ and $d^r$ to be the
types such that $d : d^l \ltdyn d^r$, and analogously for effect

(M_1, M_2) ∈(R)_j
j = 0 ∨(j = k + 1 ∧(M_1, M_2) ∈R_k)

(V_1,V_2) ∈ j
(V_1, V_2) ∈ ∧(V_1 = V_2 = ) ∨(V_1 = V_2 = )

(V_1,V_2) ∈d_i →_d_σ d_o j
(V_1, V_2) ∈d_i →_d_σ d_o ∧

∀k ≤j.
∀(V_i1, V_i2) ∈d_i k.

(V_1  V_i1, V_2 V_i2) ∈d_σ k (d_o)

(M_1, M_2) ∈d_σ j (R, A^l, A^r)
(M_1, M_2) ∈A^l A^r d_σ ∧(M_1 j+1

∨(∃k ≤j.  (M_1 j-k )
∨(∃(N_1,N_2) ∈d_σ k R ∧M_1 j-k N_1 ∧M_2 N_2)))

(M_1, M_2) ∈d_σ j (R, A^l, A^r)
(M_1, M_2) ∈A^l A^r d_σ ∧(M_2 j+1

∨(∃k ≤j. (M_2 j-k ∧M_1 )
∨(∃N_2. M_2 j-k N_2 ∧M_1 )
∨(∃(N_1,N_2) ∈d_σ k R ∧M_2 j-k N_2 ∧M_1 N_1)))

(M_1, M_2) ∈d_σ j (R, A^l, A^r)
(M_1, M_2) ∈A^l A^r d_σ ∧

(((M_1) ∧(M_2) ∧(M_1, M_2) ∈R j)

∨(∃ϵ: c d ∈d_σ,
E^l ϵ, E^r ϵ, V^l, V^r.
(V^l,V^r)  ∈(c)_j      ∧

(x^l.E^l[x^l], x^r.E^r[x^r]) ∈(d )_j
(d_σ  (R, A^l, A^r),
d_σ^rA^r)     ∧
M_1 = E^l[ϵV^l] ∧M_2 = E^r[ϵV^r]))

(x^l.M^l, x^r.M^r) ∈
(M^l, M^r) ∈c σ^lA^l σ^rA^r ∧

c j (S, σ^lA^l, σ^rA^r)
∀k ≤j. (V^l,V^r) ∈c k.
(M^l[V^l/x^l], M^r[V^r/x^r]) ∈S_k

(γ_1,γ_2) ∈Γ^ j
∀(x_1 x_2 : c) ∈Γ^.
(γ_1(x_1), γ_2(x_2)) ∈c j

Logical Relation

Many of the details are similar to prior work, especially
<cit.>, so we highlight the handling of
effect types, which is novel.
in Section <ref>.  In addition to the usual expression and
value relations, we have a result relation and a
continuation relation.  In our language, a result is
either a value, or an evaluation context $E$ wrapping a raise of an
effect $\effname$, such that $E \apart \effname$.  The result relation
specifies the conditions for two such results to be related.  Finally,
the relations are parameterized by precision derivations. In the case
of the expression and result relations, this is an effect precision
derivation, while for values and continuations, it is a value type
precision derivation.  This is analogous to the usual approach whereby
logical relation is indexed by a type. But instead of using types, we
use precision derivations, i.e., the proof that the LHS term is more
precise than the type of the RHS term.

As in previous work on logical relations for graduality, the
expression logical relation $\simierel{\cdot}{}{}$ is split into two
relations $\ltierel{\cdot}{}{}$ and $\gtierel{\cdot}{}{}$. The former
counts the steps taken by the left-hand term, while the latter counts
steps taken by the right-hand term. This is captured by the
quantitative small-step reduction $M \stepsin j N$ which means $M$
takes exactly $j$ steps to reduce to $N$. Despite needing two
relations, we are for the most part able to abstract over their
differences: most of the lemmas we prove hold for both relations with
no adjustment needed. Notable exceptions are transitivity and the
anti- and forward reduction lemmas: these lemmas make crucial use of
step counting, so naturally the side whose steps we are counting makes
a difference.

Given a step-indexed relation $R$, we define an operator $\later R$ (pronounced “later $R$”)
as follows: Terms $M_1$ and $M_2$ are related in $\later R$ at index $n$ if and only if either
$n$ is zero, or $n \ge 1$ and $M_1$ and $M_2$ are related in $R$ at index $n - 1$.

One novel aspect of our logical relation is the result relation $\simirrel{\cdot}{}{}$.
This relation relates terms $M_1$ and $M_2$ – of type $A^l$ and $A^r$ respectively –
representing either two values or two “evaluations” of raised operations. The relation
is parameterized by a step-indexed relation $R$ between values of type $A^l$ and
$A^r$ (the types of $M_1$ and $M_2$). $M_1$ and $M_2$ are related by $\simirrel{\cdot}{}{}$
when either (1) both terms are values and are related by $R$ at the appropriate step index,
or (2) there exists an effect $\epsilon$ in $d_\sigma$, values related later, and evaluation
contexts (i.e., continuations – see below) related later, such that $M_1$ is equal to
raising the effect and then wrapping it in the continuation, and likewise for $M_2$.

The relation $\simikrel{\cdot}{}{}$ relates evaluation contexts $E_1$ and $E_2$ representing continuations that accept values, similar to prior work on logical relations for continuations <cit.>.
The evaluation contexts each have a hole $\bullet$ – the type of the hole is the type of the input value to the continuation.
To enforce that the continuations accept values only, and not arbitrary terms, the inputs to the continuation
relation are actually terms $M^l$ and $M^r$ with free variables $x^l$ and $x^r$, respectively.
$E_1$ and $E_2$ also have “output” types ($A^l$ and $A^r$) and “output” effect sets ($\sigma^l$ and $\sigma^r$).
When values are plugged into $E_1$ and $E_2$, the result is two terms having types $A^l$ and $A^r$ and
effect sets $\sigma^l$ and $\sigma^r$, respectively.

§.§ Proof of Graduality

Our goal is to prove that the inequational theory is sound with
respect to the logical relation.
First we define the notion of two terms being related semantically:

\[
\Gamma^\ltdyn \vDash_{d_{\sigma}} M_1 \ltdyn M_2 \in c := \forall \sim\, \in \{<,\, >\}. \forall j \in \mathbb{N}.
\forall (\gamma_1, \gamma_2) \in \simivrel{\Gamma} {j}.
(M_1[\gamma_1], M_2[\gamma_2]) \in \simierel{d_{\sigma}} {j} {\simivrel c {}}.
\]

That is, $M_1$ and $M_2$ are related if for all $j$ and all
substitutions of values $\gamma_1$ and $\gamma_2$ related at $j$,
the resulting terms are related in $\simierel {d_\sigma} {j} {\simivrel c {}}$,
where this needs to hold both when $\sim$ is $<$ and when it is $>$.
Our goal is then to prove the following:

If $\Gamma^\ltdyn \vdash_{d_\sigma} M \ltdyn N : c$ then
$\Gamma^\ltdyn \vDash_{d_\sigma} M \ltdyn N \in c$

We provide here a high-level overview of the proof; the complete
proofs are in the appendix.

We begin by establishing variants of standard anti- and
forward-reduction lemmas as well as monadic bind.

We also prove a Löb induction principle to structure the induction
over step-indices.

With these lemmas, we first prove soundness of each of the congruence
rules for term precision, by uses of the monadic bind lemma along with
the reduction lemmas. Next, we prove soundness of the rules of the
equational theory, e.g., the $\beta$ and $\eta$ laws, and
transitivity. Finally, we prove soundness of the rules for casts and

§ DISCUSSION

Prior Work on Gradual Effects

The most significant prior work on gradual effects is
<cit.>, which defined a gradual effect system based
on the generic effect calculus of <cit.>
using an early version of the abstracting gradual typing (AGT)
framework for gradual type systems<cit.>.

While we based GrEff on effect handlers rather than the generic effect
calculus, there are significant similarities in the typing: function
types and typing judgments are indexed by a set of effect operations
in each system.

The most significant syntactic difference is that their framework is
parameterized by a fixed effect theory, whereas GrEff has explicit
support for declaration of new effects in the program. In particular,
this means that their system does not need to support modules
containing different views of the same nominal effect as we did.

They additionally support a form of partially tracked functions, in
GrEff syntax this would look like $A \to_{\effname,\dyn} B$, a
function type where the function is known specifically to possibly
raise the effect $\effname$ in addition to raising other effects.

In GrEff this partial tracking would ensure that any effects raised
with the name $\effname$ match the module's local view of the effect
typing of $\effname$.

Finally, on the semantic side, this prior work proves only a type
safety proof, whereas here we have proven graduality and the
correctness of type-based optimizations and handler optimizations.

Another related area of research is on gradual typing with delimited
continuations, which are mutually expressible with effect handlers

Takikawa et al (<cit.>) propose a gradual type system and
semantics via contracts for a language with delimited continuations
using typed prompts.

They consider only value types and untracked function types that do
not say which prompts are expected to be present.

They show that a naive contract based implementation is unsound
because a dynamically typed program can interact with a typed prompt
and thereform the prompts themselves must be equipped with contracts,
even though it does not correspond to any value being imported.

In core GrEff, this unsoundness is ruled out by using intrinsic
typing: the problem corresponds to raising an effect operation with a
different type than the type expected by the closest handler, which is
precisely what the effect type system tracks. Wrapping the prompt in
contracts is behaviorally equivalent to what is achieved by our effect
type casts.

Sekiyama, Ueda and Igarashi present a blame calculus for a language
with shift and reset <cit.>. The blame calculus
is analogous to our core GrEff language, and uses a type and effect
system for the answer types of shift/reset. They do not develop a
surface language that elaborates to this blame calculus like our
GrEff, and there is no analogue of effect operations in
shift/reset-based systems so there are no nominal aspects of their
language. Additionally, while they have an effect system to keep track
of answer types, they do not have effect casts.

Prior Approaches to Gradual Nominal Datatypes

We are also not the first to consider the combination of gradual and
nominal typing.

The closest match to our design is in Typed Racket's support for typed

In Racket, a struct is a kind of record type that (by default) is
generative in that it creates a new type tag distinct from all others.

Typed Racket supports import of untyped Racket structs into Typed
Racket, where types are assigned to the fields, and values of the
struct type are then wrapped in contracts accordingly.

This is quite close to our treatment of nominal effect operations
which can be thought of as adding new cases to the dynamic effect
monad rather than dynamic type.

Our type system is more complex however, since in our system modules
can use dynamically typed effects whereas in Typed Racket, there is no
syntactic type for dynamially typed values, when imported into typed
code the system must give a completely precise type.

Malewski et al (<cit.>) present a
design for gradual typing with nominal algebraic datatypes. Their
focus is on the gradual migration from datatypes whose cases are
open-ended to datatypes with a fixed set of constructors. They do not
consider the use-case we have where different modules have different
typings for the same nominal constructor.

Prior Work on Subtyping

Much prior work on incorporating subtyping with gradual types has
focused on the static typing aspects
<cit.>. The
most significant prior semantic work on subtyping and gradual typing
is the Abstracting Gradual Typing work <cit.> which proves the
dynamic gradual guarantee for a system with subtyping developed using
the AGT methodology. In this work we establish equivalence between
multiple different ways to combine gradual type casts and subtyping
coercions, summarized in Figure <ref>,
which are derivable from our newly identified cast/coercion ordering
principle in our equational theory
(Figure <ref>).

Towards a Practical Language Design

GrEff is intended as a proof-of-concept language design to provide the
semantic foundation for extending a language such as OCaml 5 with
gradual effect typing. We discuss the current mismatches with OCaml's
design and how these might be rectified.

First, OCaml uses extensible variant types for effects and
exceptions, whereas in GrEff effects are not first-class values. This
should not be difficult to support as the variant type can be treated
somewhat similarly to a dynamic type.

Next, OCaml supports recursive effect types, meaning that the
request or response of an effect can refer to the effect being
defined. For instance, this allows for a variant of our coroutine
example where forked threads can fork further threads. This would
complicate the metatheory of GrEff but shoul work in principle.

A final syntactic difference is that OCaml is based on
Hindley-Milner-style polymorphic type schemes, whereas GrEff is based
on a simple type system. It may be possible to adapt previous work for
gradual typing in unification-based type

Implementing gradual effects brings its own challenges. Our derivation
of the operationsl semantics is based on proving that effect casts can
be implemented as handlers, and so can be implemented by a
source-to-source transformation. However, such an implementation may
suffer from similar performance issues as other naive wrapper
semantics, which can be solved by defunctionalizing the casts
<cit.>. Additionally, strong gradual typing between
fully dynamically typed and static code can result in high performance
penalties <cit.> even with space efficient
implementations. However since effect casts would not be as pervasive
in typical programs as value type casts, it is not obvious that the
same pathological behaviors would arise in gradually effect typed
OCaml programs. This is a clear empirical question to be addressed in
future work.

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

authorpersonKenichi Asai.
Logical relations for call-by-value delimited
continuations. In booktitleRevised Selected Papers from the
Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn,
Estonia, 23-24 September 2005 (seriesTrends in Functional
Programming, Vol. volume6),
editorpersonMarko C. J. D. van Eekelen (Ed.).

[Bañados Schwerter, Garcia, and
TanterBañados Schwerter et al2014]
authorpersonFelipe Bañados Schwerter,
personRonald Garcia, and personÉric Tanter.
A Theory of Gradual Effect Systems. In
booktitleProceedings of the 19th ACM SIGPLAN International
Conference on Functional Programming (Gothenburg, Sweden)
(seriesICFP '14). pages283–295.

[Brachthäuser, Schuster, and
OstermannBrachthäuser et al2020]
authorpersonJonathan Immanuel Brachthäuser,
personPhilipp Schuster, and personKlaus Ostermann.
Effekt: Capability-passing style for type- and
effect-safe, extensible effect handlers in Scala.
journalJ. Funct. Program.  volume30
(year2020), pagese8.

[Castagna, Lanvin, Petrucciani, and
SiekCastagna et al2019]
authorpersonGiuseppe Castagna, personVictor
Lanvin, personTommaso Petrucciani, and
personJeremy G. Siek. year2019.
Gradual Typing: A New Perspective.
journalProc. ACM Program. Lang.
volume3, numberPOPL, Article articleno16
(datejan year2019), numpages32 pages.

authorpersonWasmFX Contributors.
titleWasmFX: Effect Handlers for WebAssembly.

Accessed: 2020-11-10.

[Cooper, Lindley, Wadler, and YallopCooper
et al2006]
authorpersonEzra Cooper, personSam Lindley,
personPhilip Wadler, and personJeremy Yallop.
Links: Web Programming Without Tiers. In
booktitleFormal Methods for Components and Objects, 5th
International Symposium, FMCO 2006, Amsterdam, The Netherlands, November
7-10, 2006, Revised Lectures (seriesLecture Notes in
Computer Science, Vol. volume4709). pages266–296.

[Forster, Kammar, Lindley, and PretnarForster
et al2019]
authorpersonYannick Forster, personOhad
Kammar, personSam Lindley, and personMatija
Pretnar. year2019.
On the expressive power of user-defined effects:
Effect handlers, monadic reflection, delimited control.
journalJ. Funct. Program.  volume29
(year2019), pagese15.

[Garcia and CiminiGarcia and Cimini2015]
authorpersonRonald Garcia and personMatteo
Cimini. year2015.
Principal Type Schemes for Gradual Programs. In
booktitleProceedings of the 42nd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2015, Mumbai, India, January 15-17, 2015,
editorpersonSriram K. Rajamani and
personDavid Walker (Eds.). publisherACM,

[Garcia, Clark, and TanterGarcia
et al2016]
authorpersonRonald Garcia, personAlison M.
Clark, and personÉric Tanter.
Abstracting Gradual Typing. In
booktitleACM Symposium on Principles of Programming
Languages (POPL).

[Herman, Tomb, and FlanaganHerman
et al2010]
authorpersonDavid Herman, personAaron Tomb,
and personCormac Flanagan. year2010.
Space-Efficient Gradual Typing.
journalHigher Order Symbol. Comput.
volume23, number2 (datejun
year2010), pages167–189.

[Kiselyov, Sabry, and SwordsKiselyov
et al2013]
authorpersonOleg Kiselyov, personAmr Sabry,
and personCameron Swords. year2013.
Extensible effects: an alternative to monad
transformers. In booktitleProceedings of the 2013 ACM
SIGPLAN Symposium on Haskell, Boston, MA, USA, September 23-24, 2013.
publisherACM, pages59–70.

[Lehmann and TanterLehmann and
authorpersonNico Lehmann and
personÉric Tanter. year2017.
Gradual Refinement Types. In
booktitleACM Symposium on Principles of Programming
Languages (POPL).

authorpersonDaan Leijen.
Koka: Programming with Row Polymorphic Effect
Types. In booktitleProceedings 5th Workshop on
Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble,
France, 12 April 2014 (seriesEPTCS,
Vol. volume153). pages100–126.

[Lindley, McBride, and McLaughlinLindley
et al2017]
authorpersonSam Lindley, personConor
McBride, and personCraig McLaughlin.
Do be do be do. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium
on Principles of Programming Languages, POPL 2017, Paris, France, January
18-20, 2017. publisherACM, pages500–514.

[Malewski, Greenberg, and TanterMalewski
et al2021]
authorpersonStefan Malewski, personMichael
Greenberg, and personÉric Tanter.
Gradually structured data.
journalProc. ACM Program. Lang.
volume5, numberOOPSLA (year2021),

[Marino and MillsteinMarino and
authorpersonDaniel Marino and
personTodd D. Millstein. year2009.
A generic type-and-effect system. In
booktitleProceedings of TLDI'09: 2009 ACM SIGPLAN
International Workshop on Types in Languages Design and Implementation,
Savannah, GA, USA, January 24, 2009,
editorpersonAndrew Kennedy and
personAmal Ahmed (Eds.). publisherACM,

[New and AhmedNew and Ahmed2018]
authorpersonMax S. New and personAmal
Ahmed. year2018.
Graduality from Embedding-Projection Pairs. In
booktitleInternational Conference on Functional
Programming (ICFP), St. Louis, Missouri.

[New, Jamner, and AhmedNew
et al2020]
authorpersonMax S. New, personDustin
Jamner, and personAmal Ahmed.
Graduality and parametricity: together again for
the first time.
journalProc. ACM Program. Lang.
volume4, numberPOPL (year2020),

[New and LicataNew and Licata2018]
authorpersonMax S. New and personDaniel R.
Licata. year2018.
Call-by-name Gradual Type Theory. In
booktitleFormal Structures for Computation and Deduction,
Oxford England.

[New, Licata, and AhmedNew
et al2019]
authorpersonMax S. New, personDaniel R.
Licata, and personAmal Ahmed.
Gradual Type Theory. In
booktitleACM Symposium on Principles of Programming
Languages (POPL), Cascais, Portugal.

[Piróg, Polesiuk, and
SieczkowskiPiróg et al2019]
authorpersonMaciej Piróg, personPiotr
Polesiuk, and personFilip Sieczkowski.
Typed Equivalence of Effect Handlers and Delimited
Control. In booktitle4th International Conference on Formal
Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019,
Dortmund, Germany (seriesLIPIcs,
Vol. volume131), editorpersonHerman
Geuvers (Ed.). publisherSchloss Dagstuhl - Leibniz-Zentrum
für Informatik, pages30:1–30:16.

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

[Sekiyama, Ueda, and IgarashiSekiyama
et al2015]
authorpersonTaro Sekiyama, personSoichiro
Ueda, and personAtsushi Igarashi.
Shifting the Blame - A Blame Calculus with
Delimited Control. In booktitleProgramming Languages and
Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November
30 - December 2, 2015, Proceedings (seriesLecture Notes in
Computer Science, Vol. volume9458),
editorpersonXinyu Feng and personSungwoo
Park (Eds.). publisherSpringer, pages189–207.

[Siek, Vitousek, Cimini, and BoylandSiek
et al2015]
authorpersonJeremy Siek, personMicahel
Vitousek, personMatteo Cimini, and personJohn Tang
Boyland. year2015.
Refined Criteria for Gradual Typing. In
booktitle1st Summit on Advances in Programming Languages
(seriesSNAPL 2015).

[Siek and TahaSiek and Taha2006]
authorpersonJeremy G. Siek and personWalid
Taha. year2006.
Gradual Typing for Functional Languages. In
booktitleScheme and Functional Programming Workshop
(Scheme). pages81–92.

[Siek and TahaSiek and Taha2007]
authorpersonJeremy G. Siek and personWalid
Taha. year2007.
Gradual Typing for Objects. In
booktitleEuropean Conference on Object-Oriented
Programming (ECOOP).

[Siek and VachharajaniSiek and
authorpersonJeremy G. Siek and
personManish Vachharajani. year2008.
Gradual typing with unification-based inference.
In booktitleProceedings of the 2008 Symposium on Dynamic
Languages, DLS 2008, July 8, 2008, Paphos, Cyprus,
editorpersonJohan Brichau (Ed.).
publisherACM, pages7.

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

[Takikawa, Feltey, Greenman, New, Vitek, and
FelleisenTakikawa et al2016]
authorpersonAsumu Takikawa, personDaniel
Feltey, personBen Greenman, personMax S. New,
personJan Vitek, and personMatthias Felleisen.
Is Sound Gradual Typing Dead?. In
booktitleProceedings of the 43rd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (St. Petersburg, FL, USA)
(seriesPOPL '16). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Takikawa, Strickland, and
Tobin-HochstadtTakikawa et al2013]
authorpersonAsumu Takikawa, personT. Stephen
Strickland, and personSam Tobin-Hochstadt.
Constraining Delimited Control with Contracts. In
booktitleProgramming Languages and Systems - 22nd European
Symposium on Programming, ESOP 2013, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy,
March 16-24, 2013. Proceedings (seriesLecture Notes in
Computer Science, Vol. volume7792),
editorpersonMatthias Felleisen and
personPhilippa Gardner (Eds.). publisherSpringer,

[Tobin-Hochstadt and FelleisenTobin-Hochstadt
and Felleisen2008]
authorpersonSam Tobin-Hochstadt and
personMatthias Felleisen. year2008.
The Design and Implementation of Typed Scheme. In
booktitleACM Symposium on Principles of Programming
Languages (POPL), San Francisco, California.

authorpersonPhilip Wadler.
GATE: Gradual Effect Types. In
booktitleLeveraging Applications of Formal Methods,
Verification and Validation - 10th International Symposium on Leveraging
Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17-29,
2021, Proceedings (seriesLecture Notes in Computer
Science, Vol. volume13036),
editorpersonTiziana Margaria and
personBernhard Steffen (Eds.). publisherSpringer,

[Wadler and FindlerWadler and
authorpersonPhilip Wadler and
personRobert Bruce Findler. year2009.
Well-typed programs can't be blamed. In
booktitleEuropean Symposium on Programming (ESOP) (York,
UK). pages1–16.

§ SYNTAX AND ELABORATION

We give a term assignment for effect precision in
Figure <ref>.

In it we use the notion of an effect operation being in a precision
derivation $\effarr \effname c d \in d_c$. For when $d_c$ itself is a
partial function this is just as with earlier usage, but when $d_c =
\dyn$ or $d_c = \texttt{inj}(d_c')$ we use the definition at the
bottom of the figure.

⊢d_i : A A'⊢d_e : σσ'⊢d_o : B B'
⊢d_i →_d_e d_o : A →_σB A' →_σ' B'

supp(d_c) = supp(σ_c) = supp(σ_c')

(∀c d ∈d_c, A B ∈σ_c, A'B' ∈σ_c'.

⊢c : A A' ⊢B B')

⊢d_c : σ_c σ_c'

⊢d_c : σ_c |_supp(σ_c)
⊢(d_c) : σ_c

c d ∈∈
⊢c d ∈

⊢c' d' ∈d_c c = (c') d = (d')
⊢c d ∈(d_c)

Type and Effect Precision Derivations

Thought the generating axioms are different from the simple
presentation in the body of the paper, we show that provability is not

Assuming $\sig \vdash A$ and $\sig \vdash B$, the following are equivalent

* $A \ltdyn A'$ is provable in the system in Figure <ref>

* There exists a derivation $\sig \vdash c : A \ltdyn A'$ in the  system in Figure <ref>.

Similarly, assuming $\sig \vdash \sigma$ and $\sig \vdash \sigma'$, the following are equivalent

* $\sigma \ltdyn \sigma'$ is provable in the system in Figure <ref>

* There exists a derivation $\sig \vdash c_e : \sigma \ltdyn \sigma'$ in the  system in Figure <ref>.

Next we define gradual join and meet of value and effect types in
Figure <ref>. Note that the definition is quite simple for
concrete effect sets because this is only used on effects
within the same module, so we never have to consider the case
where the two sides assign different effects to the same operation
name $\effname$.

\begin{align*}
\boolty \gjoin \boolty &= \boolty\\
(A \effto \sigma B) \gjoin (A' \effto {\sigma'} B') &=
(A \gmeet A') \effto {\sigma \gjoin \sigma'} (B \gjoin B')\\
\dyn \gjoin \sigma &= \sigma\\
\sigma \gjoin \dyn &= \sigma\\
\sigma_c \gjoin \tau_c &=
\{ \effname @ A \leadsto B \,|\, \effname @ A \leadsto B \in \sigma_c \wedge \effname \not\in\dom(\tau_c) \}\\
&\quad\cup \{ \effname @ A' \leadsto B' \,|\,  \effname \not\in\dom(\sigma_c) \wedge \effname @ A' \leadsto B' \in \tau_c \} \\
\{ \effname @ A \gjoin A' \leadsto B \gmeet B' \,|\, \effname @ A \leadsto B \in \sigma_c \wedge \effname @ A' \leadsto B' \in \tau_c \}
\end{align*}

\begin{align*}
\boolty \gjoin \boolty &= \boolty\\
(A \effto \sigma B) \gmeet (A' \effto {\sigma'} B') &=
(A \gjoin A') \effto {\sigma \gmeet \sigma'} (B \gmeet B')\\
\dyn \gmeet \sigma &= \dyn\\
\sigma \gmeet \dyn &= \dyn\\
\sigma_c \gmeet \tau_c &=
\{ \effname @ A \gmeet A' \leadsto B \gjoin B' \,|\, \effname @ A \leadsto B \in \sigma_c \wedge \effname @ A' \leadsto B' \in \tau_c \}
\end{align*}

Gradual Join and Meet

Now we define a notion of subtyping of precision derivations, which will be needed
in the proofs involving the interaction between subtyping and casts.

d_i c_i c_e d_e c_o d_o
c_i →_c_e c_o d_i →_d_e d_o

c d
(c) (d)

(d_c) ⊆(d'_c)

∀c d ∈d_c.
c' d' ∈d'_c ∧c c' ∧d' d
d_c d'_c

c ()

c d
c (d)

Subtyping of Precision Derivations

§ (IN)EQUATIONAL THEORY

In this section we describe the full inequational theory and then
prove several derivable theorems in the theory.

Note that for brevity, we use some shorthands: rather than writing out
the full $\sg^\ltdyn \vdash_{\sigma\ltdyn \tau} M \ltdyn N : A \ltdyn
B$, (1) we elide $\sg^\ltdyn$, and all rules should be interpreted as
holding under an arbitrary such contexts (2) rather than write
$\sigma\ltdyn\tau$ and $A \ltdyn B$, we use instead precision
derivations $d_\sigma$, $c$ and (3) whenever it is clear, we elide the
types as well, especially for equational rules.

First we need general call-by-value reasoning principles.

M[x:A] ≡N[x:A] V ≡V' : A
M[V/x] ≡N[V'/x]

*[right=MonadUnitL]y x N ≡N[y/x]

*[right=MonardUnitR]M x x ≡M

*[right=MonadAssoc](M x N) y P ≡M x N y P

*[right=BoolEta]M[x : ] ≡x M[/x]M[/x]

*[right=BoolBetaTru]N_tN_f ≡N_t

*[right=BoolBetaFalse]N_tN_f ≡N_f

*[right=IfEval]M N_tN_f ≡M x x N_t N_f

*[right=FunBeta](λx. M) V ≡M[V/x]

*[right=FunEta](V : A →B) ≡λx. V x

*[right=AppEval]M N ≡M x N y x y

Next, the rules specifically for raise and handlers:

*[right=HandleBetaRet]x y M ϕ≡M[x/y]

(x o N_k) y M ϕ≡

ϕ()[λo. N_k y M ϕ/k]

*[right=RaiseEval]M ≡M x x

M x N ∅ ≡M x N

∀∈(ϕ).  ψ() = ϕ()
∀∈(ψ). ∉(ϕ) ⇒ψ() = k(x)

M y N ϕ≡M y N ψ

Next, the congruence rules

x_1 x_2 : c ∈Γ^
^⊢_d_σ x_1 x_2 : c

⊢_d_σ :

⊢_d_σ :

x_1 x_2 : c ⊢_d_σ' M_1 M_2 : d

λx_1.M_1 λx_2.M_2 : c →_d_σ' d

⊢_d_σ M_1 M_2 : c →_d_σ d ⊢_d_σ N_1 N_2 : c

⊢_d_σ M_1 N_1 M_2 N_2 : d

⊢_d_σ M_1 M_2 : c

x_1 x_2 : c ⊢_d_σ N_1 N_2 : d

M_1 x_1 N_1 M_2 x_2 N_2 : d

⊢_d_σ M M' :

⊢_d_σ N_t N'_t : c
⊢_d_σ N_f N'_f : c

M N_tN_f M' N'_tN'_f : c

c : A_1 A_2 d : B_1 B_2

@ c d ∈d_σ⊢_d_σ M_1 M_2 : c

M_1  M_2 : d

⊢_d_σM M' : cy:c ⊢_d_τ N N' : d

∀@ d_i d_o ∈d_σ.
(∉(ϕ) ∧∉(ϕ') ∧: d_i d_o ∈d_τ) ∨

x:d_i, k : d_o d_τ d ⊢_d_τ ϕ() ϕ'() : d

⊢_d_τ M y N ϕM' y N' ϕ' :  d

Next, the rules for errors

⊢_d_σ^r M :  c^r
⊢_d_σ M : c

*[right=ErrStrict]E[] ≡

The generic rules for casts

⊢_d_σ M N : (c : A B) c : A A
⊢_d_σ A B M N : B

⊢_σ M : A c : A B
⊢_σ M A B M : c

*[right=ValUpEval]A B M ≡M x A B x

c : AB ⊢_σ N : B
⊢_σ A B N N : c

⊢_d_σ M N : (c: A B)
⊢_d_σ M A B N : A

*[right=ValDnEval]A B M ≡M x A B x

⊢_d_σ M N : c d_σ : στ
⊢_τστM N : c

⊢_σ M : A d_σ: στ
⊢_d_σ M στM : c

d_σ: στ⊢_τ N : A
⊢_d_σ στN N : A

d_σ: στ⊢_d_σ M N : c
⊢_σ M στN : c

And the subtyping rules

⊢_d_σ M N : cd_σ: στc : A B

d_σ' : σ' τ'c' : A' B'

σσ'A A' ττ' B B'

⊢_d_σ'M N : c'

c : A B c' : A' B' c c' ⊢_σ M : A
⊢_σA B M ≡A'B' M : B'

c : A B c' : A' B' c c' ⊢_σN : B
⊢_σA B N ≡A'B' N : σA'

c_σ: στc' : σ' τ' c_σc'_σ⊢_σM : A
⊢_τ' στM ≡σ'τ' M : A

c_σ: στc' : σ' τ' c_σc'_σ⊢_τN : A
⊢_σ'στN ≡σ'τ' N : A

In Figure <ref>, we list some derivable reasoning principles
for our inequational theory, which follow by analogous proofs to prior

AAM ≡MσσM ≡MAAM ≡MσσM ≡M

BCAB M ≡AC M ABBC M ≡A C M σ'σ”σσ' M ≡σσ” M σσ'σ'σ” M ≡σ σ” M

ABσσ'M ≡σσ'ABMABσσ'M ≡σσ'ABM

Proveable Uniqueness Theorems

We can show the following properties of the interaction between subtyping and casts axiomatically:

The following hold:

* $\sg^\ltdyn \vDash_{d_\sigma} \upcast {A'} {B'} M \ltdyn \upcast {A} {B} N : B' $.

* $\sg^\ltdyn \vDash_{d_\sigma} \dncast {A} {B} M \ltdyn \dncast {A'} {B'} N : A' $.

* $\sg^\ltdyn \vDash_{\sigma_2'} \upcast {\sigma_1'} {\sigma_2'} P \ltdyn \upcast {\sigma_1} {\sigma_2} Q : c$.

* $\sg^\ltdyn \vDash_{\sigma_1'} \dncast {\sigma_1} {\sigma_2} P \ltdyn \dncast {\sigma_1'} {\sigma_2'} Q : c$.

* We have

* [right = (ValUpL)]
* [right = (Subtyping)]
* [right = (ValUpR)]
⊢_d_σ M N : A
⊢_dσ M A B N : A B

⊢_d_σ M A B N : A' B'

⊢_dσ A' B' M A B N : B'

* Dual to the above.

* We have

* [right = (EffUpL)]
* [right = (Subtyping)]
* [right = (EffUpR)]
⊢_σ_1 P Q : c
⊢_d_σ P σ_1 σ_2 Q : c

⊢_d_σ' P σ_1 σ_2 Q : c

⊢_σ_2' σ_1' σ_2' P σ_1 σ_2 Q : c

* Dual to the above.

§ OPERATIONAL SEMANTICS

∈(ϕ) E'
E[E'[V] x N ϕ]

(E'[y]) x N ϕ

E[V x N ϕ]

E[(λx. M) V]  E[M[V/x]]

E[VxM]  E[M[V/x]]

E[N_tN_f]  E[N_t]

E[N_tN_f]  E[N_f]

E[ σσ' V ]

E[ V ]

E[ σσ' V ]

E[ V ]

∈σ' E'
E[ σσ' E'[
V] ]

E[ B B' A A' V
σ σ' E'[x] ]

E[ σσ' E'[
V] ]

E[ B B' A A' V
σ σ' E'[x] ]

E[ σ E'[
V] ]

E[ ]

E[ ↕M ]

E [M]

E[ ((A →_σB) (A' →_σ' B') V_f)  V ]

E [B B' σσ' (V_f A A' V) ]

E[ ((A →_σB) (A' →_σ' B') V_f)  V ]

E [B B' σσ' (V_f A A' V) ]

Full Operational Semantics

Δ::= σA

ΔσEA →_σB ·σNA
ΔσE  NB

⊢_σ V : A →_σB σ_i CσEA
σ_i CσV  EB

E ⊢_σN_tB ⊢_σN_fB
E N_tN_f B

ΔσEA @ A B ∈σ
ΔσE B

E A

Γ, x : A τN B

(∀(A_B_) ∈σ.
(∉(ϕ) ∧(A_B_) ∈τ)

∨(Γ, x:A_, k:B_τB τϕ() B))

τE x N ϕ B

σE A Γ, x : AσNB
E x N B

EA' ⊢A' A

Δσ'EA ⊢σ' σ

E A ⊢A B
A B E B

E B ⊢A B
A B E A

σ E A ⊢σσ'
σ' σσ' E A

σ' E A ⊢σσ'
σ σσ' E A

Typing Rules for Evaluation Contexts

An evaluation context $E_{\apart \effname}$ is one in which none of
the handler clauses in the spine of the context handles $\effname$.

(A B E)

(A B E)

E ∉σ∉σ'
(σσ' E)

E ∉σ'
(σσ' E)

E '  any effect

E ∧∉(ϕ)
(E x N ϕ)

(E  M)

(V  E)

(E N_t N_f)

(E x N)

Apartness of Effect from an Evaluation Context

§.§ Operational Semantics from First Principles

Now we show that every operational reduction is justified by our
inequational theory.

Let $\sigma \ltdyn \tau$ where $\sigma$ is a concrete effect set.

Then the upcast $\upcast \sigma \tau$ is equivalent to a handler in that for any $M : \compty \sigma A$:

\[ \upcast \sigma \tau M \equiv \hndl M x x {\phi_{\upcast \sigma \tau}}\]

where for each $\effname \in \dom(\sigma)$

\[ x,k \vdash \phi_{\upcast{\sigma}\tau}(\effname) = k(\dncast{B_\sigma}{B_\tau}\raiseOpwithM \effname {\upcast {A_\sigma}{A_\tau}}) \]

where $\effname @ A_\sigma \leadsto B_\sigma \in \sigma$ and
$\effname @ A_\tau \leadsto B_\tau \in \tau$.

Similarly, the downcast $\dncast \sigma \tau$ is equivalent to a
handler in that for any $N : \compty \tau A$:

\[
\dncast \sigma \tau M \equiv
\hndl M x x {\phi_{\dncast \sigma \tau}}
\]

where for each $\effname \in \dom(\tau)$, if $\effname
\in\dom(\sigma)$, then

\[ x,k \vdash \phi_{\dncast\sigma\tau}(\effname)
= k(\upcast{B_\sigma}{B_\tau}\raiseOpwithM \effname {\dncast {A_\sigma}{A_\tau}})
\]

and if $\effname \not\in\dom(\sigma)$, then

\[ \phi_{\dncast\sigma\tau}(\effname) = \err \]

First for the upcast case

* We want to show

\[ \upcast \sigma \tau M \ltdyn \hndl M x x {\phi_{\upcast \sigma \tau}} \]

By UpL, it is sufficient to show

\[ M \ltdyn \hndl M x x {\phi_{\upcast \sigma \tau}} \]

But by the handler $\eta$ rule, this is equivalent to showing

\[ \hndl M x x {\phi_{\sigma}} \ltdyn \hndl M x x {\phi_{\upcast \sigma \tau}} \]

where $\dom(\phi_\sigma) = \dom(\sigma)$ and $\phi_{\sigma}(\effname) =
k(\raiseOpwithM \effname x)$.
Then by congruence, we need to show that for each $\effname \in \dom(\sigma)$,

\[ k(\raiseOpwithM \effname x) \ltdyn k(\dncast {B_\sigma}{B_\tau}\raiseOpwithM \effname \upcast {A_\sigma}{A_\tau} x)\]

which follows from UpR/DnR and congruence rules

* We want to show

\[ \hndl M x x {\phi_{\upcast \sigma \tau}} \ltdyn \upcast \sigma \tau M \]

By handler $\eta$ it is sufficient to show

\[ \hndl M x x {\phi_{\upcast \sigma \tau}} \ltdyn \hndl {\upcast \sigma \tau M} x x {\phi_{\tau}} \]

where $\dom(\phi_{\tau}) = \dom(\tau)$ and $\phi_\tau(\effname) =
k(\raiseOpwithM \effname x)$.
Then $M \ltdyn {\upcast \sigma \tau M}$ by UpR and so
by congruence we need only to show for each $\effname \in \sigma$

\[ \phi_{\upcast\sigma\tau}(\effname)\ltdyn \phi_\tau(\effname) \]

which follows by a similar argument to the previous case.

Next, the downcast cases.

* We want to show

\[ \hndl N x x {\phi_{\dncast\sigma\tau }} \ltdyn \dncast \sigma \tau N \]

By DnR, it is sufficient to show

\[ \hndl N x x {\phi_{\dncast\sigma\tau }} \ltdyn N \]

By handler $\eta$ this is equivalent to showign

\[ \hndl N x x {\phi_{\dncast\sigma\tau }} \ltdyn \hndl N x x {\phi_{\tau}} \]

That is, for any $\effname \in \dom(\tau)$ that

\[ \phi_{\dncast\sigma\tau}(\effname) \ltdyn \phi_\tau(\effname) \]

There are two cases

* If $\effname \in \dom(\sigma)$, then we need to show

\[ k(\upcast {B_\sigma}{B_\tau}\raiseOpwithM \effname {\upcast {A_\sigma}{A_\tau} x})
\ltdyn k(\raiseOpwithM \effname x)\]

which follows by congruence and DnL/UpL rules.

* If $\effname \notin \dom(\sigma)$, then we need to show

\[ \err \ltdyn k(\raiseOpwithM \effname x)\]

which is immediate.

* We want to show

\[ \dncast \sigma \tau N \ltdyn \hndl N x x {\phi_{\dncast\sigma\tau}} \]

By handler $\eta$ this is equivalent to showing

\[ \hndl {(\dncast \sigma \tau N)} x x {\phi_{\sigma}} \ltdyn \hndl N x x {\phi_{\dncast\sigma\tau}} \]

By congruence and DnL this reduces to showing for each $\effname
\in \dom(\sigma)$ that

\[ \phi_\sigma(\effname) \ltdyn \phi_{\dncast\sigma\tau}(\effname)\]

since $\effname \in \dom(\sigma)$, these are each of the form:

\[ k(\raiseOpwithM \effname x) \ltdyn k(\upcast {B_\sigma}{B_\tau}\raiseOpwithM \effname {\upcast {A_\sigma}{A_\tau} x}) \]

which follows by congruence and DnR/UpR rules.

\[ \upcast {A \effto \sigma B}{A' \effto \tau B'} f
\equiv
\lambda x. \upcast B{B'}\upcast \sigma \tau (f (\dncast A {A'} x))
\]

And similarly,

\[ \dncast {A \effto \sigma B}{A' \effto \tau B'} f
\equiv
\lambda x. \dncast B{B'}\dncast \sigma \tau (f (\upcast A {A'} x))
\]

We show the upcast cases, the downcast cases are precisely dual.

* We want to show

\[ \upcast {A \effto \sigma B}{A' \effto \tau B'} f
\ltdyn
\lambda x. \upcast B{B'}\upcast \sigma \tau (f (\dncast A {A'} x))
\]

By UpL, it is sufficient to show

\[ f
\ltdyn
\lambda x. \upcast B{B'}\upcast \sigma \tau (f (\dncast A {A'} x))
\]

By $\eta$ equivalence for functions it is sufficient to show

\[ \lambda x. f x
\ltdyn
\lambda x. \upcast B{B'}\upcast \sigma \tau (f (\dncast A {A'} x))
\]

Which follows by congruence rules and UpR/DnR rules.

* We want to show

\[
\lambda x. \upcast B{B'}\upcast \sigma \tau (f (\dncast A {A'} x))
\ltdyn
\upcast {A \effto \sigma B}{A' \effto \tau B'} f
\]

By function $\eta$ it is sufficient to show

\[
\lambda x. \upcast B{B'}\upcast \sigma \tau (f (\dncast A {A'} x))
\ltdyn
\lambda y. (\upcast {A \effto \sigma B}{A' \effto \tau B'} f) y
\]

Which follows by congruence and UpL/DnL/UpR rules.

If $x,k \vdash \phi(\effname) = k(\raiseOpwithM \effname x)$, then

\[
\hndl {\raiseOpwithM \effname x} y N \phi
\equiv \letXbeboundtoYinZ {(\raiseOpwithM \effname x)} o
\hndl o y N \phi
\]

\begin{align*}
\hndl {\raiseOpwithM \effname x} y N \phi
&\equiv \hndl {(\letXbeboundtoYinZ {\raiseOpwithM \effname x} o o} y N \phi\\
&\equiv (\lambda o. \hndl o y N \phi)(\raiseOpwithM \effname x)\\
&\equiv \letXbeboundtoYinZ {(\raiseOpwithM \effname x)} o \hndl o y N \phi
\end{align*}

This lemma is useful for the cast cases of the following, as it
reduces to showing the cast is equivalent to one whose $\effname$ case
is just a re-raise.

If $E \apart \effname$, then

\[ E[\raiseOpwithM \effname x] \equiv \letXbeboundtoYinZ {\raiseOpwithM \effname x} y {E[y]}\]

By induction on $\effname \apart E$

* $\inferrule {} {\effname \apart \bullet}$

\begin{align*}
\raiseOpwithM \effname x &\equiv \letXbeboundtoYinZ {\raiseOpwithM \effname x} y y
\end{align*}

* $\inferrule
{\effname \apart E}
{\effname \apart (\upcast A B E) }$

\begin{align*}
\upcast A B E[\raiseOpwithM \effname x]
&\equiv \letXbeboundtoYinZ {E[\raiseOpwithM \effname x]} y \upcast A B y\\
&\equiv \letXbeboundtoYinZ {(\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} z E[z])} y \upcast A B y\\
\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} z
\letXbeboundtoYinZ {E[z]} y \upcast A B y\\
\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} z
\upcast A B {E[z]}
\end{align*}

* $\inferrule
{\effname \apart E}
{\effname \apart (\dncast A B E) }$

Similar to previous.

* $\inferrule
{\effname \apart E}
{\effname \apart (\raiseOpwithM{\effname'}{E})}$

\begin{align*}
\raiseOpwithM{\effname'}{E[\raiseOpwithM {\effname'} x]}
&\equiv\raiseOpwithM{\effname'}{(\letXbeboundtoYinZ {\raiseOpwithM {\effname'} x} z E[z])}\\
\letXbeboundtoYinZ {\raiseOpwithM {\effname'} x} z E[z]
\raiseOpwithM{\effname'}{()}\\
\end{align*}

* $\inferrule
{\effname \apart E \and
\effname\not\in\dom(\phi)}
{\effname \apart (\hndl {E} {y} {N} \phi)}$

Define $\psi$ to be the extension of $\phi$ with the case
$\psi(\effname) = k(\raiseOpwithM \effname x)$.

\begin{align*}
\hndl {E[\raiseOpwithM \effname x]} {y} {N} \phi
&\equiv\hndl {E[\raiseOpwithM \effname x]} {y} {N} \psi\\
&\equiv\hndl {(\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} z E[z])} {y} {N} \psi\\
&\equiv (\lambda o. \hndl {E[o]} y N \psi)(\raiseOpwithM \effname x)\\
&\equiv (\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} o \hndl {E[o]} y N \psi)\\
&\equiv (\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} o \hndl {E[o]} y N \phi)\\
\end{align*}

* $\inferrule
{\effname \apart E}
{\effname \apart (E\, M)}$

\begin{align*}
(E[\raiseOpwithM \effname x]) M
\letXbeboundtoYinZ {E[\raiseOpwithM \effname x]} f
\letXbeboundtoYinZ M y {f\,y}\\
\letXbeboundtoYinZ {(\letXbeboundtoYinZ {\raiseOpwithM \effname x} z {E[z]})} f
\letXbeboundtoYinZ M y {f\,y}\\
\letXbeboundtoYinZ {\raiseOpwithM \effname x} z
\letXbeboundtoYinZ {E[z]} f
\letXbeboundtoYinZ M y {f\,y}\\
\letXbeboundtoYinZ {\raiseOpwithM \effname x} z
\end{align*}

* $\inferrule
{\effname \apart E}
{\effname \apart (V\, E)}$

\begin{align*}
(V\,E[\raiseOpwithM \effname x])
\letXbeboundtoYinZ V f
\letXbeboundtoYinZ {E[\raiseOpwithM \effname x]} y
\letXbeboundtoYinZ V f
\letXbeboundtoYinZ {(\letXbeboundtoYinZ {\raiseOpwithM \effname x} z E[z])} y
\letXbeboundtoYinZ {(\letXbeboundtoYinZ {\raiseOpwithM \effname x} z E[z])} y
\letXbeboundtoYinZ {\raiseOpwithM \effname x} z
\letXbeboundtoYinZ {(E[z])} y
\letXbeboundtoYinZ {\raiseOpwithM \effname x} z
\end{align*}

* $\inferrule
{\effname \apart E}
{\effname \apart (\ifXthenYelseZ E {N_t} {N_f})}$

\begin{align*}
\ifXthenYelseZ {E[\raiseOpwithM \effname x]} {N_t} {N_f}
&\equiv \letXbeboundtoYinZ {(E[\raiseOpwithM \effname x])} y
\ifXthenYelseZ y {N_t} {N_f}\\
&\equiv \letXbeboundtoYinZ {(\letXbeboundtoYinZ {\raiseOpwithM \effname x} z E[z])} y
\ifXthenYelseZ y {N_t} {N_f}\\
\letXbeboundtoYinZ {\raiseOpwithM \effname x} z
\letXbeboundtoYinZ {(E[z])} y
\ifXthenYelseZ y {N_t} {N_f}\\
\letXbeboundtoYinZ {\raiseOpwithM \effname x} z
\ifXthenYelseZ {E[z]} {N_t} {N_f}\\
\end{align*}

* $\inferrule
{\effname \apart E}
{\effname \apart (\letXbeboundtoYinZ E x N)}$

\begin{align*}
\letXbeboundtoYinZ {E[\raiseOpwithM \effname x]} y N
&\equiv \letXbeboundtoYinZ {\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} z E[z]} y N\\
\letXbeboundtoYinZ {(\raiseOpwithM \effname x)} z
\letXbeboundtoYinZ {E[z]} y N
\end{align*}

If $M \stepstar M'$ then $M \equiv M'$ is derivable in the
inequational theory.

* The value handle, boolean/function $\beta$ reductions and error reduction are immediate by axioms.

\[ \inferrule
{E \apart \effname}
{\hndl {E[\raiseOpwithM \effname V]} y N \phi \equiv
\phi(\effname)[V/x,\lambda o. \hndl {E[o]} y N \phi/k]
} \]

\begin{align*}
\hndl {E[\raiseOpwithM \effname V]} y N \phi
&\equiv \hndl {(\letXbeboundtoYinZ {\raiseOpwithM \effname V} z E[z])} y N \phi\tag{Lemma\ref{lem:apart-raise}}\\
&\equiv \phi(\effname)[V/x,\lambda o. \hndl {E[o]} y N \phi/k]
\end{align*}

\[   \upcast \sigma {\tau} {V} \equiv V \]

By the following:

\begin{align*}
\upcast \sigma {\tau} {V}
&\equiv \hndl V x x {\phi_{\upcast\sigma\tau}}\tag{Lemma~\ref{lem:eff-casts-are-handlers}}\\
&\equiv V\tag{Handle $\beta$}
\end{align*}

\[ \dncast \sigma {\tau} {V} \equiv V \]
is similar to the

\[  \inferrule
{ \effname @ A \leadsto B \in \sigma \and
\effname @ A' \leadsto B' \in \tau \and
E \apart \effname}
{ \upcast \sigma {\tau} E[\raiseOpwithM {\effname} {V}]
\equiv
\letXbeboundtoYinZ
{\dncast {B} {B'} \raiseOpwithM{\effname}{\upcast {A} {A'} V}}
{\upcast {\sigma} {\tau} E[x]}

\begin{align*}
\upcast \sigma {\tau} E[\raiseOpwithM {\effname} {V}]
\hndl {(E[\raiseOpwithM {\effname} {V}])} x x {\phi_{\upcast \sigma \tau}}\tag{Lemma\ref{lem:eff-casts-are-handlers}}\\
\hndl {(\letXbeboundtoYinZ {\raiseOpwithM {\effname} {V}} z E[z])} x x {\phi_{\upcast \sigma \tau}}\tag{Lemma\ref{lem:apart-raise}}\\
\phi_{\upcast \sigma \tau}(\effname)[V/x,\lambda o. \hndl {E[o]} x x {\phi_{\upcast \sigma \tau}}]\\
&= (\lambda o. \hndl {E[o]} x x {\phi_{\upcast \sigma \tau}})(\dncast {B} {B'}\raiseOpwithM \effname {\upcast A {A'} V})\\
&\equiv (\lambda o. \upcast\sigma\tau E[o])(\dncast {B} {B'}\raiseOpwithM \effname {\upcast A {A'} V})\\
\letXbeboundtoYinZ {(\dncast {B} {B'}\raiseOpwithM \effname {\upcast A {A'} V})} o
\upcast \sigma \tau {E[o]}\\
\end{align*}

\[  \inferrule
{ \effname @ A \leadsto B \in \sigma \and
\effname @ A' \leadsto B' \in \tau \and
E \apart \effname}
{ \dncast \sigma {\tau} E[\raiseOpwithM {\effname} {V}]
\equiv
\letXbeboundtoYinZ
{\upcast {B} {B'} \raiseOpwithM{\effname}{\dncast {A} {A'} V}}
{\dncast {\sigma} {\tau} E[x]}
} \]

Similar to previous

\[    \inferrule
{ \effname \notin \sigma \and E \apart \effname}
{ \dncast \sigma {\dyn} E[ \raiseOpwithM {\effname} {V}]
\equiv
\err
\]

\begin{align*}
\dncast \sigma {\dyn} E[ \raiseOpwithM {\effname} {V}]
&\equiv \hndl {(E[ \raiseOpwithM {\effname} {V}])} x x {\phi_{\dncast\sigma\dyn}}\tag{Lemma\ref{lem:eff-casts-are-handlers}}\\
&\equiv \hndl {(\letXbeboundtoYinZ {(\raiseOpwithM {\effname} {V})} z E[z])} x x {\phi_{\dncast\sigma\dyn}}\tag{Lemma\ref{lem:apart-raise}}\\
&\equiv \err
\end{align*}

\[ \upcast \boolty \boolty V \equiv V \]
By the identity rule.

\[ \dncast \boolty \boolty V \equiv V\]
By the identity rule.

\[ { (\upcast {(A \to_\sigma B)} {(A' \to_{\tau} B')} V_f)\, V
\equiv
\upcast B {B'} \upcast \sigma {\tau} (V_f \dncast {A} {A'} V)

By the following:

\begin{align*}
(\upcast {(A \to_\sigma B)} {(A' \to_{\tau} B')} V_f)\, V &\equiv
((\lambda x.  \upcast{B}{B'}\upcast{\sigma}{\tau}(V_f (\dncast{A}{A')}x)))\, V\tag{Lemma\ref{lem:derivation-fun-casts}}\\
&\equiv\upcast{B}{B'}\upcast{\sigma}{\tau}(V_f (\dncast{A}{A')}V) \tag{$\beta\to$}
\end{align*}

* Similar to previous.

If $\cdot\vdash_\emptyset M \equiv M' : \boolty$ is derivable in the equational theory
than for any $R \in \{ \tru,\fls,\mho \}$

\[ M \stepstar R \iff M' \stepstar R \]

$\tru \equiv \fls$ is not derivable.

If $\cdot \vdash_\emptyset M \ltdyn M' : \boolty$
Then for any $R \in \{\tru,\fls\}$,

\[ M \stepstar R \Rightarrow M' \stepstar R \]

and for any $R' \in \{\tru,\fls,\err\}$,

\[ M' \stepstar R' \implies M \stepstar R' \]

§ ELABORATION

If $A \gsubty B$ then there exist types $A_h,D_h,D_l, B_l$ with

* $c_l : A \ltdyn D_l$ and $c_h : A_h \ltdyn D_h$ satisfying $c_l \subty c_h$

* $d_l : B_l \ltdyn D_l$ and $d_h : B \ltdyn D_h$ satisfying $d_l \subty d_h$

* $e_l : D_l \ltdyn D$ and $e_h : D_h \ltdyn D$ with $e_l \subty
e_h$ where $D = \lceil A \rceil = \lceil B \rceil$.

By induction on the proof of $A \gsubty A'$.

Then the four different choices of cast are all
equivalent in the inequational theory:

Given $A,A_h,B,B_l,D_l,D_h,D, c_l,c_h,d_l,d_h,e_l,e_h$ as in the
output of the previous lemma, for any $\Gamma\vdash M : \compty
{\sigma} A$, the following four terms are equivalent at type $B$.

* $\dncast{B}{D_h}\upcast{A_h}{D_h}M$

* $\dncast{B}{D_h}\upcast{A}{D_l}M$

* $\dncast{B_l}{D_l}\upcast{A}{D_l}M$

* $\dncast{B}{D}\upcast{A}{D}M$

* To show (1) is equivalent to (2), it suffices to show

\[ \upcast{A_h}{D_h}M \equiv \upcast{A}{D_l}M \]

which is an instance of the subtyping/cast rule since $c_l \ltdyn c_h$.

* Similarly to show (2) is equivalent to (3) follows from
$d_l \subty d_h$

* Lastly we show (4) is equivalent to (2).
By cast functoriality,

\[ \dncast{B}{D}\upcast{A}{D}M \equiv \dncast{B}{D_h}\dncast{D_h}{D}\upcast{D_l}{D}\upcast{A}{D_l}M\]

And by retraction the middle cast $\dncast{D_h}{D}\upcast{D_l}{D}$
is the identity.

§ LOGICAL RELATION

We introduce the following logical relations as subsets of well typed
terms in the core language. We first introduce some notation.

For a type precision derivation $d$, define $d^l$ and $d^r$ to be the
types such that $d : d^l \ltdyn d^r$. We additionally make the
analogous definition for effect precision derivations $d_\sigma$.

c     :=
{ (V^l, V^r) : (V^l) ∧(V^r) ∧
(· · ∅ V^l c^l) ∧(· · ∅ V^r c^r) }

A^l A^r d_σ     :=
{ (M^l, M^r) :
(· · d_σ^l M^l A^l) ∧(· · d_σ^r M^r A^r) }

c σ^lA^l σ^rA^r     :=
{ (x^l.M^l, x^r.M^r) :
(x^l : c^l · σ^l M^l A^l) ∧(x^r : c^r · σ^r M^r A^r) }

Well typed atoms

(M_1, M_2) ∈(R)_j
j = 0 ∨(j = k + 1 ∧(M_1, M_2) ∈R_k)

(V_1,V_2) ∈ j
(V_1, V_2) ∈ ∧

(V_1 = V_2 = ) ∨(V_1 = V_2 = )

(V_1,V_2) ∈d_i →_d_σ d_o j
(V_1, V_2) ∈d_i →_d_σ d_o ∧

∀k ≤j.
∀(V_i1, V_i2) ∈d_i k.

(V_1  V_i1, V_2 V_i2) ∈d_σ k (d_o)

(M_1, M_2) ∈d_σ j (R, A^l, A^r)
(M_1, M_2) ∈A^l A^r d_σ ∧

M_1 j+1
∨(∃k ≤j.
(M_1 j-k )
∨(∃(N_1,N_2) ∈d_σ k R ∧M_1 j-k N_1 ∧M_2 N_2))

(M_1, M_2) ∈d_σ j (R, A^l, A^r)
(M_1, M_2) ∈A^l A^r d_σ ∧

M_2 j+1
∨(∃k ≤j.
(M_2 j-k ∧M_1 )
∨(∃N_2. M_2 j-k N_2 ∧M_1 )
∨(∃(N_1,N_2) ∈d_σ k R ∧M_2 j-k N_2 ∧M_1 N_1))

(M_1, M_2) ∈d_σ j (R, A^l, A^r)
(M_1, M_2) ∈A^l A^r d_σ ∧

(((M_1) ∧(M_2) ∧(M_1, M_2) ∈R j)

∨(∃: c d ∈d_σ,
E^l , E^r , V^l, V^r.
(V^l,V^r)  ∈(c)_j      ∧

(x^l.E^l[x^l], x^r.E^r[x^r]) ∈(d )_j
(d_σ  (R, A^l, A^r),
d_σ^rA^r)     ∧
M_1 = E^l[V^l] ∧M_2 = E^r[V^r]))

(x^l.M^l, x^r.M^r) ∈
c j (S, σ^lA^l, σ^rA^r)
(M^l, M^r) ∈c σ^lA^l σ^rA^r ∧

∀k ≤j. (V^l,V^r) ∈c k.
(M^l[V^l/x^l], M^r[V^r/x^r]) ∈S_k

(γ_1,γ_2) ∈Γ^ j
∀(x_1 x_2 : c) ∈Γ^.
(γ_1(x_1), γ_2(x_2)) ∈c j

Logical Relation

§.§ Graduality

c     :=
{ (V^l, V^r) : (V^l) ∧(V^r) ∧
(· · ∅ V^l c^l) ∧(· · ∅ V^r c^r) }

A^l A^r d_σ     :=
{ (M^l, M^r) :
(· · d_σ^l M^l A^l) ∧(· · d_σ^r M^r A^r) }

c σ^lA^l σ^rA^r     :=
{ (x^l.M^l, x^r.M^r) :
(x^l : c^l · σ^l M^l A^l) ∧(x^r : c^r · σ^r M^r A^r) }

Well typed atoms

Our main goal is to prove the soundness of the inequational theory
with respect to the logical relation. That is

If $\Gamma^\ltdyn \vdash_{d_\sigma} M \ltdyn N : c$ then
$\Gamma^\ltdyn \vDash_{d_\sigma} M \ltdyn N : c$

By induction on the term precision derivation.

* (ValSubst) Lemma <ref>

* (MonadUnitL) Lemma <ref>

* (MonadUnitR) Lemma <ref>

* (MonadAssoc) Lemma <ref>

* (BoolBeta) Lemmas <ref> and <ref>

* (BoolEta) Lemma <ref>

* (IfEval) Lemma <ref>

* (FunBeta) Lemma <ref>

* (FunEta) Lemma <ref>

* (AppEval) Lemma <ref>

* (HandleBetaRet) Lemma <ref>

* (HandleBetaRaise) Lemma <ref>

* (HandleEmpty) Lemma <ref>

* (HandleExt) Lemma <ref>

* (RaiseEval) Lemma <ref>

* (Variable) Lemma <ref>

* (Let) Lemma <ref>

* (Boolean) Lemma <ref>

* (If) Lemma <ref>

* (Lambda) Lemma <ref>

* (App) Lemma <ref>

* (Raise) Lemma <ref>

* (HandleCong) Lemma <ref>

* (Transitivity) Lemma <ref>

* (ErrBot) Lemma <ref>

* (ErrStrict) Lemma <ref>

* (SubtyMon) Lemma <ref>

* (ValUpSub) Lemma <ref>

* (ValDnSub) Lemma <ref>

* (EffUpSub) Lemma <ref>

* (EffDnSub) Lemma <ref>

* (ValUpL) Follows from Lemma <ref>.

* (ValUpR) Follows from Lemma <ref>.

* (ValUpEval) Lemma <ref>

* (ValDnR) Follows from Lemma <ref>.

* (ValDnL) Follows from Lemma <ref>.

* (ValDnEval) Lemma <ref>

* (ValRetract) Lemma <ref>.

* (EffUpL) Follows from Lemma <ref>

* (EffUpR) Follows from Lemma <ref>

* (EffDnR) Follows from Lemma <ref>

* (EffDnL) Follows from Lemma <ref>

* (EffRetract) Lemma <ref>.

We begin with a few lemmas that will be useful in our proofs.

§.§.§ Lemmas

If $(V_1, V_2) \in R$, and $V_1$ and $V_2$ are values of type $A^l$ and $A^r$ respectively, then $(V_1, V_2) \in \simirrel {d_\sigma} j {(R, A^l, A^r)}$.

We will establish the first disjunct in the definition of $\simirrel{\cdot}{}{}$. This follows by assumption.

If $(V_1, V_2) \in \simirrel {d_\sigma} j (R, A^l, A^r)$, then $(V_1, V_2) \in \simierel {d_\sigma} j (R, A^l, A^r)$.

Let $\sim\, \in \{<, >\}$, and suppose $(V_1, V_2) \in \simirrel {d_\sigma} j (R, A^l, A^r)$. Notice that regardless of whether $\sim$ is $<$ or $>$, we will be able to show the last clause in the definition of $\ltierel {d_\sigma} {j} (R, A^l, A^r)$ or $\gtierel {d_\sigma} {j} (R, A^l, A^r)$. In particular, we can take $k = j$, $V_1 = V_1$, and $V_2 = V_2$, noting that $V_1$ steps to itself in $0$ steps, as does $V_2$. Thus, it remains to show that $V_1$ and $V_2$ are related by $\ltirrel {d_\sigma} {j} (R, A^l, A^r)$ or $\gtirrel {d_\sigma} {j} (R, A^l, A^r)$. This is true by assumption.

If $(V_1, V_2) \in \simivrel {c} j$, then $(V_1, V_2) \in \simierel {d_\sigma} j {\simivrel {c} {}}$.

By Lemma <ref> (with $R = \simivrel c {}$), it suffices to show that $(\sigma_1 V_1, \sigma_1 V_2) \in \simirrel {d_\sigma} j {\simivrel {c} {}}$. This is true by Lemma <ref>, again with $R = \simivrel c {}$.

Suppose $M_1 \stepsin {i_1} M_1'$ and $M_2 \stepsin {i_2} M_2'$.

If $(M_1', M_2') \in \gtierel {d_\sigma} {j - i_2} (R, A^l, A^r)$, then
$(M_1, M_2) \in \gtierel {d_\sigma} j (R, A^l, A^r)$.

Similarly, if $(M_1', M_2') \in \ltierel {d_\sigma} {j - i_1} (R, A^l, A^r)$, then
$(M_1, M_2) \in \ltierel {d_\sigma} j (R, A^l, A^r)$.

We prove the first statement; the second is analogous (and in fact easier).
The assumption that $(M_1', M_2') \in \gtierel {d_\sigma} {j - i_2} (R, A^l, A^r)$ has four cases:

* $M_2' \stepsin {j-i_2+1}$. In this case, $M_2 \stepsin {i_2} M_2' \stepsin {j-i_2+1}$, i.e, $M_2 \stepsin {j+1}$. Thus, we may assert the first disjunct in the definition of $\gtierel {d_\sigma} j (R, A^l, A^r)$.

* There exists $k \le j-i_2$ such that $M_1' \stepsin {j-i_2-k} \err$, and furthermore $M_1' \stepsin * \err$. In this case, we have that $M_2 \stepsin {i_2} M_2' \stepsin {j-i_2-k} \err$, so $M_2 \stepsin {j-k} \err$. Also, $M_1 \stepsin {i_1} M_1' \stepsin * \err$, so $M_1 \stepsin * \err$. Thus, we may assert the second disjunct.

* There exists $k \le j-i_2$ and $N_2$ such that $M_2' \stepsin {j-i_2-k} N_2$ and $M_1' \stepsin * \err$. In this case we have $M_2 \stepsin {i_2} M_2' \stepsin {j-i_2-k} N_2$, so $M_2 \stepsin {j-k} N_2$. Thus, we may assert the third disjunct.

* Similar to previous case.

Suppose $M_1 \stepsin {i_1} M_1'$ and $M_2 \stepsin {i_2} M_2'$, and that
$(M_1', M_2') \in \simierel {d_\sigma} {j - m} (R, A^l, A^r)$, where $m = \min\{i_1, i_2\}$.
Then $(M_1, M_2) \in \simierel {d_\sigma} j (R, A^l, A^r)$.

Follows from one-sided anti-reduction (Lemma <ref>) and downward closure.

Suppose $M_1 \stepsin {i_1} M_1'$ and $M_2 \stepsin {i_2} M_2'$.

If $(M_1, M_2) \in \gtierel {d_\sigma} {j + i_2} (R, A^l, A^r)$, then
$(M_1', M_2') \in \gtierel {d_\sigma} j (R, A^l, A^r)$.

Similarly, if $(M_1, M_2) \in \ltierel {d_\sigma} {j + i_1} (R, A^l, A^r)$, then
$(M_1', M_2') \in \ltierel {d_\sigma} j (R, A^l, A^r)$.

Follows from determinism of evaluation and a case analysis on the assumption that $M_1$ and $M_2$ are related.

Suppose $M_1 \stepsin {i_1} M_1'$ and $M_2 \stepsin {i_2} M_2'$, and that
$(M_1, M_2) \in \simierel {d_\sigma} {j + m} (R, A^l, A^r)$, where $m = \max\{i_1, i_2\}$.
Then $(M_1', M_2') \in \simierel {d_\sigma} j (R, A^l, A^r)$.

Follows from one-sided forward reduction (Lemma <ref>) and downward closure.

Frequently in our proofs we will encounter a situation where we know that two
evaluation contexts are related in the $\simikrel{\cdot}{}{}$ relation, that is,
substituting related values gives related outputs.
On the other hand, as a cast applied to a value is not necessarily itself a value,
we cannot reason directly about what happens when such semantic values are substituted into
related evaluation contexts. We therefore introduce the following lemma.

Suppose $E_1$ and $E_2$ are evaluation contexts that take values to values.
Let $V_1$ and $V_2$ be values (not necessarily related) such that

\[
(E_1[V_1], E_2[V_2]) \in \simierel {d_\sigma'} {j} {\simivrel {c} {}}.
\]

Furthermore, let $(E^l[x^l], E^r[x^r] \in \simikrel {c} {j} {\simierel {d_\sigma} {} {\simivrel {d} {}}})$.

\[ (E^l[E_1[V_1]], E^r[E_2[V_2]]) \in \simierel {d_\sigma} {j} {\simivrel {d} {}}. \]

We show the proof for $\sim\, =\, >$.

By assumption, we have that there exist values $V_1'$ and $V_2'$ such that
$E_1[V_1] \stepsin {i_1} V_1'$ and $E_2[V_2] \stepsin {i_2} V_2'$, for some $i_1$ and $i_2$.

Thus, $E^l[E_1[V_1]] \stepsin {i_1} E^l[V_1']$ and likewise $E^r[E_2[V_2]] \stepsin {i_2} E^r[V_2']$.

By one-sided anti-reduction (Lemma <ref>), it suffices to show that

\[ (E^l[V_1'], E^r[V_2']) \in \gtierel {d_\sigma} {j - i_2} {\gtivrel {d} {}}. \]

By assumption on $E^l$ and $E^r$ being related, it suffices to show that
$(V_1', V_2') \in \gtivrel {c} {j - i_2}$.

Now by one-sided forward reduction (Lemma <ref>), it suffices to show

\[ (E_1[V_1], E_2[V_2]) \in \gtierel {d_\sigma} {(j - i_2) + i_2} {\simivrel {c} {}}. \]

But this is precisely our assumption, so we are finished.

The reason why we needed to consider cases on $\sim$ separately is that the more “generic”/two-sided
anti-reduction and forward-reduction lemmas involve the $\min$ or $\max$ of the number of steps
taken by the two terms. These may not be equal, in which case the arithmetic wouldn't work out.
But this doesn't mean the above lemma is false.
Conceptually, what is happening is that in the two-sided variants of the lemmas,
$\sim$ could be either $>$ or $<$.
On the other hand, the key here is that $\sim$ stays the same throughout the application of
anti-reduction and forward reduction, so we are able to use the more specific, one-sided lemmas.

If $M_1 \stepsin {(i+1)}$, then $(M_1, M_2) \in \ltierel {d_\sigma} i R$.
Similarly, if $M_2 \stepsin {(i+1)}$, then $(M_1, M_2) \in \gtierel {d_\sigma} i R$.

Suppose $M_1 \stepsin {(i+1)}$. Then we may assert the first disjunct in the definition of $\ltierel {d_\sigma} i R$ to conclude that $(M_1, M_2) \in \ltierel {d_\sigma} i R$. Likewise, if $M_2 \stepsin {(i+1)}$, then we may assert the first disjunct in the defintion of $\gtierel {d_\sigma} i R$ to conclude that $(M_1, M_2) \in \gtierel {d_\sigma} i R$.

We present two trivial lemmas about the later modality. We do this to cut down on tedious reasoning about step indices within other proofs.

Let $R$ be a monotone step-indexed relation. If $(M_1, M_2) \in R_j$, then $(M_1, M_2) \in (\later R)_j$.

Suppose $(M_1, M_2) \in R_j$. If $j = 0$, then $(M_1, M_2) \in (\later R)_0$ trivially.

Otherwise, let $j = j' + 1$. By monotonicity of $R$, we have $(M_1, M_2) \in R_{j'}$, from which it follows that $(M_1, M_2) \in (\later R)_j$.

Let $R$ be a monotone step-indexed relation, and let $j$ be of the form $j = j' + 1$. If $(M_1, M_2) \in (\later R)_j$, then $(M_1, M_2) \in (\later R)_{j'}$.

Suppose $(M_1, M_2) \in (\later R)_j$. Since $j = j' + 1$, by definition of $\later$ we must have that $(M_1, M_2) \in R_{j'}$. By the previous lemma (Lemma <ref>), we conclude $(M_1, M_2) \in (\later R)_{j'}$, which is what we needed to show.

Suppose $M \stepsin 1 M'$ and $N \stepsin 1 N'$, and that
$(M', N') \in (\later \simierel {d_\sigma} {} {})_{k} {R}$.
Then $(M, N) \in \simierel {d_\sigma} {k} {R}$.

First suppose $k = 0$. Then by the time-out lemma (Lemma <ref>),
regardless of whether $\sim$ is $<$ or $>$, we have $(M, N) \in \simierel {d_\sigma} {0} R$.

Now suppose $k \ge 1$. Then by the definition of later, we have that
$(M', N') \in \simierel {d_\sigma} {k - 1} {R}$, so by anti-reduction
we have that $(M, N) \in \simierel {d_\sigma} {k} {R}$.

Let $P(n)$ be a predicate indexed by a natural number $n$.
Suppose for all natural numbers $n$, we have that $(\later^m P)(n)$ implies $P(n)$ for all $m \ge 1$.
Then $P(n)$ is true for all natural numbers $n$.

The proof is by induction on $n$. When $n = 0$, the assumption says that $(\later P)(0)$ implies $P(0)$ (we have taken $m = 1$).
So, it suffices to show that $(\later P)(0)$ holds. This is true by the definition of later.

Now let $n \ge 1$ be fixed, and suppose $P(n)$ is true. We claim that $P(n+1)$ is true.
By our assumption, it will suffice to show that $(\later P)(n+1)$ is true. (We have again chosen $m = 1$.)
By definition of later, we must show $P(n)$ is true. But $P(n)$ is true by assumption.

We now introduce a key lemma about evaluation contexts.

Note: In the below, we omit explicit mention of the types associated to the relations that parameterize $\simierel{\cdot}{}{}$ and $\simirrel{\cdot}{}{}$.

* $(M_1, M_2) \in \simierel {d_\sigma'} j {S'}$

* For all $k \le j$ and $(N_1, N_2) \in \simirrel {d_\sigma'} k {S'}$, we have $(E_1[N_1], E_2[N_2]) \in \simierel {d_\sigma} k S$,

then $( E_1[M_1], E_2[M_2] ) \in \simierel {d_\sigma} j S$.

We prove the lemma for $\sim\, =\, >$; the other case is similar. Based on assumption (1), there are four cases:

* Case $M_2 \stepsin {j+1}$. We have $E_2[M_2] \stepsin {j+1}$, so we may assert the first disjunct in the definition of $\simierel {d_\sigma} j S$ to conclude that $( E_1[M_1], E_2[M_2] ) \in \simierel {d_\sigma} j S$.

* Case $\exists k \le j$ such that $M_2 \stepsin {j-k} \err$ and $M_1 \stepsin * \err$. We have $E_2[M_2] \stepsin {j-k+1} \err$. If $k = 0$, then we have $E_2[M_2] \stepsin {j+1}$, so we may assert the first disjunct. Otherwise, if $k \ge 1$, then we may take $k' = k-1$ and observe that $E_2[M_2] \stepsin {j-k'} \err$.

* Case $\exists k \le j$, $\exists V_2$ such that $M_2 \stepsin {j-k} N_2$ and $M_1 \stepsin * \err$. We have $E_2[M_2] \stepsin {j-k} E_2[N_2]$, so we may assert the third disjunct with $k = k$ and $N_2 = E_2[N_2]$.

* Case $\exists k \le j, \exists (N_1, N_2) \in \gtirrel {d_\sigma} k {S'}$ such that $M_2 \stepsin {j-k} N_2$ and $M_1 \stepsin * N_1$. We have $E_1[M_1] \stepsin {i_1} E_1[N_1]$ for some $i_1$, and $E_2[M_2] \stepsin {j-k} E_2[N_2]$. By assumption (2), we have $(E_1[N_1], E_2[N_2]) \in \simierel {d_\sigma} k S$.
Thus, we may assert the fourth disjunct with $V_1 = E_1[N_1]$ and $V_2 = E_2[N_2]$.

Let $c : A \ltdyn A'$ and $d : B \ltdyn B'$.
Let $E_1$ and $E_2$ be evaluation contexts such that
$\hastyDRhoMT{\holeRhoT{d_\sigma'^l}{A}}{d_\sigma^l}{E_1}{B}$ and

* $(M_1, M_2) \in \simierel {d_\sigma'} j (S', A, A')$.

* For all $k \le j$ and $(V_1, V_2) \in S'_k$, we have $(E_1[V_1], E_2[V_2]) \in \simierel {d_\sigma} k (S, B, B')$.

* For all $k \le j$ and for all $\effname : c_\effname \leadsto d_\effname \in d_\sigma'$, if $E_1$ catches
$\effname$ or $E_2$ catches $\effname$, then for all $V^l, V^r \in (\later \simivrel {c_\effname} {})_k$
and all evaluation contexts $E^l \apart \effname$ and $E^r \apart \effname$ such that
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_\effname}{})_k
(\simierel{d_\sigma'} {} {(S', A, A')},
\RbngT{d_\sigma'^l}{A},
\RbngT{d_\sigma'^r}{A'})$, we have

\in \simierel {d_\sigma} k (S, B, B')$.

Then $( E_1[M_1], E_2[M_2] )
\in \simierel{d_\sigma} j (S, B, B')$.

We use Löb induction (Lemma <ref>). We assume that if the premises
of the lemma are satisfied “later”, then the conclusion holds later.
We show under this assumption that the lemma holds “now".

We first apply Lemma <ref>. The first hypothesis is immediate.
Now let $k \le j$ and let $(N_1, N_2) \in \simirrel {d_\sigma'} k (S', A, A')$. We need to show that

\[ (E_1[N_1], E_2[N_2]) \in \simierel {d_\sigma} k (S, B, B'). \]

There are two cases to consider. In the first case, $N_1$ and $N_2$ are values and $(N_1, N_2) \in \simivrel c j$.
Then by assumption (2) with $k = j$, we have $(E_1[N_1], E_2[N_2]) \in \simierel {d_\sigma} j (S, B, B')$, as needed.

In the second case, there exist
$\effname' : c' \leadsto d' \in d_\sigma'$, $E^l \apart \effname', E^r \apart \effname'$, and $V^l, V^r$ such that
$(V^l, V^r) \in (\later \simivrel{c'}{})_j$, and
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in\\
(\later \simikrel{d'}{})_j
(\simierel{d_\sigma'} {} {(S', A, A')},
\RbngT{d_\sigma'^l}{A},
\RbngT{d_\sigma'^r}{A'})$,
$N_1 = E^l[\raiseOpwithM{\effname'}{V^l}]$ and
$N_2 = E^r[\raiseOpwithM{\effname'}{V^r}]$.

$N_1' = E_1[N_1] = E_1[E^l[\raiseOpwithM{\effname'}{V^l}]]$ and
$N_2' = E_2[N_2] = E_2[E^r[\raiseOpwithM{\effname'}{V^r}]]$.

We need to show that

\[
( N_1', N_2' )
\in \simierel {d_\sigma} j {(S, B, B')}.
\]

We now consider whether one of $E_1$ or $E_2$ catches $\effname'$, or whether neither catches it.
In the former case, assumption (3) immediately implies the desired result.

Now suppose neither $E_1$ nor $E_2$ catches $\effname$. In this case, note that since
$\effname' \apart E^l$ and $\effname' \apart E_1$, we have $\effname' \apart E_1[E^l]$.

Likewise, we have $\effname' \apart E_2[E^r]$.
It follows that $N_1'$ and $N_2'$ are stuck terms, i.e., they do not step.
Thus, it suffices to show that

\[
( N_1', N_2' )
\in \simirrel {d_\sigma} j {(S, B, B')}.
\]

We first claim $(V^l, V^r) \in (\later \simivrel{c'}{})_{j}$.
Since $(V^l, V^r) \in (\later \simivrel{c'}{})_j$,
this follows by Lemma <ref>.

We now claim that

\[
( x^l.(E_1[E^l[x^l]]), x^r.(E_2[E^r[x^r]]) ) \in\\
(\later \simikrel{d'}{})_{j}
(\simierel{d_\sigma} {} {(S, B, B')},
\RbngT{d_\sigma^l}{B},
\RbngT{d_\sigma^r}{B'}).
\]

To this end, let $k \le j$ and let $(V'^l, V'^r) \in (\later \simivrel {d'} {})_k$. We need to show that

\[
( E_1[E^l[V'^l]], E_2[E^r[V'^r]] ) \in
(\later \simierel{d_\sigma} {} {})_{k} {(S, B, B')}.
\]

By the Löb induction hypothesis, it suffices to show that the three hypotheses of the lemma hold
We claim that $(E^l[V'^l], E^r[V'^r]) \in (\simierel{d_\sigma'} {k} {\simivrel c {}})$.
To see this, recall our assumption that

\[
( x^l.E^l[x^l], x^r.E^r[x^r] ) \in
(\later \simikrel{d'}{})_j
(\simierel{d_\sigma'} {} {\simivrel c {}}).
\]

Thus, we have that $( E^l[V'^l], E^r[V'^r] ) \in (\later \simierel{d_\sigma'} {} {})_{k} ({\simivrel c {}})$,
which is what we needed to show.

We now introduce a few lemmas about precision derivations. We first show how we may “compose” precision derivations:

* If $c : A \ltdyn B$ and
$d : B \ltdyn C$ then
$c \circ d : A \ltdyn C$.

* If $d_\sigma : \sigma \ltdyn \sigma'$ and
$d_\sigma' : \sigma' \ltdyn \sigma''$ then
$d_\sigma \circ d_\sigma' : \sigma \ltdyn \sigma''$.

We prove these statements simultaneously by induction on $d$ and $d_\sigma'$.

* Case $d = \boolty$. We have $B = C = \boolty$, so $c = \boolty$ (the reflexivity derivation). Thus, we may take $c \circ d = \boolty$.

* Case $d = d_i \to_{d_\sigma} d_o$. Inspecting the rules in figure <ref>,
we see that $B = B_i \to_{B_\sigma} B_o$ and $C = C_i \to_{C_\sigma} C_o$. Thus, we must have $A = A_i \to_{A_\sigma} A_o$,
which means that $c = c_i \to_{c_\sigma} c_o$.

We may take $c \circ d = (c_i \circ d_i) \to_{c_\sigma \circ d_\sigma} (c_o \circ d_o)$.
By our inductive hypotheses, we have
(1) $c_i \circ d_i : A_i \ltdyn C_i$,
(2) $c_\sigma \circ d_\sigma : A_\sigma \ltdyn C_\sigma$, and
(3) $c_o \circ d_o : A_o \ltdyn C_o$.
Now, using the type precision formation rule for functions, we get that $(c_i \circ d_i) \to_{c_\sigma \circ d_\sigma} (c_o \circ d_o) : (A_i \to_{A_\sigma} A_o \ltdyn C_i \to_{C_\sigma} C_o)$.