# Dependent Types and Fibred Computational Effects

- 10 Citations
- 528 Downloads

## Abstract

We study the interplay between dependent types and general computational effects. We define a language with both value types and terms, and computation types and terms, where types depend only on value terms. We use computational \(\varSigma \)-types to account for type-dependency in the sequential composition of computations. Our language design is justified by a natural class of categorical models. We account for both algebraic and non-algebraic effects. We also show how to extend the language with general recursion, using continuous families of cpos.

## 1 Introduction

While dependent types have proven very useful on their own, for both programming and theorem proving, one also seeks a general way to combine them with computational effects, such as I/O, state, continuations, or recursion, so as to write more practical, concise, or clearer programs. However, despite the study of each of the two fields being well advanced, their combination presents difficulties, as recognised already by Moggi [25].

One puzzling problem is what to make of a type *A*(*M*) if *M* can raise an effect. We do not know a general denotational semantics for such types, though there may be one (there is one for local names [28]). Pragmatically, the situation depends on the nature of the computational effects considered. For effects not requiring interaction with the program runtime, such as local names [28] or general recursion [7], one need not restrict *M*, as computing *A*(*M*) then only depends on static information. However, this does not work well in general, as some effects, e.g., I/O, do crucially depend on interaction with the program runtime, and so then will the computation of *A*(*M*). As one consequence, extending a coarse-grained language, e.g., Moggi’s computational lambda calculus [24], with dependent types seems not to give a general solution, as the natural elimination rule for \(\varPi \)-types produces types of the form *A*(*M*) (and cf. Levy [20, Sect. 12.4.1]).

A natural move to try to solve these problems is to allow types to depend only on value terms. This is the route we take in this paper and it does lead to a natural general semantics. While at first such a choice might seem limiting, we recover dependency on the statically available information about computational effects by inspecting the structure of thunked computations.

*A*and computation types \(\underline{C}\), as in Call-By-Push-Value (CBPV) [20] and the Enriched Effect Calculus (EEC) [9]. Then the variables in types range only over value types, as desired. However, a further problem then arises: the usual typing rule

*x*may occur freely in \(\underline{C}(x)\) in the conclusion. An evident move here is to prohibit

*x*from occurring freely in \(\underline{C}\), as, e.g., advocated by Levy [20, Sect. 12.4.1] and Brady [5]. However, this seems too restrictive: to make the most of dependent types, it is desirable for the type of an effectful program to depend on values produced by preceding computations. As an example, consider combining monadic parsing [16] with dependent types and applying it to the parsing of well-typed syntax. Then it is natural to decompose the parsing of function applications into a parser for the function and a parser for the argument, where the type of the latter crucially depends on the domain of the type of the parsed function.

*computational*\(\varSigma \)

*-types*\({\varSigma x \!:\! A. \underline{C}(x)}\), whose use is inspired by the algebraic treatment of computational effects [31]. To explain these, suppose computation types denote algebras for the algebraic theory of boolean-valued read-only store [35, Sect. III.A]. Now let us consider the composite effectful program

*M*(2), which has type \(\underline{C}(2)\), or as

*M*(3), which has type \(\underline{C}(3)\). So the whole computation yields an element of the coproduct of algebras \(\underline{C}(2) + \underline{C}(3)\). This pattern also recurs with other computational effects, and dependency on value types other than natural numbers: hence the computational \(\varSigma \)-types. These types enable us to type sequential composition by “closing-off” the free variable

*x*in \(\underline{C}(x)\): using the hypothesis of (*) we derive

We aim to put these ideas together at a *foundational* level, comparable with the levels at which the two fields have been studied separately. In contrast, the existing work on combining dependent types with first-class computational effects has concerned only *particular* kinds of effects (e.g., [7, 26, 28, 37]). Other authors have used dependent types in existing languages to *represent* effects using DSLs (e.g., [5, 13, 23]). There has, however, been no work combining dependent types with *general, first class* computational effects.

In Sect. 2, we define a small dependently-typed language with computational effects, combining features from Martin-Löf type theory (MLTT) [22] and computational languages separating values and computations, such as CBPV or EEC. The language design we propose is justified in Sect. 3 in terms of a sound and complete interpretation in a class of categorical models naturally combining (i) comprehension categories arising from the semantics of dependent types; and (ii) adjunctions arising from the semantics of computational effects. In Sect. 4, we extend the language and its semantics with algebraic effects. In Sect. 5, we extend the language and its semantics with general recursion.

## 2 A Dependently-typed Effectful Language

We now define the syntax and equational theory of our dependently-typed effectful language, making a clear distinction between values and computations, at both type and term levels: the value fragment of our language is based on MLTT; the computational fragment is greatly influenced by CBPV and EEC.

*Variables.* We assume two countable sets: of *value variables*, ranged over by \(x, y, \ldots \); and of *computation variables*, ranged over by \(z, \ldots \). The former are treated as in MLTT: they are intuitionistic, and enjoy structural rules of weakening and contraction. The latter, on the other hand, are treated linearly, as in EEC, and play a crucial role in the elimination rule for computational \(\varSigma \)-types.

*Types.*Our

*value types*\(A, B, \ldots \) are given as in MLTT, except for the type \(U\underline{C}\) of thunks, familiar from CBPV. To keep the presentation simple and focussed on the computational fragment of our language, we omit value sum types and general inductive types, both of which can be easily added. Our

*computation types*\(\underline{C}, \underline{D}, \ldots \) generalise those of CBPV and EEC. The grammar of types is

*FA*is the type of computations returning values of type

*A*. The computational \(\varSigma \)- and \(\varPi \)-types are the natural dependently-typed generalisations of EEC’s computational tensor and function types: \(!A \otimes \underline{C}\), \(A \rightarrow \underline{C}\). Rules defining well-formed value contexts \({\vdash \varGamma }\) and types \({\varGamma \,\vdash \, A}\), \({\varGamma \,\vdash \, \underline{C}}\) are given in Fig. 1.

*Terms.*We let \(V, W, \ldots \) to range over

*value terms*. These are given as in MLTT, except for thunked computations \(\mathtt {thunk~} M\), familiar from CBPV. Compared to CBPV, we include both value functions and complex values to accommodate pure programs on which the types of our language could depend. Regarding effectful programs, we further distinguish between

*computation terms*, ranged over by \(M, N, \ldots \) and

