-
Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We study the categorical structure of the Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ and characterise fibred limits, colimits, and monoidal structures. Next, we give sufficient conditions for the monoidal closure of the total category $Σ_\mathcal{C} \mathcal{L}$ of a Grothendieck construction of an indexed category…
▽ More
We study the categorical structure of the Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ and characterise fibred limits, colimits, and monoidal structures. Next, we give sufficient conditions for the monoidal closure of the total category $Σ_\mathcal{C} \mathcal{L}$ of a Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$. Our analysis is a generalization of Gödel's Dialectica interpretation, and it relies on a novel notion of $Σ$-tractable monoidal structure. As we will see, $Σ$-tractable coproducts simultaneously generalize cocartesian coclosed structures, biproducts and extensive coproducts. We analyse when the closed structure is fibred -- usually it is not.
△ Less
Submitted 21 May, 2024; v1 submitted 13 May, 2024;
originally announced May 2024.
-
Free Doubly-Infinitary Distributive Categories are Cartesian Closed
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We delve into the concept of categories with products that distribute over coproducts, which we call doubly-infinitary distributive categories. We show various instances of doubly-infinitary distributive categories aiming for a comparative analysis with established notions such as extensivity, infinitary distributiveness, and cartesian closedness. Our exploration reveals that this condition repres…
▽ More
We delve into the concept of categories with products that distribute over coproducts, which we call doubly-infinitary distributive categories. We show various instances of doubly-infinitary distributive categories aiming for a comparative analysis with established notions such as extensivity, infinitary distributiveness, and cartesian closedness. Our exploration reveals that this condition represents a substantial extension beyond the classical understanding of infinitary distributive categories. Our main theorem establishes that free doubly-infinitary distributive categories are cartesian closed. We end the paper with remarks on non-canonical isomorphisms, open questions, and future work.
△ Less
Submitted 30 March, 2024; v1 submitted 15 March, 2024;
originally announced March 2024.
-
Efficient CHAD
Authors:
Tom Smeding,
Matthijs Vákár
Abstract:
We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple, composable, and generally applicable reverse-mode automatic differentiation (AD) technique that has the correct computational complexity that we would expect of reverse-mode AD. Specifically, we show that the standard optimisations of sparse vector…
▽ More
We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple, composable, and generally applicable reverse-mode automatic differentiation (AD) technique that has the correct computational complexity that we would expect of reverse-mode AD. Specifically, we show that the standard optimisations of sparse vectors and state-passing style code (as well as defunctionalisation/closure conversion, for higher-order languages) give us a purely functional algorithm that is most of the way to the correct complexity, with (functional) mutable updates taking care of the final log-factors. We provide an Agda formalisation of our complexity proof. Finally, we discuss how the techniques apply to differentiating parallel functional array programs: the key observations are 1) that all required mutability is (commutative, associative) accumulation, which lets us preserve task-parallelism and 2) that we can write down data-parallel derivatives for most data-parallel array primitives.
△ Less
Submitted 20 October, 2023; v1 submitted 7 July, 2023;
originally announced July 2023.
-
Logical Relations for Partial Features and Automatic Differentiation Correctness
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a very straightforward proof of correctness of practical forward- and reverse-mode dual numbers style automatic differentiation (AD) on ML-family languages. The…
▽ More
We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a very straightforward proof of correctness of practical forward- and reverse-mode dual numbers style automatic differentiation (AD) on ML-family languages. The key idea is to combine it with a suitable open logical relations technique for reasoning about differentiable partial functions (a suitable lifting of the partiality monad to logical relations), which we introduce.
△ Less
Submitted 23 October, 2022; v1 submitted 16 October, 2022;
originally announced October 2022.
-
Automatic Differentiation for ML-family languages: correctness via logical relations
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We give a simple, direct and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of Automatic Differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show ho…
▽ More
We give a simple, direct and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of Automatic Differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show how this code transformation provides us with correct forward- and reverse-mode AD.
The starting point is to interpret a functional programming language as a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD code transformation and the basic $ω$-cpo semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument.
The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $ω$-cpos.
△ Less
Submitted 14 June, 2024; v1 submitted 14 October, 2022;
originally announced October 2022.
-
Parallel Dual-Numbers Reverse AD
Authors:
Tom Smeding,
Matthijs Vákár
Abstract:
Where dual-numbers forward-mode automatic differentiation (AD) pairs each scalar value with its tangent value, dual-numbers reverse-mode AD attempts to achieve reverse AD using a similarly simple idea: by pairing each scalar value with a backpropagator function. Its correctness and efficiency on higher-order input languages have been analysed by Brunel, Mazza and Pagani, but this analysis used a c…
▽ More
Where dual-numbers forward-mode automatic differentiation (AD) pairs each scalar value with its tangent value, dual-numbers reverse-mode AD attempts to achieve reverse AD using a similarly simple idea: by pairing each scalar value with a backpropagator function. Its correctness and efficiency on higher-order input languages have been analysed by Brunel, Mazza and Pagani, but this analysis used a custom operational semantics for which it is unclear whether it can be implemented efficiently. We take inspiration from their use of linear factoring to optimise dual-numbers reverse-mode AD to an algorithm that has the correct complexity and enjoys an efficient implementation in a standard functional language with support for mutable arrays, such as Haskell. Aside from the linear factoring ingredient, our optimisation steps consist of well-known ideas from the functional programming community. We demonstrate the use of our technique by providing a practical implementation that differentiates most of Haskell98. Where previous work on dual numbers reverse AD has required sequentialisation to construct the reverse pass, we demonstrate that we can apply our technique to task-parallel source programs and generate a task-parallel derivative computation.
△ Less
Submitted 7 May, 2024; v1 submitted 7 July, 2022;
originally announced July 2022.
-
Dual-Numbers Reverse AD, Efficiently
Authors:
Tom Smeding,
Matthijs Vákár
Abstract:
Where dual-numbers forward-mode automatic differentiation (AD) pairs each scalar value with its tangent derivative, dual-numbers /reverse-mode/ AD attempts to achieve reverse AD using a similarly simple idea: by pairing each scalar value with a backpropagator function. Its correctness and efficiency on higher-order input languages have been analysed by Brunel, Mazza and Pagani, but this analysis w…
▽ More
Where dual-numbers forward-mode automatic differentiation (AD) pairs each scalar value with its tangent derivative, dual-numbers /reverse-mode/ AD attempts to achieve reverse AD using a similarly simple idea: by pairing each scalar value with a backpropagator function. Its correctness and efficiency on higher-order input languages have been analysed by Brunel, Mazza and Pagani, but this analysis was on a custom operational semantics for which it is unclear whether it can be implemented efficiently. We take inspiration from their use of /linear factoring/ to optimise dual-numbers reverse-mode AD to an algorithm that has the correct complexity and enjoys an efficient implementation in a standard functional language with resource-linear types, such as Haskell. Aside from the linear factoring ingredient, our optimisation steps consist of well-known ideas from the functional programming community. Furthermore, we observe a connection with classical imperative taping-based reverse AD, as well as Kmett's 'ad' Haskell library, recently analysed by Krawiec et al. We demonstrate the practical use of our technique by providing a performant implementation that differentiates most of Haskell98.
△ Less
Submitted 23 May, 2022;
originally announced May 2022.
-
CHAD for Expressive Total Languages
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) to total functional programming languages with expressive type systems featuring the combination of - tuple types; - sum types; - inductive types; - coinductive types; - function types. We achieve this by analysing the categorical semantics of such types in $Σ$-types (Grothendieck constructions)…
▽ More
We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) to total functional programming languages with expressive type systems featuring the combination of - tuple types; - sum types; - inductive types; - coinductive types; - function types. We achieve this by analysing the categorical semantics of such types in $Σ$-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward and reverse mode automatic differentiation (AD) on total functional programming languages with expressive type systems.
△ Less
Submitted 3 April, 2023; v1 submitted 1 October, 2021;
originally announced October 2021.
-
CHAD: Combinatory Homomorphic Automatic Differentiation
Authors:
Matthijs Vákár,
Tom Smeding
Abstract:
We introduce Combinatory Homomorphic Automatic Differentiation (CHAD), a principled, pure, provably correct define-then-run method for performing forward and reverse mode automatic differentiation (AD) on programming languages with expressive features. It implements AD as a compositional, type-respecting source-code transformation that generates purely functional code. This code transformation is…
▽ More
We introduce Combinatory Homomorphic Automatic Differentiation (CHAD), a principled, pure, provably correct define-then-run method for performing forward and reverse mode automatic differentiation (AD) on programming languages with expressive features. It implements AD as a compositional, type-respecting source-code transformation that generates purely functional code. This code transformation is principled in the sense that it is the unique homomorphic (structure preserving) extension to expressive languages of Elliott's well-known and unambiguous definitions of AD for a first-order functional language. Correctness of the method follows by a (compositional) logical relations argument that shows that the semantics of the syntactic derivative is the usual calculus derivative of the semantics of the original program.
In their most elegant formulation, the transformations generate code with linear types. However, the code transformations can be implemented in a standard functional language lacking linear types: while the correctness proof requires tracking of linearity, the actual transformations do not. In fact, even in a standard functional language, we can get all of the type-safety that linear types give us: we can implement all linear types used to type the transformations as abstract types, by using a basic module system.
In this paper, we detail the method when applied to a simple higher-order language for manipulating statically sized arrays. However, we explain how the methodology applies, more generally, to functional languages with other expressive features. Finally, we discuss how the scope of CHAD extends beyond applications in AD to other dynamic program analyses that accumulate data in a commutative monoid.
△ Less
Submitted 8 June, 2022; v1 submitted 29 March, 2021;
originally announced March 2021.
-
Higher Order Automatic Differentiation of Higher Order Functions
Authors:
Mathieu Huot,
Sam Staton,
Matthijs Vákár
Abstract:
We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets…
▽ More
We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Throughout, we show how the analysis extends to AD methods for computing higher order derivatives using a Taylor approximation.
△ Less
Submitted 21 March, 2022; v1 submitted 17 January, 2021;
originally announced January 2021.
-
Conditional independence by typing
Authors:
Maria I. Gorinova,
Andrew D. Gordon,
Charles Sutton,
Matthijs Vákár
Abstract:
A central goal of probabilistic programming languages (PPLs) is to separate modelling from inference. However, this goal is hard to achieve in practice. Users are often forced to re-write their models in order to improve efficiency of inference or meet restrictions imposed by the PPL. Conditional independence (CI) relationships among parameters are a crucial aspect of probabilistic models that cap…
▽ More
A central goal of probabilistic programming languages (PPLs) is to separate modelling from inference. However, this goal is hard to achieve in practice. Users are often forced to re-write their models in order to improve efficiency of inference or meet restrictions imposed by the PPL. Conditional independence (CI) relationships among parameters are a crucial aspect of probabilistic models that capture a qualitative summary of the specified model and can facilitate more efficient inference. We present an information flow type system for probabilistic programming that captures conditional independence (CI) relationships, and show that, for a well-typed program in our system, the distribution it implements is guaranteed to have certain CI-relationships. Further, by using type inference, we can statically deduce which CI-properties are present in a specified model. As a practical application, we consider the problem of how to perform inference on models with mixed discrete and continuous parameters. Inference on such models is challenging in many existing PPLs, but can be improved through a workaround, where the discrete parameters are used implicitly, at the expense of manual model re-writing. We present a source-to-source semantics-preserving transformation, which uses our CI-type system to automate this workaround by eliminating the discrete parameters from a probabilistic program. The resulting program can be seen as a hybrid inference algorithm on the original program, where continuous parameters can be drawn using efficient gradient-based inference methods, while the discrete parameters are inferred using variable elimination. We implement our CI-type system and its example application in SlicStan: a compositional variant of Stan.
△ Less
Submitted 18 February, 2022; v1 submitted 22 October, 2020;
originally announced October 2020.
-
Transforming Probabilistic Programs for Model Checking
Authors:
Ryan Bernstein,
Matthijs Vákár,
Jeannette Wing
Abstract:
Probabilistic programming is perfectly suited to reliable and transparent data science, as it allows the user to specify their models in a high-level language without worrying about the complexities of how to fit the models. Static analysis of probabilistic programs presents even further opportunities for enabling a high-level style of programming, by automating time-consuming and error-prone task…
▽ More
Probabilistic programming is perfectly suited to reliable and transparent data science, as it allows the user to specify their models in a high-level language without worrying about the complexities of how to fit the models. Static analysis of probabilistic programs presents even further opportunities for enabling a high-level style of programming, by automating time-consuming and error-prone tasks. We apply static analysis to probabilistic programs to automate large parts of two crucial model checking methods: Prior Predictive Checks and Simulation-Based Calibration. Our method transforms a probabilistic program specifying a density function into an efficient forward-sampling form. To achieve this transformation, we extract a factor graph from a probabilistic program using static analysis, generate a set of proposal directed acyclic graphs using a SAT solver, select a graph which will produce provably correct sampling code, then generate one or more sampling programs. We allow minimal user interaction to broaden the scope of application beyond what is possible with static analysis alone. We present an implementation targeting the popular Stan probabilistic programming language, automating large parts of a robust Bayesian workflow for a wide community of probabilistic programming users.
△ Less
Submitted 21 August, 2020;
originally announced August 2020.
-
Reverse AD at Higher Types: Pure, Principled and Denotationally Correct
Authors:
Matthijs Vákár
Abstract:
We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant for…
▽ More
We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant formulation, the transformations generate code with linear types. However, we demonstrate how the transformations can be implemented in a standard functional language without sacrificing correctness. To do so, we make use of abstract data types to represent the required linear types, e.g. through the use of a basic module system.
△ Less
Submitted 22 January, 2021; v1 submitted 10 July, 2020;
originally announced July 2020.
-
Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
Authors:
Matthijs Vákár
Abstract:
We present semantic correctness proofs of forward-mode Automatic Differentiation (AD) for languages with sources of partiality such as partial operations, lazy conditionals on real parameters, iteration, and term and type recursion. We first define an AD macro on a standard call-by-value language with some primitive operations for smooth partial functions and constructs for real conditionals and i…
▽ More
We present semantic correctness proofs of forward-mode Automatic Differentiation (AD) for languages with sources of partiality such as partial operations, lazy conditionals on real parameters, iteration, and term and type recursion. We first define an AD macro on a standard call-by-value language with some primitive operations for smooth partial functions and constructs for real conditionals and iteration, as a unique structure preserving macro determined by its action on the primitive operations. We define a semantics for the language in terms of diffeological spaces, where the key idea is to make use of a suitable partiality monad. A semantic logical relations argument, constructed through a subsconing construction over diffeological spaces, yields a correctness proof of the defined AD macro. A key insight is that, to reason about differentiation at sum types, we work with relations which form sheaves. Next, we extend our language with term and type recursion. To model this in our semantics, we introduce a new notion of space, suitable for modeling both recursion and differentiation, by equipping a diffeological space with a compatible $ω$cpo-structure. We demonstrate that our whole development extends to this setting. By making use of a semantic, rather than syntactic, logical relations argument, we circumvent the usual technicalities of logical relations techniques for type recursion.
△ Less
Submitted 27 May, 2024; v1 submitted 10 July, 2020;
originally announced July 2020.
-
Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing
Authors:
Mathieu Huot,
Sam Staton,
Matthijs Vákár
Abstract:
We present semantic correctness proofs of Automatic Differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets…
▽ More
We present semantic correctness proofs of Automatic Differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Finally, we sketch how the analysis extends to other AD methods by considering a continuation-based method.
△ Less
Submitted 1 April, 2020; v1 submitted 7 January, 2020;
originally announced January 2020.
-
A Domain Theory for Statistical Probabilistic Programming
Authors:
Matthijs Vákár,
Ohad Kammar,
Sam Staton
Abstract:
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance da…
▽ More
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity.
Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
△ Less
Submitted 29 July, 2021; v1 submitted 10 November, 2018;
originally announced November 2018.
-
Denotational validation of higher-order Bayesian inference
Authors:
Adam Ścibior,
Ohad Kammar,
Matthijs Vákár,
Sam Staton,
Hongseok Yang,
Yufei Cai,
Klaus Ostermann,
Sean K. Moss,
Chris Heunen,
Zoubin Ghahramani
Abstract:
We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such…
▽ More
We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics. Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions. We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock's synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.
△ Less
Submitted 8 November, 2017;
originally announced November 2017.
-
In Search of Effectful Dependent Types
Authors:
Matthijs Vákár
Abstract:
Real world programming languages crucially depend on the availability of computational effects to achieve programming convenience and expressive power as well as program efficiency. Logical frameworks rely on predicates, or dependent types, to express detailed logical properties about entities. According to the Curry-Howard correspondence, programming languages and logical frameworks should be ver…
▽ More
Real world programming languages crucially depend on the availability of computational effects to achieve programming convenience and expressive power as well as program efficiency. Logical frameworks rely on predicates, or dependent types, to express detailed logical properties about entities. According to the Curry-Howard correspondence, programming languages and logical frameworks should be very closely related. However, a language that has both good support for real programming and serious proving is still missing from the programming languages zoo. We believe this is due to a fundamental lack of understanding of how dependent types should interact with computational effects. In this thesis, we make a contribution towards such an understanding, with a focus on semantic methods.
△ Less
Submitted 6 December, 2017; v1 submitted 24 June, 2017;
originally announced June 2017.
-
An Effectful Treatment of Dependent Types
Authors:
Matthijs Vákár
Abstract:
We extend Levy's call-by-push-value (CBPV) analysis from simple to dependent type theory (DTT) in order to study the interaction between computational effects and dependent types. We define the naive system of dependently typed CBPV, dCBPV-, and its extension with a principle of Kleisli extensions for dependent functions, dCBPV+. We investigate these systems from the points of view of syntax, cate…
▽ More
We extend Levy's call-by-push-value (CBPV) analysis from simple to dependent type theory (DTT) in order to study the interaction between computational effects and dependent types. We define the naive system of dependently typed CBPV, dCBPV-, and its extension with a principle of Kleisli extensions for dependent functions, dCBPV+. We investigate these systems from the points of view of syntax, categorical semantics, concrete models and operational semantics, in presence of a range of effects. We observe that, while the expressive power of dCBPV+ is needed if we want well-defined call-by-value (CBV) and call-by-name (CBN) translations of DTT, it is a less straightforward system than dCBPV-, in presence of some effects. Indeed, to be able to construct specific models and to retain the subject reduction property in the operational semantics, we are required to impose certain subtyping conditions, the idea being that the type of a computation may only become more (not less) specified as certain effects are executed.
△ Less
Submitted 14 March, 2016;
originally announced March 2016.
-
A Framework for Dependent Types and Effects
Authors:
Matthijs Vákár
Abstract:
We generalise Levy's call-by-push-value (CBPV) to dependent type theory, to gain a better understanding of how to combine dependent types with effects. We define a dependently typed extension of CBPV, dCBPV-, and show that it has a very natural small-step operational semantics, which satisfies subject reduction and (depending on the effects present) determinism and strong normalization, and an ele…
▽ More
We generalise Levy's call-by-push-value (CBPV) to dependent type theory, to gain a better understanding of how to combine dependent types with effects. We define a dependently typed extension of CBPV, dCBPV-, and show that it has a very natural small-step operational semantics, which satisfies subject reduction and (depending on the effects present) determinism and strong normalization, and an elegant categorical semantics, which - surprisingly - is no more complicated than the simply typed semantics.
We have full and faithful translations from a dependently typed version of Moggi's monadic metalanguage and of a call-by-name (CBN) dependent type theory into dCBPV- which give rise to the expected operational behaviour. However, it turns out that dCBPV- does not suffice to encode call-by-value (CBV) dependent type theory or the strong (dependent) elimination rules for positive connectives in CBN-dependent type theory.
To mend this problem, we discuss a second, more expressive system dCBPV+, which additionally has a principle of Kleisli extension for dependent functions. We obtain the desired CBV- and CBN-translations of dependent type theory into dCBPV+. It too has a natural categorical semantics and operational semantics. However, depending on the effects we consider, we may lose uniqueness of typing, as the type of a computation may become more specified as certain effects are executed. This idea can be neatly formalized using a notion of subtyping.
We hope that the theoretical framework of this paper on the one hand provides at least a partial answer to the fundamental type theoretic question of how one can understand the relationship between computational effects and dependent types. On the other hand, we hope it can contribute a small-step towards the ultimate goal of an elegant fully fledged language for certified effectful programming.
△ Less
Submitted 14 March, 2016; v1 submitted 25 December, 2015;
originally announced December 2015.
-
Games for Dependent Types
Authors:
Samson Abramsky,
Radha Jagadeesan,
Matthijs Vákár
Abstract:
We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free winning strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied.
We show it contains a submodel as a full…
▽ More
We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free winning strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied.
We show it contains a submodel as a full subcategory which gives a faithful model of DTT with Pi-, 1-, Sigma- and intensional Id-types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id-types, as well as at the class of types where we allow for one strictly positive occurrence of an Id-type. Definability for the full type hierarchy with Id-types remains to be investigated.
△ Less
Submitted 20 August, 2015;
originally announced August 2015.
-
A Categorical Semantics for Linear Logical Frameworks
Authors:
Matthijs Vákár
Abstract:
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In par…
▽ More
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.
△ Less
Submitted 20 January, 2015;
originally announced January 2015.
-
Syntax and Semantics of Linear Dependent Types
Authors:
Matthijs Vákár
Abstract:
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In par…
▽ More
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.
△ Less
Submitted 16 January, 2015; v1 submitted 30 April, 2014;
originally announced May 2014.
