Let’s start the blog off by tempting Wadler’s Law! (Actually, Wadler’s Law does not align with my experience. Perhaps due to the now-well-known nature of the Law itself and the perjorative view it implies of discussions of syntax, I’ve found that hardly anyone else ever wants to talk about syntax at all! At least I’m not the only one.)

My current project is to enhance Narya with Multimodal Type Theory. (I always intended to do that, but I’m doing it now because I hope that it will be useful in completing the implementation of HOTT; more on that later.) I’ll have more to say about the implementation later, but right now I’m pondering some questions of concrete syntax.

Syntax for modes

In modern modal type theories, the modal behavior is parametrized by a mode theory: a 2-category whose objects are called modes and whose morphisms are called mode morphisms or modalities. There is a separate ordinary type theory at each mode, and the modalities induce modal operators mapping between them: a modality μ : p → q can induce a modal operator taking p-types to q-types.

In the literature on modal type theory, one tends to find judgments annotated by mode, such as Γ ⊢ A typeₚ or Γ ⊢ A type @ p. In the concrete syntax of a proof assistant (at least, of Narya), the only judgment the user interacts with is a typing judgment. But it would be quite annoying to have to constantly write x :ₚ A or x : A @ p.

I think a workable solution to this is to say that the names of modes are the same as the names of the corresponding universes of types at that mode. Thus, if there is only one mode, that mode is called Type. If there is another mode of “discrete types”, as in dTT, we could call that mode Disc, and so on. Then when we use one of these universe-names, it indicates directly which mode the corresponding type lives at, and the modes of essentially all other judgments should be inferrable.

Syntax for modal variables

The way modern modal type theories incorporate the modalities is that some variables are annotated by some modality. In general, a variable in a context or judgment at mode q can be annotated by a modality μ : p → q, in which case the type of that variable must live at mode p (in a context which is “locked” by the modality μ, but that’s a story for another day). Semantically, such a variable has the covariant modal operator associated to μ applied to its type, but syntactically it is a judgmental structure used to give rules for that modal operator as a type former.

There are two ways that these modal annotations are generally denoted syntactically in the literature. One is to modify the typing colon. For example, in crisp/spatial type theory the modal variables are denoted x ∷ A. The corresponding modal operator, say ♭, can then be defined as an inductive type generated by a constructor with a modal argument:

def ♭ (A ∷ Type) : Type ≔ data [
| flat. (x ∷ A) : ♭ A ]

If there are multiple modalities, this style requires additional “kinds of colons”. There are a limited number of Unicode colon-like operators, but of course we can make more by combining characters:

(x :~ A) (y :: B) (z :# C) (w ∷♯ D)

and so on.

This approach has the advantage of conciseness. However, it has several drawbacks:

  • There are, to be sure, an unbounded number of colon-operators, but it seems a little awkward to have to keep thinking of a new one whenever we need a new modality, and we’ll quickly run out of the nicest-looking ones like ∷.

  • Are :: and ∷ two different operators, or is the second a Unicode-variation of the first? What characters are allowed in a colon-operator? Narya’s existing lexer allows x:A to mean x : A because : is an ASCII symbol while x and A are identifiers. I don’t want to give that up, but without modification the same wouldn’t be true of x∷A, which would be inconsistent and surprising.

  • We need a “name” to refer to each modality, for instance in error messages like ♯-annotated variable is inaccessible behind ♭ lock. We could use the colon-operators as names, like :#-annotated variable is inaccessible behind ∷ lock, but that looks a little ugly and could be hard to understand. And if modalities had names that were different from their colon-operators, the user would have to remember which names go with which colons.

  • Some mode theories are finitely generated but not finite, and the user (or whoever specifies the mode theory) can only be expected to explicitly give names or colon-operators to the generators. If the lock is a composite of generators, then we need to be able to say something like ♯-annotated variable is inaccessible behind ♭ ♭ ♭ lock, which looks even uglier and more confusing as :#-annotated variable is inaccessible behind ∷ ∷ ∷ lock.

The other syntax for modal annotations in the literature is the one in the MTT paper, where the type is annotated with the modality and a bar operator: x : (♭ | A). This solves all of these problems since we can use a more natural “name” for the modality such as ♭, and a sequence of names to represent a composite of modalities as in x : (♭ ♭ | A). I’ve resisted using this syntax on paper because I think it’s fairly verbose, but something like it may be unavoidable in an implementation.

I am thinking of simplifying it a bit by removing the parentheses around ♭ | A, since in practice an annotated variable is always inside outer parentheses anyway, as for instance in a modal function type (x : ♭ | A) → B x. And as long as the modality names are valid identifiers (not ASCII symbols), the Narya lexer would allow us to write this as (x :♭| A) → B x, which is not that far from the modified-colon approach. I’m curious if anyone else has thoughts.

One specific thing to note is that the names of modalities would (I think) be a separate category from other identifiers. In particular, even if ♭ is a modality name, one could also def ♭ to mean something inside the theory, without risk of parsing ambiguity since the : and | always bracket a modality name. Of course, defining ♭ to mean something totally different would be confusing, but we might very well want to use it for the modal operator defined as above:

def ♭ (A :♭| Type) : Type ≔ data [
| flat. (x :♭| A) : ♭ A ]

Syntax for key operators

To use a modally annotated variable, you have to “unlock” it with a “key” that is a 2-cell in the mode 2-category. In the simplest case, if μ : p → p is an endo-modality, then to use a variable x :μ| A you need to unlock it with a 2-cell α : μ ⇒ idₚ. More generally, if μ : p → q then x :μ| A can be unlocked with α : μ ⇒ ν if the context is “locked” by ν (I’m omitting what that means because I want to concentrate right now on syntax).

Many mode theories are locally posetal, so such 2-cells are unique when they exist. In that case, there’s no need for a syntax for them as they can be inferred automatically. But for a general mode theory, there might be multiple parallel 2-cells, so the user needs a way to specify which they want to use for unlocking.

Key operators have some formal similarities to higher-dimensional degeneracies, so I’ve been tempted to use a superscript syntax for them akin to Narya’s existing x⁽ᵉᵉ⁾ for degeneracies. However, on balance I think this would be too unwieldy: the superscripts would get too long to be easily readable.

One simple approach is a function-like prefix notation, so for instance α x would mean x unlocked with the key 2-cell α. (This also has a precedent in degeneracies, where refl x means the same as x⁽ᵉ⁾.)

In the case of a mode theory that’s finitely generated but not finite, where only the generating 2-cells have names, we need to derive names for the non-generating ones. I think we can get away without syntax for “vertical” composites of 2-cells (along 1-cells), because the key action of such a composite is just a composite of actions, so we can just write β (α x) instead of having a syntax for composing α and β.

Notating horizontal composition (along 0-cells) is more tricky. The simplest option would be something like α β x. As long as the names of 2-cells are not also available as identifiers, I think this would be technically unambiguous — but it could still be confusing, with α β f x meaning “act on the function-variable f with the horizontal composite of 2-cells α β, then apply the result to the argument x”.

A more verbose option would be for all key actions to be labeled by some keyword or symbol, such as key α x or 🗝️ α x. Then the first argument would always be a 2-cell, perhaps including a parenthesized (horizontal) composite of generating 2-cells: 🗝️ (α β) x.

We could combine the two options by saying that if the 2-cell argument is just a single generator, the key can be omitted: α x means 🗝️ α x, but 🗝️ (α β) x has no analogous abbreviated form. However, unlike the pure-key option, this would require that the names of 2-cells can’t be re-used for user definitions.

I’m especially curious if anyone else has thoughts about this. Which versions look best to you? If we need a “key” label, do you prefer the keyword key, the symbol 🗝️ (or 🔑), or something else?