The dominant framework for modal dependent type theory today is MTT by Gratzer, Kavvos, Nuyts, and Birkedal, in which modalities and modal cells act contravariantly on contexts, with modal operators on types characterized as “dependent right adjoints” to these context operations. Specifically, if ℳ is the 2-category of modes, the context structure of (a model of) MTT is a 2-functor from ℳ to Cat that is contravariant on both 1-cells and 2-cells. The action of a 1-cell is called a lock and the action of a 2-cell is called a key.

The implication of this for syntax is that there are now two new ways to build context morphisms (substitutions):

  • If θ : Γ → Δ is a substitution at mode q, and μ : p → q is a modality, there is a locked substitution θ/μ : Γ/μ → Δ/μ at mode p.
  • If Γ is a context at mode q, and α : μ ⇒ ν : p → q is a modal 2-cell, there is a keyed substitution Γ\α : Γ/ν → Γ/μ. Note that this is contravariant, but because substitutions in turn act contravariantly on terms, modal 2-cells act covariantly on terms.

If we view substitutions as inductively generated by all the CwF operations on them, including composition and weakening, then we can simply add these constructors to all the others. That’s what the original MTT paper did.

However, in practice we like to think of ordinary substitutions as having a “canonical form” that is just a list of terms, one for each type in the codomain context, all defined in the domain context. In ordinary type theory, composition can be defined as an operation on these canonical substitutions: to compose θ : Γ → Δ with ϕ : Δ → Υ we just act with θ on all the terms in ϕ. We can similarly define weakening by weakening each term, and so on.

But in modal type theory this breaks. Our first thought might be that a modal substitution should be a list of terms interspersed with locks and keys, but that’s not enough. For example:

  1. Suppose α : μ ⇒ ν ∘ ρ; then Γ\α : Γ/ν∘ρ → Γ/μ. But Γ/ν∘ρ = Γ/ν/ρ, and we should be able to weaken that by adding a type in between ν and ρ to give a substitution Γ/ν,(x:A)/ρ → Γ/μ.
  2. Suppose β : ν ∘ ρ ⇒ σ; then a term Γ/ν ⊢ a:A yields a substitution Γ/ν → Γ/ν,(x:A), which we can lock to get Γ/ν/ρ → Γ/ν,(x:A)/ρ, and we should be able to compose this with Γ\β to get Γ/σ → Γ/ν,(x:A)/ρ.

Neither of these weakened or composite substitutions can be “reduced” to just a list of terms, locks, and keys.

For semantic purposes, inductively generated substitutions work fine, as long as we also quotient them by the CwF axioms. But for implementation, it’s convenient to have some more canonical representation. For instance, in traditional normalization-by-evaluation, we use an “environment” which is basically a substitution from a “value context” to a “term context”, represented as a list of values. During evaluation we then look up variable indices into this list to find their values. How can we do that for a modal type theory?

Even more problematically, how can we check whether two environments are equal? Equality of environments may not be a standard operation in NbE, but it’s necessary for the way Narya implements metavariables, which in turn is the only way I’ve been able to think of to do it in modal type theory. The problem with a metavariable is that it is created in some context, but it may escape that context and be used elsewhere. Often people talk about “lifting” a metavariable to a global definition by abstracting it over all the variables in its context; but there isn’t really any way to “abstract over” a modal lock in the context. (The closest thing is applying a modal operator, but that’s not as strict.) Instead, Narya remembers the context of each metavariable, and when it’s used elsewhere, stores the environment that was substituted into that context. But that means to check the equality of metavariables, we have to check the equality of environments.

The first implementation of MTT by Stassen, Gratzer, and Birkedal, called mitten, avoided this problem by restricting to locally posetal mode theories, where there is at most one 2-cell between any two modalities. This means that the identity of 2-cells doesn’t need to be tracked, and so they can be essentially omitted entirely from the environments, reducing them to lists of terms again. However, for Narya I wanted to allow more general mode theories, so we need something different.

Locks and prekeys

The usual “canonical form” of subsitutions is also inductively generated; it’s just that the generators are different from the CwF operations. Their generators are:

  1. There is an empty substitution () : Γ → ε to the empty context with any domain.
  2. Given θ : Γ → Δ and a term Γ ⊢ a : A[θ], there is an extended substitution (θ,a) : Γ → (Δ,x:A).

This is a very common sort of thing in type theory: by changing the signature we get a presentation of the free structure that requires fewer equational axioms, sometimes none at all.

