# Handling Fibred Algebraic Effects

Danel Ahman

► To cite this version:

Danel Ahman. Handling Fibred Algebraic Effects. Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), pp.1-29. 10.1145/3158095. hal-01672734

HAL Id: hal-01672734

https://hal.science/hal-01672734

Submitted on 12 Oct 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Handling Fibred Algebraic Effects

DANEL AHMAN, Inria Paris, France

We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar's effect theories, whose dependently typed operations allow us to capture precise notions of computation, e.g., state with location-dependent store types and dependently typed update monads. Our treatment of handlers is based on an observation that their conventional term-level definition leads to unsound program equivalences being derivable in languages that include a notion of homomorphism. We solve this problem by giving handlers a novel type-based treatment via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a set of value terms (the operations), capturing Plotkin and Pretnar's insight that effect handlers denote algebras. We then show that the conventional presentation of handlers can be routinely derived, and demonstrate that this type-based treatment of handlers provides a useful mechanism for reasoning about effectful computations. We also equip the resulting language with a sound denotational semantics based on families fibrations.

CCS Concepts: • Software and its engineering → Functional languages; • Theory of computation → Type theory; Control primitives; Type structures; Program specifications; Denotational semantics;

Additional Key Words and Phrases: Dependent Types, Algebraic Effects, Handlers of Algebraic Effects

## ACM Reference Format:

Danel Ahman. 2018. Handling Fibred Algebraic Effects. *Proc. ACM Program. Lang.* 2, POPL, Article 7 (January 2018), 29 pages. https://doi.org/10.1145/3158095

# 1 INTRODUCTION

An important feature of many widely-used programming languages is their support for computational effects (e.g., raising exceptions, accessing memory, performing I/O), which allows programmers to write more efficient and conceptually clearer programs. Therefore, if dependently typed languages are to live up to their promise of providing a lightweight means for integrating formal verification and practical programming, we must first understand how to properly account for computational effects in such languages. While there already exists a range of work on combining these two fields (e.g., Ahman et al. [2016, 2017]; Brady [2013]; Casinghino [2014]; Hancock and Setzer [2000]; McBride [2011]; Nanevski et al. [2008]; Pédrot and Tabareau [2017]; Pitts et al. [2015]), there is still a gap between the rigorous and comprehensive understanding we have of computational effects in the simply typed setting, and what we know about them in the presence of dependent types. For example, in the mentioned works, either the mathematical foundations of the languages developed are not settled, the available effects are limited, or they lack a systematic treatment of (equational) effect specification. In this paper we contribute to the intersection of these two fields by investigating how to combine dependent types with algebraic effects and their handlers.

*Algebraic effects* form a wide class of computational effects that lend themselves to specification using operations and equations; examples include exceptions, state, input-output, nondeterminism, probability, etc. Their study originated with the pioneering work of Plotkin and Power [2001, 2002];

Author's address: Danel Ahman, Prosecco Team, Inria Paris, 2 rue Simone Iff, Paris, 75012, France, danel.ahman@inria.fr.

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2018 Copyright held by the owner/author(s).
2475-1421/2018/1-ART7
https://doi.org/10.1145/3158095
and they have since been successfully applied to, e.g., modularly combining different effects [Hyland et al. 2006] and effect-dependent program optimisations [Kammar and Plotkin 2012]. A key insight of Plotkin and Power was that most of Moggi's monads [Moggi 1989, 1991] are determined by algebraic presentations, with the notable exception of continuations, which are not algebraic.

A major role in the recent rise of interest in algebraic effects can be attributed to their handlers. These were introduced by Plotkin and Pretnar [2013] as a generalisation of exception handlers to all algebraic effects, based on the insight that handlers denote user-defined algebras for the given notion of computation, and the handling construct denotes the homomorphism induced by the universal property of the free algebra. From a programming language perspective, an effect handler

$$ \{\mathrm{op}_x(x') \mapsto N_{\mathrm{op}}\}_{\mathrm{op} \in \mathcal{S}_{\mathrm{eff}}} $$

provides redefinitions of the algebraic operations in the signature $\mathcal{S}_{\mathrm{eff}}$, and the handling construct

$$ M \text{ handled with } \{\mathrm{op}_x(x') \mapsto N_{\mathrm{op}}\}_{\mathrm{op} \in \mathcal{S}_{\mathrm{eff}}} \text{ to } y:A \text{ in } N_{\mathrm{ret}} $$

then recursively traverses the given program $M$, replacing each algebraic operation $op$ with the corresponding user-defined computation term $N_{op}$, e.g., as illustrated by the following $\beta$-equation:

$$ \begin{aligned} & \Gamma \vdash (\mathrm{op}_V^{FA}(y'.M)) \text{ handled with } \{\mathrm{op}_x(x') \mapsto N_{\mathrm{op}}\}_{\mathrm{op} \in \mathcal{S}_{\mathrm{eff}}} \text{ to } y:A \text{ in } N_{\mathrm{ret}} \\ & = N_{\mathrm{op}}[V/x, \lambda y':O[V/x].\text{thunk } H/x'] : \underline{C} \end{aligned} $$

where, for better readability, we abbreviate the recursive call to the handling construct as

$$ H \stackrel{\mathrm{def}}{=} M \text{ handled with } \{\mathrm{op}_x(x') \mapsto N_{\mathrm{op}}\}_{\mathrm{op} \in \mathcal{S}_{\mathrm{eff}}} \text{ to } y:A \text{ in } N_{\mathrm{ret}} $$

Plotkin and Pretnar [2013] also showed that handlers can be used to neatly implement timeouts, rollbacks, stream redirection, etc. More recently, handlers have also gained popularity as a practical and modular programming language abstraction, allowing one to write programs generically in terms of algebraic operations, and then use handlers to modularly provide different fit-for-purpose implementations for these programs. A prototypical example of this approach involves implementing the state operations (get and put) using their natural representation as state-passing functions $\mathrm{St} \to A \times \mathrm{St}$. In order to support this style of programming, existing languages have been extended with algebraic effects and their handlers [Hillerström and Lindley 2016; Kammar et al. 2013; Leijen 2017], and new languages have been built around them [Bauer and Pretnar 2015; Lindley et al. 2017]. However, being simply typed, these languages do not allow the programmer to (equationally) specify the intended behaviour of the computational effects at hand, and thus provide no guarantees that the defined handlers satisfy these specifications, a gap we aim to fill.

The main contributions of this paper are: i) a dependently typed generalisation of Plotkin and Pretnar's effect theories (§3.1); ii) an observation that the conventional term-level definition of effect handlers leads to unsound program equivalences being derivable in languages that include a notion of homomorphism (§4.1); iii) a new computation type, the user-defined algebra type, giving a type-based treatment of handlers and solving the above-mentioned problem with unsound program equivalences (§4.2); iv) a derivation of the conventional term-level definition of handlers from our type-based treatment (§4.3); v) a demonstration that such handlers provide a useful mechanism for reasoning about effectful computations (§7); and vi) a natural denotational semantics for the resulting language based on families fibrations and models of countable Lawvere theories (§8).

This paper is based on §6 and §7 of the author's PhD thesis [Ahman 2017] in which variants of these contributions are presented in a system where the equational proof obligations used in the type-based treatment of handlers are given by definitional equations instead of propositional ones.
## 2 EMLTT: THE UNDERLYING EFFECTFUL DEPENDENTLY TYPED LANGUAGE

We begin with an overview of the language we use as a basis for studying algebraic effects and their handlers in the dependently typed setting, namely, the effectful dependently typed language proposed by Ahman et al. [2016]. This language is a natural extension of Martin-Löf's [1975] intensional type theory (MLTT) with computational effects. It makes a clear distinction between values and computations, both at the level of types and terms, analogously to simply typed languages such as Call-By-Push-Value (CBPV) [Levy 2004] and the Enriched Effect Calculus (EEC) [Egger et al. 2014]. Specifically, we base our work in this paper on a minor extension of Ahman et al.'s language, as explained below. Following Ahman [2017], we refer to this extended language as EMLTT.

As usual for dependently typed languages, EMLTT's types and terms are defined mutually inductively. First, one assumes countable sets of *value variables* x, y, ... and *computation variables* z, ... Next, the grammar of *value types A, B, ...* and *computation types C, D, ...* is given by

$$ 
\begin{align*}
A &::= \text{Nat} \mid 1 \mid 0 \mid A+B \mid \Sigma x:A.B \mid \Pi x:A.B \mid V=A.W \mid U_C \mid C \to D \\
C &::= FA \mid \Sigma x:A.C \mid \Pi x:A.C
\end{align*}
$$

Analogously to Ahman et al. [2016], we omit general inductive types and use natural numbers as a representative example. Compared to op. cit., our value types also include the empty type 0, the sum type $A+B$, and the homomorphic function type $C \to D$. We include the first two as to specify signatures of algebraic effects (see §3.2); and the latter as it is useful for writing effectful code without excessive thunking and forcing, and because it enables us to eliminate values into homomorphism terms, as discussed later in this section. Further, as standard, we write $A \times B$ and $A \to B$ for $\Sigma x:A.B$ and $\Pi x:A.B$ when the value variable $x$ does not appear free in $B$. Finally, we note that $FA$ is the type of possibly effectful computations that return values of type $A$.

Next, the grammar of EMLTT's *value terms* $V, W, ...$ is given by

$$ 
\begin{align*}
V &::= x \mid \star \mid \text{zero} \mid \text{succ } V \mid \text{nat-elim}_{x.A}(V_z, y_1.y_2.V_s, V) \mid \text{case } V \text{ of } \text{of}_{x.A}() \\
  &\qquad \mid \text{inl}_{A+B} V \mid \text{inr}_{A+B} V \mid \text{case } V \text{ of } \text{of}_{x.B} (\text{inl}(y_1:A_1) \mapsto W_1, \text{inr}(y_2:A_2) \mapsto W_2) \\
  &\qquad \mid \langle V, W \rangle_{(x:A).B} \mid \text{pm } V \text{ as } (x_1:A_1, x_2:A_2) \text{ in } y.B \quad W \mid \lambda x:A.V \mid V(W)_{(x:A).B} \mid \lambda z:C.K \\
  &\qquad \mid \text{refl } V \mid \text{eq-elim}_A(x_1.x_2.x_3.B, y.W, V_1, V_2, V_p) \mid \text{fun-ext}_{(x:A).B}(V_1, V_2, W_p) \mid \text{thunk } M
\end{align*}
$$

Observe that in addition to the introduction and elimination forms for the types inherited from MLTT, value terms also include *thunks* of computations and *homomorphic lambda abstractions*. Compared to Ahman et al. [2016] and Ahman [2017], in this paper we further include the axiom of *function extensionality*, so as to enable reasoning about proof obligations given by propositional equalities between functions, e.g., as used in §4.2 for our type-based treatment of effect handlers.

Regarding effectful programs, EMLTT makes a distinction between *computation terms* $M, N, ...$ and *homomorphism terms* $K, L, ...$. The grammar of these two kinds of terms is given by

$$ 
\begin{align*}
M &::= \text{force}_C V \mid \text{return } V \mid M \text{ to } x:A \text{ in}_C N & K &::= z \mid K \text{ to } x:A \text{ in}_C M \\
  &\quad \mid \langle V, M \rangle_{(x:A).C} \mid M \text{ to } (x:A, z:C) \text{ in}_D K & &\quad \mid \langle V, K \rangle_{(x:A).C} \mid K \text{ to } (x:A, z:C) \text{ in}_D L \\
  &\quad \mid \lambda x:A.M \mid M(V)_{(x:A).C} \mid V(M)_{C,D} & &\quad \mid \lambda x:A.K \mid K(V)_{(x:A).C} \mid V(K)_{C,D}
\end{align*}
$$

Computation terms include standard term formers: returning a value, sequential composition, lambda abstraction, and function application. They also include forcing of thunks, introduction and elimination forms for the computational $\Sigma$-type, and homomorphic function applications. Homomorphism terms differ from computation terms in two respects: on the one hand, they do not include `force_C V` and `return V`; on the other hand, they include computation variables $z$, which have to be used i) linearly and ii) in a way that ensures that the computation bound to $z$ “happens”
**Value types:**

$$ \frac{\Gamma \vdash \Gamma \Gamma \vdash Nat}{\Gamma \vdash V : A \quad \Gamma \vdash W : A \quad \Gamma \vdash C \quad \Gamma \vdash C \quad \Gamma \vdash D} $$

**Computation types:**

$$ \frac{\Gamma \vdash A \quad \Gamma \vdash FA \quad \Gamma, x : A \vdash C \quad \Gamma, x : A \vdash C}{\Gamma \vdash \Sigma x : A \vdash C \quad \Gamma \vdash \Pi x : A \vdash C} $$

**Value terms:**

$$ \frac{\Gamma \vdash V : A \quad \Gamma \vdash V_p : V_1 = A \quad V_2 \quad \Gamma, y : A \vdash W : B[y/x_1, y/x_2, \text{refl } y/x_3]}{\Gamma \vdash refl V : V = A \quad \Gamma \vdash \text{eq-elim}_A(x_1.x_2.x_3.B, y.W, V_1, V_2, V_p) : B[V_1/x_1, V_2/x_2, V_p/x_3]} \quad \Gamma \vdash M : C \\ \frac{\Gamma \vdash V_1 : \Pi x : A.B \quad \Gamma \vdash V_2 : \Pi x : A.B \quad \Gamma \vdash W_p : \Pi x : A.(V_1(x)_{(x:A).B} = B \quad V_2(x)_{(x:A).B})}{\Gamma \vdash \text{fun-ext}_{(x:A).B}(V_1, V_2, W_p) : V_1 = \Pi x : A.B \quad V_2} \quad \Gamma \vdash z : C \vdash K : D \\ \frac{\Gamma \vdash \lambda z : C.K : C \to D}{\Gamma \vdash \lambda x : C.K : C \to D} $$

**Computation terms:**

$$ \frac{\Gamma \vdash V : U_C \quad \Gamma \vdash V : A \quad \Gamma \vdash M : FA \quad \Gamma \vdash C \quad \Gamma, x : A \vdash N : C}{\Gamma \vdash \text{force}_C V : C \quad \Gamma \vdash \text{return } V : FA \quad \Gamma \vdash M \text{ to } x : A \text{ in } C : C \quad \Gamma \vdash V : C \to D \quad \Gamma \vdash M : C} $$

**Homomorphism terms:**

$$ \frac{\Gamma \vdash C \quad \Gamma |z : C \vdash K : FA \quad \Gamma \vdash D \quad \Gamma, x : A \vdash M : D}{\Gamma |z : C \vdash K \text{ to } x : A \text{ in } D : M : D} \quad \frac{\Gamma \vdash V : A \quad \Gamma, x : A \vdash D \quad \Gamma |z : C \vdash K : D}{\Gamma |z : C \vdash (V, K)_{(x:A).D} : \Sigma x : A.D} \\ \frac{\Gamma |z_1 : C \vdash K : \Sigma x : A.D_1 \quad \Gamma \vdash D_2 \quad \Gamma, x : A \vdash z_2 : D_1 \vdash L : D_2}{\Gamma |z_1 : C \vdash K \text{ to } (x : A, z_2 : D_1) \text{ in } D_2 : L : D_2} \quad \frac{\Gamma \vdash C \quad \Gamma, x : A \vdash z : C \vdash K : D}{\Gamma |z : C \vdash \lambda x : A.K : \Pi x : A.D} \\ \frac{\Gamma, x : A \vdash D \quad \Gamma |z : C \vdash K : \Pi x : A.D \quad \Gamma \vdash V : A}{\Gamma |z : C \vdash K(V)_{(x:A).D} : D[V/x]} \quad \frac{\Gamma \vdash V : D_1 \to D_2 \quad \Gamma |z : C \vdash K : D_1}{\Gamma |z : C \vdash V(K)_{D_1, D_2} : D_2} $$

<caption>Fig. 1. Selected formation and typing rules for EMLTT's types and terms.</caption>

first" in a term containing it. Omitting the two term formers and using computation variables in this way guarantees that every K denotes a homomorphism in the models we consider in §8.

As such, homomorphism terms were crucial for Ahman et al. [2016] in enabling the elimination form for the computational Σ-type Σx:A.C to be defined correctly. Namely, a term of this type is eliminated into a pair of variables, one denoting a value and the other a computation. To preserve the intended left-to-right evaluation order of one's program, it is crucial that the variable denoting a computation is evaluated first, and not discarded or duplicated arbitrarily, which is guaranteed by how homomorphism terms are defined and how computation variables are used in them.

The *well-formed syntax* of EMLTT is defined using judgements (see Fig. 1) of well-formed value contexts $\Gamma \vdash \Gamma$, value types $\Gamma \vdash A$, and computation types $\Gamma \vdash C$; and well-typed value terms $\Gamma \vdash V : A$, computation terms $\Gamma \vdash M : C$, and homomorphism terms $\Gamma |z : C \vdash K : D$. *Contexts* $\Gamma$ are lists of distinct value variables, each annotated with a value type; and with the *empty context* written as $\diamond$.

As one can readily use thunking and forcing (and homomorphic functions) to eliminate values into computation terms (resp. homomorphism terms), these elimination forms are not included primitively. For example, one can eliminate natural numbers into computation terms as follows:

$$ \text{nat-elim}_{x.C}(M_z, y_1.y_2.M_s, V) \stackrel{\text{def}}{=} \text{force}_{C[V/x]}(\text{nat-elim}_{x.UC}(\text{thunk } M_z, y_1.y_2.\text{thunk } M_s, V)) $$

and (non-dependently) into homomorphism terms as follows:

$$ \text{nat-elim}_{C}(K_z, y.K_s, V) \stackrel{\text{def}}{=} (\text{nat-elim}_{x_1.C \to C}(\lambda z : C.K_z, y.x_2.\lambda z : C.K_s[x_2 \ \mathit{z}/z], V)) \ \mathit{z} $$
**Value terms:**

$$ \frac{\Gamma \vdash A \quad \Gamma, x_1:A, x_2:A, x_3:x_1 =_A x_2 \vdash B \quad \Gamma \vdash V : A \quad \Gamma, y:A \vdash W : B[y/x_1, y/x_2, \text{refl } y/x_3]}{\Gamma \vdash \text{eq-elim}_A(x_1.x_2.x_3.B, y.W, V, V, \text{refl } V) = W[V/y] : B[V/x_1, V/x_2, \text{refl } V/x_3]} $$

$$ \frac{\Gamma \vdash V : U_C}{\Gamma \vdash \text{thunk } (\text{force}_C V) = V : U_C} \qquad \frac{\Gamma \vdash V : C \to \underline{D}}{\Gamma \vdash V = \lambda z : C.V(z)_{C,D} : C \to \underline{D}} $$

**Computation terms:**

$$ \frac{\Gamma \vdash V : A \quad \Gamma \vdash C \quad \Gamma, x:A \vdash M : C}{\Gamma \vdash (\text{return } V) \text{ to } x:A \text{ in } C = M : M[V/x] : C} \qquad \frac{\Gamma \vdash M : FA \quad \Gamma \vdash C \quad \Gamma |z:FA \vdash K : C}{\Gamma \vdash M \text{ to } x:A \text{ in } C K[\text{return } x/z] = K[M/z] : C} $$

$$ \frac{\Gamma \vdash M : C}{\Gamma \vdash \text{force}_C (\text{thunk } M) = M : C} \qquad \frac{\Gamma \vdash M : C \quad \Gamma |z:C \vdash K : \underline{D}}{\Gamma \vdash (\lambda z:C.K)(M)_{C,D} = K[M/z] : \underline{D}} $$

**Homomorphism terms:**

$$ \frac{\Gamma \vdash V : A \quad \Gamma |z_1:C \vdash K : \underline{D_1}[V/x] \quad \Gamma \vdash \underline{D_2} \quad \Gamma, x:A |z_2:D_1 \vdash L : \underline{D_2}}{\Gamma |z_1:C \vdash \langle V, K \rangle_{(x:A).\underline{D_1}} \text{ to } (x:A, z_2:D_1) \text{ in } \underline{D_2} \quad L = L[V/x][K/z_2] : \underline{D_2}} $$

$$ \frac{\Gamma, x:A \vdash \underline{D_1} \quad \Gamma |z_1:C \vdash K \quad \Sigma x:A.\underline{D_1} \quad \Gamma \vdash \underline{D_2} \quad \Gamma |z_3:\Sigma x:A.\underline{D_1} \vdash K \quad \underline{D_2}}{\Gamma |z_1:C \vdash K \text{ to } (x:A, z_2:D_1) \text{ in } \underline{D_2} \quad L[\langle x, z_2 \rangle_{(x:A).\underline{D_1}}/z_3] = L[K/z_3] : \underline{D_2}} $$

$$ \frac{\Gamma \vdash C \quad \Gamma, x:A |z:C \vdash K : \underline{D} \quad \Gamma \vdash V : A}{\Gamma |z:C \vdash (\lambda x:A.K)(V)_{(x:A).\underline{D}} = K[V/x] : \underline{D}[V/x]} \qquad \frac{\Gamma, x:A \vdash \underline{D} \quad \Gamma |z:C \vdash K : \Pi x:A.\underline{D}}{\Gamma |z:C \vdash K = \lambda x:A.K(x)_{(x:A).\underline{D}} : \Pi x:A.\underline{D}} $$

<caption>Fig. 2. Selected definitional equations from EMLTT’s equational theory.</caption>

where we assume that $FCV(K_z) = FCV(K_s) = z$, and where $x_1$ and $x_2$ are chosen fresh.<fnref n="1" />

Analogously to Ahman et al. [2016], we decorate value, computation, and homomorphism terms with a number of type annotations. We use these annotations to define the denotational semantics of EMLTT on raw expressions, so as to avoid well-known coherence problems arising in the interpretation of dependently typed languages; this is a standard technique in the literature [Hofmann 1997; Streicher 1991]. For better readability, we often omit these type annotations in examples.

The well-formed syntax of EMLTT is defined mutually inductively with its *equational theory* (see Fig. 2), consisting of a collection of mutually defined equivalence relations given by *definitional equations* between well-formed value contexts, written $\vdash \Gamma_1 = \Gamma_2$; well-formed types, written $\Gamma \vdash A = B$ and $\Gamma \vdash C = \underline{D}$; and well-typed terms, written $\Gamma \vdash V = W : A$, $\Gamma \vdash M = N : C$, and $\Gamma |z:C \vdash K = L : \underline{D}$. These equations interact with well-formed syntax via conversion rules, such as

$$ \frac{\vdash \Gamma_1 = \Gamma_2 \quad \Gamma_1 \vdash V : A_1 \quad \Gamma_1 \vdash A_1 = A_2}{\Gamma_2 \vdash V : A_2} \qquad \frac{\vdash \Gamma_1 = \Gamma_2 \quad \Gamma_1 \vdash M : \underline{C_1} \quad \Gamma_1 \vdash \underline{C_1} = \underline{C_2}}{\Gamma_2 \vdash M : \underline{C_2}} $$

Note that as EMLTT is based on Martin-Löf’s intensional type theory, the elimination form for propositional equality $V =_A W$ supports a $\beta$-equation but not an $\eta$-equation (see Fig. 2). Similarly, the elimination form for natural numbers also only supports $\beta$-equations. In both cases, this is done so as to avoid known sources of undecidability for typechecking and the equational theory—for more details, see the analysis by Hofmann [1995], and by Okada and Scott [1999], respectively.

Regarding the meta-theory of EMLTT, one can readily prove standard weakening and substitution results, the latter for both value and computation variables. For example, we write $A[V/x]$ for the substitution of $V$ for $x$ in A. Analogously, we write $K[M/z]$ for the substitution of $M$ for $z$ in K.

<footnote n="1">¹FCV(K) denotes the free computation variable of the homomorphism term K.</footnote>
The definitions of both kinds of substitution are straightforward: they proceed by recursion on the structure of the given type or term, making use of the standard convention of identifying types and terms that differ only in the names of bound variables, and assuming that in any definition, etc., the bound variables of types and terms are chosen to be different from any free variables.

We conclude by recalling from Ahman et al. [2016] that one of the notable features of EMLTT is the computational Σ-type Σx:A.C. This computation type provides a uniform means to account for type-dependency in sequential composition, allowing one to “close-off” the type of the second computation with Σx:A.C before using the typing rule for sequential composition that prohibits x to appear free in the type of the second computation. A similar restriction on free variables also appears in other typing rules for effectful programs. As a consequence, EMLTT lends itself to a very natural general denotational semantics based on fibred adjunctions, as studied in detail in Ahman [2017]; Ahman et al. [2016]. Thus, one says that the computational effects in EMLTT are fibred.

# 3 FIBRED ALGEBRAIC EFFECTS

In this section we develop a formal means for specifying computational effects in EMLTT using operations and equations, based on a natural dependently typed generalisation of the effect theories of Plotkin and Pretnar [2013]. We note that while algebraic effects were already discussed by the author in the context of EMLTT in Ahman et al. [2016], they were treated much more informally compared to this paper, e.g., without making precise any particular notion of effect theory.

## 3.1 Fibred Effect Theories

We begin by identifying the fragment of EMLTT which we use to define the types of our operations.

A value type is *pure* if it is built up from only Nat, 1, Σx:A.B, Πx:A.B, 0, A + B, and V =A W, where V, W, and A are all pure in propositional equality V =A W. A value term is *pure* if it does not contain thunks of computations and homomorphic lambda abstractions, and all its type annotations are pure. This notion of pureness extends straightforwardly to contexts—a value context Γ is *pure* if Aᵢ is pure for every xᵢ:Aᵢ ∈ Γ. Note that this fragment of EMLTT corresponds precisely to MLTT.

Assuming a countable set of *effect variables* w, ..., we now define our notion of fibred effect theory. We begin by defining corresponding signatures of operation symbols and then add equations between derivable effect terms, so as to specify both the effects at hand and their behaviour.

A fibred effect signature $S_{\text{eff}}$ consists of a finite set of typed operation symbols $\text{op} : (x:I) \to O$, where $\diamond \vdash I$ and $x:I \vdash O$ are required to be pure value types, called the *input* and *output* type of $\text{op}$.

The *effect terms* $T$ that one can derive from the given fibred effect signature $S_{\text{eff}}$ are given by

$$ T ::= w(V) \mid \text{op}_V(y.T) \mid \text{pm} V \text{ as } (x_1:A_1, x_2:A_2) \text{ in } T \\ \mid \text{case } V \text{ of } (\text{inl}(x_1:A_1) \mapsto T_1, \text{inr}(x_2:A_2) \mapsto T_2) $$

with the involved value types and value terms all required to be pure. We follow the convention of omitting V in $\text{op}_V(y.T)$ when the input type of op is 1, and y when the output type of op is 1. In future, if one were to discover computationally interesting examples needing the elimination forms of other value types (e.g., Nat), then these can be accommodated in effect terms straightforwardly.

An *effect context* Δ is a list of distinct effect variables annotated with pure value types. We say that Δ is *well-formed* in a pure value context Γ, written Γ ⊢ Δ, if ⊢ Γ and Γ ⊢ Aᵢ for every wᵢ: Aᵢ ∈ Δ. Intuitively, each effect variable w:A denotes a continuation that expects a value of type A.

*Well-formed effect terms* are then defined using the judgement Γ | Δ ⊢ T as follows:

$$ \frac{\Gamma \vdash \Delta_1, w:A, \Delta_2 \quad \Gamma \vdash V : A \quad \Gamma \vdash V : I \quad \Gamma \vdash \Delta \quad \Gamma, y:O[V/x] | \Delta \vdash T}{\Gamma | \Delta_1, w:A, \Delta_2 \vdash w(V)} \quad (\text{op} : (x:I) \to O \in S_{\text{eff}}) $$
$$ \frac{\Gamma \vdash V : \Sigma x_1 : A_1 \cdot A_2 \qquad \Gamma \vdash V : A_1 + A_2}{\Gamma \vdash \Delta \quad \Gamma, x_1 : A_1, x_2 : A_2 | \Delta \vdash T \qquad \Gamma \vdash \Delta \quad \Gamma, x_1 : A_1 | \Delta \vdash T_1 \quad \Gamma, x_2 : A_2 | \Delta \vdash T_2}{\Gamma | \Delta \vdash \text{pm } V \text{ as } (x_1 : A_1, x_2 : A_2) \text{ in } T \qquad \Gamma | \Delta \vdash \text{case } V \text{ of } (\text{inl}(x_1 : A_1) \mapsto T_1, \text{inr}(x_2 : A_2) \mapsto T_2)} $$

Finally, a fibred effect theory $\mathcal{T}_{\text{eff}} = (S_{\text{eff}}, \mathcal{E}_{\text{eff}})$ is given by a fibred effect signature $S_{\text{eff}}$ and a finite set $\mathcal{E}_{\text{eff}}$ of equations $\Gamma | \Delta \vdash T_1 = T_2$ between well-formed effect terms $\Gamma | \Delta \vdash T_1$ and $\Gamma | \Delta \vdash T_2$.

In order to simplify the presentation of typing rules involving fibred effect theories, we assume $\Gamma = x_1:A_1, \dots, x_n:A_n$ and $\Delta = w_1:A'_1, \dots, w_m:A'_m$ when quantifying over the variables of $\Gamma, \Delta$.

## 3.2 Examples of Fibred Effect Theories

As our fibred effect theories are a natural dependently typed generalisation of Plotkin and Pretnar's effect theories, we can capture all the effects they can, e.g., assuming a pure value type $\diamond \vdash \text{Exc}$ of exception names, the theory $\mathcal{T}_{\text{EXC}}$ of exceptions is given by one operation symbol raise : $\text{Exc} \to 0$ and no equations. Another standard example is the theory $\mathcal{T}_{\text{ND}}$ of nondeterminism, which is given by one operation symbol or : $1 \to 1 + 1$ and three equations that make or into a semilattice operation.

On the other hand, as the operation symbols of our fibred effect theories are dependently typed, compared to Plotkin and Pretnar's, we can naturally capture more precise notions of computation. We discuss two such examples below: i) a variant of Plotkin and Power's [2002] theory of global state in which the type of stored values is allowed to be dependent on memory locations; and ii) Ahman and Uustalu's [2014] dependently typed update monads that model state in which the store is changed not by overwriting but instead by applying (store-dependent) updates to it, examples of which include non-overflowing buffers and non-underflowing stacks—see op. cit. for details.

**Global state.** First, assume given pure value types of memory locations and values stored at them:

$$ \diamond \vdash \text{Loc} \qquad x : \text{Loc} \vdash \text{Val} $$

such that the propositional equality on Loc is decidable, i.e., we assume given a pure value term:

$$ \diamond \vdash \text{isDec}_{\text{Loc}} : \Pi x : \text{Loc} \cdot \Pi x' : \text{Loc} \cdot (x =_{\text{Loc}} x') + (x =_{\text{Loc}} x' \to 0) $$

We use this assumption below to specify the two fibred effect theory equations that describe the commutativity of reading and writing at different memory locations (4th and 5th equation below). We also use this assumption, and results one can derive from it, to construct proofs of equational proof obligations when we define predicates on effectful computations using effect handlers in §7.

The fibred effect signature $S_{\text{GS}}$ of global state is then given by the two operation symbols

$$ \text{get} : (x : \text{Loc}) \to \text{Val} \qquad \text{put} : \Sigma x : \text{Loc} \cdot \text{Val} \to 1 $$

The idea here is that get denotes an effectful command that returns the current value of the store at the given location; and put denotes a command that overwrites the store at the given location.

The corresponding fibred effect theory $\mathcal{T}_{\text{GS}}$ is then given by the following five equations:

$$ x : \text{Loc} | w : 1 \vdash \text{get}_x(y.\text{put}_{\langle x, y \rangle}(w(\star))) = w(\star) $$

$$ x : \text{Loc}, y : \text{Val} | w : \text{Val} \vdash \text{put}_{\langle x, y \rangle}(\text{get}_x(y' \cdot w(y')))) = \text{put}_{\langle x, y \rangle}(w(y)) $$