*homomorphism terms*, ranged over by \(K,L,\ldots \). We decorate our terms with certain type-annotations, so that we can later define the denotational semantics on raw syntax — a standard approach in the literature [15, 36]. We omit these annotations in informal discussion. The grammar of terms is

Our *computation terms* share many similarities with those in CBPV, but additionally include the introduction and elimination rules for computational \(\varSigma \)-types, given by pairing \(\langle V,M \rangle \) and pattern-matching \({M \mathtt {~to~} \langle x,z \rangle \mathtt {~in~} K}\), whose syntax is similar to that for computational tensor types \(!A \otimes \underline{C}\) in EEC.

As with the linear terms in EEC, our *homomorphism terms* contain computation variables *z* used linearly. From an operational perspective, the typing rules for homomorphism terms ensure that a computation bound to *z* always happens first in a well-typed term containing it. So, when eliminating a pair \(\langle V,M \rangle \), *M* always happens before the rest of *K* in the compound term \({\langle V,M \rangle \mathtt {~to~} \langle x,z \rangle \mathtt {~in~} K}\), thus preserving the intended left-to-right evaluation order. This use of computation variables ensures that homomorphism terms denote algebra homomorphisms in the examples based on Eilenberg-Moore algebras of monads, or on algebraic effects [31]: hence the name. Similar forms of linearity are also present in CBPV with stacks [20, Sect. 2.3.4]; indeed, homomorphism terms can be viewed as a programmer-friendly syntax for dependently-typed stack terms.

The linear use of computation variables is also reminiscent of recent work on combining dependent and linear types in languages with distinguished intuitionistic and linear fragments [19, 38]. That work is designed to capture the adjunction models of intuitionistic linear logic [3]; in contrast, our language is designed to capture the computational nature of certain adjunctions.

*Equations.* We equip our language with an equational theory, consisting of equations between well-formed types, written \({\varGamma \vdash A = B}\) and \({\varGamma \vdash \underline{C} = \underline{D}}\); and well-typed terms, written \({\varGamma \vdash V = W:A}\), \({\varGamma \vdash M = N:\underline{C}}\) and \({\varGamma \,\vert \,z \!:\! \underline{C} \vdash K = L:\underline{D}}\). The equations between types consist of reflexivity equations for \(\mathsf {Nat}\) and 1, and congruence rules for all the other type formers. We omit the equations between value terms as they are standard from MLTT with natural numbers and intensional identity types [15, 22]. The rules for equations between computation and homomorphism terms are given in Fig. 3. We leave the well-typedness assumptions about the constituent terms implicit, and omit type conversion, equivalence, and congruence rules. Many of the equations in Fig. 3 are familiar from EEC, modulo the dependent-typing. Compared to other computational languages, such as [24], standard equations that may seem missing from the theory, such as associativity of sequential composition, are in fact derivable.

*Some meta-theory.* The substitution of value terms for value variables has a straightforward mutually recursive definition. We write *A*[*V* / *x*] for the substitution of *V* for *x* in *A*. The substitution of computation and homomorphism terms for computation variables is also routine, recursing only in the sub-terms where linearly used computation variables can appear. We write *K*[*M* / *z*] for the substitution of *M* for *z* in *K*. Then, standard weakening and substitution rules for value variables are admissible for all judgments of our language. In addition, further substitution rules for computation variables are admissible for judgments \({\varGamma \,\vert \,z \!:\! \underline{C} \vdash K{\,:\,}\underline{D}}\) and \({\varGamma \,\vert \,z \!:\! \underline{C} \vdash K = L:\underline{D}}\), covering the substitution of both computation and homomorphism terms for computation variables.

## 3 Denotational Semantics

The denotational semantics of our language is based on standard fibred category theory. To make our work more accessible, we recall some preliminaries of this theory and suggest [18] for more details. Fibred category theory provides a natural framework for developing the semantics of dependently-typed languages, where: (i) functors model type-dependency; (ii) split fibrations model substitution; and (iii) closed comprehension categories model \(\varSigma \)- and \(\varPi \)-types. The ideas we develop can also be expressed in terms of other models of dependent types, such as categories with families, or categories with attributes [15, 27].

### 3.1 Fibred Category Theory Preliminaries

*Fibrations.* Given a functor \({p : \mathcal {E} \longrightarrow \mathcal {B}}\), a morphism \({g : A \longrightarrow B}\) is called a *Cartesian lifting* of \({f : X \longrightarrow Y}\) if \({p(g) = f}\) and for all \({i : C \longrightarrow B}\) and \({j : p(C) \longrightarrow X}\), such that \({p(i) = f \circ j}\) in \(\mathcal {B}\), there exists a unique \(h : C \longrightarrow A\) over *j* such that \(g \,\circ \, h = i\). The functor \({p : \mathcal {E} \longrightarrow \mathcal {B}}\) is called a *fibration* if for every *B* in \(\mathcal {E}\) and \(f : X \longrightarrow p(B)\) in \(\mathcal {B}\) there exists a Cartesian lifting \(g : A \longrightarrow B\) of *f* in \(\mathcal {E}\). A morphism \(f : A \longrightarrow B\) in \(\mathcal {E}\) is called *vertical* if \(p(A) = p(B) = X\) and \(p(f) = \mathsf {id}_{X}\). For any *X* in \(\mathcal {B}\), we write \(\mathcal {E}_X\) for the *fibre over X*, i.e., for the subcategory of \(\mathcal {E}\) consisting of objects over *X* and vertical morphisms. A fibration is called *cloven* if it comes with a choice of Cartesian liftings. We write \({\overline{f}(B) : f^*(B) \longrightarrow B}\) for the chosen Cartesian lifting of \({f : X \longrightarrow p(B)}\). In cloven fibrations, every \(\mathcal {B}\)-morphism \({f : X \longrightarrow Y}\) determines a *reindexing functor*\({f^* : \mathcal {E}_Y \longrightarrow \mathcal {E}_X}\), satisfying \({(\mathsf {id}_X)^* \cong \mathsf {id}_{\mathcal {E}_X}}\) and \({(g \circ f)^* \cong f^* \circ g^*}\). A cloven fibration is said to be *split* if these two isomorphisms are identities.