In modal type theory, we must restate these using modes and modal annotations. And I believe we can get a canonical form for modal substitutions if we add two more generators of substitutions: one for locks and another for prekeys (precomposition with keys).

  1. For any context Γ at mode p, there is an empty substitution () : Γ → ε to the empty context.
  2. Given a substitution θ : Γ → Δ at mode q, a modality μ : p → q, and a term Γ/μ ⊢ a : A[θ] at mode p, there is an extended substitution (θ,a) : Γ → (Δ,x:μ|A).
  3. Given a modality μ : p → q, and a substitution θ : Γ → Δ at mode q, there is a locked substitution θ/μ : Γ/μ → Δ/μ at mode p.
  4. Given a modal 2-cell α : μ ⇒ ν : p → q, and a substitution θ : Γ/μ → Δ at mode p, if we have a telescope Γ ⊢ Ψ such that the composite of the locks in Ψ is ν, then there is a prekeyed substitution θ\α : (Γ,Ψ) → Δ.

The lock constructor is the same one I mentioned above, but the prekey requires some explanation. The idea is that θ\α is obtained by composing θ : Γ/μ → Δ with the key substitution Γ\α : Γ/ν → Γ/μ, then possibly decomposing ν as a composite and weakening in between the factors.

Of course, the original key substitutions mentioned above are the special case of a prekey applied to the identity on a locked context. Also, these constructors suffice to represent the two novel examples of substitutions I mentioned above. First, given α : μ ⇒ ν ∘ ρ, then Γ/ν,(x:A)/ρ → Γ/μ is just a prekey of the identity of Γ/μ by α. Second, given β : ν ∘ ρ ⇒ σ and Γ/ν ⊢ a:A, we have (1,a)/ρ : Γ/ν∘ρ → Γ/ν,(x:A)/ρ and thus a prekey (1,a)/ρ\α : Γ/σ → Γ/ν,(x:A)/ρ.

I have not written out a paper proof that every substitution is representable in terms of these constructors, but I believe such a proof is implicit in the Narya code. The main point is to show that two substitutions built from these operations can be composed to give another built in the same way. (Weakening is also a special case of prekeying, with the identity 2-cell.) To do this, we induct on the second substitution, and whenever we reach a lock or a prekey, we remove pieces of the first substitution corresponding to the matching locks in its codomain, then recurse. In Narya this manifests as the evaluation of a term-environment in a value-environment, eval_env.

The variable-lookup and equality-checking algorithms are similar. Regarding the second, equality is still a nontrivial relation: we’ve trimmed out some of the fat, but one substitution still has multiple representations in terms of our generators. For instance, locking twice should be the same as locking by the composite, and likewise for prekeying twice. The equality-checking algorithm handles this by accumulating locks and prekeys as it removes them and only comparing them when the accumulation stops at a value.

Free modalities

The algorithm is significantly simplified by a further assumption Narya makes about its mode theories: that the 1-category of 1-cells (modalities) is freely generated. This is convenient for the internal representation, and also means that no equality-checking algorithm for modalities is needed. It also trims a bit more fat from the representation of substitutions (and contexts): we make the basic locking operation act on a generating modality, and define general locking as a composite of these, thereby obtaining functoriality for free. No essential generality is lost thereby, since any 2-category is equivalent to one whose 1-category of 1-cells is free (its “cofibrant replacement”).

I don’t actually know to what extent Narya’s algorithms would work without this simplification. If I had to guess, I would guess that they would work, but require a lot more explicit annotations.

Let-only

I currently have a pull request open that adds to Narya an explicit syntax for describing the action of a full substitution. It looks like this:

let only x : A ≔ M
and y : B ≔ N
and lock △□
and key ε
and z : C ≔ P
in Q

Here the body term Q is typechecked in a context consisting of only the specified variables and locks; in this case

x:A, y:B, /△□ z:C

Furthermore, for this context to be well-formed, A must be a closed type, while B depends only on x:A, and so on. Any variables that exist outside the let only are not visible to the types or the body. The terms M, N, P, on the other hand, are defined using any ambient variables available outside the let only and not the new variables x,y,z, even those that come textually before them. These terms, together with the specified locks and prekeys, assemble into a substitution from the ambient context to the new one (x:A, y:B, /△□ z:C), and the result of the let only expression is the application of this substitition to the body term Q.

This syntax might be useful if you’re translating some argument written in semantic CwF-language into internal Narya syntax. However, its main intended purpose is to give a nicer way to display metavariables (which, recall, save the environment in which they were evaluated). That code isn’t done yet, though.

The let only syntax also supports higher-dimensional substitutions, which are the basic ingredient in Narya’s normalization algorithm for observational parametricity and HOTT. But I think I’ll postpone describing those to another day.