key: cord-0060369-ri2xwb6o authors: Kura, Satoshi title: A General Semantic Construction of Dependent Refinement Type Systems, Categorically date: 2021-03-23 journal: Foundations of Software Science and Computation Structures DOI: 10.1007/978-3-030-71995-1_21 sha: be728c092183e17537e8e32d3464147163bba9ab doc_id: 60369 cord_uid: ri2xwb6o Dependent refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness. Dependent refinement types [6] are types equipped with predicates that restrict values in the types. They are used to specify preconditions and postconditions which may depend on input values and to verify that programs satisfy the specifications. Many dependent refinement types systems are proposed [5, 6, 13, 14, 25] and implemented in, e.g., F [23, 24] and LiquidHaskell [19, 26, 27] . In this paper, we address the question: "How are dependent refinement type systems, underlying type systems, and predicate logic related from the viewpoint of categorical semantics?" Although most existing dependent refinement type systems are proved to be sound using operational semantics, we believe that categorical semantics is more suitable for the general understanding of their nature, especially when we consider general computational effects and various kinds of predicate logic (e.g., for relational verification). This understanding will provide guidelines to design new dependent refinement type systems. Our answer to the question is a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic. More concretely, given a closed comprehension category (CCompC for short) for interpreting an underlying type system and a fibration for predicate logic, we combine them to obtain another CCompC that can interpret a dependent refinement type system built from the underlying type system and the predicate logic. For example, consider giving an interpretation to the term "x : {int | x ≥ 0} x + 1 : {v : int | v = x + 1}" in a dependent refinement type system. Its underlying term is "x : int x + 1 : int," and we assume that it is interpreted as the successor function of Z in Set. The problem here is how to refine this interpretation with predicates. In dependent refinement types, predicates may depend on the variables in contexts. In this example, the type "x : {int | x ≥ 0} {v : int | v = x + 1}" depends on the variable x. Thus, the interpretation of such types must be a predicate on the context and the type, i.e., As a result, the term in the dependent refinement type system is interpreted as the interpretation in the underlying type system together with the property that if the input satisfies preconditions, then the output satisfies postconditions. (1) We formalize this refinement process as a construction of liftings of CCompCs, which are used to interpret dependent type theories. Assume that we have a pair of a CCompC p : E → B for interpreting underlying type systems and a fibration q : P → B for predicate logic satisfying certain conditions. Then we construct a CCompC {E | P} → P for interpreting dependent refinement type systems. This construction also yields a morphism of CCompCs from {E | P} → P to p : E → B in Fig. 1 . Given the simple fibration s(Set) → Set for underlying type systems and the subobject fibration Sub(Set) → Set for predicate logic, then we get interpretations like (1) . We extend the construction of liftings of CCompCs to liftings of fibred monads [1] on CCompCs, which is motivated by the fact that many dependent refinement type systems have computational effects, e.g., exception (like division and assertion), divergence, nondeterminism [25] , and probability [5] . Assume that we have a fibred monadT on p : E → B, a monad T on B, and a liftingṪ of T along q : P → B. Under a certain condition that roughly claims thatT and T represent the same computational effects, we construct a fibred monad on {E | P} → P, which is a lifting ofT in the same spirit of the given liftingṪ . This situation is rather realistic because the fibred monadT on the CCompC p : E → B is often induced from the monad T on the base category B. The liftingṪ of the monad T along p : P → B specifies how to map predicates P ∈ P X on values X ∈ B to predicatesṪ P ∈ P T X on computations T X, which enables us to express, for example, total/partial correctness and may/must nondeterminism [1] . We explain the usage of these categorical constructions by giving semantics to a dependent refinement type system with computational effects, which is based on [4] . Our system also supports subtyping relations induced by logical implication. We prove soundness of the dependent refinement type system. Finally, we discuss how to handle recursion in dependent refinement type systems. In [4] , Ahman gives semantics to recursion in a specific model, i.e., the fibration of continuous families of ω-cpos CFam(CPO) → CPO. We consider more general characterization of recursion by adapting Conway operators for CCompCs, which enables us to lift the structure for recursion. We show that a rule for partial correctness in our dependent refinement type system is sound under the existence of a generalized Conway operator. Our contributions are summarized as follows. -We provide a general construction of liftings of CCompCs from given CCom-pCs and posetal fibrations satisfying certain conditions, as a semantic counterpart of construction of dependent refinement type systems from underlying type systems and predicate logic. We extend this to liftings of fibred monads on the underlying CCompCs to model computational effects. -We consider a type system (based on EMLTT [2] [3] [4] ) that includes most of basic features of dependent refinement type systems and prove its soundness in the liftings of CCompCs obtained from the above construction. -We define Conway operators for dependent type systems. This generalizes the treatment of general recursion in [4] . We prove soundness of the typing rule for partial correctness of recursion under the existence of a lifting of Conway operators. We review basic definitions and fix notations for comprehension categories, which are used as categorical models for dependent type theories. We assume basic knowledge of fibrations (see e.g. [10] ). Let p : E → B be a fibration (opfibration). We denote the cartesian (cocartesian) lifting over u : is the reindexing (coreindexing) functor. We call p : E → B a posetal fibration if p is a fibration such that each fibre category is a poset. Note that the fibration p : E → B is split and faithful if p is posetal. A comprehension category is a functor P : E → B → such that the composite cod • P : E → B is a fibration and P maps cartesian morphisms to pullbacks in B. A comprehension category P is full if P is fully faithful. A comprehension category with unit is a fibration p : E → B that has a fibred terminal object 1 : B → E and a comprehension functor {−} : E → B which is a right adjoint of the fibred terminal object functor 1 {−}. Projection π X : {X} → pX is defined by π X = p 1 {−} X for each X ∈ E. Intuitively, E represents a collection of types Γ A in dependent type theories; B represents a collection of contexts Γ ; p : E → B is the mapping (Γ A) → Γ ; 1 : B → E is the unit type Γ → (Γ 1); and {−} is the mapping (Γ A) → Γ, x : A where x is a fresh variable. The comprehension category with unit p : E → B induces several structures. It induces a comprehension category P defined by PX = π X . The adjunction 1 {−} defines the bijection s : E I (1I, X) ∼ = {f : I → {X} | π X • f = id I } between vertical morphisms in E and sections in B. For each X, Y ∈ E I , we have an isomorphism φ : . Consider the pullback square P(π X (Y )) where X, Y ∈ E I . By the universal property of pullbacks, we have the Let p : E → B be a comprehension category with unit and q : D → B be a fibration. The fibration q has p-products if π * X : D pX → D {X} has a right adjoint π * X X for each X ∈ E and these adjunctions satisfy the BC (Beck-Chevalley) condition for each pullback square Pf where P is a comprehension category induced by p and f is a cartesian morphism in E. Similarly, we define p-coproducts by X π * X and p-equality by Eq X δ * X plus the BC condition for each cartesian morphism (see [10, Definition 9.3.5] for detail). A comprehension category with unit p : E → B admits products (coproducts) if it has p-products (p-coproducts). The coproducts are strong if the canonical morphism κ : is a full comprehension category with unit that admits products and strong coproducts and has a terminal object in the base category. A split closed comprehension category (SCCompC) is a CCompC such that p is a split fibration, and the BC condition for products and coproducts holds strictly (i.e., canonical isomorphisms are identities). For example, the simple fibration s B : s(B) → B on a cartesian closed category B is a SCCompC (see [ In this section, we give a construction of liftings of SCCompCs with strong fibred coproducts from given SCCompCs with strong fibred coproducts for underlying types and posetal fibrations for predicate logic satisfying appropriate conditions. Let p : E → B be a SCCompC for underlying type systems. Let q : P → B be a posetal fibration with fibred finite products for predicate logic. Definition 1. We define a category {E | P} by the pullback of q → : P → → B → along P : E → B → where the comprehension category P is induced by p : E → B. That is, objects are tuples (X, P, Q) where X ∈ E, P ∈ P pX , Q ∈ P {X} , and Q ≤ π * X P ; and morphisms are tuples (f, g, h) : (X, P, Q) → (X , P , Q ) where f : X → X , g : P → P , h : Q → Q , pf = qg, and {f } = qh. The intuition of this definition is as follows. For each object (X, P, Q) ∈ {E | P}, X represents a type Γ A in the underlying type system, P represents a predicate on the context Γ , and Q represents the conjunction of a predicate on Γ, v : A and the predicate P (thus Q ≤ π * X P is imposed). Note that Let {p | q} : {E | P} → P be a functor defined by cod • (q → ) * P, that is, (X, P, Q) → P . The functor {p | q} inherits most of the CCompC structure of p : E → B. Lemma 2. The functor {p | q} : {E | P} → P is a split fibration. The cartesian lifting of g : P → P is given by where π is a projection for fibred products. The rest of the proof is omitted. The existence of products in {p | q} requires additional conditions. Then, this gives products in {p | q} but we omit the lengthy proof. As a result, we get a lifting of SCCompCs over p : E → B. Theorem 5. If p : E → B is a SCCompC and q : P → B is a fibred ccc that has p-products, then {p | q} : {E | P} → P is a SCCompC. Moreover, (P * (q → ), q) : {p | q} → p is a morphism of SCCompCs, i.e., a split fibred functor that preserves the CCompC structure strictly. Proof. By Lemma 3 and Lemma 4. A terminal object in P exists because B has a terminal object and q : P → B has fibred terminal objects. It is almost obvious that (P * (q → ), q) preserves the structure of CCompCs. Example 7. Let erel : ERel → Set be the fibration of endorelations defined by change-of-base from Sub(Set) → Set along the functor X → X × X. The fibration erel is a fibred ccc and has products (i.e. right adjoints of reindexing functors that satisfy the BC condition for each pullback square). Therefore, erel has p-products for any comprehension category with unit p. If we apply Theorem 5 to erel and the simple fibration s Set : s(Set) → Set, then products are defined similarly to Example 6. where (I, X) ∈ Fam(Set), P ⊆ I, and Q ⊆ i∈P Xi ⊆ i∈I Xi. Note that subsets Q ⊆ i∈I Xi have a one-to-one correspondence with families of subsets (Qi ⊆ Xi) i∈I when we A sufficient condition for {p | q} : {E | P} → P to have strong fibred coproducts is given by the following lemma, which is analogous to [9, Prop. 4.5.8]. Lemma 9. If (1) p : E → B is a CCompC that has strong fibred coproducts (2) for each X, Y ∈ E I , X , Y ∈ E I , u : I → I , and pair of cartesian liftings f : X → X and g : Y → Y over u, the following two squares are pullbacks satisfy the BC condition for each pullback squares and Frobenius, then {p | q} : {E | P} → P has strong fibred coproducts, and the fibred functor (P * (q → ), q) : {p | q} → p strictly preserves fibred coproducts. Proof. We define fibred coproducts by (X, P, Q)+(Y, P, R) = (X +Y, P, We omit the rest of the proof. Note that if q is fibred bicartesian closed, then q is a fibred distributive category. ((I, X), P, Q) Suppose we have a SCCompC p : E → B and a posetal fibration q : P → B as ingredients for {p | q} : {E | P} → P in Theorem 5. We explain how to construct a fibred monad on {p | q} : {E | P} → P from monads on p and q. First, we assume that a monad T on B and a fibred monadT on p : E → B are given. These monads are intended to represent the same computational effects in underlying type systems, but T is more "primitive" thanT , andT is induced from T in some natural way. For example, we can use the maybe monad or the powerset monad on Set as T and defineT by (I, X) → (I, T X) on the simple fibration s(Set) → Set. In such a situation, we often have an oplax monad morphism (Definition 11) θ : {T (−)} → T {−}. Intuitively, θ extends the action ofT on types to contexts, just like strengths of strong monads. We also need a liftingṪ of T along q : P → B to specify a mapping from predicates on values in X ∈ B to predicates on computations in T X [1] . Given all these ingredients and some additional conditions, we define a fibred monad on {p | q} : {E | P} → P, which is a lifting of the fibred monadT on p : E → B. Definition 11 (oplax monad morphism). Let C, D be categories, F : C → D be a functor, and (S, η S , µ S ), (T, η T , µ T ) be monads on C and D, respectively. A natural transformation θ : F S → T F is an oplax monad morphism if θ respects units and multiplications. Let T be a monad on B,T be a fibred monad on p : E → B in the 2-category Fib B of fibrations over B, θ : {T (−)} → T {−} be an oplax monad morphism, andṪ be a fibred lifting [1] of T along q : P → B. If holds for each X ∈ E, P ∈ P pX and Q ∈ P {X} , then there exists a fibred monad S on {p | q} : {E | P} → P in Fib P such that the fibred functor {p | q} → p in Theorem 5 is a fibred monad morphism from S toT . Proof. We define S(X, P, Q) = (T X, P, π * T X P ∧ θ * Ṫ Q). Then the monad structure ofT lifts to S. The assumption (3) is required to prove that S is fibred. Let T be the maybe monad (−) + { * }. There are two fibred liftings of T : for each (P ⊆ I) ∈ Sub(Set). The liftingṪ 1 corresponds to partial correctness, andṪ 2 corresponds to total correctness. The fibred monads on {s Set | sub Set } defined in Theorem 12 fromṪ 1 andṪ 2 are given by respectively. Here, we leave the left/right injection of coproducts implicit. For each monad T on Set, we have a split fibred monad on the family fibration Fam(Set) → Set defined byT (I, X) = (I, T • X). We have an oplax monad morphism θ : i∈I T Xi → T i∈I Xi defined by the cotupling [(T ι i ) i∈I ] : i∈I T Xi → T i∈I Xi where ι i : Xi → i∈I Xi is the i-th injection. The condition (3) holds for any fibred lifting of T along the subobject fibration Sub(Set) → Set. Moreover, we have ι * i θ * Ṫ Q =Ṫ ι * i Q for each Q ∈ Sub(Set) i∈I Xi , so the monad in Theorem 12 is given by (I, X), P, (Qi ⊆ Xi) i∈I → (I, T • X), P, (Ṫ Qi ⊆ T Xi) i∈I . We consider a concrete dependent refinement type system with computational effects and define sound semantics to show that the SCCompC defined in Theorem 5 has sufficient structures for dependent refinement types. Here, we consider two type systems. One is an underlying type system that is a fragment of EMLTT [2] [3] [4] . The other is a refinement of the underlying type system that has refinement types {v : A | p} and a subtyping relation Γ A <: B induced by logical implication. The two type systems share a common syntax for terms while types are more expressive in the refinement type system. We consider liftings of fibred adjunction models to interpret the refinement type system. Here, Theorem 12 can be used to obtain a lifting of fibred adjunction models via Eilenberg-Moore construction. We prove a soundness theorem that claims if a term is well-typed in the refinement type system, then the interpretation of the term has a lifting along the morphism of CCompCs defined in Theorem 5. We define the underlying dependent type system by a slightly modified version of a fragment of EMLTT [2] [3] [4] . We remove some of the types and terms from the original for simplicity. We parameterize our type system with a set of base type constructors (ranged over by b) and a set of value constants (ranged over by c) for convenience. We implicitly assume that variables in Γ are mutually different. We use many type annotations in the syntax of terms for a technical reason, but we might omit them if they are clear from the context. We define substitution Fig. 2 . Some typing rules for the underlying type system. We use fibred adjunction models to interpret terms and types. We adapt the definition for our fragment of EMLTT as follows. Definition 15 (Fibred adjunction models) . A fibred adjunction model is a fibred adjunction F U : r → p where p : E → B is a SCCompC with strong fibred coproducts and r : C → B is a fibration with p-products. The Eilenberg-Moore fibration of a CCompC p : E → B inherits products in p [2, Theorem 4.3.24] and thus gives an example of fibred adjunction models. Lemma 16. Given a SCCompC p : E → B with strong fibred products and a split fibred monad T on p, then the Eilenberg-Moore adjunction of T is a fibred adjunction model. We assume that a fibred adjunction model F U : r → p between p : E → B and r : C → B is given and that interpretations of base type constructors b ∈ E and value constants c ∈ E 1 (1, X) (for some X ∈ E 1 ) are given. We define a partial interpretation − of the following form for raw syntax. Most of the definition of − are the same as [2] . For base type constructors b and value constants c, we define − as follows. Here, left-hand sides are defined if right-hand sides are defined. A → Type such that ; A is defined, and c ∈ E 1 (1, ; ty(c) ) holds if ; ty(c) ∈ E 1 is defined. Interpretations − of well-formed contexts and types and welltyped terms are defined. If two contexts, types, or terms are definitionally equal, then their interpretations are equal. We define syntax for logical formulas by where a ranges over predicate symbols. Here, we added and V = A W for typing rule for the unique value of the unit type and variables of base types (i.e. for selfification [18] ), respectively, which we describe later. However, there is a large amount of freedom to choose the syntax of logical formulas. The least requirement here is that logical formulas can be interpreted in a posetal fibration q : P → B, and interpretations of logical formulas admit semantic weakening, substitution, and conversion in the sense of [2, Proposition 5.2.4, 5.2.6]. So, we can almost freely add or remove logical connectives and quantifiers as long as q : P → B admits them. We define a standard judgement of well-formedness for logical formulas. Some of the rules for well-formedness are shown in Fig. 3 Logical formulas are interpreted in the fibration q : P → B. We assume that interpretation a ∈ P { ;A } for each predicate symbol a : A → Prop is given. The interpretation Γ p ∈ P Γ is standard and defined inductively for each well-formed formulas. For example: where a : A → Prop is a predicate symbol and s is the bijection defined in §2. We refine the underlying type system by adding predicates to base types and the unit type. From now on, we use subscript A u for types in the underlying type system to distinguish them from types in the refinement type system. We use the same definition of terms as the underlying type system and the same set of base type constructors and value constants. Argument types of base type constructors b : A u → Type are also the same, but types ty(c) assigned to value constants c are redefined as refinement types. Given a type A (or C) in the refinement type system, we define its underlying type |A| (or |C|) by induction where predicates are eliminated in the base cases. Underlying contexts |Γ | are also defined by | | = and |Γ, x : Fig. 4 . Some typing rules for the refinement type system. Judgements in the refinement type system are as follows. We have judgements for well-formedness or well-typedness for contexts, types and terms in the refinement type system, which are denoted in the same way as the underlying type system. We do not consider definitional equalities for terms because they are the same as the underlying type system. Instead, we add judgements for subtyping between types and contexts. They are denoted by Γ 1 <: Γ 2 for context, Γ A <: B for value types, and Γ C <: D for computation types. Most of term and type formation rules are similar to the underlying type system. We listed some of the non-trivial modifications of typing rules in Fig. 4 . We add typing rules for {v : b Bu (V ) | p} and {v : 1 | p}. Subtyping for these types are defined by judgements Γ ; v : A u | p q for logical implication. Here, Γ ; v : A u | p q means "assumptions in Γ and p implies q" where p and q are well-formed formulas in the context |Γ |, v : A u . We do not specify derivation rules for the judgement Γ ; v : A u | p q but assume soundness of the judgement (explained later). We allow "selfification" [18] for variables of base types. Subtyping for Σx:A.B, U C, F A, and Πx:A.C are defined covariantly except the argument type A of Πx:A.C, which is contravariant. We have the rule of subsumption. Value constants are typed with a refined type assignment ty(c). The unique value * of the unit type has type {v : 1 | }. Lemma 18. If we eliminate predicates in the refinement types from well-formed contexts, types and terms, then we get well-formed contexts, types and terms of the underlying type system. -If Γ , then |Γ |. If Γ A, then |Γ | |A|. If Γ C, then |Γ | |C|. -If Γ 1 <: Γ 2 , then |Γ 1 | = |Γ 2 |. If Γ A <: B, then |Γ | |A| = |B|. If Γ C <: D, then |Γ | |C| = |D|. Proof. By induction on the derivation of judgements. Each typing rule in the refinement type system has a corresponding rule in the underlying system. We can express conditional branching using the elimination rule of the fibred coproduct type 1 + 1. For example, assume we have a base type We can define if x ≤ y then M else N to be a syntax sugar for where (≤ ) = force (≤). Note that M and N are typed in contexts that have v : {v : 1 | x ≤ y} or v : {v : 1 | x > y} depending on the result of comparison. Definition 20 (lifting of fibred adjunction models). Suppose that we have two fibred adjunction models F U : q → p between p : E → B and q : C → B andḞ U : s → r between r : U → P and s : D → P. The fibred adjunction modelḞ U is a lifting of F U if there exists functors u : U → E, v : D → C, and t : P → B such that these functors strictly preserve all structures ofḞ U to those of F U . That is, (u, t) : r → p and (v, t) : s → q are split fibred functors, the pair of fibred functor (u, t) and (v, t) is a map of adjunctions in the 2-category Fib, (u, t) strictly preserves the CCompC structure and fibred coproducts, and (v, t) maps r-products to p-products in the strict sense. We assume that a lifting of fibred adjunction models is given as follows. Here, we assume more than just a lifting of fibred adjunction models by requiring the specific SCCompC {p | q} with strong fibred coproducts, and the split functor (u, q) : {p | q} → p defined in Theorem 5 and Lemma 9. The underlying fibred adjunction model F U is used for the underlying type system in §5.1, and q : P → B is for predicate logic in §5.2. One way to obtain such liftings of fibred adjunction models is to apply the Eilenberg-Moore construction to the monad morphism in Theorem 12, but in general we do not restrict C and D to be Eilenberg-Moore categories. We further assume that q has p-equalities to interpret logical formulas of the form V = A W . We define partial interpretation of refinement types Γ ∈ P, Γ ; A ∈ {E | P} Γ , and Γ ; C ∈ D Γ similarly to the underlying type system but with the following modification. Here, we make use of the definition of {E | P}. For each (X, P, Q), (X , P , Q ) ∈ {E | P}, we define a semantic subtyping relation (X, P, Q) <: (X , P , Q ) by the conjunction of X = X , P = P , and Q ≤ Q . In other words, we have (X, P, Q) <: (X , P , Q ) if and only if there exists a morphism (id X , id P , h) : (X, P, Q) → (X , P , Q ) that is mapped to identities by u : {E | P} → E and {p | q} : {E | P} → P. Lemma 21. -If Γ is defined, then |Γ | is defined and equal to q Γ . -If Γ ; A is defined, then |Γ |; |A| is defined and equal to u Γ ; A . -If Γ ; C is defined, then |Γ |; |C| is defined and equal to v Γ ; C . Proof. By simultaneous induction. The case of {v : A u | p} is obvious, and other cases follow from the definition of liftings of fibred adjunction models. We do not specify syntactic derivation rules for judgement for logical implication Γ ; v : A u | p q. Instead, we assume soundness of Γ ; v : A u | p q in the following sense: π * |Γ |;Au Γ ∧ |Γ |, v : A u p ≤ |Γ |, v : A u q holds in P |Γ |,v:Au . For example, we can define a derivation rule for logical implication Γ ; v : A u | p q from derivation rules for predicate logic Γ u | p q ("p implies q in the context Γ u "). This is done by collecting predicates in context Γ by and defining a derivation rule for judgement for logical implication Γ ; v : If the derivation rules for predicate logic Γ u | p q is sound (i.e., Γ u | p q implies Γ u p ≤ Γ u q ), then so are the derivation rule for Γ ; v : A u | p q. This technique is used in, e.g., [27] . Theorem 22 (Soundness). Assume that Γ ; v : A u | p q is sound in the sense described above, b ∈ E { ;A } holds for each b : A → Type if ; A is defined, and c ∈ {E | P} 1 (1, ; ty(c) ) holds if ; ty(c) ∈ {E | P} 1 is defined. Then we have the following. -If Γ , then Γ ∈ P is defined. If Γ A, then Γ ; A ∈ {E | P} Γ is defined. If Γ C, then Γ ; C ∈ D Γ is defined. -If Γ 1 <: Γ 2 , then Γ 1 ≤ Γ 2 in a fibre category of P. Since we have the bijection s : {E | P} P (1P, (X, P, Q)) → {f : P → Q | π (X,P,Q) • f = id P } for each (X, P, Q) ∈ {E | P}, we obtain liftings of interpretations of terms along q : P → B. We consider how to deal with general recursion in dependent refinement type systems. In [4] , Ahman used a specific model of the fibration CFam(CPO) → CPO of continuous families of ω-cpos to extend EMLTT with recursion. However, we need to identify the structure that characterizes recursion to lift recursion from the underlying type system to dependent refinement type systems. So, we consider a generalization of Conway operators [22] and prove the soundness of the underlying and the dependent refinement type system extended with typing rules for recursion. This extension enables us to reason about partial correctness of general recursion. Unfortunately, we still do not know an example of liftings of Conway operators, although (1) CFam(CPO) → CPO does have a Conway operator and (2) the soundness of the refinement type system with recursion holds under the existence of a lifting of Conway operators. We leave this problem for future work. The notion of Conway operators for cartesian categories is defined in [22] . We adapt the definition for comprehension categories with unit. We allow partially defined Conway operators because we need those defined only on interpretations of computation types. Definition 25 (Conway operator for comprehension categories with unit). Let p : E → B be a comprehension category with unit and K ⊆ E be a collection of objects. A Conway operator for the comprehension category with unit p defined on K is a family of mappings (−) ‡ : E I (X, X) → E I (1I, X) for each X ∈ E I ∩ K such that the following conditions are satisfied. (Naturality) For each X ∈ K, f ∈ E I (X, X), and u : Syntax. We add recursion µx : U C.M to the syntax of computation terms. We also add typing rules in Fig. 5 . Semantics. Assume we have a fibred adjunction model F U : r → p where p : E → B and r : C → B. We need a Conway operator defined on objects in { Γ ; U C | Γ C} ⊆ E. However, here is a circular definition because Γ ; U C may contain terms of the form µx : U D.M , whose interpretations are defined by the Conway operator. So, we use a slightly stronger condition. A Conway operator defined on computation types is a Conway operator defined on K ⊆ E such that K satisfies the following conditions. (1) Given a Conway operator defined on computation types, we interpret µx : Proposition 29. Soundness (Proposition 17) holds for the underlying type system extended with general recursion. Proof. By induction. We can prove that the given Conway operator is defined on { Γ ; U C | Γ C} ⊆ E by [2, Proposition 4.1.14]. Syntax. We add the typing rule for Γ µx:U C.M : C in Fig. 5 to the refinement type system. Here, recall that we remove definitional equalities when we consider the refinement type system. We consider liftings of Conway operators to interpret recursion in the refinement type system. Lemma 31. Let (u, v) be a morphism of CCompCs defined in Theorem 5. Assume p : E → B has a Conway operator (−) ‡ defined on K ⊆ E. The CCompC {E | P} → P has a lifting of the Conway operator defined on L ⊆ {E | P} if uL ⊆ K and for each (X, P, Q) ∈ L and f ∈ {E | P} P ((X, P, Q), (X, P, Q)), {f ‡ } has a lifting π * 1pX P → Q along q : P → B. Proof. Let (f, id P , h) : (X, P, Q) → (X, P, Q) be a morphism in {E | P} where (X, P, Q) ∈ L. We define a Conway operator by (f, id P , h) = (f ‡ , id P , h ) : (1pX, P, π * 1pX P ) → (X, P, Q) where h is a lifting of {f ‡ }. We assume that a lifting of fibred adjunction models (4) together with a lifting of Conway operators defined on computation types is given. Theorem 32. Soundness (Theorem 22) holds for the refinement type system extended with general recursion. Consider the fibration CFam(CPO) → CPO for the underlying type system with recursion. To support recursion in our refinement type system, a natural choice of a fibration for predicate logic is the fibration of admissible subsets Adm(CPO) → CPO because the least fixed point of an ω-continuous function f : X → X is given by lfpf = n f n (⊥). However, we cannot apply Theorem 5 because Adm(CPO) → CPO is not a fibred ccc [9, §4.3.2] . Specifically, it is not clear whether this combination admits products. We believe that our approach is quite natural but leave giving concrete examples of liftings of Conway operators for future work. Dependent refinement types. Historically, there are two kinds of refinement types. One is datasort refinement types [7] , which are subsets of underlying types but not necessarily dependent. The other is index refinement types [28] . A typical example of index refinement types is a type of lists indexed by natural numbers that represent the length of lists. Nowadays, the word "refinement types" includes datasort and index refinement types, and moreover, mixtures of them. Among a wide variety of the meaning of refinement types, we focus on types equipped with predicates that may depend on other terms [6, 20] , which we call dependent refinement types or just refinement types. Dependent refinement types are widely studied [5, 13, 14, 25] , and implemented in, e.g., F [23, 24] and LiquidHaskell [19, 26, 27] . However, most studies focus on decidable type systems, and only a few consider categorical semantics. We expect that some of the existing refinement type systems are combined with effect systems. For example, a dependent refinement type system for nondeterminism and partial/total correctness proposed in [25] contains types for computations indexed by quantifiers Q 1 Q 2 where Q 1 , Q 2 ∈ {∀, ∃}. Here, Q 1 represents may/must nondeterminism, and Q 2 represents total/partial correctness. It has been shown that Q 1 Q 2 corresponds to four cartesian liftings of the monad P + ((−) + 1) [1, 12] . We conjecture that these liftings are connected by monad morphisms and hence yield a lattice-graded monad. Another example is a relational refinement type system for differential privacy [5] . Their system seems to use a graded lifting of the distribution monad where the lifting is graded by privacy parameters, as pointed out in [21] . We leave for future work combining our refinement type system with effect systems based on graded monads [8, 11, 15] . Categorical semantics. Our interpretation of refinement type systems is based on a morphism of CCompCs, which is a similar strategy to [16] . The difference is that our paper focuses on dependent refinement types and makes the role of predicate logic explicit by giving a semantic construction of refinement type systems from given underlying type systems and predicate logic. Combining dependent types and computational effects is discussed in [2] [3] [4] . Although their aim is not at refinement types, their system is a basis for the design and semantics of our refinement type system with computational effects. Semantics for types of the form {v : A u | p} are characterized categorically as right adjoints of terminal object functors in [10, Chapter 11] . Such types are called subset types there. They consider the situation where a given CCompC p : E → B is already rich enough to interpret {v : A u | p}, and do not aim to interpret refinement type systems by liftings of CCompCs. Moreover, we cannot directly use the interpretations in [10] for our CCompC {E | P} → P because we are not given a fibration for predicate logic whose base category is P. We provided a general construction of liftings of CCompCs from combinations of CCompCs and posetal fibrations satisfying certain conditions. This can be seen as a semantic counterpart of constructing dependent refinement type systems from underlying type systems and predicate logic. We identified sufficient conditions for several structures in underlying type systems (e.g. products, coproducts, fibred coproducts, fibred monads, and Conway operators) to lift to dependent refinement type systems. We proved the soundness of a dependent refinement type system with computational effects with respect to interpretations in CCompCs obtained from the general construction. We aim to extend our dependent refinement type system by combining effect systems based on graded monads [8, 11, 15] . We hope that this extension will give us a more expressive framework that subsumes, for example, dependent refinement type systems in [5, 25] . Another direction is to define interpretations of {v : A u | p} in the style of subset types in [10, Chapter 11] . Lastly, we are interested in finding more examples of possible combinations of underlying type systems and predicate logic (especially for recursion in dependent refinement type systems but not limited to this) so that we can find a new practical application of this paper. Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. Weakest preconditions in fibrations Fibred Computational Effects Handling fibred algebraic effects Dependent types and fibred computational effects Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy Hybrid type checking Refinement types for ML Towards a Formal Theory of Graded Monads Fibrations, logical predicates and indeterminates Categorical Logic and Type Theory Parametric effect monads and semantics of effect systems Compositional reasoning and decidable checking for dependent contract types Gradual refinement types Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order Functors are Type Refinement Systems Notions of computation and monads Dynamic Typing with Dependent Types Liquid types Subtypes for specifications: Predicate subtyping in PVS Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy Complete axioms for categorical fixed-point operators Secure distributed programming with value-dependent types Verifying higher-order programs with the dijkstra monad Relatively complete refinement type system for verification of higher-order non-deterministic programs Abstract Refinement Types Refinement types for Haskell Eliminating array bound checking through dependent types Acknowledgement. We thank Shin-ya Katsumata, Hiroshi Unno and the anonymous referees for helpful comments. This work was supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603).