Given split fibrations \({p : \mathcal {V} \longrightarrow \mathcal {B}}\) and \({q : \mathcal {C} \longrightarrow \mathcal {B}}\), a *split fibred functor*\({F : p \longrightarrow q}\) is given by a functor \({F : \mathcal {V} \longrightarrow \mathcal {C}}\), such that \(q \circ F = p\) and *F* preserves the chosen Cartesian morphisms on-the-nose. Given two split fibred functors \({F , G : p \longrightarrow q}\), a *split fibred natural transformation*\(\alpha : F \Rightarrow G\) is given by a natural transformation \({\alpha : F \Rightarrow G}\), in which every component of \(\alpha \) is vertical. A *split fibred adjunction*\({F \dashv U : q \longrightarrow p}\) is given by split fibred functors \({F : p \longrightarrow q}\) and \({U : q \longrightarrow p}\), together with split fibred natural transformations \({\eta : \mathsf {id}_\mathcal {V} \longrightarrow U \circ F}\) and \({\varepsilon : F \circ U \longrightarrow \mathsf {id}_\mathcal {C}}\), subject to the standard unit-counit laws for adjunctions.

*Comprehension categories.* A *(split) comprehension category with unit* is given by a (split) fibration \(p : \mathcal {E} \longrightarrow \mathcal {B}\), together with a comprehension-admitting terminal object functor \({1 : \mathcal {B} \longrightarrow \mathcal {E}}\), i.e., 1 has a right adjoint \({\{-\} : \mathcal {E} \longrightarrow \mathcal {B}}\); it is said to be *full* when the functor \(A \overset{\pi _{(-)}}{\mapsto } p(\varepsilon ^{1 \dashv \{-\}}_A) : \mathcal {E} \longrightarrow \mathcal {B}^\rightarrow \) is full and faithful. For all *A* in \(\mathcal {E}\), the \(\mathcal {B}\)-morphism \(\pi _A : \{A\} \longrightarrow p(A)\) is called a *projection map*. The corresponding reindexing functor \(\pi _A^* : \mathcal {E}_{p(A)} \longrightarrow \mathcal {E}_{\{A\}}\) is called the *weakening functor*. For every comprehension category with unit \(p : \mathcal {E} \longrightarrow \mathcal {B}\), we have an isomorphism \( \mathcal {E}_{p(A)}(1_{p(A)}, A) \,\,\cong \,\, \{g : p(A) \longrightarrow \{A\} \,\vert \,\pi _A \circ g = \mathsf {id}_{p(A)}\} \), for all *A* in \(\mathcal {E}\). As a notational convention, we write \(\mathtt {s}(f) : p(A) \longrightarrow \{A\}\) for the section corresponding to the global element \(f : 1_{p(A)} \longrightarrow A\), given by \(\{f\} \,\circ \, \eta _A^{1 \dashv \{-\}}\).

A comprehension category with unit \(p : \mathcal {E} \longrightarrow \mathcal {B}\) is said to have *dependent products* (resp. *weak dependent sums*) when the weakening functors \(\pi _A^*\) have right adjoints \(\varPi _A\) (resp. left adjoints \(\varSigma _A\)), for all *A* in \(\mathcal {E}\), satisfying the Beck-Chevalley condition: for all Cartesian morphisms \(f : A \longrightarrow B\), the canonical natural transformation \({(p(f))^* \circ \varPi _B \longrightarrow \varPi _A \circ \{f\}^*}\) (resp. \({\varSigma _A \circ \{f\}^* \longrightarrow (p(f))^* \circ \varSigma _B}\)) is an isomorphism. A comprehension category with unit \(p : \mathcal {E} \longrightarrow \mathcal {B}\) is said to have *strong dependent sums* when it has weak dependent sums, s.t. for all *B* in \(\mathcal {E}_{\{A\}}\), the morphism \(\{\overline{\pi _A}(\varSigma _A B) \circ \eta _B^{\varSigma _A \dashv \,\pi _A^*}\} : \{B\} \longrightarrow \{\varSigma _A B\}\) is an isomorphism.

*Split closed comprehension categories.* In order to define fibred adjunction models in Sect. 3.2, we use a particularly well-behaved class of comprehension categories (from the perspective of interpreting type theory), namely, those that are split and closed. A *split closed comprehension category* (SCCompC) is a split full comprehension category with unit \({p : \mathcal {E} \longrightarrow \mathcal {B}}\), where the base category \(\mathcal {B}\) has a terminal object; the fibred terminal objects are preserved on-the-nose by reindexing; and which has dependent products and strong dependent sums, for which the isomorphisms in the Beck-Chevalley conditions are identities.

*Natural numbers.* A SCCompC \(p : \mathcal {E} \longrightarrow \mathcal {B}\) is said to support *weak natural numbers* if there exists an object \(\mathbb {N}\) in \(\mathcal {E}_1\) and vertical morphisms \( {\mathsf {zero}: 1_1 \longrightarrow \mathbb {N}} \), \( {\mathsf {succ}: \mathbb {N}\longrightarrow \mathbb {N}} \), s.t. for all *X* in \(\mathcal {B}\), *A* in \(\mathcal {E}_{\{!_X^*(\mathbb {N})\}}\), \(h_z : 1_X \longrightarrow (\mathtt {s}(!_X^*(\mathsf {zero})))^*(A)\) in \(\mathcal {E}_X\) and \(h_s : 1_{\{A\}} \longrightarrow \pi _A^*(\{!_X^*(\mathsf {succ})\}^* (A))\) in \(\mathcal {E}_{\{A\}}\), there exists \( h : 1_{\{!^*_X(\mathbb {N})\}} \longrightarrow A \) in \(\mathcal {E}_{\{!^*_X(\mathbb {N})\}}\), satisfying \((\mathtt {s}(!_X^*(\mathsf {zero})))^*(h) = h_z\) and \(\pi _A^*(\{!_X^*(\mathsf {succ})\}^* (h)) = h_s\).

We present \(\mathbb {N}\) axiomatically rather than using weak initial algebras since our language and its models do not assume coproducts. Moreover, discussing the semantics of inductive types and their fibred induction principles in full generality [10] would digress too much from our central theme.