$$ x : \text{Loc}, y_1 : \text{Val}, y_2 : \text{Val} | w : 1 \vdash \text{put}_{\langle x, y_1 \rangle}(\text{put}_{\langle x, y_2 \rangle}(w(\star))) = \text{put}_{\langle x, y_2 \rangle}(w(\star)) $$

$$ \begin{aligned} x_1 : \text{Loc}, x_2 : \text{Loc} | w : \text{Val}[x_1/x] \times \text{Val}[x_2/x] &\vdash \text{get}_{x_1}(y_1.\text{get}_{x_2}(y_2 \cdot w(\langle y_1, y_2 \rangle))) \\ &= \text{get}_{x_2}(y_2.\text{get}_{x_1}(y_1 \cdot w(\langle y_1, y_2 \rangle))) \end{aligned} \quad (x_1 \neq x_2) $$
$$
\begin{align*}
x_1: \text{Loc}, x_2: \text{Loc}, y_1: \text{Val}[x_1/x], y_2: \text{Val}[x_2/x] \mid w: 1 \vdash \text{put}_{(x_1, y_1)}(\text{put}_{(x_2, y_2)}(w(\star))) \\
&= \text{put}_{(x_2, y_2)}(\text{put}_{(x_1, y_1)}(w(\star))) \quad (x_1 \neq x_2)
\end{align*}
$$

where the last two equations include a side-condition that requires the locations $x_1$ and $x_2$ to be different. Similarly to Plotkin and Pretnar's effect theories, this is simply an informal shorthand notation. Formally, the right-hand sides of these two equations are written using case analysis on the assumed term `isDecLoc x_1 x_2`, e.g., the right-hand side of the last equation is formally given by

$$
\begin{array}{l}
\text{case } (\text{isDec}_{\text{Loc}} x_1 x_2) \text{ of } (\text{inh}(y_p : x_1 =_{\text{Loc}} x_2) \quad \mapsto \quad \text{put}_{(x_1, y_1)}(\text{put}_{(x_2, y_2)}(w(\star))), \\
\qquad \text{inh}(y_p : x_1 =_{\text{Loc}} x_2 \to 0) \quad \mapsto \quad \text{put}_{(x_2, y_2)}(\text{put}_{(x_1, y_1)}(w(\star))))
\end{array}
$$

Observe how these five equations describe the expected behaviour of `get` and `put`: trivial store changes are not observable (1st equation); `get` returns the most recent value the store has been set to (2nd equation); `put` overwrites the content of the store (3rd equation); and `gets` and `puts` at different locations are independent and commute with each other (4th and 5th equation).

**Dependently typed update monads.** To begin with, we assume given pure value types

$\diamond \vdash \text{St} \quad x : \text{St} \vdash \text{Upd}$

of store values and store updates, respectively, together with well-typed closed pure value terms

$\downarrow : \Pi x : \text{St. Upd} \to \text{St} \quad \circ : \Pi x : \text{St. Upd} \quad \oplus : \Pi x : \text{St. } \Pi y : \text{Upd. Upd}[x \downarrow y/x] \to \text{Upd}$

satisfying the following propositional equalities (for better readability, we omit the type annotations on these equations, and write the first argument to $\oplus$ as a subscript; we also leave implicit the use of the standard transport operation (e.g., see §7.1) in transporting $W$ and $W_3$ in the last two equations along the first two equations so as to ensure that both sides of these equations are well-typed):

$V \downarrow (o V) = V \qquad V \downarrow (W_1 \oplus_V W_2) = (V \downarrow W_1) \downarrow W_2$

$W \oplus_V (o (V \downarrow W)) = W \quad (o V) \oplus_V W = W \quad (W_1 \oplus_V W_2) \oplus_V W_3 = W_1 \oplus_V (W_2 \oplus_{V \downarrow W_1} W_3)$

In the literature, this structure is commonly called a *directed container* [Ahman et al. 2014]. For dependently typed update monads, the high-level idea is that `(Upd, \circ, \oplus)` forms a dependently typed monoid of store updates which can be applied to the store values via its action $\downarrow$ on St.

The signature $S_{\text{UPD}}$ of a dependently typed update monad is then given by two operation symbols:

$\text{lookup} : 1 \to \text{St} \quad \text{update} : \Pi x : \text{St. Upd} \to 1$

The idea here is that `lookup` denotes an effectful command that returns the current value of the store; and `update` denotes a command that applies an appropriate update to the current store (from the family of updates given as its input). The dependency of `Upd` on `St` provides fine-grain control over which updates are applicable to which store values, and allows this to be enforced statically.

The corresponding fibred effect theory $\mathcal{T}_{\text{UPD}}$ is then given by the following three equations:

$\diamond | w: 1 \vdash \text{lookup}(x.update_{\lambda y: \text{St.} o y}(w(\star))) = w(\star)$

$$
\begin{align*}
x : (\Pi x' : \text{St. Upd}[x'/x]) \mid w : \text{St} \times \text{St} \vdash \text{lookup}(y.update_x(\text{lookup}(y'.w(\langle y, y' \rangle)))) \\
&= \text{lookup}(y.update_x(w(\langle y, y \downarrow (x y) \rangle)))
\end{align*}
$$

$$
\begin{align*}
x : (\Pi x' : \text{St. Upd}[x'/x]), y : (\Pi y' : \text{St. Upd}[y'/x]) \mid w: 1 \vdash & \text{update}_x(\text{update}_y(w(\star))) \\
& = \text{update}_{\lambda x''.(x x'') \oplus_{x'''} (y(x'' \downarrow (x x'')))}(w(\star))
\end{align*}
$$
$$
\begin{align*}
\langle \mathrm{w}_j (V) \rangle &\stackrel{\mathrm{def}}{=} V'_j (V[\vec{V}_i / \vec{x}_i]) \\
\langle \mathrm{op}_V (y.T) \rangle &\stackrel{\mathrm{def}}{=} W_{\mathrm{op}} \langle V[\vec{V}_i / \vec{x}_i], \lambda y: O[V[\vec{V}_i / \vec{x}_i] / x] \cdot \langle T \rangle \rangle \\
\langle \mathrm{pm} V \text{ as } (y_1:B_1, y_2:B_2) \text{ in } T \rangle &\stackrel{\mathrm{def}}{=} \mathrm{pm} V[\vec{V}_i / \vec{x}_i] \text{ as } (y_1:B_1[\vec{V}_i / \vec{x}_i], y_2:B_2[\vec{V}_i / \vec{x}_i]) \text{ in } \langle T \rangle \\
\langle \mathrm{case} V \text{ of } (\mathrm{inl}(y_1:B_1) \mapsto T_1, \mathrm{inr}(y_2:B_2) \mapsto T_2) \rangle &\stackrel{\mathrm{def}}{=} \mathrm{case} V[\vec{V}_i / \vec{x}_i] \text{ of } (\mathrm{inl}(y_1:B_1[\vec{V}_i / \vec{x}_i]) \mapsto \langle T_1 \rangle, \\
&\phantom{\stackrel{\mathrm{def}}{=} \mathrm{case} V[\vec{V}_i / \vec{x}_i] \text{ of } (\mathrm{inl}(y_1:B_1[\vec{V}_i / \vec{x}_i]) \mapsto \langle T_1 \rangle,} \mathrm{inr}(y_2:B_2[\vec{V}_i / \vec{x}_i]) \mapsto \langle T_2 \rangle)
\end{align*}
$$

<caption>Fig. 3. Translation of effect terms into value terms.</caption>

These equations are similar to the first three equations of the global state theory $\mathcal{T}_{\text{GS}}$, but instead of an overwriting behaviour, they describe how the store is changed using updates. In particular, observe how $\oplus$ is used to combine subsequent updates, and how $\circ$ gives us “do nothing” updates.

## 3.3 Extending EMLTT with Fibred Algebraic Effects

Next, we show how to extend EMLTT with algebraic effects given by a fibred effect theory $\mathcal{T}_{\text{eff}}$.

First, we extend the grammar of EMLTT's computation terms with *algebraic operations*:

$$M ::= \dots \mid \mathrm{op}_{\vec{V}}^{C}(y.M)$$

for all operation symbols $\mathrm{op}: (x:I) \to O \in \mathcal{S}_{\text{eff}}$ and computation types $\underline{C}$.

Next, in order to extend the well-formed syntax of EMLTT with a corresponding typing rule and definitional equations, we first define a translation of effect terms into value terms. In particular, given an effect term $\Gamma \mid \Delta \vdash T$, a value type $A$, value terms $V_i$ (for all $x_i: A_i \in \Gamma$), value terms $V'_j$ (for all $w_j: A'_j \in \Delta$), and value terms $W_{\text{op}}$ (for all op: $(x:I) \to O \in \mathcal{S}_{\text{eff}}$), we define the *translation of T* into a value term $\langle T \rangle_{A; \vec{V}_i; \vec{V}'_j; \overline{W_{\text{op}}}}$ by recursion on the structure of T, as given in detail in Fig. 3. For better readability, we write $\vec{V}_i$ for $\{V_1, \dots, V_n\}$ in the translation, and similarly for $\vec{V}'_j$ and $\overline{W_{\text{op}}}$.

While we omit the subscripts in Fig. 3 so as to improve readability, it is important to note that in the cases where the given effect term involves variable bindings, the set of value terms $\vec{V}_i$ is extended with the corresponding variables in the right-hand side, e.g., in the second case we have

$$\langle \mathrm{op}_V(y.T) \rangle_{A; \vec{V}_i; \vec{V}'_j; \overline{W_{\mathrm{op}}}} \stackrel{\mathrm{def}}{=} W_{\mathrm{op}} \langle V[\vec{V}_i / \vec{x}_i], \lambda y: O[V[\vec{V}_i / \vec{x}_i] / x] \cdot \langle T \rangle \rangle_{A; \vec{V}_i, y; \vec{V}'_j; \overline{W_{\mathrm{op}}}}$$

While it might be more intuitive and natural to translate effect terms directly into EMLTT's computation terms, giving the translation from effect terms into value terms allows us to later reuse this translation in §4 when we extend EMLTT with handlers of fibred algebraic effects.

We only translate well-formed effect terms $\Gamma \mid \Delta \vdash T$ because it makes it easier to account for substituting value terms $V'_j$ (denoting continuations) for effect variables—various subsequent results refer to substituting value terms for all variables in $\Delta$, not just for the free ones appearing in $T$.

Using this translation of effect terms into value terms, we can now define the typing rule and definitional equations for algebraic operations, as given in Fig. 4. It is worth noting that for presentational convenience, we include the equations given in $\mathcal{E}_{\text{eff}}$ as definitional equations between value terms. The corresponding equations between computation terms are easily derivable, e.g.,

$$\Gamma \vdash \mathrm{get}_{\vec{V}}^{C}(y.\mathrm{put}_{\langle V, y \rangle}^{C}(M)) = M : \underline{C}$$

can be derived from the translation of the corresponding equation in the global state theory $\mathcal{T}_{\text{GS}}$.
Typing rule for algebraic operations:

$$ \frac{\Gamma \vdash V : I \quad \Gamma \vdash \underline{C} \quad \Gamma, y:O[V/x] \vdash M : \underline{C}}{\Gamma \vdash \operatorname{op}_{\bar{V}}^{\underline{C}}(y.M) : \underline{C}} (\operatorname{op} : (x:I) \to O \in S_{\text{eff}}) $$

Congruence equations:

$$ \frac{\Gamma \vdash V = W : I \quad \Gamma \vdash \underline{C} = \underline{D} \quad \Gamma, y:O[V/x] \vdash M = N : \underline{C}}{\Gamma \vdash \operatorname{op}_{\bar{V}}^{\underline{C}}(y.M) = \operatorname{op}_{\bar{W}}^{\underline{D}}(y.N) : \underline{C}} (\operatorname{op} : (x:I) \to O \in S_{\text{eff}}) $$

General algebraicity equations:

$$ \frac{\Gamma \vdash V : I \quad \Gamma, y:O[V/x] \vdash M : \underline{C} \quad \Gamma | z : \underline{C} \vdash K : \underline{D}}{\Gamma \vdash K[\operatorname{op}_{\bar{V}}^{\underline{C}}(y.M)/z] = \operatorname{op}_{\bar{V}}^{\underline{D}}(y.K[M/z]) : \underline{D}} (\operatorname{op} : (x:I) \to O \in S_{\text{eff}}) $$

Equations from the given fibred effect theory:

$$ \frac{\Gamma' \vdash V_i : A_i[V_1/x_1, \dots, V_{i-1}/x_{i-1}] \quad (1 \le i \le n) \\ \Gamma' \vdash \underline{C} \quad \Gamma' \vdash V'_j : A'_j[\vec{V_i}/\vec{x_i}] \to \underline{UC} \quad (1 \le j \le m) \\ \Gamma' \vdash (\langle T_1 \rangle)_{\underline{UC}; \vec{V_i}; \vec{V'_j}; \overline{W_{op}}} = (\langle T_2 \rangle)_{\underline{UC}; \vec{V_i}; \vec{V'_j}; \overline{W_{op}}} : \underline{UC}}{\Gamma | \Delta \vdash T_1 = T_2 \in \mathcal{E}_{\text{eff}}} $$

where the well-typed value terms $\Gamma' \vdash W_{op} : (\Sigma x : I.O \to \underline{UC}) \to \underline{UC}$ are defined as follows:

$$ W_{op} \stackrel{\text{def}}{=} \lambda x' : (\Sigma x : I.O \to \underline{UC}) . \text{pm } x' \text{ as } (x : I, y : O \to \underline{UC}) \text{ in chunk } (\operatorname{op}_{\bar{x}}^{\underline{C}}(y' . \text{force}_{\underline{C}}(y y'))$$

for all op : (x:I) → O ∈ S<sub>eff</sub>.

<caption>Fig. 4. Rules for extending EMLTT with fibred algebraic effects.</caption>

# 4 HANDLERS VIA THE USER-DEFINED ALGEBRA TYPE

## 4.1 A Problem with Adding Conventional Handlers to EMLTT

Before we show how to extend EMLTT with handlers of fibred algebraic effects using the user-defined algebra type, we first explain how extending EMLTT with the conventional term-level definition of handlers quickly leads to unsound program equivalences becoming derivable.

First, recall from §1 that Plotkin and Pretnar (and others since) include handlers in effectful languages by extending the syntax of computation terms with the following handling construct:

$$ M \text{ handled with } \{\operatorname{op}_x(x')\} \mapsto N_{op} \}_{op \in S_{\text{eff}}} \text{ to } y:A \text{ in } N_{\text{ret}} $$

whose semantics is given using the mediating homomorphism from the free algebra over A to the algebra denoted by the handler $\{\operatorname{op}_x(x')\} \mapsto N_{op}\}_{op \in S_{\text{eff}}}$. However, when extending a language that includes a notion of homomorphism, such as EMLTT with its homomorphism terms, this algebraic understanding of handlers suggests that one ought to also extend the given notion of homomorphism with a corresponding handling construct. Unfortunately, if one simply adds

$$ K \text{ handled with } \{\operatorname{op}_x(x')\} \mapsto N_{op} \}_{op \in S_{\text{eff}}} \text{ to } y:A \text{ in } N_{\text{ret}} $$

to EMLTT, the combination of i) the $\beta$-equations associated with the handling construct (see §1) and ii) the general algebraicity equations (see Fig. 4) gives rise to unsound definitional equations.

To explain this problem in more detail, let us consider the theory $\mathcal{T}_{I/O}$ of interactive input-output of bits, given by two operation symbols, read : 1 $\to$ 1 + 1 and write : 1 + 1 $\to$ 1, and no equations.
Next, we define a handler that negates all bits read from the input and written to the output:

$$ \text{read}(x') \mapsto \text{read}^{F1}(y.\text{force}(x' \neg y)) \qquad \text{write}_x(x') \mapsto \text{write}_{-x}^{F1}(\text{force}(x' \star)) $$

where $\neg: 1+1 \rightarrow 1+1$ denotes negation of bits, swapping the left and right injections into $1+1$.

Now, let us consider handling a simple program, $\text{write}_{\text{inl}}^{F1}(\star)$ (return $\star$), using the handler we defined above.<fnref n="2" /> On the one hand, using the $\beta$-equations for handling (see §1), we can prove that

$$ \begin{align*} \Gamma \vdash (\text{write}_{\text{inl}}^{F1}(\star) \text{ (return } \star \text{)}) \text{ handled with } & \{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}} \text{ to } y:1 \text{ in return } \star \\ &= \text{write}_{-(\text{inl } \star)}^{F1}((\text{return } \star) \text{ handled with } \{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}} \text{ to } y:1 \text{ in return } \star) \\ &= \text{write}_{-(\text{inl } \star)}^{F1}(\text{return } \star) \\ &= \text{write}_{\text{inr } \star}^{F1}(\text{return } \star) : F1 \end{align*} $$

On the other hand, using the general algebraicity equations (see Fig. 4), which ensure that homomorphism terms indeed behave as if they were algebra homomorphisms, we can prove that

$$ \begin{align*} \Gamma \vdash (\text{write}_{\text{inl}}^{F1}(\star) \text{ (return } \star \text{)}) \text{ handled with } & \{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}} \text{ to } y:1 \text{ in return } \star \\ &= (z \text{ handled with } \{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}} \text{ to } y:1 \text{ in return } \star)[\text{write}_{\text{inl}}^{F1}(\star)(\text{return } \star)/z] \\ &= \text{write}_{\text{inl}}^{F1}((z \text{ handled with } \{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}} \text{ to } y:1 \text{ in return } \star)[\text{return } \star/z]) \\ &= \text{write}_{\text{inl}}^{F1}((\text{return } \star) \text{ handled with } \{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}} \text{ to } y:1 \text{ in return } \star) \\ &= \text{write}_{\text{inl}}^{F1}(\text{return } \star) : F1 \end{align*} $$

Finally, by combining these two sequences of equations using transitivity, we can prove that

$$ \Gamma \vdash \text{write}_{\text{inr } \star}^{F1}(\text{return } \star) = \text{write}_{\text{inl } \star}^{F1}(\text{return } \star) : F1 $$

which is clearly only valid in trivial models of interactive output, and thus should not be derivable.

The source of this problem lies in the term-level definition of handlers in their usual presentation. In particular, while the homomorphic behaviour of homomorphism terms is determined exclusively by the computation types involved (via the general algebraicity equations), the type of the above handling construct contains no trace of the algebra denoted by the handler $\{\text{op}_x(x') \mapsto N_{\text{op}}\}_{\text{op} \in S_{\text{l/O}}}$.⁵

It is worth noting that this problem is not inherent to EMLTT but also arises in the simply typed setting, e.g., when combining handlers of algebraic effects with CBPV and its stack terms, or with EEC and its linear (computation) terms. For example, CBPV with stack terms and exception handlers has been investigated by Levy [2006]. However, compared to the solution we propose in this paper, Levy follows the opposite direction: namely, while we aim to simultaneously accommodate effect handlers and make sure that homomorphism terms still denote algebra homomorphisms, Levy changes the syntax and equational theory of stack terms so that they can accommodate exception handlers, but with the cost of stack terms not denoting algebra homomorphisms any more.

Finally, we note that the reason why Plotkin and Pretnar [2013] were able to give a sound denotational semantics to their language was precisely due to their choice of using CBPV *without* stack terms, i.e., without a notion of homomorphism, only with value and computation terms.

## 4.2 Extending EMLTT with the User-Defined Algebra Type

In this section we solve the problems of §4.1 by giving handlers a novel type-based treatment that internalises Plotkin and Pretnar's insight that they denote algebras for the given effect theory.

<footnote n="2">²Note that for this illustrative example, we could have omitted read and only considered the signature of interactive output.</footnote>
First, given a fibred effect theory $\mathcal{T}_{\text{eff}}$, we extend EMLTT with the user-defined algebra type:

$$ \underline{C} ::= \dots | \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle $$

which pairs a value type A (the carrier) with two sets of value terms, $\vec{V}_{op}$ (the operations) and $\vec{W}_{eq}$ (the proofs of equational proof obligations showing that $\vec{V}_{op}$ satisfy the equations given in $\mathcal{E}_{\text{eff}}$).

We also extend EMLTT's computation and homomorphism terms with two composition operations:

$$ M ::= \dots | M \text{ as } x: U\underline{C} \text{ in } \overleftarrow{W}_{op;\underline{D}} N $$

$$ K ::= \dots | K \text{ as } x: U\underline{C} \text{ in } \overleftarrow{W}_{op;\underline{D}} N $$

where $\vec{W}_{op}$ are proofs of equational proof obligations showing that the computation term $N$ behaves as if it was a homomorphism term—we discuss this in detail below. These term formers also provide elimination forms for the user-defined algebra type when $\underline{C}$ is $\langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle$; we also note that terms of this type are introduced by forcing thunks of type $U\langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle$, i.e., value terms of type A.

For better readability, we write $\overrightarrow{ref}$ for $\vec{W}_{eq}$ and $\vec{W}_{op}$ in the rest of this paper when all the proof witnesses are given by reflexivity, i.e., when the corresponding equational proof obligations hold definitionally. Also for better readability, we write $\langle A; \vec{V}_{op} \rangle$ for $\langle A; \vec{V}_{op}; \emptyset \rangle$ when $\mathcal{E}_{\text{eff}}$ is empty.

It is worth noting that in principle we could have restricted these composition operations to only the user-defined algebra type $\langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle$, but then we would not have been able to derive a useful isomorphism of computation types to coerce computations between a general $\underline{C}$ and its canonical representation as a user-defined algebra type—see Prop. 4.1 for details of this type isomorphism.

Conceptually, these composition operations are a form of explicit substitution of chunked computations for value variables. For example, in this extension of EMLTT we will be able to show that $M$ as $x: U\underline{C}$ in $\overleftarrow{W}_{op;\underline{D}} N$ is definitionally equal to $N[\text{thunk } M/x]$. As such, the value variable $x$ refers to the whole of (the chunk of) $M$, compared to, e.g., sequential composition $M$ to $x:A$ in $N$, where the value variable $x$ is used to bind only the value produced by $M$. However, it is also important to note that we do not allow arbitrary computation terms to be used in these composition operations. In particular, the typing rules of $M$ as $x: U\underline{C}$ in $\overleftarrow{W}_{op;\underline{D}} N$ and $K$ as $x: U\underline{C}$ in $\overleftarrow{W}_{op;\underline{D}} N$ require that the value variable $x$ is used in the computation term $N$ as if it was a computation variable, in that $x$ must not be duplicated or discarded arbitrarily. We do this in order to ensure that $N$ behaves as if it was a homomorphism term, so that in $N[\text{thunk } M/x]$ the effects of $M$ would be guaranteed to “happen before” those of $N$. However, rather than trying to extend EMLTT further with some form of linearity for such value variables, we impose these requirements via equational proof obligations, requiring that $N$ commutes with algebraic operations (when substituted for $x$ via chunking). As mentioned earlier, the proofs of these proof obligations are given by the value terms $\vec{W}_{op}$.

We make this discussion formal in Fig. 5 by giving the rules for extending EMLTT's well-formed syntax and equational theory with the user-defined algebra type and composition operations, using the following auxiliary judgement in the rules concerning the two composition operations:

$$ \Gamma, y: U\underline{C} \vdash_{\text{hom}} N : \underline{D} \text{ witnessed by } \vec{W}_{op} $$

which holds iff $N$ behaves like a homomorphism from the algebra denoted by $\underline{C}$ to that denoted by $\underline{D}$, witnessed by $\vec{W}_{op}$, i.e., $\Gamma, y: U\underline{C} \vdash N : \underline{D}$ and we have for each op: $(x:I) \to O \in \mathcal{S}_{\text{eff}}$ a proof

$$ \begin{aligned} \Gamma \vdash W_{op} : & \lambda x : I. \lambda x' : O \to U\underline{C}.\text{thunk}(N[\text{thunk}(\text{op}_{x}^{\underline{C}}(x'', \text{force}_{\underline{C}}(x'x''))/y)]) = \\ & \lambda x : I. \lambda x' : O \to U\underline{C}.\text{thunk}(\text{op}_{x}^{\underline{D}}(x'', N[x'x''/y])) \end{aligned} $$
**Formation rule for the user-defined algebra type:**

$$ \Gamma' \vdash A \quad \Gamma' \vdash V_{op} : (\Sigma x : I \to A) \to A \quad (\text{op} : (x : I) \to O \in S_{\text{eff}} \text{ and } \Gamma | \Delta \vdash T_1 = T_2 \in \mathcal{E}_{\text{eff}}) $$

$$ \Gamma' \vdash W_{eq} : \lambda x'_i : \widehat{A_i}. \lambda x_{wj} : \widehat{A'_j} \to A. (\|T_1\|)_{A; x'_j; \vec{x}_{wj}; \vec{V}_{op}} = \lambda x'_i : \widehat{\overline{A_i}}. \lambda x_{wj} : \widehat{\overline{A'_j}} \to A. (\|T_2\|)_{A; x'_i; \vec{x}_{wj}; \vec{V}_{op}} $$

$$ \Gamma' \vdash \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle $$

where $\widehat{A_i} \stackrel{\text{def}}{=} A_i[x'_1/x_1, \dots, x'_{i-1}/x_{i-1}]$ and $\widehat{A'_j} \stackrel{\text{def}}{=} A'_j[x'_1/x_1, \dots, x'_n/x_n]$; and where we write $\lambda x'_i : \widehat{A_i}$, $\widehat{\lambda x_{wj}} : \widehat{A'_j} \to A$, $\Pi \lambda x'_i : \widehat{A_i}$, and $\widehat{\lambda A'_j} \to A$ for sequences of lambda abstractions and function types.

**Typing rules for the composition operations:**

$$ \Gamma \vdash M : \underline{C} \quad \Gamma \vdash \underline{D} \\ \frac{\Gamma, x : U\underline{C} \quad \Gamma_{\text{hom}} : \underline{D} \quad \text{witnessed by } \vec{W}_{op}}{\Gamma \vdash M \text{ as } x : U\underline{C} \quad \text{in } \vec{W}_{op}; \underline{D} \quad N : \underline{D}} $$

$$ \Gamma | z : \underline{C} \vdash K : \underline{D_1} \quad \Gamma \vdash \underline{D_2} \\ \frac{\Gamma, x : U\underline{D_1} \quad \Gamma_{\text{hom}} : \underline{D_2} \quad \text{witnessed by } \vec{W}_{op}}{\Gamma | z : \underline{C} \vdash K \text{ as } x : U\underline{D_1} \quad \text{in } \vec{W}_{op}; \underline{D_2} \quad N : \underline{D_2}} $$

**Congruence equations:**

$$ \frac{\Gamma \vdash \langle A; \vec{V}_{op}; \vec{V}_{eq} \rangle \quad \Gamma \vdash \langle B; \vec{W}_{op}; \vec{W}_{eq} \rangle \quad \Gamma \vdash A = B}{\Gamma \vdash V_{eq} = W_{op} : (\Sigma x : I \to A) \to A \quad (\text{op} : (x : I) \to O)} $$

$$ \Gamma \vdash \langle A; \vec{V}_{op}; \vec{V}_{eq} \rangle = \langle B; \vec{W}_{op}; \vec{W}_{eq} \rangle $$

plus similar equations for composition operations (note the proof irrelevant treatment of $\vec{V}_{eq}$ and $\vec{W}_{eq}$).

**$\beta$-equation for the user-defined algebra type:**

$$ \frac{\Gamma \vdash \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle}{\Gamma \vdash U \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle} = A $$

capturing the intuition that $A$ denotes the carrier of the algebra denoted by $\langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle$.

**$\beta$- and $\eta$-equations for the composition operations:**

$$ \frac{\Gamma \vdash V : U\underline{C} \quad \Gamma \vdash \underline{D} \quad \Gamma, x : U\underline{C} \quad \Gamma_{\text{hom}} : \underline{D} \quad \text{witnessed by } \vec{W}_{op}}{\Gamma \vdash (\text{force}_{\underline{C}} V) \text{ as } x : U\underline{C} \quad \text{in } \vec{W}_{op}; \underline{D} \quad M = M[V/x] : \underline{D}} $$

$$ \frac{\Gamma \vdash M : \underline{C} \quad \Gamma | z : \underline{C} \vdash K : \underline{D}}{\Gamma \vdash M \text{ as } x : U\underline{C} \quad \text{in } \underset{\text{refl}:\underline{D}}{\overline{\text{in}}} \quad K[\text{force}_{\underline{C}} x/z] = K[M/z] : \underline{D}} $$

$$ \frac{\Gamma | z_1 : \underline{C} \vdash K : \underline{D_1} \quad \Gamma | z_2 : \underline{D_1} \vdash L : \underline{D_2}}{\Gamma | z_1 : \underline{C} \vdash K \text{ as } x : U\underline{D_1} \quad \text{in } \underset{\text{refl}:\underline{D_2}}{\overline{\text{in}}} \quad L[\text{force}_{\underline{D_1}} x/z_2] = L[K/z_2] : \underline{D_2}} $$

capturing the intuition that composition operations are a form of explicit substitution of thunks.

**$\eta$-equation for algebraic operations:**

$$ \frac{\Gamma \vdash V : I \quad \Gamma \vdash \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle \quad \Gamma, y : O[V/x] \vdash M : \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle}{\Gamma \vdash \text{op}_V \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle (y, M)} \quad (\text{op} : (x : I) \to O \in S_{\text{eff}}) $$

$$ = \text{force}_{\langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle} (V_{op} \langle V, \lambda y : O[V/x] \cdot \text{thunk } M \rangle) : \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle $$

capturing the intuition that $\vec{V}_{op}$ denote the operations of the algebra denoted by $\langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle$.

<caption>Fig. 5. Rules for extending EMLTT with the user-defined algebra type and the composition operations.</caption>
It is worth noting that by defining this extension of EMLTT using propositional proof obligations instead of definitional ones, as in Ahman [2017], we introduce a form of *equality reflection* into the language. Namely, in any model of this extension of EMLTT, the propositional proof obligations proved by $\overrightarrow{W}_{eq}$ and $\overrightarrow{W}_{op}$ have to also ensure that the corresponding definitional equations are validated in the given model, so as to validate the definitional equations given for algebraic effects in Fig. 4. Based on this extensional nature of these proof obligations, we have naturally chosen to treat them as proof irrelevant in the user-defined algebra type and the composition operations, namely, by not comparing their proofs for definitional equality in the congruence rules (see Fig. 5).

It is also useful to note that if one works exclusively with equation-free fibred effect theories, e.g., as used in the various simply typed languages mentioned in §1 that support algebraic effects and their handlers, then the equational proof obligations used in the typing rule of $\langle A; \overrightarrow{V}_{op}; \overrightarrow{W}_{eq} \rangle$ hold vacuously, and thus do not put any additional burden on the programmer. However, the possibility of also being able to specify effects using equations ensures that the fit-for-purpose handler implementations of the given notion of computation, say, global state, are indeed correct.

We conclude this section by highlighting that we have not included an $\eta$-equation for $\langle A; \overrightarrow{V}_{op}; \overrightarrow{W}_{eq} \rangle$. We do so because it does not hold in the Lawvere theories based semantics we give to this extension of EMLTT in §8. Instead, as promised earlier, we can construct a corresponding type isomorphism.

**PROPOSITION 4.1.** *Given a computation type $\Gamma \vdash \underline{C}$, there exists a computation type isomorphism $\Gamma \vdash \underline{C} \cong \langle UC; \overrightarrow{V}_{op}; \overrightarrow{refl} \rangle$, where each value term $\Gamma \vdash V_{op} : (\Sigma x: I.O \to UC) \to UC$ is given by* 

$$V_{op} \stackrel{\text{def}}{=} \lambda y : (\Sigma x: I.O \to UC). \text{pm } y \text{ as } (x: I, x' : O \to UC) \text{ in trunk } (\text{op}_{\underline{x}}^{\underline{C}}(y'.\text{force}_{\underline{C}}(x' y'))$$

**PROOF.** This type isomorphism is witnessed by the following two homomorphic functions:

$$\Gamma \vdash \lambda z : \underline{C}. z \text{ as } x : UC \text{ in force}_{\langle UC; \overrightarrow{V}_{op}; \overrightarrow{refl} \rangle} x : \underline{C} \dashv \langle UC; \overrightarrow{V}_{op}; \overrightarrow{refl} \rangle \\ \Gamma \vdash \lambda z : \langle UC; \overrightarrow{V}_{op}; \overrightarrow{refl} \rangle. z \text{ as } x : U \langle UC; \overrightarrow{V}_{op}; \overrightarrow{refl} \rangle \text{ in force}_{\underline{C}} x : \langle UC; \overrightarrow{V}_{op}; \overrightarrow{refl} \rangle \dashv \underline{C}$$

□

## 4.3 Deriving the Conventional Term-Level Definition of Handlers

We now show how to derive the conventional term-level definition of handlers from our type-based treatment. In particular, we define the *handling construct* using sequential composition as follows:

$$M \text{ handled with } (\{\text{op}_x(x') \mapsto N_{op}\}_{op \in S_{\text{eff}}}; \overrightarrow{W}_{\text{eq}}) \text{ to } y: A \text{ in } \underline{C} N_{\text{ret}} \\ \stackrel{\text{def}}{=} \\ \text{force}_{\underline{C}} \text{ (trunk } (M \text{ to } y: A \text{ in force}_{\langle UC; \overrightarrow{V}_{op}; \overrightarrow{W}_{\text{eq}} \rangle} \text{ (trunk } N_{\text{ret}} \text{)))}$$

where the value terms $V_{op}$ are defined as follows:

$$V_{op} \stackrel{\text{def}}{=} \lambda x'' : (\Sigma x: I.O \to UC). \text{pm } x'' \text{ as } (x: I, x' : O \to UC) \text{ in trunk } N_{op}$$

Observe that compared to the work of Plotkin and Pretnar [2013], who do not enforce the correctness of their handlers during typechecking and therefore have to give semantics to their language using Kleene equality, we require the set of user-defined computation terms $N_{op}$ to satisfy the equations given in $\mathcal{E}_{\text{eff}}$ (as witnessed by the value terms $\overrightarrow{W}_{eq}$), so as to statically ensure that the given computation terms $N_{op}$ indeed form an algebra. In particular, Plotkin and Pretnar do not enforce the correctness of their handlers during typechecking because it is in general an undecidable problem [Plotkin and Pretnar 2013, §6]. In contrast, by having defined the corresponding equational
proof obligations in this paper using propositional equality, we can naturally accommodate manual user-provided proofs of equations that one cannot establish through automatic means.

The expected typing rule and definitional $\beta$-equations are then routinely derivable for this definition of the handling construct.

**PROPOSITION 4.2.** *The following typing rule is derivable:*

$$ 
\begin{gather*}
\Gamma \vdash M : FA \quad \Gamma \vdash \langle UC; \overrightarrow{V_{op}}; \overrightarrow{W_{eq}} \rangle \quad \Gamma, y : A \vdash N_{ret} : \underline{C} \\
\Gamma \vdash M \text{ handled with } (\{\text{op}_x(x') \mapsto N_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } \underline{C} \text{, } N_{ret} : \underline{C}
\end{gather*}
$$

where each value term $V_{op}$ is derived from the corresponding computation term $N_{op}$ as defined above.

**PROPOSITION 4.3.** *The following definitional $\beta$-equations are derivable:*

$$ 
\begin{gather*}
\Gamma \vdash V : I \quad \Gamma, y' : O[V/x] \vdash M : FA \quad \Gamma \vdash \langle UC; \overrightarrow{V_{op}}; \overrightarrow{W_{eq}} \rangle \quad \Gamma, y : A \vdash N_{ret} : \underline{C} \\
\Gamma \vdash (\text{op}_V^{FA}(y'.M)) \text{ handled with } (\{\text{op}_x(x') \mapsto N_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } \underline{C} \text{, } N_{ret} \\
= N_{op}[V/x, \lambda y' : O[V/x].\text{thunk } H/x'] : \underline{C}
\end{gather*}
$$

$$ 
\begin{gather*}
\Gamma \vdash V : A \quad \Gamma \vdash \langle UC; \overrightarrow{V_{op}}; \overrightarrow{W_{eq}} \rangle \quad \Gamma, y : A \vdash N_{ret} : \underline{C} \\
\Gamma \vdash (\text{return } V) \text{ handled with } (\{\text{op}_x(x') \mapsto N_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } \underline{C} \text{, } N_{ret} \\
= N_{ret}[V/y] : \underline{C}
\end{gather*}
$$

where

$$ H \stackrel{\text{def}}{=} M \text{ handled with } (\{\text{op}_x(x') \mapsto N_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } \underline{C} \text{, } N_{ret} $$

and each value term $V_{op}$ is derived from the corresponding computation term $N_{op}$ as defined above.

## 4.4 Handling Computations into Values

We conclude this section by noting that in addition to the standard "handle into computation terms" handling construct we derived in §4.3, we can also use the user-defined algebra type and sequential composition to define a handling construct that allows computations to be handled directly into value terms, e.g., as briefly discussed in Ahman and Staton [2013] in the context of Levy's [2004] fine-grain call-by-value language. This "handle into value terms" handling construct is given by

$$ 
\begin{gather*}
M \text{ handled with } (\{\text{op}_x(x') \mapsto V_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } B \text{, } V_{ret} \\
\stackrel{\text{def}}{=} \\
\text{thunk } (M \text{ to } y : A \text{ in force } \langle B; \overrightarrow{W_{op}}; \overrightarrow{W_{eq}} \rangle \text{, } V_{ret})
\end{gather*}
$$

where the value terms $W_{op}$ are defined as follows:

$$ W_{op} \stackrel{\text{def}}{=} \lambda x'' : (\Sigma x : I.O \to B). \text{pm } x'' \text{ as } (x : I, x' : O \to B) \text{ in } V_{op} $$

and it satisfies the expected typing rule and definitional $\beta$-equations:

$$ 
\begin{gather*}
\Gamma \vdash M : FA \quad \Gamma \vdash \langle B; \overrightarrow{W_{op}}; \overrightarrow{W_{eq}} \rangle \quad \Gamma, y : A \vdash V_{ret} : B \\
\Gamma \vdash M \text{ handled with } (\{\text{op}_x(x') \mapsto V_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } B \text{, } V_{ret} : B \\
\Gamma \vdash V : I \quad \Gamma, y' : O[V/x] \vdash M : FA \quad \Gamma \vdash \langle B; \overrightarrow{W_{op}}; \overrightarrow{W_{eq}} \rangle \quad \Gamma, y : A \vdash V_{ret} : B \\
\Gamma \vdash (\text{op}_V^{FA}(y'.M)) \text{ handled with } (\{\text{op}_x(x') \mapsto V_{op}\}_{op \in S_{eff}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } B \text{, } V_{ret} \\
= V_{op}[V/x, \lambda y' : O[V/x].H/x'] : B
\end{gather*}
$$
$$ \begin{array}{l} \Gamma \vdash V : A \quad \Gamma \vdash \langle B; \overrightarrow{W_{op}}; \overrightarrow{W_{eq}} \rangle \quad \Gamma, y : A \vdash V_{ret} : B \\ \Gamma \vdash (\text{return } V) \text{ handled with } (\{\text{op}_x(x') \mapsto V_{op}\}_{op \in S_{\text{eff}}}; \overrightarrow{W_{eq}}) \text{ to } y : A \text{ in } B \quad V_{ret} \\ = V_{ret}[V/y] : B \end{array} $$

where

$$ H \stackrel{\text{def}}{=} M \text{ handled with } (\{\text{op}_x(x') \mapsto V_{op}\}_{op \in S_{\text{eff}}}; \overrightarrow{W_{\text{eq}}}) \text{ to } y : A \text{ in } B \quad V_{\text{ret}} $$

In the case the set of equations $\mathcal{E}_{\text{eff}}$ is empty, we write this handling construct simply as

$$ M \text{ handled with } \{\text{op}_x(x') \mapsto V_{op}\}_{op \in S_{\text{eff}}} \text{ to } y : A \text{ in } B \quad V_{\text{ret}} $$

# 5 BASIC META-THEORY

We now discuss some properties of our extension of EMLTT with algebraic effects and their handlers.

## 5.1 Weakening and Substitution

We begin by noting that, as expected, weakening is admissible for value variables.

**THEOREM 5.1 (WEAKENING).** Given $\Gamma_1, \Gamma_2 \vdash B, \Gamma_1 \vdash A$, and $x$ such that $x \notin \text{Vars}(\Gamma_1) \cup \text{Vars}(\Gamma_2)$, then $\Gamma_1, x:A, \Gamma_2 \vdash B$, and similarly for all other judgements of types, terms, and definitional equations.

Next, we note that, as also expected, substitution is admissible for both value and computation variables. As various typing rules and definitional equations now include (translations of) effect terms, we also need to prove the corresponding property for the translation of effect terms.

**PROPOSITION 5.2.** Given $\Gamma \mid \Delta \vdash T$, a value type $A$, value terms $V_i$ (for all $x_i : A_i \in \Gamma$), $V'_j$ (for all $w_j : A'_j \in \Delta$), and $W_{op}$ (for all op : ($x:I \to O \in S_{\text{eff}}$), a value variable $y$, and a value term $W$, then

$$ (\|T\|)_{A;\overrightarrow{V_i};\overrightarrow{V'_j};\overrightarrow{W_{op}}} [W/y] = (\|T\|)_{A[W/y];\overrightarrow{V_i}[W/y];\overrightarrow{V'_j}[W/y];\overrightarrow{W_{op}}[W/y]} $$

**THEOREM 5.3 (SUBSTITUTION).**

* Given $\Gamma_1, x:A, \Gamma_2 \vdash B$ and $\Gamma_1 \vdash V : A$, then $\Gamma_1, \Gamma_2 [V/x] \vdash B [V/x]$, and similarly for other judgements of types, terms, and definitional equations.

* Given $\Gamma \mid z:C \vdash K : D$ and $\Gamma \vdash M : C$, then $\Gamma \vdash K[M/z] : D$.

* Given $\Gamma \mid z_2:D_1 \vdash L : D_2$ and $\Gamma \mid z_1:C \vdash K : D_1$, then $\Gamma \mid z_1:C \vdash L[K/z_2] : D_2$.

Finally, we note that judgements of well-formed types, etc. only refer to well-formed contexts, etc. To this end, we also need to show that under suitable assumptions, $(\|T\|)_{A;\overrightarrow{V_i};\overrightarrow{V'_j};\overrightarrow{W_{op}}}$ is well-typed.

**PROPOSITION 5.4.** Given $\Gamma \mid \Delta \vdash T$ and $\Gamma'$, such that $\Gamma' \vdash A$ and the value terms in the subscripts are well-typed in $\Gamma'$ (as required in Fig. 4), then we have $\Gamma' \vdash (\|T\|)_{A;\overrightarrow{V_i};\overrightarrow{V'_j};\overrightarrow{W_{op}}}: A$.

**PROPOSITION 5.5.** Given $\Gamma \mid \Delta \vdash T$ and $\Gamma'$, such that $\Gamma' \vdash A = B$ and the corresponding value terms in the subscripts are definitionally equal in $\Gamma'$ (analogously to the typing in Fig. 4), then we have

$$ \Gamma' \vdash (\|T\|)_{A;\overrightarrow{V_i};\overrightarrow{V'_j};\overrightarrow{W_{op}}} = (\|T\|)_{B;\overrightarrow{W_i};\overrightarrow{W'_j};\overrightarrow{W_{op}}} : A $$

**THEOREM 5.6.** Given $\Gamma \vdash V : A$, then $\Gamma \vdash K$ and $\Gamma \vdash A$, and similarly for all other judgements.
## 5.2 Derivable Definitional Equations

To begin with, one can derive specialised versions of the general algebraicity equations from Fig. 4.

**PROPOSITION 5.7.** We can derive the following specialised algebraicity equations:

$$ \frac{\Gamma \vdash V : I \quad \Gamma, y:O[V/x] \vdash M : FA \quad \Gamma \vdash \underline{C} \quad \Gamma, y' : A \vdash N : \underline{C}}{\Gamma \vdash \operatorname{op}_V^{FA}(y.M) \text{ to } y' : A \text{ in } N = \operatorname{op}_V^{\underline{C}}(y.M \text{ to } y' : A \text{ in } N) : \underline{C}} \text{ (op : (x:I) } \to \} O \in S_{\text{eff}} $$

and analogously for other homomorphism term formers.

Next, we present some useful derivable equations for the composition operations.

**PROPOSITION 5.8.** We can derive the following unitality and associativity equations:

$$ \frac{\Gamma \vdash M : \underline{C}}{\Gamma \vdash M \text{ as } x : \underline{UC} \text{ in force}_{\underline{C}} x = M : \underline{C}} $$

$$ \frac{\Gamma \vdash M : \underline{C}_1 \quad \Gamma \vdash \underline{C}_2 \quad \Gamma \vdash \underline{D}}{\Gamma \vdash M \text{ as } x_1 : \underline{UC}_1 \text{ in } (N_1 \text{ as } x_2 : \underline{UC}_2 \text{ in } N_2) = (M \text{ as } x_1 : \underline{UC}_1 \text{ in } N_1) \text{ as } x_2 : \underline{UC}_2 \text{ in } N_2 : \underline{D}} \text{ (witnessed by } \overrightarrow{W_{op}} \text{, witnessed by } \overrightarrow{W'_{op}} \text{)} $$

and analogously for the composition operation for homomorphism terms.

**PROPOSITION 5.9.** We can derive the following interaction equations:

$$ \frac{\Gamma \vdash M : FA \quad \Gamma \vdash \underline{C} \quad \Gamma \vdash \underline{D}}{\Gamma \vdash M \text{ to } x_1 : A \text{ in } (N_1 \text{ as } x_2 : \underline{UC} \text{ in } N_2) = (M \text{ to } x_1 : A \text{ in } N_1) \text{ as } x_2 : \underline{UC} \text{ in } N_2 : \underline{D}} \text{ witnessed by } \overrightarrow{W_{op}} $$

$$ \frac{\Gamma \vdash M : \underline{C} \quad \Gamma, x_1 : \underline{UC} \quad \Gamma_{\text{hom}} : N_1 : FA \text{ witnessed by } \overrightarrow{W_{op}} \quad \Gamma \vdash \underline{D} \quad \Gamma, x_2 : A \vdash N_2 : \underline{D}}{\Gamma \vdash M \text{ as } x_1 : \underline{UC} \text{ in } (N_1 \text{ to } x_2 : A \text{ in } N_2) = (M \text{ as } x_1 : \underline{UC} \text{ in } N_1) \text{ to } x_2 : A \text{ in } N_2 : \underline{D}} $$

and analogously for computational pattern-matching, and the corresponding homomorphism terms.

**PROPOSITION 5.10.** The composition operations commute with computational pairing, computational lambda abstraction, and computational and homomorphic function applications, e.g., we have

$$ \frac{\Gamma \vdash M : \underline{C} \quad \Gamma \vdash V : A \quad \Gamma, y : A \vdash \underline{D}}{\Gamma, x : \underline{UC} \quad \Gamma_{\text{hom}} : N : \underline{D}[V/y] \text{ witnessed by } \overrightarrow{W_{op}}} \quad \frac{\Gamma \vdash M : \underline{C} \quad \Gamma \vdash V : \underline{D}_1 \quad \Gamma, y_1 : \underline{UC} \quad \Gamma_{\text{hom}} : N : \underline{D}_1 \text{ witnessed by } \overrightarrow{W_{op}}}{\Gamma \vdash M \text{ as } x : \underline{UC} \text{ in } \langle V, N \rangle = \langle V, M \text{ as } x : \underline{UC} \text{ in } N \rangle : \Sigma y : A. \underline{D}} $$

$$ \frac{\Gamma \vdash M : \underline{C} \quad \Gamma \vdash V : \underline{D}_1 \quad \Gamma, y_1 : \underline{UC} \quad \Gamma_{\text{hom}} : N : \underline{D}_1 \text{ witnessed by } \overrightarrow{W_{op}}}{\Gamma \vdash M \text{ as } y_1 : \underline{UC} \text{ in } V N = V (M \text{ as } y_1 : \underline{UC} \text{ in } N) : \underline{D}_2} $$

To improve the readability of the last three propositions, we have omitted the proofs of the equational proof obligations from the terms in the conclusions. These proofs are all constructed straightforwardly, by combining equational reasoning using definitional equations with the axiom of function extensionality $\text{fun-ext}_{(x:A).B}(V_1, V_2, W_p)$, the transitivity and congruence rules we can derive from the elimination form for propositional equality, and the proofs given in the premises.

# 6 ALTERNATIVE PRESENTATIONS OF THE LANGUAGE

We now briefly discuss some alternative presentations of EMLTT and our extensions to it.
## 6.1 Different Definition of the Auxiliary Judgement

First, for typing the composition operations, we could have defined the auxiliary judgement

$$ \Gamma, y: \overline{UC} \vdash_{\hom} N : \underline{D} \text{ witnessed by } \overrightarrow{W_{op}} $$

not using a set of proof witnesses $\overrightarrow{W_{op}}$ typed as

$$ \Gamma \vdash W_{op} : \lambda x : I. \lambda x' : O \rightarrow UC.\thinspace.thunk(N[\thinspace.thunk(op_x^C(x'', force_C(x' x''))/y)] = \\ \lambda x : I. \lambda x' : O \rightarrow UC.\thinspace.thunk(op_x^D(x'', N[x' x''/y])) $$

but instead using a single witness $W$ based on Munch-Maccagnoni's [2013] notion of linearity:<fnref n="3" />

$$ \Gamma \vdash W : \lambda x : UFA.\lambda x' : A \rightarrow UC.\thinspace.thunk(N[\thinspace.thunk((force_{FA} x) \text{ to } x'' : A \text{ in } C \text{ force } C(x' x''))/y]) = \\ \lambda x : UFA.\lambda x' : A \rightarrow UC.\thinspace.thunk((force_{FA} x) \text{ to } x'' : A \text{ in } \underline{D} \text{ N}[x' x''/y]) $$

The former definition of this auxiliary judgement follows from the latter by straightforward equational reasoning (taking $A$ to be equal to $O$), while latter definition can be shown to follow from the former by using Plotkin and Pretnar's principle of computational induction for algebraic computational effects, which states that every computation term of type FA is either a returned value or built from computation terms using algebraic operations [Plotkin and Pretnar 2008].

While the latter definition is also applicable in languages with computational effects other than algebraic (e.g., as used by Levy [2017] to characterise general isomorphisms between computation types), we chose the former due to its more intuitive reading in the setting of algebraic effects.

## 6.2 Replacing Homomorphism Terms with the Auxiliary Judgement

Second, note that we could have omitted computation variables and homomorphism terms from EMLTT altogether. Instead, we could have used value variables and the auxiliary judgement $\Gamma, x: \overline{UC} \vdash_{\hom} N : \underline{D}$ witnessed by $\overrightarrow{W_{op}}$ (see §4.2 and §6.1) to define and type the elimination form for the computational $\Sigma$-type, analogously to the composition operations introduced in §4.2. In more detail, this alternative presentation would involve the following elimination form for $\Sigma x : A.C$:

$$ \frac{\Gamma \vdash M : \Sigma x : A.C \quad \Gamma \vdash \underline{D} \quad \Gamma, x : A, y : \overline{UC} \vdash_{\hom} N : \underline{D} \text{ witnessed by } \overrightarrow{W_{op}}}{\Gamma \vdash M \text{ to } (x : A, y : \overline{UC}) \text{ in } \overleftarrow{\text{in}}_{\overrightarrow{W_{op}}; \underline{D}} N : \underline{D}} $$

where $M$ is now eliminated into a pair of values, with the auxiliary judgement ensuring that the computation term $N$ behaves in the value variable $y$ as if it was a homomorphism term. To add to this, we would also need to include specialised algebraicity equations from Prop. 5.7 in the equational theory of the language, so as to replace the general algebraicity equations from Fig. 4.

In this paper we chose to include both homomorphism terms and the above-mentioned auxiliary judgement for two reasons. First, as one of the main aims of this paper was to show how to extend the language in Ahman et al. [2016] with handlers of fibred algebraic effects, we wanted to keep the underlying language close to op. cit. Second, aesthetically, using homomorphism terms provides a cleaner presentation of the elimination form for $\Sigma x : A.C$, compared to equational proof obligations.

# 7 USING HANDLERS TO REASON ABOUT EFFECTFUL COMPUTATIONS

In this section we demonstrate that in addition to being a practical programming abstraction, handlers also provide a useful mechanism for reasoning about effectful computations. Namely, we show that the "handle into value terms" handling construct we defined in §4.4 provides the programmer with a convenient alternative to using propositional equality on thunks for defining

<footnote n="3">³Note that the value variables $x$, $x'$, and $x''$ are assigned different types in the two definitions of the auxiliary judgement.</footnote>
predicates on effectful computations. Specifically, we consider two kinds of natural examples of this approach: i) lifting predicates from return values to effectful computations (§7.1); and ii) specifying patterns of allowed effects (§7.2). These examples are also accompanied by a formalisation¹, based on a shallow embedding of the relevant value fragment of EMLTT in AGDA [The Agda Team 2017].

In order to facilitate reasoning based on the "handle into value terms" handling construct, we first introduce a universe à la Tarski [Martin-Löf 1984] by extending EMLTT with a universe $\mathcal{U}$ of value types, a corresponding decoding function $\mathrm{El}(V)$, and the corresponding codes of value types:

$$A ::= \dots \mid \mathcal{U} \mid \mathrm{El}(V)$$

$$V ::= \dots \mid \mathrm{nat-c} \mid \mathrm{one-c} \mid \mathrm{zero-c} \mid \mathrm{sum-c}(V, W) \mid \mathrm{sig-c}(V, x, W) \mid \mathrm{pi-c}(V, x, W)$$

We also extend EMLTT with corresponding typing rules and definitional equations, e.g., we include

$$\frac{\Gamma \vdash V : \mathcal{U} \quad \Gamma, x : \mathrm{El}(V) \vdash W : \mathcal{U}}{\Gamma \vdash \mathrm{pi-c}(V, x, W) : \mathcal{U}} \qquad \frac{\Gamma \vdash V : \mathcal{U} \quad \Gamma, x : \mathrm{El}(V) \vdash W : \mathcal{U}}{\Gamma \vdash \mathrm{El}(\mathrm{pi-c}(V, x, W)) = \Pi x : \mathrm{El}(V) \cdot \mathrm{El}(W)}$$

Using this universe, we can now define predicates on effectful computations (of type FA) as value terms of the form $\Gamma \vdash V : UFA \to \mathcal{U}$, with the aim of using these predicates to refine (thunks of) computations using the value $\Sigma$-type, i.e., as $\Sigma x : UFA \cdot \mathrm{El}(Vx)$. In detail, we define the predicates $\Gamma \vdash V : UFA \to \mathcal{U}$ by i) equipping $\mathcal{U}$ (or a type we define using it) with an algebra for the given effect theory, and ii) by using the "handle into value terms" handling construct we defined in §4.4.

It is worth noting that our approach of defining type-theoretic predicates on effectful computations by equipping the universe $\mathcal{U}$ with an algebra structure (essentially, we are defining types that depend on effectful computations in a "well-behaved" manner) is reminiscent of the recent work by Pédrot and Tabareau [2017]. In particular, their monadic translation of dependent type theories crucially relies on equipping universes with an algebra structure for a given monad.

## 7.1 Lifting Predicates from Return Values to Effectful Computations

**Input-output.** Lifting predicates from return values to computations is easiest when the given effect theory does not contain equations. Thus, let us consider the theory $\mathcal{T}_{I/O}$ of input-output of bits from §4.1 for our first example; other equation-free fibred algebraic effects admit similar reasoning.

Assuming given a predicate $\Gamma \vdash V_P : A \to \mathcal{U}$ on A, we can lift $V_P$ to a predicate $V_P^\flat$ on UFA by

$$V_P^\flat \stackrel{\mathrm{def}}{=} \lambda y : UFA. (\mathrm{force}_{FA} y) \text{ handled with } \{\mathrm{op}_x(x') \mapsto V_{op}\}_{\mathrm{op} \in S_{I/O}} \text{ to } y' : A \mathrm{in} \mathcal{U} (V_P y')$$

where we define the code of bits as bit-c $\stackrel{\mathrm{def}}{=} \mathrm{sum-c}(\mathrm{one-c}, \mathrm{one-c})$, and where

$$x:1, x':1 \mapsto \mathcal{U} \vdash V_{\mathrm{read}} \stackrel{\mathrm{def}}{=} \mathrm{sig-c}(\mathrm{bit-c}, y', x' y') : \mathcal{U}$$

$$x:1, x':1 \mapsto \mathcal{U} \vdash V_{\mathrm{write}} \stackrel{\mathrm{def}}{=} x' \star : \mathcal{U}$$

On closer inspection, we can see that $V_P^\flat$ agrees with the possibility modality from Evaluation Logic [Pitts 1991], in that a computation term satisfies $V_P^\flat$ if there exists a return value that satisfies the given predicate $V_P$. Further, observe that if we were to replace sig-c (code for value $\Sigma$-type, i.e., existential quantification) with pi-c (code for value $\Pi$-type, i.e., universal quantification), we would get a necessity modality that holds when all the return values of the given computation satisfy $V_P$.

**Global state.** For our second example of lifting predicates from return values to computations, we consider an effect theory that also includes equations, the theory $\mathcal{T}_{GS}$ of global state from §3.2.

<footnote n="4">⁴The AGDA formalisation of the examples presented in §7 is available at https://github.com/danelahman/POPL18/</footnote>
In particular, when we define the type of stores as $S \stackrel{\text{def}}{=} \Pi x: \text{Loc} \cdot \text{Val}$, then assuming given a predicate $\Gamma \vdash V_Q : A \to S \to \mathcal{U}$ on return values and final stores, we can define a predicate

$$V_Q \stackrel{\text{def}}{=} \lambda y: UFA. \lambda x_S : S. \text{fst} \left( \left( \text{force}_{FA} y \right) \text{ handled with } \left( \{ \text{op}_x(x') \mapsto V_{op}\}_{\text{op} \in S_{GS}}; \overrightarrow{W_{eq}} \right) \text{ to } y' : A \text{ in } S \to u \times_S V_{\text{ret}} \right) x_S \right)$$

on (thunks of) computations and initial stores, with $V_{\text{get}}$, $V_{\text{put}}$, and $V_{\text{ret}}$ defined as follows:

$$\Gamma, x: \text{Loc}, x' : \text{Val} \to S \to \mathcal{U} \times S \vdash V_{\text{get}} \stackrel{\text{def}}{=} \lambda x_S : S. x' (\text{sel } x_S x) x_S : S \to \mathcal{U} \times S$$

$$\Gamma, x:(\Sigma x:\text{Loc}.\text{Val}), x':1 \to S \to \mathcal{U} \times S \vdash V_{\text{put}} \stackrel{\text{def}}{=} \lambda x_S : S. x' \star (\text{upd } x_S x) : S \to \mathcal{U} \times S$$

$$\Gamma, y' : A \vdash V_{\text{ret}} \stackrel{\text{def}}{=} \lambda x_S : S. \langle V_Q, y' x_S, x_S \rangle : S \to \mathcal{U} \times S$$

and where we define the selection and update operations on stores as $\text{sel } V_S V \stackrel{\text{def}}{=} V_S V$ and $\text{upd } V_S V \stackrel{\text{def}}{=} \text{pm } V$ as $(x: \text{Loc}, y: \text{Val})$ in

$$\lambda x' : \text{Loc. case } (\text{isDec}_{\text{Loc}} x x') \text{ of } (\text{inl}(y_p : x =_{\text{Loc}} x') \mapsto \text{transport}_{\text{Val}} x x' y_p y, \\ \text{inr}(y_p : x =_{\text{Loc}} x' \to 0) \mapsto \text{sel } V_S x')$$

with $\text{transport}_{\text{Val}} : \Pi x_l : \text{Loc} \cdot \Pi x'_l : \text{Loc} \cdot \Pi y_p : x_l =_{\text{Loc}} x'_l$. $\text{Val}[x_l/x] \to \text{Val}[x'_l/x]$ being the standard transport operation for propositional equality that one can derive from its elimination principle.

While we omit details of the witnesses of the proof obligations corresponding to the equations given in §3.2, referring the interested reader to the AGDA formalisation for details, we want to highlight that the use of transport$_{Val}$ in the definition of upd means that in order to construct the proof witness $W_{eq}$ for the second of the five global state equations, namely, for $\text{put}_{(x,y)}(\text{get}_x(y',w(y'))) = \text{put}_{(x,y)}(w(y))$, we need Loc to be a set in the sense of Homotopy Type Theory [The Univalent Foundations Program 2013]. That is, we need there to be a pure value term

$$\diamond \vdash \text{isSet}_{\text{Loc}} : \Pi x: \text{Loc} \cdot \Pi x' : \text{Loc} \cdot \Pi y : x =_{\text{Loc}} x' \cdot \Pi y' : x =_{\text{Loc}} x' \cdot y =_{x=_{\text{Loc}} x'} y'$$

Using Hedberg's theorem [Hedberg 1998], we can readily derive this property from $\text{isDec}_{\text{Loc}}$ that we assumed in §3.2. Returning to the proof witness $W_{eq}$, we note that its definition amounts to having to prove transport$_{Val}$ $x x y_p y =_{\text{Val}} y$ for an arbitrary equality proof $y_p : x =_{\text{Loc}} x$, which we can do using the derived property $\text{isSet}_{\text{Loc}}$, i.e., using $\text{isSet}_{\text{Loc}} x x y_p$ ($\text{refl } x$) : $y_p =_{x=_{\text{Loc}} x} \text{refl } x$.

From the perspective of programming with computational effects, having to require Loc to have decidable equality (and thus to be a set) is not a significant drawback because the natural choice for Loc, namely, the finite coproduct of 1s denoting a finite set of memory locations, can be easily shown to have decidable equality. It is also worth noting that if Val were not dependent on Loc, then we could define the case of upd that currently uses transport$_{Val}$ simply as $\text{inl}(y_p : x =_{\text{Loc}} x') \mapsto y$.

Finally, on closer inspection, we can see that $V_Q$ corresponds to Dijkstra's weakest precondition semantics of stateful programs [Dijkstra 1975], e.g., the following definitional equations hold:

$$\Gamma \vdash V_Q \text{ (thunk (return } V)) : V_S = V_Q V V_S : \mathcal{U}$$

$$\Gamma \vdash V_Q \text{ (thunk } \langle \text{get}_{V_i}^{FA}(y,M) \rangle \text{)} : V_S = V_Q \text{ (thunk } M[\text{sel } V_S V_i / y] \text{)} : V_S : \mathcal{U}$$

$$\Gamma \vdash V_Q \text{ (thunk } \langle \text{put}_{\langle V_i, V \rangle}^{FA}(M) \rangle \text{)} : V_S = V_Q \text{ (thunk } M \text{)} (\text{upd } V_S \langle V_i, V \rangle) : \mathcal{U}$$

That is, e.g., $V_Q$ holds of the term $\text{put}_{\langle V_i, V \rangle}^{FA}(M)$ in state $V_S$ iff it holds of $M$ in state $\text{upd } V_S \langle V_i, V \rangle$.

## 7.2 Specifying Patterns of Allowed Effects in Computations

Analogously to lifting predicates from return values to effectful computations, specifying patterns of allowed effects is easiest when the given fibred effect theory does not contain any equations. Thus, for simplicity, we again consider the theory $\mathcal{T}_{I/O}$ of input-output of bits for our examples.
**Disallowing writes.** We begin by considering a coarse grained example of disallowing all writes:

$V_{\text{no-w}} \stackrel{\text{def}}{=} \lambda y: \mathit{UFA}. (\mathit{force}_{\mathit{FA}} y)$ handled with $\{\mathit{op}_x(x') \mapsto V_{\mathit{op}}\}_{\mathit{op} \in S_{\mathit{I/O}}}$ to $y': A \text{ in} \mathcal{U}$ one-c

where $V_{\text{read}}$ and $V_{\text{write}}$ are defined as follows:

$$x:1, x':1+1 \to \mathcal{U} \vdash V_{\text{read}} \stackrel{\text{def}}{=} \text{pi-c}(\text{bit-c}, y'.x' y') : \mathcal{U}$$

$$x:1+1, x':1 \to \mathcal{U} \vdash V_{\text{write}} \stackrel{\text{def}}{=} \text{zero-c} : \mathcal{U}$$

For example, the computation term $\text{read}^{\text{FA}}(x.\text{write}_V^{\text{FA}}(M))$ does not satisfy $V_{\text{no-w}}$ because we have

$$\Gamma \vdash \text{El}(V_{\text{no-w}}(\text{trunk}(\text{read}^{\text{FA}}(y.\text{write}_V^{\text{FA}}(M))))) = \Pi y:1+1.0 \cong 0$$

**Patterns of reads and writes.** As a more fine grained example, we consider specifications on effectful computations in the style of session types [Honda et al. 1998], given by allowed patterns of I/O-effects. First, we assume an inductive type Protocol with the following three constructors:

$r : (1+1 \to \text{Protocol}) \to \text{Protocol}$

$w : (1+1 \to \mathcal{U}) \to \text{Protocol} \to \text{Protocol}$

$e : \text{Protocol}$

describing *patterns of allowed I/O-effects*. Intuitively, $r$ specifies that the next allowed I/O-effect is reading; $w$ specifies that the next allowed I/O-effect is writing, with the value written required to satisfy the predicate given as an argument to $w$; and $e$ specifies that no further communication must happen (i.e., end of communication). The Protocol-valued arguments of the constructors $r$ and $w$ specify how the computation is allowed to evolve after reading and writing, respectively.

Then, given some particular protocol $\Gamma \vdash V_{\text{pr}} : \text{Protocol}$, we can define a corresponding predicate

$$V_{\hat{\text{pr}}} \stackrel{\text{def}}{=} \lambda y: \mathit{UFA}. ((\text{force}_{\mathit{FA}} y) \text{ handled with } \{\mathit{op}_x(x') \mapsto V_{\mathit{op}}\}_{\mathit{op} \in S_{\mathit{I/O}}}) \text{ to } y' : A \text{ in } \mathcal{P}_{\text{Protocol}} \to \mathcal{U} V_{\text{ret}}) V_{\text{pr}}$$

where the value terms $V_{\text{read}}$, $V_{\text{write}}$, and $V_{\text{ret}}$ are defined as follows (for better readability, we give their structural-recursive definitions by pattern-matching on their arguments of type Protocol):

$$\Gamma, x:1, x':1+1 \to \text{Protocol} \to \mathcal{U} \vdash V_{\text{read}} (r V'_{\text{pr}}) \stackrel{\text{def}}{=} \text{pi-c}(\text{bit-c}, y'.(x' y') (V'_{\text{pr}} y')) : \mathcal{U}$$

$$\Gamma, x:1+1, x':1 \to \text{Protocol} \to \mathcal{U} \vdash V_{\text{write}} (w V_p V'_{\text{pr}}) \stackrel{\text{def}}{=} \text{sig-c}(V_p x, y'. x' \star V'_{\text{pr}}) : \mathcal{U}$$

$$\Gamma, y' : A \vdash V_{\text{ret}} e \stackrel{\text{def}}{=} \text{one-c} : \mathcal{U}$$

with all other cases defined as zero-c. As a result, a computation satisfies the predicate $V_{\hat{\text{pr}}}$ if and only if its I/O-effects precisely follow the specific pattern of I/O-effects allowed by the protocol $V_{\text{pr}}$.

This example can be easily extended to also account for *sets* of patterns of allowed I/O-effects. For instance, we could extend the inductive type Protocol with a fourth constructor or, typed as or : Protocol → Protocol → Protocol, and correspondingly extend the above definitions of value terms $V \in \{V_{\text{read}}, V_{\text{write}}, V_{\text{ret}}\}$ each with a new case given by $V (V'_{\text{pr}} \text{ or } V''_{\text{pr}}) \stackrel{\text{def}}{=} \text{sum-c}(V V'_{\text{pr}}, V V''_{\text{pr}})$.

Finally, we highlight that it is easy combine these specifications with those discussed in §7.1, namely, by replacing one-c in the definition of $V_{\text{ret}}$ with a suitable predicate $V_p$ on return values.

# 8 SEMANTICS

We conclude by describing how to give a natural denotational semantics to our extension of eMLTT with fibred algebraic effects and their handlers. This semantics is an instance of a more general class of models, based on *fibrations* (functors with extra structure for modelling substitution, Σ- and Π-types, etc.) and *adjunctions* between them, as studied by Ahman [2017]; Ahman et al. [2016].

We proceed in three steps. First, we recall how the pure fragment of eMLTT is interpreted in the families of sets fibration, a prototypical model of dependent types. Next, we show how to derive a
countable Lawvere theory $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ from the given fibred effect theory $\mathcal{T}_{\text{eff}}$. Finally, we show how to define the interpretation of the rest of our extension of EMLTT using families of models of $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$.

## 8.1 Families Fibrations

We begin by giving a brief overview of the kinds of fibrations we use for defining the denotational semantics of our extension of EMLTT. For a more detailed treatment of fibrations and their use in modelling various type theories and logics, we refer the reader to the book by Jacobs [1999].

Given a category $C$, it is well-known that one can define a new category $\text{Fam}(C)$ of $C$-valued families. Its objects are pairs $(X, A)$ of a set $X$ and a functor $A : X \to C$ (treating $X$ as a discrete category); and the morphisms $(X, A) \to (Y, B)$ are pairs of a function $f : X \to Y$ and a natural transformation $g : A \to B \circ f$. The corresponding $C$-valued families fibration $\text{fam}_C : \text{Fam}(C) \to \text{Set}$ is then defined on objects as $\text{fam}_C(X, A) \stackrel{\text{def}}{=} X$ and on morphisms as $\text{fam}_C(f, g) \stackrel{\text{def}}{=} f$.

Next, for any set $X$, the category $\text{Fam}_X(C)$ is called the fibre over $X$; this is a subcategory of $\text{Fam}(C)$ whose objects and morphisms are of the form $(X, A)$ and $(\text{id}_X, g)$. Given a function $f : X \to Y$, the corresponding reindexing functor $f^* : \text{Fam}_Y(C) \to \text{Fam}_X(C)$ is given on objects by $f^*(Y, A) \stackrel{\text{def}}{=} (X, A \circ f)$, and analogously on morphisms. As standard in the literature, we write $\bar{f}(Y, A) \stackrel{\text{def}}{=} (f, (\text{id}_{A(f(x))})_x) : f^*(Y, A) \to (Y, A)$ for the Cartesian morphism over $f : X \to Y$.

We get a prototypical model of dependent types when we take $C \stackrel{\text{def}}{=} \text{Set}$, the category of sets and functions. In this case, there also exists a pair of adjunctions $\text{fam}_{\text{Set}} \dashv 1 \dashv \{-\}$, where the terminal object functor $1 : \text{Set} \to \text{Fam}(\text{Set})$ is given by $1(X) \stackrel{\text{def}}{=} (X, x \mapsto \{\star\})$, and the comprehension functor $\{-\} : \text{Fam}(\text{Set}) \to \text{Set}$ is given by $\{(X, A)\} \stackrel{\text{def}}{=} \coprod_{x \in X} A(x)$. The latter functor provides a natural semantics for context extension, together with the canonical projection maps $\pi_{(X,A)} : \{(X, A)\} \to X$.

## 8.2 Interpretation of the Pure Fragment of EMLTT

We now recall how the pure fragment of EMLTT (i.e., MLTT) is interpreted in the families of sets fibration $\text{fam}_{\text{Set}} : \text{Fam}(\text{Set}) \to \text{Set}$. For more details about the interpretation of this fragment of EMLTT, we refer the reader to the relevant sections in Ahman [2017]; Ahman et al. [2016], and to Streicher [1991] whose treatment of the categorical semantics of MLTT the former two build on.

In detail, the interpretation of the pure fragment of EMLTT is defined as a *partial interpretation function* $\llbracket - \rrbracket$, which, if defined, maps a context $\Gamma$ to a set $\llbracket \Gamma \rrbracket$; a context $\Gamma$ and value type $A$ to an object $\llbracket \Gamma; A \rrbracket$ in $\text{Fam}_{\llbracket \Gamma \rrbracket}(\text{Set})$; and a context $\Gamma$ and value term $V$ to $\llbracket \Gamma; V \rrbracket : 1(\llbracket \Gamma \rrbracket) \to (\llbracket \Gamma \rrbracket, A)$ in $\text{Fam}_{\llbracket \Gamma \rrbracket}(\text{Set})$, for some $A : \llbracket \Gamma \rrbracket \to \text{Set}$. For better readability, we denote the first and second components of $\llbracket \Gamma; A \rrbracket$ and $\llbracket \Gamma; V \rrbracket$ using subscripts 1, 2, i.e., we write $(\llbracket \Gamma; A \rrbracket)_1, \llbracket \Gamma; A \rrbracket_2)$ for $\llbracket \Gamma; A \rrbracket$.

First, the value types Nat, 1, 0, and $A+B$ are interpreted using the corresponding categorical structure in the fibres of $\text{Fam}(\text{Set})$ as follows, assuming that $\llbracket \Gamma \rrbracket$, $\llbracket \Gamma; A \rrbracket$, and $\llbracket \Gamma; B \rrbracket$ are defined:

$$ \llbracket \Gamma; \text{Nat} \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \mathbb{N}) \qquad \llbracket \Gamma; 1 \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \{\star\}) = 1(\llbracket \Gamma \rrbracket) \qquad \llbracket \Gamma; 0 \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \emptyset) \\ \llbracket \Gamma; A + B \rrbracket \stackrel{\text{def}}{=} \llbracket \Gamma; A \rrbracket + \llbracket \Gamma; B \rrbracket = (\llbracket \Gamma \rrbracket, \gamma \mapsto \llbracket \Gamma; A \rrbracket_2(\gamma) + \llbracket \Gamma; B \rrbracket_2(\gamma)) $$

Next, assuming that $\llbracket \Gamma; A \rrbracket$ and $\llbracket \Gamma, x : A; B \rrbracket$ are defined, with $\llbracket \Gamma, x : A; B \rrbracket_1 = \coprod_{Y \in \llbracket \Gamma \rrbracket} \llbracket \Gamma; A \rrbracket_2(\gamma)$, then

$$ \llbracket \Gamma; \Sigma x : A.B \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \coprod_{a \in \llbracket \Gamma; A \rrbracket_2(\gamma)} (\llbracket \Gamma, x : A; B \rrbracket_2(\langle \gamma, a \rangle))) \\ \llbracket \Gamma; \Pi x : A.B \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \coprod_{a \in \llbracket \Gamma; A \rrbracket_2(\gamma)} (\llbracket \Gamma, x : A; B \rrbracket_2(\langle \gamma, a \rangle))) $$

Finally, propositional equality is interpreted as the equality between the interpretations of terms:

$$ \llbracket \Gamma; V =_A W \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \{\star | (\llbracket \Gamma; V \rrbracket)_\gamma(\star) = (\llbracket \Gamma; W \rrbracket)_\gamma(\star)) \}) $$
assuming that $[[\Gamma; V]] : 1([[[\Gamma]]) \to ([[[\Gamma; A]])$ and $[[\Gamma; W]] : 1([[[\Gamma]]) \to ([[[\Gamma; A]])$ are both defined. In the rest of this paper, we often leave such routine preconditions to the definedness of $[[–]]$ implicit.

In §8.5, we rely on this extensional nature of the semantics of propositional equality for showing that the interpretations of the proof witnesses involved in the typing of the user-defined algebra type and the composition operations are enough to validate the corresponding definitional equations.

Next, the interpretation of the universe $\mathcal{U}$ is based on the semantics of induction-recursion [Dybjer and Setzer 1999; Ghani et al. 2013]: we first construct the initial algebra $\mu\Phi$ of an endofunctor $\Phi$ on Fam(|Set|)$^5$ corresponding to the signature of codes of value types given in §7, and then define

$$[[\Gamma; \mathcal{U}]] \stackrel{\text{def}}{=} ([[[\Gamma]]], \gamma \mapsto \mu\Phi_1) \qquad [[\Gamma; \text{El}(V)]] \stackrel{\text{def}}{=} ([[[\Gamma]]], \gamma \mapsto \mu\Phi_2 (([[\Gamma; V]]_2)_\gamma(\star)))$$

Finally, as an example of the interpretation of value terms, $\text{inl}_{A+B} V$ is interpreted as follows:

$$[[\Gamma; \text{inl}_{A+B} V]]_1 \stackrel{\text{def}}{=} \text{id}_{[[\Gamma]]} \qquad ([[[\Gamma; \text{inl}_{A+B} V]]_2)_\gamma \stackrel{\text{def}}{=} \text{inl}_{[[\Gamma; A]]_2(\gamma) + [[\Gamma; B]]_2(\gamma)} \circ ([[[\Gamma; V]]_2)_\gamma$$

The soundness theorems for MLTT and EMLTT then tell us that the a priori partial $[[–]]$ is in fact defined on well-formed pure syntax and that it validates the corresponding definitional equations.

## 8.3 Deriving a Countable Lawvere Theory from a Fibred Effect Theory

Next, we show how to derive a countable Lawvere theory from the given fibred effect theory $\mathcal{T}_{\text{eff}}$.

We begin by recalling some basic definitions and results about countable Lawvere theories and their models. We refer the reader to Power [2006] for a more detailed overview of the area.

A countable Lawvere theory consists of a small category $\mathcal{L}$ with countable products and a strict countable-product preserving identity-on-objects functor $I: \mathcal{N}_1^{\text{op}} \to \mathcal{L}$, where $\mathcal{N}_1$ is the skeleton of the category of countable sets and all functions between them. In other words, an object of $\mathcal{N}_1$ is either a natural number or the distinguished element $\omega$ denoting the cardinality of countable sets.

A model of a countable Lawvere theory $\mathcal{L}$ in a category $C$ with countable products is a countable-product preserving functor $M: \mathcal{L} \to C$. A morphism from $M_1: \mathcal{L} \to C$ to $M_2: \mathcal{L} \to C$ is given by a natural transformation $h: M_1 \to M_2$. This gives us the category Mod($\mathcal{L}, C$).

Conceptually, a countable Lawvere theory is nothing but an abstract category-theoretic description of the clone of countable equational theories [Grätzer 1979]. In particular, one often thinks of the morphisms $n \to 1$ in $\mathcal{L}$ as terms in $n$ free variables, and of the morphisms $n \to m$ as $m$-tuples of terms in $n$ free variables. Analogously, the models of a countable Lawvere theory correspond to the models of the countable equational theories whose clone this countable Lawvere theory is.

We also recall that there exists a canonical forgetful functor $U_{\mathcal{L}}: \text{Mod}(\mathcal{L}, C) \to C$, given on objects by $U_{\mathcal{L}}(M) \stackrel{\text{def}}{=} M(1)$. It is then well-known that if $C$ is locally countably presentable [Adamek and Rosicky 1994], the functor $U_{\mathcal{L}}$ has a left adjoint $F_{\mathcal{L}}: C \to \text{Mod}(\mathcal{L}, C)$. Importantly for the purposes of this paper, the category Set of sets and functions is locally countably presentable.

Next, in order to be able to derive a countable Lawvere theory $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ from the given fibred effect theory $\mathcal{T}_{\text{eff}}$, we require $\mathcal{T}_{\text{eff}}$ to be countable. In particular, this means that for all op: $(x: I) \to O \in S_{\text{eff}}$, we require $[[x: I; O]]_2$ to be a family of countable sets. Furthermore, we also require $[[\Gamma; A'_j]]_2$ to be a family of countable sets, for all equations $\Gamma | \Delta \vdash T_1 = T_2 \in \mathcal{E}_{\text{eff}}$ and effect variables $w_j: A'_j \in \Delta$.

We can then construct $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ by expanding $\mathcal{T}_{\text{eff}}$ into a countable equational theory [Grätzer 1979], analogously to how Plotkin and Pretnar [2013] expanded their effect theories. More specifically, $S_{\text{eff}}$ determines a countable signature consisting of operation symbols $\text{op}_i: |[[x: I; O]]_2((\star, i))|$, for all op: $(x: I) \to O \in S_{\text{eff}}$ and $i \in [[\diamond; I]]_2(\star)$. Every effect term $\Gamma | \Delta \vdash T$ then naturally determines terms $\Delta^Y \vdash T^Y$ derivable from this countable signature (for all $\gamma \in [[\Gamma]]$), where $\Delta^Y$ consists of

<footnote>$^5$|Set| denotes the discrete variant of Set; it is used to accommodate the contravariance arising from decoding the $\Pi$-type.</footnote>
variables $x_{w_j}^a$ for all $w_j : A_j \in \Delta$ and $a \in [[\Gamma; A'_j]]_2(\gamma)$. In detail, the terms $T^\gamma$ are defined as follows:

$$ (w_j(V))^\gamma \quad \stackrel{\text{def}}{=} \quad x_{w_j}^{([\Gamma; V]_2)_\gamma(\star)} $$

$$ (\text{op}_V(y.T))^\gamma \quad \stackrel{\text{def}}{=} \quad \text{op}_{([\Gamma; V]_2)_\gamma(\star)}(T^{(y,o)}) \quad 1 \le o \le \|x:I;O\|_2((\star, ([\Gamma; V]_2)_\gamma(\star))) \| $$

$$ (\text{pm } V \text{ as } (y_1:B_1, y_2:B_2) \text{ in } T)^\gamma \quad \stackrel{\text{def}}{=} \quad T^{\langle y, b_1 \rangle, b_2} \quad (\text{when } ([\Gamma; V]_2)_\gamma(\star) = \langle b_1, b_2 \rangle) $$

$$ (\text{case V of } (\text{inl}(y_1) \mapsto T_1, \text{inr}(y_2) \mapsto T_2))^\gamma \stackrel{\text{def}}{=} T_1^{(y, b)} \quad (\text{when } ([\Gamma; V]_2)_\gamma(\star) = \text{inl } b) $$

$$ (\text{case V of } (\text{inl}(y_1) \mapsto T_1, \text{inr}(y_2) \mapsto T_2))^\gamma \stackrel{\text{def}}{=} T_2^{(y, b)} \quad (\text{when } ([\Gamma; V]_2)_\gamma(\star) = \text{inr } b) $$

We get a countable equational theory by taking equations $\Delta^\gamma \vdash T_1^\gamma = T_2^\gamma$, for all $\Gamma | \Delta \vdash T_1 = T_2 \in \mathcal{E}_{\text{eff}}$ and $\gamma \in [[\Gamma]]$, and closing them under the standard rules of reflexivity, symmetry, transitivity, etc.

The countable Lawvere theory $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ is then given by taking the morphisms $n \to m$ in $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ to be $m$-tuples $(\vec{x}_i \vdash t_j)_{1 \le j \le m}$ of equivalence classes of terms in $n$ variables (in the countable equational theory defined above). The identity morphisms are given by tuples of variables, while the composition of morphisms is given by substitution. We define the functor $I_{\mathcal{T}_{\text{eff}}}: \mathfrak{S}_1^{\text{op}} \to \mathcal{L}_{\mathcal{T}_{\text{eff}}}$ by $I_{\mathcal{T}_{\text{eff}}}(n) \stackrel{\text{def}}{=} n$ and $I_{\mathcal{T}_{\text{eff}}}(f) \stackrel{\text{def}}{=} (\vec{x}_i \vdash x_{f(j)})_{1 \le j \le m} : n \to m$. It is then easy to verify both that $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ has countable products (given using the cardinal sum in $\mathfrak{S}_1$) and that $I_{\mathcal{T}_{\text{eff}}}$ strictly preserves them.

**PROPOSITION 8.1.** *$\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ is a countable Lawvere theory.*

For better readability, we write Mod for Mod($\mathcal{L}_{\mathcal{T}_{\text{eff}}}$, Set) in the rest of this paper. In addition, a useful well-known property of Mod that we use later is that it is both complete and cocomplete.

We conclude by highlighting that for any set $A$, one can intuitively think of the free model $F_{\mathcal{L}_{\mathcal{T}_{\text{eff}}}}(A)$ as being given by the set of equivalence classes of computation trees built from the operations of the given fibred effect theory $\mathcal{T}_{\text{eff}}$, with the leaves of these trees given by elements of the set $A$.

## 8.4 Interpretation of the Non-Pure Fragment of EMLTT

Next, we show how to extend the interpretation of the pure fragment of EMLTT to the rest of our extension of EMLTT with fibred algebraic effects and their handlers, based on the fibred adjunction

<figure><img src="image_3.png" /></figure>

where the two fibred functors $F$ and $U$ are defined (on objects) as

$$ F(X, A) \stackrel{\text{def}}{=} (X, F_{\mathcal{L}_{\mathcal{T}_{\text{eff}}}} \circ A) \qquad U(X, \underline{C}) \stackrel{\text{def}}{=} (X, U_{\mathcal{L}_{\mathcal{T}_{\text{eff}}}} \circ \underline{C}) $$

That the functors $F$ and $U$ indeed form a fibred adjunction suitable for modelling EMLTT is an instance of a more general result about the models of EMLTT—see Ahman et al. [2016, Thm. 3].

Using this fibred adjunction, we can now extend the definition of $[[\cdot]]$ that we gave in §8.2 so that, if defined, it maps a context $\Gamma$ and a computation type $\underline{C}$ to an object $[[\Gamma; \underline{C}]]$ in $\text{Fam}_{[[\Gamma]]}(\text{Mod})$; a context $\Gamma$ and a computation term $M$ to a morphism $[[\Gamma; M]] : 1([\Gamma]) \to U([\Gamma; \underline{C}])$ in $\text{Fam}_{[[\Gamma]]}(\text{Set})$, for some $\underline{C} : [[\Gamma]] \to \text{Mod}$; and a context $\Gamma$, a variable $z$, a computation type $\underline{C}$, and a homomorphism term $K$ to a morphism $[[\Gamma; z:\underline{C}; K]] : [[\Gamma; \underline{C}] \to ([\Gamma], \underline{D})$ in $\text{Fam}_{[[\Gamma]]}(\text{Mod})$, for some $\underline{D} : [[\Gamma]] \to \text{Mod}$.
In particular, the interpretation of the types $\underline{C} \to \underline{D}$, $\underline{UC}$, and $\underline{FA}$ is defined as follows:

$$ \begin{align*} \llbracket \Gamma; \underline{C} \to \underline{D} \rrbracket &\stackrel{\text{def}}{=} \llbracket \Gamma \rrbracket, \gamma \mapsto \operatorname{Hom}_{\operatorname{Mod}}(\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma), \llbracket \Gamma; \underline{D} \rrbracket_2(\gamma)) \\ \llbracket \Gamma; \underline{UC} \rrbracket &\stackrel{\text{def}}{=} U(\llbracket \Gamma; \underline{C} \rrbracket) \quad \llbracket \Gamma; \underline{FA} \rrbracket \stackrel{\text{def}}{=} F(\llbracket \Gamma; \underline{A} \rrbracket) \end{align*} $$

The computational $\Pi$- and $\Sigma$-types are interpreted similarly to their value counterparts, using the set-indexed products and coproducts in $\operatorname{Mod}$, which exist because $\operatorname{Mod}$ is complete and cocomplete.

We omit the definition of $\llbracket - \rrbracket$ for the cases (of computation and homomorphism terms) that are already covered in great detail in Ahman et al. [2016], and instead concentrate on demonstrating how to define the interpretation function $\llbracket - \rrbracket$ for algebraic operations, the user-defined algebra type, and the two composition operations. Diagrammatic and more detailed treatment of these cases of the definition of $\llbracket - \rrbracket$ can be found in §6 and §7 of the author's PhD thesis [Ahman 2017].

First, we define $\llbracket - \rrbracket$ on algebraic operations $\operatorname{op}_{\underline{V}}^{\underline{C}}(y.M)$ as follows:

$$ (\llbracket \Gamma; \operatorname{op}_{\underline{V}}^{\underline{C}}(y.M) \rrbracket_2)_\gamma \stackrel{\text{def}}{=} \operatorname{op}_{(\llbracket \Gamma; \underline{C} \rrbracket_2)_\gamma(\star)} \circ \prod_o (\llbracket \Gamma, y:O[V/x]; M \rrbracket_2)_{\langle\gamma, o\rangle} \circ \langle \mathrm{id}_1 \rangle_o : 1 \to U_{\mathcal{L}_{\mathrm{eff}}} (\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma)) $$

where $\operatorname{op}_{(\llbracket \Gamma; \underline{C} \rrbracket_2)_\gamma(\star)}$ is the corresponding operation of $\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma)$, given by the following composite:

$$ (\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma))(\vec{x}_o \vdash \operatorname{op}_{(\llbracket \Gamma; V \rrbracket_2)_\gamma(\star)}(x_o)_o) \circ \iota : \prod_{o \in \llbracket \Gamma; O[V/x] \rrbracket_2(\gamma)} (\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma))(1) \to (\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma))(1) $$

where $\iota$ is the canonical countable-product preservation isomorphism

$$ \prod_{o \in \llbracket \Gamma; O[V/x] \rrbracket_2(\gamma)} (\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma))(1) \cong (\llbracket \Gamma; \underline{C} \rrbracket_2(\gamma))(\llbracket \Gamma; O[V/x] \rrbracket_2(\gamma)) $$

Next, we define $\llbracket - \rrbracket$ on the user-defined algebra type $\langle A, \{V_{op}\}_{op \in S_{eff}} \rangle$ as follows:

$$ \llbracket \Gamma; \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle \rrbracket \stackrel{\text{def}}{=} (\llbracket \Gamma \rrbracket, \gamma \mapsto \mathcal{M}^\gamma) $$

where the functors $\mathcal{M}^\gamma : \mathcal{L}_{\mathcal{T}_{\mathrm{eff}}}$ — Set are defined on morphisms of the form $n \to 1$ as follows:$^6$

$$ \mathcal{M}^{\gamma}(n) \stackrel{\text{def}}{=} \prod_{1 \le j \le n} \llbracket \Gamma; A \rrbracket_2(\gamma) \qquad \mathcal{M}^{\gamma}(\vec{x}_j \vdash x_j) \stackrel{\text{def}}{=} \operatorname{proj}_j $$

$$ \mathcal{M}^{\gamma}(\Delta \vdash \operatorname{op}_i(t_o)_{1 \le o \le |\llbracket x: I; O \rrbracket_2((\star, i))|}) \stackrel{\text{def}}{=} f_{\operatorname{op}_i}^{\gamma} \circ \langle \mathcal{M}^{\gamma}(\Delta \vdash t_o) \rangle_{o \in \llbracket x: I; O \rrbracket_2((\star, i))} $$

where the function $f_{\operatorname{op}_i}^{\gamma}$ is derived from $\llbracket \Gamma; V_{op} \rrbracket$ as follows:

$$ f_{\operatorname{op}_i}^{\gamma} \stackrel{\text{def}}{=} f \mapsto \operatorname{proj}_{(i, f)} (\llbracket \Gamma; V_{\operatorname{op}_i} \rrbracket_2)_\gamma(\star) : \prod_{o \in \llbracket x: I; O \rrbracket_2((\star, i))} \llbracket \Gamma; A \rrbracket_2(\gamma) \to \llbracket \Gamma; A \rrbracket_2(\gamma) $$

It is worth noting that each $\mathcal{M}^\gamma$ extends straightforwardly to $m$-tuples of terms, so as to account for all morphisms in $\mathcal{L}_{\mathcal{T}_{\mathrm{eff}}}$, i.e., those of the form $n \to m$ for a general $m$. Specifically, we have that

$$ \mathcal{M}^{\gamma}((\Delta \vdash t)_{1 \le j \le m}) = \langle \mathcal{M}^{\gamma}(\Delta \vdash t) \rangle_{1 \le j \le m} $$

We also note that for $\llbracket \Gamma; \langle A; \vec{V}_{op}; \vec{W}_{eq} \rangle \rrbracket$ to be defined, we additionally require that $\mathcal{M}^\gamma$ validates the equations given in $\mathcal{E}_{\mathrm{eff}}$. Namely, we require for all $\Gamma' | \Delta \vdash T_1 = T_2 \in \mathcal{E}_{\mathrm{eff}}$ and $\gamma' \in \llbracket \Gamma' \rrbracket$ that

$$ \mathcal{M}^{\gamma}(\Delta^{\prime} \vdash T_{1}^{\prime}) = \mathcal{M}^{\gamma}(\Delta^{\prime} \vdash T_{2}^{\prime}) $$

Finally, we define $\llbracket - \rrbracket$ on the two composition operations as follows:

$$ (\llbracket \Gamma; M \text{ as } x: \underline{UC} \text{ in } \overline{W_{op}; \underline{D}} N \rrbracket_2)_\gamma \stackrel{\text{def}}{=} f^\gamma \circ (\llbracket \Gamma; M \rrbracket_2)_\gamma : 1 \to U_{\mathcal{L}_{\mathrm{eff}}} (\llbracket \Gamma; \underline{D} \rrbracket_2(\gamma)) $$

$$ (\llbracket \Gamma; z: \underline{C}^{\prime}; K \text{ as } x: \underline{UC} \text{ in } \overline{W_{op}; \underline{D}} N \rrbracket_2)_\gamma \stackrel{\text{def}}{=} \operatorname{hom}(f^\gamma) \circ (\llbracket \Gamma; z: \underline{C}^{\prime}; K \rrbracket_2)_\gamma : \llbracket \Gamma; \underline{C}^{\prime} \rrbracket_2(\gamma) \to \llbracket \Gamma; \underline{D} \rrbracket_2(\gamma) $$

<footnote>$^6$We use the notation $\prod_{1 \le j \le n} \llbracket \Gamma; A \rrbracket_2(\gamma)$ to mean the finite product $\llbracket \Gamma; A \rrbracket_2(\gamma) \times \dots \times \llbracket \Gamma; A \rrbracket_2(\gamma)$ when $n$ is a natural number, and $\prod_{m \in \mathbb{N}} \llbracket \Gamma; A \rrbracket_2(\gamma)$ when $n$ is the distinguished symbol $\omega$. In particular, we have $\mathcal{M}^\gamma(1) = \llbracket \Gamma; A \rrbracket_2(\gamma)$.</footnote>
where the function $f^γ$ is derived from $\llbracket \Gamma, x:UC; N \rrbracket$ as follows:

$$f^γ \stackrel{\text{def}}{=} c \mapsto (\llbracket \Gamma, x:UC; N \rrbracket_2)_{(\gamma, c)}(\star) : U_{\mathcal{L}_{\text{eff}}}(\llbracket \Gamma; C \rrbracket_2(\gamma)) \to U_{\mathcal{L}_{\text{eff}}}(\llbracket \Gamma; D \rrbracket_2(\gamma))$$

and where $\text{hom}(f^γ)$ is a morphism of models of $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$, given by components

$$(\text{hom}(f^\gamma))_n \stackrel{\text{def}}{=} \iota_{\llbracket \Gamma; D \rrbracket_2(\gamma)} \circ \prod_{1 \le j \le n} (f^\gamma) \circ \iota_{\llbracket \Gamma; C \rrbracket_2(\gamma)}^{-1} : (\llbracket \Gamma; C \rrbracket_2(\gamma))(n) \to (\llbracket \Gamma; D \rrbracket_2(\gamma))(n)$$

where $\iota_{\llbracket \Gamma; C \rrbracket_2(\gamma)}$ and $\iota_{\llbracket \Gamma; D \rrbracket_2(\gamma)}$ are the canonical countable-product preservation isomorphisms

$$\prod_{1 \le j \le n} (\llbracket \Gamma; C \rrbracket_2(\gamma))(1) \cong (\llbracket \Gamma; C \rrbracket_2(\gamma))(n) \qquad \prod_{1 \le j \le n} (\llbracket \Gamma; D \rrbracket_2(\gamma))(1) \cong (\llbracket \Gamma; D \rrbracket_2(\gamma))(n)$$

We note that for these two cases of $\llbracket - \rrbracket$ to be defined, we require that $f^γ$ commutes with the operations of $\llbracket \Gamma; C \rrbracket_2(\gamma)$ and $\llbracket \Gamma; D \rrbracket_2(\gamma)$, for all $i \in \llbracket \star; I \rrbracket_2(\star)$, as depicted in the following diagram:

<figure><img src="image_4.png" /></figure>

## 8.5 Soundness

In order to establish the soundness of the interpretation $\llbracket - \rrbracket$ we defined above in §8.2 and §8.4, we first formulate and prove standard semantic weakening and substitution results. In particular, we begin by defining standard a priori partial semantic projection and substitution morphisms

$$\text{proj}_{\Gamma_1; x:A; \Gamma_2} : \llbracket \Gamma_1, x:A, \Gamma_2 \rrbracket \to \llbracket \Gamma_1, \Gamma_2 \rrbracket \qquad \text{subst}_{\Gamma_1; x:A; \Gamma_2; V} : \llbracket \Gamma_1, \Gamma_2[V/x] \rrbracket \to \llbracket \Gamma_1, x:A, \Gamma_2 \rrbracket$$

by induction on the size of $\Gamma_2$ as follows:

$$\text{proj}_{\Gamma_1; x:A; \star} \stackrel{\text{def}}{=} \pi_{\llbracket \Gamma_1; A \rrbracket} \qquad \text{proj}_{\Gamma_1; x:A; \Gamma_2; y:B} \stackrel{\text{def}}{=} \overline{\{\text{proj}_{\Gamma_1; x:A; \Gamma_2} (\llbracket \Gamma_1, \Gamma_2; B \rrbracket)\}}$$

$$\text{subst}_{\Gamma_1; x:A; \star; V} \stackrel{\text{def}}{=} \llbracket \Gamma; V \rrbracket \qquad \text{subst}_{\Gamma_1; x:A; \Gamma_2; y:B; V} \stackrel{\text{def}}{=} \overline{\{\text{subst}_{\Gamma_1; x:A; \Gamma_2; V} (\llbracket \Gamma_1, x:A, \Gamma_2; B \rrbracket)\}}$$

Next, we show that both morphisms are defined if the interpretations of the involved contexts, types, and terms are defined; and that reindexing along them models weakening and substitution. These results also extend to account for weakening and substitution with multiple value variables.

**PROPOSITION 8.2.** Given value contexts $\Gamma_1$ and $\Gamma_2$, a value type $A$, and a value variable $x$ such that $\llbracket \Gamma_1, \Gamma_2 \rrbracket \in \text{Set}$ and $\llbracket \Gamma_1, x:A, \Gamma_2 \rrbracket \in \text{Set}$, then i) the semantic projection morphism $\text{proj}_{\Gamma_1; x:A; \Gamma_2}$ is defined; and ii) given a value type $B$ such that $\llbracket \Gamma_1, \Gamma_2; B \rrbracket \in \text{Fam}_{\llbracket \Gamma_1, \Gamma_2 \rrbracket}(\text{Set})$, we have

$$\llbracket \Gamma_1, x:A, \Gamma_2; B \rrbracket = \text{proj}^*_{\Gamma_1; x:A; \Gamma_2} (\llbracket \Gamma_1, \Gamma_2; B \rrbracket)$$

and similarly for computation types, and value, computation, and homomorphism terms.

**PROPOSITION 8.3.** Given value contexts $\Gamma_1$ and $\Gamma_2$, a value type $A$, a value variable $x$, and a value term $V$ such that $\llbracket \Gamma_1; V \rrbracket : 1(\llbracket \Gamma_1 \rrbracket) \to \llbracket \Gamma_1; A \rrbracket$, $\llbracket \Gamma_1, x:A, \Gamma_2 \rrbracket \in \text{Set}$, and $\llbracket \Gamma_1, \Gamma_2[V/x] \rrbracket \in \text{Set}$, then i) the semantic substitution morphism $\text{subst}_{\Gamma_1; x:A; \Gamma_2; V}$ is defined; and ii) given a value type $B$ such that $\llbracket \Gamma_1, x:A, \Gamma_2; B \rrbracket \in \text{Fam}_{\llbracket \Gamma_1, x:A, \Gamma_2 \rrbracket}(\text{Set})$, we have

$$\llbracket \Gamma_1, \Gamma_2[V/x]; B[V/x] \rrbracket = \text{subst}^*_{\Gamma_1; x:A; \Gamma_2; V} (\llbracket \Gamma_1, x:A, \Gamma_2; B \rrbracket)$$

and similarly for computation types, and value, computation, and homomorphism terms.

In addition, we show that substituting computation and homomorphism terms for computation variables corresponds to the composition of the morphisms that the given terms denote.
**PROPOSITION 8.4.** Given a value context $\Gamma$, a computation variable $z$, a computation type $\mathcal{C}$, a computation term $M$, and a homomorphism term $K$ such that $[\Gamma; M] : 1([\Gamma]) \to U([\Gamma; \mathcal{C}])$ and $[\Gamma; z : \mathcal{C}; K] : [\Gamma; \mathcal{C}] \to ([\Gamma], \underline{D})$, for some $\underline{D} : [\Gamma] \to \text{Mod}$, then

$$[\Gamma; K[M/z]] = U([\Gamma; z : \mathcal{C}; K]) \circ [\Gamma; M]$$

**PROPOSITION 8.5.** Given a value context $\Gamma$, computation variables $z_1$ and $z_2$, computation types $\mathcal{C}_1$ and $\mathcal{C}_2$, and homomorphism terms $K$ and $L$ such that $[\Gamma; z_1 : \mathcal{C}_1; K] : [\Gamma; \mathcal{C}_1] \to [\Gamma; \mathcal{C}_2]$ and $[\Gamma; z_2 : \mathcal{C}_2; L] : [\Gamma; \mathcal{C}_2] \to ([\Gamma], \underline{D})$, for some $\underline{D} : [\Gamma] \to \text{Mod}$, then

$$[\Gamma; z_1 : \mathcal{C}_1; L[K/z_2]] = [\Gamma; z_2 : \mathcal{C}_2; L] \circ [\Gamma; z_1 : \mathcal{C}_1; K]$$

Finally, we prove the main soundness theorem for our language.

**THEOREM 8.6 (SOUNDNESS).** $[\neg]$ is defined on all well-formed contexts, well-formed types, and well-typed terms, and it identifies definitionally equal contexts, types, and terms.

**PROOF.** We prove this theorem by induction on the given derivations. For the definitional equations that correspond to the equations given in $\mathcal{E}_{\text{eff}}$ (see Fig. 4), we recall that these equations hold in the countable Lawvere theory $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ by construction. Therefore, all models of $\mathcal{L}_{\mathcal{T}_{\text{eff}}}$ validate them, including those modelling our computation types. For computation types, we prove that $[\Gamma; \langle A; \overrightarrow{V_{op}}; \overrightarrow{W_{eq}} \rangle]$ is defined by observing that the interpretations of the proof witnesses $\overrightarrow{W_{eq}}$ ensure that each $M^\gamma$ validates the equations given in $\mathcal{E}_{\text{eff}}$, as required in §8.4. For computation terms, we prove that $[\Gamma; M \text{ as } x : U\mathcal{C} \text{ in } \overrightarrow{W_{op}}; \overrightarrow{D}]$ is defined by observing that the interpretations of the proof witnesses $\overrightarrow{W_{op}}$ ensure that the functions $f^\gamma$ derived from $[\Gamma, x : U\mathcal{C}; N]$ commute with the operations of $[\Gamma; \mathcal{C}]_2(\gamma)$ and $[\Gamma; \underline{D}]_2(\gamma)$, as required in §8.4; the homomorphism term case is analogous. $\square$

# 9 CONCLUSION AND FUTURE WORK

In this paper we have given a comprehensive account of algebraic effects and their handlers in the dependently typed setting. In particular, we gave handlers a novel type-based treatment and demonstrated that being able to handle computations into values provides a useful mechanism for reasoning about effectful computations. We also showed how to equip the resulting language with a denotational semantics based on families fibrations and models of countable Lawvere theories.

In future, we plan to combine our type-based treatment of handlers with effect-typing [Kammar et al. 2013] and multi-handlers [Lindley et al. 2017]. We also plan to investigate extending eMLTT with local effects, such as local state (e.g., Staton [2013]). In particular, while we could use our fibred effect theories to express the operations and equations of the theory of local state, our current strategy of giving semantics to our language using the corresponding countable Lawvere theories and their (set-theoretic) models would not give a desired result for local effects. Namely, it is well-known that there are no non-trivial set-theoretic models of the theory of local state [Staton 2013, Prop. 6]. Instead, we plan to generalise from fibrations based on models of countable Lawvere theories to fibrations based on the presheaf models of Staton's parameterised algebraic theories.

# ACKNOWLEDGMENTS

The bulk of this work was done when I was a PhD student at the University of Edinburgh. I am grateful to James Cheney, Paul Levy, Sam Lindley, Gordon Plotkin, Tarmo Uustalu, and the anonymous reviewers for their helpful comments and useful discussions. I also thank Neel Krishnaswami, in particular, for reminding me of Hedberg's theorem for §7.1. This work was supported, in part, by the Estonian scholarship program Kristjan Jaak, which is funded and managed by the Archimedes Foundation; and by the European Research Council under ERC Starting Grant SECOMP (715753).
REFERENCES

J. Adamek and J. Rosicky. 1994. *Locally Presentable and Accessible Categories*. Number 189 in London Mathematical Society Lecture Note Series. Cambridge Univ. Press.

D. Ahman. 2017. *Fibred Computational Effects*. Ph.D. Dissertation. School of Informatics, University of Edinburgh.

D. Ahman, J. Chapman, and T. Uustalu. 2014. When is a container a comonad? *Logical Methods in Computer Science* 10, 3 (2014).

D. Ahman, N. Ghani, and G. D. Plotkin. 2016. Dependent Types and Fibred Computational Effects. In *Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016 (LNCS)*, Vol. 9634. Springer, 1–19.

D. Ahman, C. Hriţcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, and N. Swamy. 2017. Dijkstra Monads for Free. In *Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL 2017*. ACM, 515–529.

D. Ahman and S. Staton. 2013. Normalization by Evaluation and Algebraic Effects. In *Proc. of 29th Conf. on the Mathematical Foundations of Programming Semantics, MFPS XXIX (ENTCS)*, Vol. 298. Elsevier, 51–69.

D. Ahman and T. Uustalu. 2014. Update Monads: Cointerpreting Directed Containers. In *Post-proc. of 19th Meeting "Types for Proofs and Programs"*, TYPES 2013 (LIPIcs), Vol. 26. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, 1–23.

A. Bauer and M. Pretnar. 2015. Programming with algebraic effects and handlers. *J. Log. Algebr. Meth. Program.* 84, 1 (2015), 108–123.

E. Brady. 2013. Programming and reasoning with algebraic effects and dependent types. In *Proc. of 18th ACM SIGPLAN Int. Conf. on Functional Programming*, ICFP 2013. ACM, 133–144.

C. Casinghino. 2014. *Combining Proofs and Programs*. Ph.D. Dissertation. University of Pennsylvania.

E. W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. *CACM* 18, 8 (1975), 5.

P. Dybjer and A. Setzer. 1999. A Finite Axiomatization of Inductive-Recursive Definitions. In *Proc. 4th Int. Conf. on Typed Lambda Calculi and Applications, TLCA'99 (LNCS)*, Vol. 1581. Springer, 129–146.

J. Egger, R. E. Møgelberg, and A. Simpson. 2014. The enriched effect calculus: syntax and semantics. *J. Log. Comput.* 24, 3 (2014), 615–654.

N. Ghani, L. Malatesta, F. N. Forsberg, and A. Setzer. 2013. Fibred Data Types. In *Proc. of 28th Ann. Symp. on Logic in Computer Science, LICS 2013*. IEEE Computer Society, 243–252.

G. A. Grätzer. 1979. *Universal Algebra* (2nd ed.). Springer.

P. Hancock and A. Setzer. 2000. Interactive programs in dependent type theory. In *Proc. of 14th Ann. Conf. of the EACSL on Computer Science Logic, CSL 2000 (LNCS)*, Vol. 1862. Springer, 317–331.

M. Hedberg. 1998. A Coherence Theorem for Martin-Löf's Type Theory. *J. Funct. Program.* 8, 4 (1998), 413–436.

D. Hillerström and S. Lindley. 2016. Liberating Effects with Rows and Handlers. In *Proc. of 1st Wksh. on Type-Driven Development, TyDe 2016*. ACM, 15–27.

M. Hofmann. 1995. *Extensional concepts in intensional type theory*. Ph.D. Dissertation. Laboratory for Foundations in Computer Science, University of Edinburgh.

M. Hofmann. 1997. Syntax and Semantics of Dependent Types. In *Semantics and Logics of Computation*. Cambridge Univ. Press, 79–130.

K. Honda, V. T. Vasconcelos, and M. Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In *Proc. of 7th European Symp. on Programming, ESOP 1998 (LNCS)*, Vol. 1381. Springer, 122–138.

M. Hyland, G. Plotkin, and J. Power. 2006. Combining effects: Sum and tensor. *Theor. Comput. Sci.* 357, 1–3 (2006), 70–99.

B. Jacobs. 1999. *Categorical Logic and Type Theory*. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Elsevier.

O. Kammar, S. Lindley, and N. Oury. 2013. Handlers in Action. In *Proc. of 18th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2013*. ACM, 145–158.

O. Kammar and G. D. Plotkin. 2012. Algebraic Foundations for Effect-dependent Optimisations. In *Proc. of 39th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2012*. ACM, 349–360.

D. Leijen. 2017. Type Directed Compilation of Row-Typed Algebraic Effects. In *Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL 2017*. ACM, 486–499.

P. B. Levy. 2004. *Call-By-Push-Value: A Functional/Imperative Synthesis*. Semantics Structures in Computation, Vol. 2. Springer.

P. B. Levy. 2006. Monads and Adjunctions for Global Exceptions. *ENTCS* 158 (2006), 261–287.

P. B. Levy. 2017. Contextual isomorphisms. In *Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL 2017*. ACM, 400–414.

S. Lindley, C. McBride, and C. McLaughlin. 2017. Do Be Do Be Do. In *Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL 2017*. ACM, 500–514.

P. Martin-Löf. 1975. An intuitionistic theory of types, Predicative part. In *Proc. of Logic Colloquium 1973*. North-Holland, 73–118.
P. Martin-Löf. 1984. *Intuitionistic Type Theory*. Bibliopolis.

C. McBride. 2011. Functional Pearl: Kleisli arrows of outrageous fortune. *J. Funct. Program*. (2011). (To appear).

E. Moggi. 1989. Computational Lambda-Calculus and Monads. In *Proc. of 4th Ann. Symp. on Logic in Computer Science, LICS '89*. IEEE, 14–23.

E. Moggi. 1991. Notions of Computation and Monads. *Inf. Comput*. 93, 1 (1991), 55–92.

G. Munch-Maccagnoni. 2013. *Syntax and Models of a non-Associative Composition of Programs and Proofs*. Ph.D. Dissertation. Univ. Paris Diderot.

A. Nanevski, G. Morrisett, and L. Birkedal. 2008. Hoare Type Theory, polymorphism and separation. *J. Funct. Program*. 18, 5–6 (2008), 865–911.

M. Okada and P. J. Scott. 1999. A Note on Rewriting Theory for Uniqueness of Iteration. *Theory Appl. Categ.* 6, 4 (1999), 47–64.

P.-M. Pédrot and N. Tabareau. 2017. An Effectful Way to Eliminate Addiction to Dependence. In *Proc. of 32nd Ann. Symp. on Logic in Computer Science, LICS 2017*. 1–12.

A. M. Pitts. 1991. Evaluation Logic. In *Proc. IVth Higher Order Workshop (Workshops in Computing)*. Springer, 162–189.

A. M. Pitts, J. Matthiesen, and J. Derikx. 2015. A Dependent Type Theory with Abstractable Names. In *Proc. of 9th Wksh. on Logical and Semantic Frameworks, with Applications, LSFA 2014 (ENTCS)*, Vol. 312. Elsevier, 19–50.

G. Plotkin and J. Power. 2001. Semantics for Algebraic Operations. In *Proc. of 17th Conf. on the Mathematical Foundations of Programming Semantics, MFPS XVII (ENTCS)*, Vol. 45. Elsevier, 332–345.

G. D. Plotkin and J. Power. 2002. Notions of Computation Determine Monads. In *Proc. of 5th Int. Conf. on Foundations of Software Science and Computation Structures, FOSSACS 2002 (LNCS)*, Vol. 2303. Springer, 342–356.

G. D. Plotkin and M. Pretnar. 2008. A Logic for Algebraic Effects. In *Proc. of 23rd Ann. IEEE Symp. on Logic in Computer Science, LICS 2008*. IEEE, 118–129.

G. D. Plotkin and M. Pretnar. 2013. Handling Algebraic Effects. *Logical Methods in Computer Science* 9, 4:23 (2013).

J. Power. 2006. Countable Lawvere Theories and Computational Effects. In *Proc. of 3rd Irish Conf. on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2004 (ENTCS)*, Vol. 161. Elsevier, 59–71.

S. Staton. 2013. Instances of Computational Effects: An Algebraic Perspective. In *Proc. of 28th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS 2013*. IEEE, 519–519.

T. Streicher. 1991. *Semantics of Type Theory. Correctness, Completeness and Independence Results*. Birkhäuser Boston.

The Agda Team. 2017. The Agda Wiki. Available at http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php. (2017).

The Univalent Foundations Program. 2013. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study. Available at: https://homotopytypetheory.org/book/.