We describe semantic structures relevant for interpreting dependent types for statistical and probabilistic modelling. Our development extends the theory of quasi-Borel spaces (qbses) of Staton et. al, which support simply-typed, higher-order probability theory with continuous distributions. It is well-known that qbses can interpret a dependent-type theory supporting dependent function-spaces through the codomain fibration. We define an equivalent split fibration based on the family fibration, which we call quasi-Borel families (qbfs), characterise its structure, equip it with fibred monads of measures and probability, and use them to develop dependently-typed probability theory. We characterise the structure of the qbf fibration that is relevant for dependently-typed probability theory in elementary form. Our characterisations include: context extension, dependent pairs, dependent functions, extensional identity types, fibred products and coproducts, subspaces, a universe of propositions, and straightforward internalisation and externalisation principles for discrete spaces. We use these concepts to define fibred distribution and probability monads, the semantic structure needed to interpret probability distributions under a dependent context. We show that this structure satisfies a fibred version of Kock’s synthetic measure theory. We also use these concepts to develop a qbs counterpart to Kolmogorov’s conditional expectation. Our main result is a version of the conditional expectation that, under standard regularity assumptions, is measurable in both the random variables we are conditioning, and the observation map we are conditioning by.

Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes. We construct an affine calculus for $1$-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach's fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion, and induction over probability measures and natural numbers. We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.

The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.

Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about FPC ⊕ , a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics of FPC ⊕ , as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence.

The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.

Over the past decade, a number of languages for functional reactive programming (FRP) have been suggested, which use modal types to ensure properties like causality, productivity and lack of space leaks. So far, almost all of these languages have included a modal operator for delay on a global clock. For some applications, however, a global clock is unnatural and leads to leaky abstractions as well as inefficient implementations. While modal languages without a global clock have been proposed, no operational properties have been proved about them, yet. This paper proposes Async RaTT, a new modal language for asynchronous FRP, equipped with an operational semantics mapping complete programs to machines that take asynchronous input signals and produce output signals. The main novelty of Async RaTT is a new modality for asynchronous delay, allowing each output channel to be associated at runtime with the set of input channels it depends on, thus causing the machine to only compute new output when necessary. We prove a series of operational properties including causality, productivity and lack of space leaks. We also show that, although the set of input channels associated with an output channel can change during execution, upper bounds on these can be determined statically by the type system.

We present Clocked Cubical Type Theory, the first type theory combining multi-clocked guarded recursion with the features of Cubical Type Theory. Guarded recursion is an abstract form of step-indexing, which can be used for construction of advanced programming language models. In its multi-clocked version, it can also be used for coinductive programming and reasoning, encoding productivity in types. Combining this with Higher Inductive Types (HITs) the encoding extends to coinductive types that are traditionally hard to represent in type theory, such as the type of finitely branching labelled transition systems.

When designing languages for functional reactive programming (FRP) the main challenge is to provide the user with a simple, flexible interface for writing programs on a high level of abstraction while ensuring that all programs can be implemented efficiently in a low-level language. To meet this challenge, a new family of modal FRP languages has been proposed, in which variants of Nakano's guarded fixed point operator are used for writing recursive programs guaranteeing properties such as causality and productivity. As an apparent extension to this it has also been suggested to use Linear Temporal Logic (LTL) as a language for reactive programming through the Curry-Howard isomorphism, allowing properties such as termination, liveness and fairness to be encoded in types. However, these two ideas are in conflict with each other, since the fixed point operator introduces non-termination into the inductive types that are supposed to provide termination guarantees. In this paper we show that by regarding the modal time step operator of LTL a submodality of the one used for guarded recursion (rather than equating them), one can obtain a modal type system capable of expressing liveness properties while retaining the power of the guarded fixed point operator. We introduce the language Lively RaTT, a modal FRP language with a guarded fixed point operator and an `until' type constructor as in LTL, and show how to program with events and fair streams. Using a step-indexed Kripke logical relation we prove operational properties of Lively RaTT including productivity and causality as well as the termination and liveness properties expected of types from LTL. Finally, we prove that the type system of Lively RaTT guarantees the absence of implicit space leaks.

Abstract In recent years, we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory and spatial and cohesive type theory. In this paper, we study modal dependent type theory: dependent type theory with an operator satisfying (a dependent version of) the K axiom of modal logic. We investigate both semantics and syntax. For the semantics, we introduce categories with families with a dependent right adjoint (CwDRA) and show that the examples above can be presented as such. Indeed, we show that any category with finite limits and an adjunction of endofunctors give rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal λ-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

Abstract We present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model theclock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques. Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all programs are causal, and can be implemented without introducing space leaks and time leaks. To this end, some FRP languages do not give direct access to signals, but just to signal functions. Recently, modal types have been suggested as an alternative approach to ensuring causality in FRP languages in the synchronous case, giving direct access to the signal and event abstractions. This paper presents Simply RaTT , a new modal calculus for reactive programming. Unlike prior calculi, Simply RaTT uses a Fitch-style approach to modal types, which simplifies the type system and makes programs more concise. Echoing a previous result by Krishnaswami for a different language, we devise an operational semantics that safely executes Simply RaTT programs without space leaks. We also identify a source of time leaks present in other modal FRP languages: The unfolding of fixed points in delayed computations. The Fitch-style presentation allows an easy way to rules out these leaks, which appears not to be possible in the more traditional dual context approach.