*Identity types.* Following the axiomatic presentation given by Warren [39], a SCCompC \(p : \mathcal {E} \longrightarrow \mathcal {B}\) is said to support *identity types*, if, for all *A* in \(\mathcal {E}\), there exists an object \(\mathsf {Id}_A\) in \(\mathcal {E}_{\{\pi _A^*(A)\}}\), and \( \mathtt {r}_A : 1_{\{A\}} \longrightarrow \delta _A^*(\mathsf {Id}_A) \) in \(\mathcal {E}_{\{A\}}\), such that for all *B* in \(\mathcal {E}_{\{\mathsf {Id}_A\}}\) and \( f : 1_{\{A\}} \longrightarrow (\mathtt {s}(\mathtt {r}_{A}))^*(\{\overline{\delta _A}(\mathsf {Id}_A)\}^*(B)) \) in \(\mathcal {E}_{\{A\}}\), there exists \( \mathtt {i}_{A,B} (f) : 1_{\{\mathsf {Id}_A\}} \longrightarrow B \) in \(\mathcal {E}_{\{\mathsf {Id}_A\}}\), satisfying \( (\mathtt {s}(\mathtt {r}_{A}))^*(\{\overline{\delta _A}(\mathsf {Id}_A)\}^*(\mathtt {i}_{A,B} (f))) = f \). These identity types are also required to satisfy a split Beck-Chevalley condition: for all Cartesian morphisms \({f : A \longrightarrow B}\), we must have \( \{f'\}^* (\mathsf {Id}_B) = \mathsf {Id}_{A} \) in \(\mathcal {E}_{\{\pi ^*_A(A)\}}\), where \(f' : \pi ^*_A(A) \longrightarrow \pi ^*_B(B)\) is the unique mediating morphism over \(\{f\}\), arising from \(\overline{\pi _B}(B) : \pi ^*_B(B) \longrightarrow B\) being a Cartesian morphism. As in [18, Sect. 9.3.5], the *diagonal morphisms*\(\delta _A\) arise from pullback squares of the form

### 3.2 Interpretation of Our Language in Fibred Adjunction Models

A *fibred adjunction model* is given by a SCCompC \({p : \mathcal {V} \longrightarrow \mathcal {B}}\), a split fibration \({q : \mathcal {C} \longrightarrow \mathcal {B}}\), and a split fibred adjunction \({F \dashv U : q \longrightarrow p}\), such that *p* supports identity types and weak natural numbers (in the sense of Sect. 3.1), and *q* supports split dependent products and sums with respect to *p* as depicted in

The split dependent products and sums in *q*, with respect to *p*, are defined as left and right adjoints to the weakening functors \(\pi ^*_A : \mathcal {C}_{p(A)} \longrightarrow \mathcal {C}_{\{A\}}\), required to satisfy the analogues of the split Beck-Chevalley conditions from Sect. 3.1.

Given a SCCompC \({p : \mathcal {V} \longrightarrow \mathcal {B}}\) that supports identity types and weak natural numbers, we can always pick the identity adjunction \({{\mathsf {id}_{\mathcal {V}} \dashv \mathsf {id}_{\mathcal {V}} : {\mathcal {V}} \longrightarrow {\mathcal {V}}}}\) to construct a corresponding “effect-free” fibred adjunction model. Further, we can construct a restricted form of adjunction models (without identity types) from models of EEC with weak natural numbers [9], i.e., from \(\mathcal {D}\)-enriched adjunctions \(F_{\text {EEC}} \dashv U_{\text {EEC}} : \mathcal {E} \longrightarrow \mathcal {D}\), where \(\mathcal {D}\) is Cartesian closed and has a weak NNO, \(\mathcal {E}\) is \(\mathcal {D}\)-enriched and has all \(\mathcal {D}\)-tensors and -cotensors. These models are based on a computational variant \(q : \mathsf {s}(\mathcal {D},\mathcal {E}) \longrightarrow \mathcal {D}\) of the the simple fibration \(p : \mathsf {s}(\mathcal {D}) \longrightarrow \mathcal {D}\) [18, Theorem 10.5.5]. In particular, the objects of \(\mathsf {s}(\mathcal {D},\mathcal {E})\) are pairs \((X,\underline{C})\) of a \(\mathcal {D}\)-object *X* and a \(\mathcal {E}\)-object \(\underline{C}\); and the morphisms \({(X,\underline{C}) \longrightarrow (Y,\underline{D})}\) are pairs (*f*, *g*) of morphisms, with \({f : X \longrightarrow Y}\) in \(\mathcal {D}\) and \({g : X \otimes \underline{C} \longrightarrow \underline{D}}\) in \(\mathcal {E}\).

*Interpretation.* Following Streicher [36] and Hoffmann [15], we define the interpretation of our language in fibred adjunction models by first giving a *partial interpretation function*\(\llbracket - \rrbracket \) on raw syntax and then proving that \(\llbracket - \rrbracket \) is defined on well-formed expressions. We do so because of the well-known issue in interpreting dependently-typed languages: as the derivations of judgments are not unique, due to the type conversion rules, defining the interpretation on the derivations would require simultaneously proving that the definition is coherent.

*A*to an object \(\llbracket \varGamma ;A \rrbracket \) in \(\mathcal {V}_{\llbracket \varGamma \rrbracket }\); a pair of a context \(\varGamma \) and computation type \(\underline{C}\) to an object \(\llbracket \varGamma ;\underline{C} \rrbracket \) in \(\mathcal {C}_{\llbracket \varGamma \rrbracket }\); a pair of a context \(\varGamma \) and a value term

*V*to an object

*A*and a morphism \(\llbracket \varGamma ;V \rrbracket : 1_{\llbracket \varGamma \rrbracket } \longrightarrow A\) in \(\mathcal {V}_{\llbracket \varGamma \rrbracket }\); a pair of a context \(\varGamma \) and a computation term

*M*to an object \(\underline{C}\) in \(\mathcal {C}_{\llbracket \varGamma \rrbracket }\) and a morphism \(\llbracket \varGamma ;M \rrbracket : 1_{\llbracket \varGamma \rrbracket } \longrightarrow U(\underline{C})\) in \(\mathcal {V}_{\llbracket \varGamma \rrbracket }\); and a triple of a context \(\varGamma \), a computation type \(\underline{C}\) and a homomorphism term

*K*to an object \(\underline{D}\) and a morphism \(\llbracket \varGamma ;\underline{C};K \rrbracket : \llbracket \varGamma ;\underline{C} \rrbracket \longrightarrow \underline{D}\) in \(\mathcal {C}_{\llbracket \varGamma \rrbracket }\). We define these different cases of \(\llbracket - \rrbracket \) simultaneously by induction on the depth of the argument expressions. In the definition, it is convenient to use Kleene equality \(\simeq \) where two sides of an equation are equal if either they are both defined and equal or they are both undefined. For contexts, \(\llbracket - \rrbracket \) is defined as

where the vertical morphisms \(\llbracket \varGamma , x \!:\! A;M \rrbracket ^\dagger \), \(\big [\llbracket \varGamma , x \!:\! A, \underline{D}_1;L \rrbracket \big ]\) and \(\lambda \llbracket \varGamma ;\underline{C};K \rrbracket \) are derived using the adjunctions involved in the definition of fibred adjunction models. Similarly to [15, 36], we make some of the cases of the definition (implicitly) conditional on the denotations of sub-terms having a particular form, based on the type-annotations with which we have decorated our terms.

### **Theorem 1**

**(Soundness).** The partial interpretation function \(\llbracket - \rrbracket \) is defined on well-formed contexts, well-formed types and well-typed terms. In addition, the interpretation identifies types and terms that are equal in the equational theory.

Similarly to [15, 36], the proof of soundness relies on lemmas relating weakening and substitution in the syntax to reindexing in fibred adjunction models.

*The classifying model.* We now show that the interpretation of our language in fibred adjunction models is complete by constructing its classifying model.

First, in the classifying fibred adjunction model the objects of \(\mathcal {B}\) are given by equivalence classes of well-formed value contexts \(\varGamma \). The morphisms \(\varGamma _1 \longrightarrow \varGamma _2\) are given by equivalence classes of tuples of value terms \(\varvec{V} = ( V_1, \ldots , V_m )\), where \({\varGamma _2 = y_1 \!:\! B_1, \ldots , y_m \!:\! B_m}\) and \(\varGamma _1\,\vdash \, V_i{\,:\,}B_i[V_1/y_1, \ldots , V_{i-1}/y_{i-1}]\), for all \({1 \le i \le m}\).

Next, the objects of the total category \(\mathcal {V}\) are given by equivalence classes of value types \({\varGamma \,\vdash \, A}\) and its morphisms \({\varGamma _1\,\vdash \, A \longrightarrow \varGamma _2\,\vdash \, B}\) by equivalence classes of tuples of value terms \(( \varvec{V}, V )\), where \(\varvec{V}\) are typed as in \(\mathcal {B}\), and *V* is typed as \({\varGamma _1, x \!:\! A\,\vdash \, V{\,:\,}B[\varvec{V}/\varGamma _2]}\). The objects and morphisms of \(\mathcal {C}\) are defined similarly: as equivalence classes of computation types \(\varGamma \,\vdash \, \underline{C}\); and as equivalence classes of tuples of terms \(( \varvec{V}, K )\), where *K* is typed as \({\varGamma _1 \,\vert \,z \!:\! \underline{C} \vdash K{\,:\,}\underline{D}[\varvec{V}/\varGamma _2]}\). The fibrations *p* and *q* are defined by context projections, i.e., by \(p(\varGamma \,\vdash \, A) =\varGamma \).

*FA*and \(U\underline{C}\), given by

### **Proposition 1**

The above definitions, based on the syntax of our language, constitute a fibred adjunction model, called the classifying model of our language.

Finally, we can use this result to prove the completeness of the interpretation.

### **Theorem 2**

**(Completeness).** If two types or two terms of our language are identified in all fibred adjunction models, they are equal in the equational theory.

### 3.3 Fibred Adjunction Models Based on the Families Fibration

We now discuss some examples of fibred adjunction models based on the prototypical model of dependent types, the families fibration \({p : \mathsf {Fam}(\mathcal {D}) \longrightarrow \mathsf {Set}}\). The objects of \(\mathsf {Fam}(\mathcal {D})\) are given by pairs (*X* , *A*) of a set *X* and an *X*-indexed family of \(\mathcal {D}\)-objects \({A : X \longrightarrow ob(\mathcal {D})}\); the morphisms \({(X,A) \longrightarrow (Y,B)}\) are pairs \((f, \{ g_x \}_{x \in X})\) of a function \({f : X \longrightarrow Y}\) and a *X*-indexed family of \(\mathcal {D}\)-morphisms \(\{ g_x : A(x) \longrightarrow B(f(x)) \}_{x \in X}\). The functor *p* is defined by first projection, i.e. by \(p(X,A) =X\). In fact, *p* is a split fibration: the reindexing functors \(f^*\) are defined by pre-composition, i.e. by \(f^*(Y,B) =(X , B \circ f)\) for all \(f : X \longrightarrow Y\). In our examples, we take \(\mathcal {D}\) to be \(\mathsf {Set}\). In this case, *p* is a SCCompC [18, Sect. 10.5]. The examples we discuss below are instances of the following general result, building on the fact that adjunctions can be lifted to families fibrations [18, Example 1.8.7(i)].

### **Theorem 3**

Given \(F \dashv U : \mathcal {E} \longrightarrow \mathsf {Set}\), such that \(\mathcal {E}\) has both set-indexed products and coproducts, the fibrations \({p : \mathsf {Fam}(\mathsf {Set}) \longrightarrow \mathsf {Set}}\) and \({q : \mathsf {Fam}(\mathcal {E}) \longrightarrow \mathsf {Set}}\), together with the pointwise lifting of \(F \dashv U\), determine a fibred adjunction model.

*q*as

The first collection of examples we discuss are based on Eilenberg-Moore algebras (EM-algebras) for a monad \((T, \eta , \mu )\) on \(\mathsf {Set}\). As standard, we write \(\mathsf {Set}^T\) for the category of EM-algebras. Its objects are given by pairs \((X , \alpha )\) of a set *X* and a function \(\alpha : TX \longrightarrow X\) such that \(\alpha \,\circ \, T(\alpha ) = \alpha \,\circ \, \mu _X\) and \(\alpha \,\circ \, \eta _X = \mathsf {id}_X\); its morphisms \((X,\alpha ) \longrightarrow (Y,\beta )\) are given by functions \(f : X \longrightarrow Y\) such that \(\beta \,\circ \, T(f) = f \,\circ \, \alpha \). There is a canonical EM-adjunction \(F^T \dashv U^T : \mathsf {Set}^T \longrightarrow \mathsf {Set}\).

### **Corollary 1**

Given a monad \((T, \eta , \mu )\) on \(\mathsf {Set}\), the EM-adjunction \({F^T \dashv U^T}\) and the families fibration \({p : \mathsf {Fam}(\mathsf {Set}) \longrightarrow \mathsf {Set}}\) determine a fibred adjunction model.

A particularly well-behaved collection of fibred adjunction models arises from the algebraic treatment of computational effects [31], namely, from monads arising from countable Lawvere theories. These are exactly the monads on \(\mathsf {Set}\) that are of countable rank [33, Theorem 2.8]. As discussed in [17], such monads combine easily, in terms of combining the operations and equations of the corresponding countable Lawvere theories. We recall that every countable Lawvere theory \(\mathcal {L}\) induces a category \(\mathsf {Mod}(\mathcal {L},\mathsf {Set})\) of models of \(\mathcal {L}\) in \(\mathsf {Set}\), with an associated forgetful functor \({U_{\mathcal {L}} : \mathsf {Mod}(\mathcal {L},\mathsf {Set}) \longrightarrow \mathsf {Set}}\) [33]. As \(\mathsf {Set}\) is locally countably presentable [1], \(U_{\mathcal {L}}\) has a left adjoint \(F_{\mathcal {L}}\), inducing an equivalence of categories between \(\mathsf {Mod}(\mathcal {L},\mathsf {Set})\) and \(\mathsf {Set}^{T_{\mathcal {L}}}\), for \({T_\mathcal {L} =U_{\mathcal {L}} \circ F_{\mathcal {L}}}\). Importantly for us, \(\mathsf {Mod}(\mathcal {L},\mathsf {Set})\) is both complete and cocomplete, e.g., because \(T_\mathcal {L}\) has countable rank and \(\mathsf {Set}\) is complete and cocomplete, see [4, Theorem 4.3.6]. Therefore, \(\mathsf {Mod}(\mathcal {L},\mathsf {Set})\) has set-indexed products and set-indexed coproducts and we get:

### **Corollary 2**

For any countable Lawvere theory \(\mathcal {L}\), the adjunction \({F_{\mathcal {L}} \dashv U_{\mathcal {L}}}\) and the families fibration \({p : \mathsf {Fam}(\mathsf {Set}) \longrightarrow \mathsf {Set}}\) determine a fibred adjunction model.

Finally, we present two computationally motivated examples arising from Theorem 3 and decompositions of monads \((T, \eta , \mu )\) on \(\mathsf {Set}\) into adjunctions other than \({F^T \dashv U^T}\). In particular, we consider the continuations monad \(R^{R^{(-)}}\) and the global state monad \(((-) \times S)^S\). These monads can be decomposed into the adjunctions \({R^{(-)} \dashv R^{(-)} : \mathsf {Set}^{\text {op}} \longrightarrow \mathsf {Set}}\) and \({(-) \times S \dashv (-)^S : \mathsf {Set}\longrightarrow \mathsf {Set}}\), where \(\mathsf {Set}^{\text {op}}\) inherits set-indexed products and set-indexed coproducts trivially from \(\mathsf {Set}\).

### **Corollary 3**

The adjunctions \({R^{(-)} \dashv R^{(-)}}\) and \({(-) \times S \dashv (-)^S}\) together with the families fibration \({p : \mathsf {Fam}(\mathsf {Set}) \longrightarrow \mathsf {Set}}\) determine fibred adjunction models.

## 4 Extending the Language with Algebraic Effects

Until now we have have not said how computational effects, such as I/O, state, exceptions, etc., arise in our language and how programmers can program with them. In this section, we make the source of computational effects explicit, by drawing ideas from the algebraic treatment of computational effects [31].

### 4.1 Algebraic Effects in the Syntax

*collection of typed operation symbols*

*input type*and \(x_{\mathsf {in}} \!:\! I\,\vdash \, O\) the

*output type*of \(\mathsf {op}\). We restrict

*I*and

*O*to be

*pure value types*, i.e., value types that do not contain

*U*.

The operation symbols we consider can also come equipped with a *collection of equations*, describing their intended computational behaviour. We extend our language with the corresponding equations between computation terms.

*general algebraicity equation*:

### 4.2 Algebraic Effects in the Semantics

*fibred adjunction model supports algebraic operations*if for all \(\mathsf {op}: (x_{\mathsf {in}} \!:\! I) \longrightarrow O\), there exist vertical morphisms

*U*is a split fibred functor, it can be shown that the \(\llbracket \mathsf {op} \rrbracket _{\underline{C}}\)’s are preserved by reindexing. If the given collection of operation symbols also comes with associated equations, these vertical morphisms are additionally required to satisfy these equations.

Finally, we note how algebraic operations can be characterised in the fibred adjunction models based on the families fibration and EM-algebras of a monad.

### **Proposition 2**

## 5 Extending the Language with General Recursion

We now show how to extend our language with general recursion, considering it as a computational effect to keep the MLTT fragment of our language effect-free.

### 5.1 Recursion in the Syntax

*fixed point operation*\(\mu x \!:\! U\underline{C}.M\). The corresponding typing rule is given by

*discrete value types*, to be able to interpret this extended language in models based on continuous families of cpos. These discrete types are

### 5.2 Domain-Theoretic Semantics for Recursion

We build the denotational semantics for the language with recursion around the *SCCompC of continuous families*\({p : \mathsf {CFam}(\mathcal {CPO}) \longrightarrow \mathcal {CPO}}\) [18, Sect. 10.6]. Compared to [18], we use \(\omega \)-complete partial orders instead of directed-complete partial orders, because the former constitute a locally countably presentable category, whereas the latter do not [1, Example 1.14(4)]; and we need local presentability for fibred adjunction models based on the algebraic treatment of computational effects. An overview of the relevant domain theory can be found in [11, 29].

*X*,

*A*) of a cpo

