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!

Instances of computational effects: an algebraic perspective

(Link).

Authors: Sam Staton (University of Cambridge)

Conference: Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), June 25-28, 2013, New Orleans, USA.

Journal reference: Proceedings to appear.

Comments: Google Scholar Updates's top recommendation this week was something a bit different - my old PhD supervisor Andrew Pitts has just released the first full book ever published on the relatively new field of nominal sets, titled Nominal Sets: Names and Symmetry in Computer Science. As a recommendation to read it is of course very much in line with my interests, but as a recommendation to write about on this blog within a week's notice it is not so realistic (Google Books offer a preview if you're curious).

Let's turn instead to the second recommendation in my queue, which happens to also stem from Cambridge. In fact it is a sequel to the Staton paper I wrote about four months ago, continuing his development of parameterized algebra. Please refer to my earlier post for a reminder of what that is.

In this paper parameterized algebra is put to work to talk about computational effects. If we think of a computer program as a process that, after some computation, returns a result, a (side) effect refers to things the computer does while that result is being produced. For example, the computer might write something on the screen, or change something in memory. Less obviously, if the program can accept user input this is also a sort of side effect. Whether such events are treated as side effects or as part of the value returned is somewhat flexible, and can differ by programming paradigm or language, but separating computations into the values they calculate and the effects they produce en route is hard to avoid entirely, even in the relatively 'pure' world of functional programming.

A big development in functional programming that allowed effects to be handled more transparently came with Moggi's 1991 paper Notions of computation and monads. Monads are a concept we've encountered a few times on this blog, most extensively here, and essentially give a concise category theoretic way to describe equationally defined, or algebraic, models. Monads are a core concept of category theory because of their relationship to the basic idea of adjunctions, but hardly seem candidates to impact the working practices of your average Haskell programmer. And yet, Moggi and later authors showed that monads are a nice way to 'package up' effects in functional programs to make effectful programs more structured.

The next big milestone in the intellectual history behind this paper is Plotkin and Power's 2002 Notions of computation determine monads, deliberately titled as a sequel to Moggi's classic. This paper essentially dialed the practical issue - effects - back to the original theory - equational definitions - and asked how the monads used to handle effects can be defined equationally. This work was in a sense experimental, as it gave a few examples of how such definitions were both possible and illuminating without building any sort of general theory. Staton to an extent follows this example-driven approach, looking at computational effects that can be thought of as multiple instances of a general concept, such as writing to a specific memory bit being an instance of the general idea of writing to memory. However he moves beyond the examples to argue that the effects in question are correctly captured by his theory of parameterized algebra, which hence provides a syntactic and semantic framework through which many interesting side effects can be defined, categorised, and studied.