In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity. Guarded recursion in the sense of Nakano has recently been suggested as a possible approach to dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This paper studies the notion of bisimilarity for guarded recursive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. We prove that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). As a worked example we study a guarded notion of labelled transition systems, and show that, as a special case of the general theorem, path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.

Guarded recursion in the sense of Nakano allows general recursive types and terms to be added to type theory without breaking consistency. Recent work has demonstrated applications of guarded recursion such as programming with codata, reasoning about coinductive types, as well as constructing and reasoning about denotational models of general recursive types. Guarded recursion can also be used as an abstract form of step-indexing for reasoning about programming languages with advanced features. Ultimately, we would like to have an implementation of a type theory with guarded recursion in which all these applications can be carried out and machine-checked. In this paper, we take a step towards this goal by devising a suitable reduction semantics. We present Clocked Type Theory, a new type theory for guarded recursion that is more suitable for reduction semantics than the existing ones. We prove confluence, strong normalisation and canonicity for its reduction semantics, constructing the theoretical basis for a future implementation. We show how coinductive types as exemplified by streams can be encoded, and derive that the type system ensures productivity of stream definitions.

We present guarded dependent type theory, $$\mathsf {gDTT}$$ , an extensional dependent type theory with a ‘later’ modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of $$\mathsf {gDTT}$$ are novel type and term formers involving what we call ‘delayed substitutions’. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model.

Guarded recursion is a form of recursion where recursive calls are guarded by delay modalities. Previous work has shown how guarded recursion is useful for reasoning operationally about programming languages with advanced features including general references, recursive types, countable non-determinism and concurrency.

This article introduces the enriched effect calculus, which extends established type theories for computational effects with primitives from linear logic. The new calculus provides a formalism for expressing linear aspects of computational effects; e.g. the linear usage of imperative features such as state and/or continuations. The enriched effect calculus is implemented as an extension of a basic effect calculus without linear primitives, which is closely related to Moggi's computational metalanguage, Filinski's effect PCF and Levy's call-by-push-value. We present syntactic results showing: the fidelity of the behaviour of the linear connectives of the enriched effect calculus; the conservativity of the enriched effect calculus over its non-linear core (the effect calculus); and the non-conservativity of intuitionistic linear logic when considered as an extension of the enriched effect calculus. The second half of the article investigates models for the enriched effect calculus, based on enriched category theory. We give several examples of such models, relating them to models of standard effect calculi (such as those based on monads), and to models of intuitionistic linear logic. We also prove soundness and completeness.

Guarded recursive functions and types are useful for giving semantics to advanced programming languages and for higher-order programming with infinite data types, such as streams, e.g., for modeling reactive systems. We propose an extension of intensional type theory with rules for forming fixed points of guarded recursive functions. Guarded recursive types can be formed simply by taking fixed points of guarded recursive functions on the universe of types. Moreover, we present a general model construction for constructing models of the intensional type theory with guarded recursive functions and types. When applied to the groupoid model of intensional type theory with the universe of small discrete groupoids, the construction gives a model of guarded recursion for which there is a one-to-one correspondence between fixed points of functions on the universe of types and fixed points of (suitable) operators on types. In particular, we find that the functor category Grpdωopfrom the preordered set of natural numbers to the category of groupoids is a model of intensional type theory with guarded recursive types.

We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S.

This paper shows how PILLY(Polymorphic Intuitionistic/Linear Lambda calculus with a fixed point combinatorY) with parametric polymorphism can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using Plotkin's encodings of recursive types in PILLY, we show how parametric models of PILLYgive rise to models of FPC, which is a simply typed lambda calculus with recursive types and an operational call-by-value semantics, reflecting a classical result from domain theory. Essentially, this interpretation is an interpretation of intuitionistic logic into linear logic first discovered by Girard, which in this paper is extended to deal with recursive types. Of particular interest is a model based on ‘admissible’ pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is to the author's knowledge the first denotational model of a non-linear language with parametric polymorphism and recursive types.

According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Many programs, however, exhibit computational effects. In this paper, we develop a framework for extending the notion of relational parametricity to languages with effects.

We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed types. In the case of recursive types, the reasoning principle is a mixed induction/coinduction principle, with the curious property that coinduction holds for general relations, but induction only for a limited collection of ``admissible'' relations. A similar property was observed in Pitts' 1995 analysis of recursive types in domain theory. In a future paper we will develop a category theoretic notion of models of the logic presented here, and show how the results developed in the logic can be transferred to the models.

We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin. The logic can be used to reason about parametric models, such that we may prove consequences of parametricity that to our knowledge have not been proved before for existing category-theoretic notions of relational parametricity. We provide examples of parametric models and describe a way of constructing parametric models from given models of the second-order lambda calculus.