*X*and a continuous functor \({A : X \longrightarrow \mathcal {CPO}^{\text {EP}}}\) (a

*continuous family*), treating

*X*as a category and valued in the category of embedding-projection pairs. The morphisms \({(X,A) \longrightarrow (Y,B)}\) are pairs \((f , \{g_x\}_{x \in \vert X \vert })\) of a continuous function \({f : X \longrightarrow Y}\) and a family of continuous functions \({\{g_x : A(x) \longrightarrow B(f(x))\}_{x \in \vert X \vert }}\), satisfying

*A*to be a continuous family of discrete cpos, matching the changes we made in the syntax of our language, and then define

*A*is necessary for \(\langle x , a , a' \rangle \mapsto \coprod _{\{ \star \,\vert \,a = a'\}} 1\) to constitute a continuous functor: if

*A*would not be discrete, then from \(\langle x_1 , a_1 , a_1' \rangle \sqsubseteq \langle x_2 , a_2 , a_2' \rangle \) and \(a_1 = a_1'\) it would not follow that \(a_2 = a_2'\), and vice versa, which we need for defining the embedding-projection pair between \(\coprod _{\{ \star \,\vert \,a_1 = a_1'\}} 1\) and \(\coprod _{\{ \star \,\vert \,a_2 = a_2'\}} 1\).

