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 "First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees"

(Link). Slightly confusingly, the authors earlier published a shorter conference article with the same name.

Authors: Lars Birkedal (IT University of Copenhagen), Rasmus Ejlers Møgelberg (IT University of Copenhagen), Jan Schwinghammer (Saarland University), and Kristian Støvring (University of Copenhagen)

Reference: Birkedal, L., Møgelberg, R. E., Schwinghammer, J., & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8.

Why this paper? Cited by A Formal Logic for Formal Category Theory, Classifying topoi in synthetic guarded domain theory, and A metalanguage for cost-aware denotational semantics

This paper, which has been very influential on a chunk of my career, nicely pieces together some practically minded applications in program verification with the more abstract world of category theory.

The practical motivations are very similar to the step-indexing paper I discussed a few weeks ago, namely type systems with recursive features that appear difficult to reason about without getting trapped in unsolvable circularities. In the key example of this paper, a programming language with higher-order store (i.e. the ability to store typed programs in memory) forces one to define the meaning of types in terms of the meaning of the store, but also to define the meaning of the store in terms of the meanings of types! In the step-indexing approach, one works around these circularities by invoking a natural number that decreases towards zero as the program computes; this paper does something quite similar, but in the name of “avoiding tedious calculations with step indices” it instead asks us to work in a topos which naturally supports this sort of notion of steps.

A topos is, very roughly, a ‘mathematical universe’ (or category) which contains the mathematical machinery one would expect to have in set theory. For example, a subobject classifier is an object of truth values. We might expect to have just the two values, True and False – and indeed there are toposes for which this is so – but in the topos of this paper, the topos of trees, one can see the subobject classifier as the set of all natural numbers, along with the infinite value ω. One can consider 0 as False, ω as True, and each positive integer n as ‘not falsified by the first n steps of computation’ (this is not quite how this paper presents things, but is the point of view taken for example by a later paper of mine). This is quite a nice way to think about computations that unfold over time: consider two streams (infinite lists); they are 1-equal if their first elements agree, 2-equal if their first two elements agree, and so on to only reach ω, or ‘true’, equality if there is no index on which they will ever be unequal. In other words, working inside the topos of trees gives you access to a logic that allows you to talk about certain aspects of computer programs that are harder to describe with more conventional logic. In particular, instead of working directly with the indices, one instead can do a lot with a modality (new logical connective) called ‘later’ than helps hide those details away while preserving the ability to make the sort of arguments for which one would otherwise explicitly involve step indices.

As well as the logical point of view which comes from working with the subobject classifier, one can also use the topos of trees as a denotational semantics (mathematical meaning) for types in various ways, whether one is reasoning about a typed programming language, or using dependent type theory to construct a formal mathematical argument. Looked at through this prism, instead of viewing a type as standing in for its set of elements, one can view types as an infinite series of sets that become more and more precise or informative over time. For example, the type of streams is not merely the set of infinite sequences, but instead an infinite string of sets that at step 1 reveal only their first elements, at step 2 reveal their first two elements, and so on. The modality `later’ now reappears in slightly different guise as a type-former; one needs to check that self-references are guarded by later in order to ensure one has a meaningful recursive type definition. This idea of checking syntax for guardedness in order to ensure that recursive definitions are good is quite old, but usually takes place at the level of the syntax of terms. By lifting this check to the level of types we get the advantages that well-behaved type systems usually confer, particularly modularity – the ability to stick any two good programs together, provided their types agree, without their combination going wrong.