Discussing "Multimodal Dependent Type Theory"

(Link)

Authors: Daniel Gratzer (Aarhus University), G. A. Kavvos (Aarhus University), Andreas Nuyts (KU Leuven), and Lars Birkedal (Aarhus University)

Reference: Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2021. Multimodal Dependent Type Theory. In Logical Methods in Computer Science, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:11)2021

Why this reference? Cited by A Categorical Normalization Proof for the Modal Lambda-Calculus, Fitch-Style Applicative Functors, and Commuting Cohesions

I’ve discussed the links between types and modal logic a few times on this blog, most notably two weeks ago, when I discussed Davies and Pfenning’s addition of a certain modality into a simply typed functional language. This paper, based on the shorter conference paper of the previous year, extends the state of play by introducing a general recipe for integrating modalities, including multiple modalities at once, into dependent type theory. As long as the recipe is followed (as we will see, this is not always exactly possible) certain desirable properties such as canonicity can be guaranteed, rather than working from scratch to derive such properties every time a formally new modal type theory is proposed.

The two main technologies making this possible are Fitch-style type theory, which I discussed two weeks ago, and the mode theories introduced recently by Licata and Shulman. Given how recently I’ve discussed Fitch-style types I’ll restrain myself to briefly say that these provide a setting for modal type theory that is appealingly general and close to informal modal reasoning, and that their usual formulation is modified here to push some of the complexity of the system from the modal elimination rules to the variable rules, which turns out to be beneficial due to avoidance of certain ‘trimming’ operations on contexts.

Mode theories are three layer structures organised as 2-categories (for some applications, some of these layers may be trivial). These layers are best illustrated through the example of guarded recursion, a setting in which types are regarded as unfolding over time, which is helpful for ensuring that certain recursive constructions avoid the impossible circularity of parts that are constructed in terms of other parts that are not constructed yet. The first layer of a mode theory are the modes, which correspond to different dependent type theories. Often one mode suffices, but with guarded recursion it is convenient to have two, allowing the programmer to switch back and forth between regarding types as varying over time, or as lacking this property; in the latter mode, ‘vanilla’ dependent type theory suffices. The second layer are the modalities, which map from mode to mode. With guarded recursion, the ‘later’ modality starts and finishes in the time-varying mode, but is meaningless in constant mode; two further modalities allow passage between the varying and constant modes. The third layer, of 2-cells, define maps between modalities, which give fine control over details such as whether an S4-like modality is idempotent.

The guarded recursion example is also helpful for observing some of the limitations of this setup. The ‘Löb induction’ property of the later modality, a technical requirement that gives guarded recursion its power and significance, cannot be expressed in a mode theory and must be imposed on top of the iteration of the general recipe. By leaving the recipe, the powerful general theorems proved about recipe-obeying type theories are no longer guaranteed to apply. More generally, the notion of mode theory as 2-category is quite abstract and it will be interesting to see development of how they are realised as syntax, and how their limitations can be understood.

Another limitation, not so significant in the case of guarded recursion but of interest elsewhere, is that every modality that fits into the framework is a ‘necessity’ or ‘box’ style of modality, commuting with products. Some modalities of interest elsewhere are the ‘possibility’ or ‘diamond’ modalities, which (usually) commute with coproducts instead. Admittedly such modalities currently have considerably less application as types that the modalities of this paper, but I am not completely clear whether that will be an enduring truth, or it is something that is true because we do not have good general understanding of how to fit them into type theory.

Next week my paper-picking algorithm will see me consider a direct sequel paper to this one, so it will be interesting to see how these important and relevant ideas continue to develop.

Discussing "The Coq Proof Assistant"

(Link)

Authors: The Coq Development Team

Reference: The Coq Development Team. The Coq proof assistant, Version 8.16, September 5 2022

Why this reference? Cited by Type Theory as a Language Workbench and Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

This blog is a project to encourage myself to read more widely, and hopefully spread some knowledge to those who stumble across it, by looking at multiple-cited papers in my recent Google Scholar recommendations. Yet papers are not the only thing that gets cited; I’ve looked at books, monumental pairs of books, and now, my first software. Reviewing software in a week is not an obvious task, as the ‘content’ of software is not encapsulated by looking at source code, but also lives beyond the software in the ecosystem around it – tutorials, libraries, applications, active forums and communities, and so forth. In order to make this task tractable, I’ve decided to concentrate on the Coq User Manual as my reference, and use that to give an overview of Coq.

At its base, Coq is an implementation of a certain version of Martin-Löf Type theory. The intention as usual is to provide a type system expressive enough to naturally express mathematical statements, along with tools to allow users to attempt to prove these statements in an interactive style, with the computer checking each step and assisting with automatic proving where possible. Coq has enjoyed conspicuous success in this, with the manual making particular mention of the CompCert verified C compiler and verification of the four colour theorem.

The name, which is French for rooster but inevitably attracts sniggers, is a play on CoC, the Calculus of Constructions, the version of type theory the original software was based on in 1983. It also works as a pun on the name of Thierry Coquand, whose PhD thesis provided the original impetus (the original software was mostly written by Gérard Huet). The version of type theory that is currently the basis of Coq is CIC, the Calculus of Inductive Constructions, as introduced by Coquand and Christine Paulin-Mohring. This does not mean that the underlying type theory is fixed and static however; for example there was major development on the treatment of coinduction between versions 8.5 and 8.9 (2015-18), and there are currently two elements of the trusted base that are labelled as experimental (universe polymorphism and a type of proof-irrelevant propositions).

The first layer built on top of the implementation of the core language CIC are the language extensions, which are translated to the core language in a process called elaboration. To give some idea of relative sizes, the manual spends 97 pages on the core language, and 120 on the extensions. Features such as implicit coercions and typeclasses allow the user to write more natural looking mathematical statements with less clutter, wherever said clutter can be inferred automatically.

The ability to express mathematical statements is not particularly valuable without the ability to prove them. Naively, one might expect proofs to proceed in a functional style, as CIC is essentially a functional language with a particularly expressive type system. Indeed, every Coq proof is ‘really’ a functional program, which can be inspected. But in practice these programs are not written directly in functional style but rather generated in imperative style by commands called tactics, which are called in sequence and modify the state of a proof (its current goals and assumptions). Some tactics are fairly low level, for example moving the left hand side of an implication goal into the assumptions. Others are considerably more sophisticated, attempting to automatically discover non-trivial proofs in a style reminiscent of the logic programming language Prolog. There is also a bifurcation between two major packages of tactics, the standard collection and an independently produced collection SSReflect; these are intended to be merged in the future. Note that neither of these collections of tactics, nor any others, need to be trusted: they attempt to produce proofs, but these ‘proofs’ are not accepted until the core language type-checks them successfully.

If the default tactics are not sufficient, users can create their own using a language called Ltac. This language is described by the manual as somewhat ad hoc and unclear in its semantics, and so another currently experimental feature (good enough that users are encouraged to try it) is Ltac2, a tactic-definition language enhanced with desirable programming language features such as types.

As one would expect for a mature language, there have been a range of libraries and plugins developed for Coq. Again, even the most basic libraries do not need to be trusted, as they can be checked by the core type checker. There are also several choices of IDEs, a range of introductory books and tutorials, and so on. One style of plugin that is of particular note is the ability to extract code from Coq to other programming languages (currently Haskell, Scheme, and OCaml). At best, this creates certified-correct code that can run in a more efficient system than Coq. At worst, code extraction is not completely reliable due to mismatches between the semantics of Coq and the target languages, and so the manual even features a brief section colourfully titled “Extraction’s horror museum”.