For modeling computation terms involving recursion, we assume a \(\mathcal {CPO}\)-enriched monad \((T, \eta ,\mu )\) on \(\mathcal {CPO}\), such that its EM-algebras are pointed and the morphisms between them are strict; or equivalently, we assume that the given monad supports a least zero-ary algebraic operation, in the sense of [30, Sect. 6]. For modeling computational \(\varSigma \)-types, we further assume that \(\mathcal {CPO}^T\) has reflexive coequalizers. We can then model our computation types in the split fibration \({q : \mathsf {CFam}(\mathcal {CPO}^T) \longrightarrow \mathcal {CPO}}\), defined analogously to *p* above. Monads satisfying these conditions arise naturally from the algebraic treatment of computational effects: from \(\mathcal {CPO}\)-enriched countable Lawvere theories [17] with a least constant.

The dependent products and sums in *q*, with respect to *p*, are defined using the cpo-indexed products and coproducts in \(\mathcal {CPO}^T\). First, the cpo-indexed product \(\prod _{X} \underline{C}\) in \(\mathcal {CPO}^T\) is directly inherited from \(\mathcal {CPO}\), being defined on the carrier \(\prod _{X} (U^T \circ \underline{C})\). On the other hand, analogously to Sect. 3.3, the cpo-indexed coproduct \(\coprod _{X} \underline{C}\) cannot be defined simply by taking \(\coprod _{X} (U^T \circ \underline{C})\) as the carrier. Instead, we construct \(\coprod _{X} \underline{C}\) as the reflexive coequalizer for a diagram similar to the one used in Sect. 3.3, with the difference that here we would use the free algebras over cpo-indexed coproducts rather than over set-indexed coproducts.

