Discussing "Normalization for Multimodal Type Theory"

(Link)

Author: Daniel Gratzer (Aarhus University)

Reference: Daniel Gratzer. 2022. Normalization for Multimodal Type Theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '22). Association for Computing Machinery, New York, NY, USA, Article 2, 1–13. https://doi.org/10.1145/3531130.3532398

Why this reference? Cited by Semantics of Multimodal Adjoint Type Theory, A Categorical Normalization Proof for the Modal Lambda-Calculus, and For the Metatheory of Type Theory, Internal Sconing Is Enough

While my reading program for this blog often sends me bouncing around from subject to subject, this blog post is exactly the sequel to the last one, as one of the authors of the Multimodal Type Theory paper tackles the question of normalisation for these systems. Normalisation is the property that all programs in a language terminate; this is not a typical property of programming languages but is important for dependent types: as terms can appear in types, type checking can require execution of arbitrary code, and so termination of type checking in general requires termination of all possible programs. Terminating type checking is a standard requirement, but is particularly desirable when we use type theories to formalise mathematics. In this paradigm type checking corresponds to proof checking, and it seems a bizarre violation of usual practice for it to be impossible to decide whether a putative proof of a theorem is indeed valid.

Proving normalisation of even quite simple type theories, such as the simply typed lambda calculus, is not easy (although the techniques are now well studied and understood). While evaluation is sometimes called ‘reduction’, in fact terms do not reduce in size, or in any other obvious sense, as they compute. Matters get even more difficult in this paper, which refers to not one system, but multiple different type theories depending on one’s choice of mode theory. A recent proof of the property for one particular modal type theory was not encouraging, requiring a 77 page technical report to state all details. This paper also has a companion technical report weighing in at a comparatively svelte 39 pages, and yet proves the result for all modal type theories in the framework (provided that the mode theory chosen is not itself undecidable). How is this possible?

The technology behind this is Synthetic Tait Computability, as developed quite recently by Sterling and Harper. I am not yet entirely on top of this material, and frankly probably need to become so to appreciate the technical details of this quite dense paper (at least the Aarhus group, to which I used to belong, are good about publishing longer follow-ups in journals rather than leaving work in ultra-terse conference-truncated form, as sometimes happens with important or promising work in our field, so a more approachable but still reviewed version of this work might well be coming).

Given the technical prerequisites, perhaps a blow-by-blow of the development will not be so illuminating in a short blog post. Suffice it to say that the approach is deeply category theoretic; even the syntax is defined (it is claimed as a theorem, but looks more like a definition to me) to be an initial model, where model is defined as a certain 2-functor (this would provide a form of ‘fully annotated’ syntax which would probably be the target of an elaboration algorithm rather than pleasant to work with directly, but this is outside the bounds of this paper). Similarly, the normalisation algorithm is defined via the construction of a 'normalisation cosmos' (a cosmos is a weaker notion of model, avoiding some strictness requirements). While I am used to the denotational semantics (‘mathematical meaning’) of type theory being expressed in such terms, and syntax as initial model is OK as well, defining syntactic algorithms via category theory is a bit of a new one on me. It’s always good to have plenty to learn!

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.