Despite having a more complex categorical definition, the cpo-indexed coproducts in \(\mathcal {CPO}^T\) have the same universal property as those in \(\mathcal {CPO}\). We first recall Jacobs’s remark [18, Sect. 10.6] that \(\coprod _{X} A\) results from applying the Grothendieck construction to *A*. By a result of Gray [12], \(\coprod _{X} A\) can also be understood as the oplax colimit of *A* in \(\mathcal {CPO}\). In \(\mathcal {CPO}^T\), the situation is analogous:

### **Proposition 3**

\(\coprod _X \underline{C}\) is the oplax colimit of \({\underline{C} : X \longrightarrow (\mathcal {CPO}^T)^{\text {EP}}}\) in \(\mathcal {CPO}^T\).

Similarly to Sect. 3.3, the split fibred adjunction \(F \dashv U : q \longrightarrow p\) is defined from \(F^T \dashv U^T\) by post-composition, i.e., by setting \(F(X,A) =(X, F^T \circ A)\), where \({F^T \circ \, A}\) is a continuous functor because of the \(\mathcal {CPO}\)-enrichment of \(F^T\) and the limit-colimit coincidences in \(\mathcal {CPO}^{\text {EP}}\) and \((\mathcal {CPO}^T)^{\text {EP}}\). *U* is defined analogously.

### **Theorem 4**

Given a monad \((T, \eta , \mu )\) on \(\mathcal {CPO}\) satisfying the conditions given in this section, the fibred adjunction model built from \({p : \mathsf {CFam}(\mathcal {CPO}) \longrightarrow \mathcal {CPO}}\) and \({F^T \dashv U^T}\) is a model of the equational theory extended with fixed point unfolding.

Finally, we note that the other obvious candidate \({\mathsf {cod} : \mathcal {CPO}^\rightarrow \longrightarrow \mathcal {CPO}}\), even if made split [8, 14], is not a SCCompC, because of [18, Theorem 10.5.5] and:

### **Proposition 4**

\(\mathcal {CPO}\) is not locally Cartesian closed.

In particular, the condition that every base change functor has to have a right adjoint fails because some of these functors do not preserve all colimits, e.g., given a non-empty cpo *X*, the pullback of the epimorphism \({n \mapsto n : \mathbb {N}_= \longrightarrow \mathbb {N}_\omega }\) in \(\mathcal {CPO}/\mathbb {N}_\omega \) along the constant map \({x \mapsto \omega : X \longrightarrow \mathbb {N}_\omega }\) is not an epimorphism.

## 6 Conclusions and Future Work

We addressed the problem of finding a mathematically natural combination of dependent types and computational effects. We were motivated by: (i) the success similar foundations have had in driving the study of computational effects in the simply-typed setting; and (ii) the success of dependently-typed programming in generating a number of concrete attempts to combine dependent types with computational effects. Our solution is mathematically natural, combining comprehension categories, arising from the semantics of dependent types, with adjunctions, arising from the semantics of computational effects. It is also general, covering a variety of algebraic and non-algebraic effects, and can be extended to accommodate general recursion. For future work, a natural next step is to investigate operational semantics, leading towards an implementation.

We are also working on a fibred generalisation of Atkey’s parametrised notions of computation [2], aiming at a semantic account of the effects in Idris [5, 6].

## References

- 1.Adamek, J., Rosicky, J.: Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge (1994)CrossRefzbMATHGoogle Scholar
- 2.Atkey, R.: Algebras for parameterised monads. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 3–17. Springer, Heidelberg (2009)CrossRefGoogle Scholar
- 3.Benton, P.N.: A mixed linear and non-linear logic: proofs, terms and models. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933. Springer, Heidelberg (1995)CrossRefGoogle Scholar
- 4.Borceux, F.: Handbook of Categorical Algebra. Categories and Structures, vol. 2. Cambridge University Press, Cambridge (1994)CrossRefzbMATHGoogle Scholar
- 5.Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: Morrisett, G., Uustalu, T. (eds.) Proceedings of 18th International Conference on Functional Programming, ICFP 2013, pp. 133–144. ACM (2013)Google Scholar
- 6.Brady, E.: Resource-dependent algebraic effects. In: Hage, J., McCarthy, J. (eds.) TFP 2014. LNCS, vol. 8843, pp. 18–33. Springer, Heidelberg (2015)Google Scholar
- 7.Casinghino, C., Sjöbergberg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: Sewell, P. (ed.) Proceedings of 41st Annual Symposium on Principles of Programming Languages, POPL 2014, pp. 33–45. ACM (2014)Google Scholar
- 8.Clairambault, P., Dybjer, P.: The biequivalence of locally cartesian closed categories and martin-löf type theories. In: Ong, L. (ed.) Typed Lambda Calculi and Applications. LNCS, vol. 6690, pp. 91–106. Springer, Heidelberg (2011)CrossRefGoogle Scholar
- 9.Egger, J., Møgelberg, R.E., Simpson, A.: The enriched effect calculus: syntax and semantics. J. Log. Comput.
**24**(3), 615–654 (2014)MathSciNetCrossRefzbMATHGoogle Scholar - 10.Ghani, N., Johann, P., Fumex, C.: Indexed induction and coinduction, fibrationally. Logical Methods Comput. Sci.
**9**(3:6), 1–31 (2013). doi: 10.2168/LMCS-9(3:6)2013 MathSciNetzbMATHGoogle Scholar - 11.Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices and Domains. Cambridge University Press, Cambridge (2003)CrossRefzbMATHGoogle Scholar
- 12.Gray, J.W.: The categorical comprehension scheme. In: Gray, J.W. (ed.) Category Theory, Homology Theory and Their Applications III. Lecture Notes in Mathematics, vol. 99, pp. 242–312. Springer, Heidelberg (1969)CrossRefGoogle Scholar
- 13.Hancock, P., Setzer, A.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 317–331. Springer, Heidelberg (2000)Google Scholar
- 14.Hofmann, M.: On the interpretation of type theory in locally cartesian closed. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427–441. Springer, Heidelberg (1995)CrossRefGoogle Scholar
- 15.Hofmann, M.: Syntax and semantics of dependent types. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, pp. 79–130. Cambridge University Press, Cambridge (1997)CrossRefGoogle Scholar
- 16.Hutton, G., Meijer, E.: Monadic parsing in Haskell. J. Funct. Program.
**8**(4), 437–444 (1998)CrossRefzbMATHGoogle Scholar - 17.Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci.
**357**(1–3), 70–99 (2006)MathSciNetCrossRefzbMATHGoogle Scholar - 18.Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999)zbMATHGoogle Scholar
- 19.Krishnaswami, N.R., Pradic, P., Benton, N.: Integrating linear and dependent types. In: Walker, D. (ed.) Proceedings of 42nd Annual Symposium on Principles of Programming Languages, POPL 2015, pp. 17–30. ACM (2015)Google Scholar
- 20.Levy, P.B.: Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Springer, Heidelberg (2004)zbMATHGoogle Scholar
- 21.Linton, F.: Coequalizers in categories of algebras. In: Eckmann, B. (ed.) Seminar on Triples and Categorical Homology Theory. Lecture Notes in Mathematics, vol. 80, pp. 75–90. Springer, Heidelberg (1969)CrossRefGoogle Scholar
- 22.Martin-Löf, P.: An intuitionisitc theory of types, predicative part. In: Rose, E., Shepherdson, J.C. (eds.) Proceedings of Logic Colloquium 1973, pp. 73–118. North-Holland (1975)Google Scholar
- 23.McBride, C.: Functional pearl: Kleisli arrows of outrageous fortune. J. Funct. Program. (To appear)Google Scholar
- 24.Moggi, E.: Computational lambda-calculus and monads. In: Parikh, R. (ed.) Proceedings of 4th Annual Symposium on Logic in Computer Science, LICS 1989, pp. 14–23. IEEE (1989)Google Scholar
- 25.Moggi, E.: Notions of computation and monads. Inf. Comput.
**93**(1), 55–92 (1991)MathSciNetCrossRefzbMATHGoogle Scholar - 26.Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program.
**18**(5–6), 865–911 (2008)MathSciNetCrossRefzbMATHGoogle Scholar - 27.Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. Algebraic and Logical Structures, vol. 5, pp. 39–128. Oxford University Press, Oxford (2000). chap. 2Google Scholar
- 28.Pitts, A.M., Matthiesen, J., Derikx, J.: A dependent type theory with abstractable names. In: Mackie, I., Ayala-Rincon, M. (eds.) Proceedings of 9th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2014. ENTCS, vol. 312, pp. 19–50. Elsevier (2015)Google Scholar
- 29.Plotkin, G.: Pisa notes (on domain theory) (1983)Google Scholar
- 30.Plotkin, G., Power, J.: Semantics for algebraic operations. In: Brookes, S., Mislove, M. (eds.) Proceedings of 17th Conference on the Mathematical Foundations of Programming Semantics, MFPS XVII. ENTCS, vol. 45, pp. 332–345. Elsevier (2001)Google Scholar
- 31.Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)CrossRefGoogle Scholar
- 32.Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Logical Methods Comput. Sci.
**9**(4:23), 1–36 (2013). doi: 10.2168/LMCS-9(4:23)2013 MathSciNetzbMATHGoogle Scholar - 33.Power, J.: Countable Lawvere theories and computational effects. In: Seda, A.K., Hurley, T., Schellekens, M., an Airchinnigh, M.M., Strong, G.(eds.) Proceedings of 3rd Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2004. ENTCS, vol. 161, pp. 59–71. Elsevier (2006)Google Scholar
- 34.Pretnar, M.: The Logic and Handling of Algebraic Effects. Ph.D. thesis, School of Informatics, University of Edinburgh (2010)Google Scholar
- 35.Staton, S.: Instances of computational effects: an algebraic perspective. In: Kupferman, O. (ed.) Proceedings of 28th Annual Symposium on Logic in Computer Science, LICS 2013, pp. 519–519. IEEE, June 2013Google Scholar
- 36.Streicher, T.: Semantics of Type Theory. Birkhäuser, Boston (1991)CrossRefzbMATHGoogle Scholar
- 37.Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: Flanagan, C. (ed.) Proceedings of 34th Conference on Programming Language Design and Implementation, PLDI 2013, pp. 387–398. ACM (2013)Google Scholar
- 38.Vákár, M.: A categorical semantics for linear logical frameworks. In: Pitts, A. (ed.) FOSSACS 2015. LNCS, vol. 9034, pp. 102–116. Springer, Heidelberg (2015)CrossRefGoogle Scholar
- 39.Warren, M.A.: Homotopy Theoretic Aspects of Constructive Type Theory. Ph.D. thesis, Department of Philosophy, Carnegie Mellon University (2008)Google Scholar