Modal parametric discreteness
As remarked under Modal type theory, in general modal features and observational higher-dimensional features “commute” past each other without interacting, e.g. the higher-dimensional versions of modal canonical types are again modal canonical types in the same way. This section describes one way that modal type theory can interact with parametricity, and the next section External parametricity describes another; both are inspired by (and generalize) displayed type theory.
These features require -parametric, and by default we will assume -direction p,rel,Br. They also require choosing a modified mode theory called a “discrete” mode theory. The built-in discrete mode theories, along with the ordinary mode theory they modify, their restrictions on the arity, and their “discrete” modalities and modes (to be explained below) and potential “parametricity locker” modalities (to be explained in Modally guarded parametricity), are:
Command-line flag |
Base theory |
Arity |
Discretes |
Param. Locker |
|---|---|---|---|---|
|
|
any |
|
– |
|
|
any |
|
|
|
|
any |
|
|
|
|
any |
|
– |
|
|
1 only |
|
|
|
|
1 only |
|
– |
|
|
any |
|
|
|
|
any |
|
|
|
|
any |
|
– |
|
|
1 only |
|
|
|
|
any |
|
|
|
|
1 only |
|
– |
Some discrete mode theories also differ from their base theories by having more pellucid modalities:
△is pellucid in-discrete-coreflection,-discrete-adjunction, and-discrete-local.△is pellucid in-discrete-gwpt, and in the external case so are◇and△◇.Also in the external case,
◇and△◇are pellucid in-discrete-tconn(as is△, as in-tconn).
The reasons for these changes, and for the other choices in the table, will be explained in Semantics of modal parametricity.
Discrete modalities
A type is said to be (parametrically) discrete if its “bridges are equalities”. In the binary case, this means that Br A a₀ a₁ is equivalent to eq A a₀ a₁, the Martin-Löf identity type that is generated by rfl. : eq A a a, and similarly in higher dimensions. For other arities, we can similarly assert that Br A a₀ a₁ is equivalent to an “n-ary identity type” generated by a single constructor. For instance, in arity 3 a type is discrete if Br A a₀ a₁ a₂ is equivalent to eq3 A a₀ a₁ a₂ generated by rfl. : eq3 A a a a, and so on.
A mode theory can declare any of its modalities to be discrete (a.k.a. nonparametric), which means semantically that all the types in the image of its modal operator are discrete. Syntactically, however, this is ensured not by an axiom, but by altering the computation rules for modal types involving that modality, essentially building in the elimination rule for eq wherever there would be a Br. We will discuss these modified rules below.
In addition to modalities being discrete, a mode can also be declared as discrete. This means that types at that mode have no higher-dimensional versions at all.
For compatibility, it is required that a modality whose source or target mode is discrete must also be discrete. There is also a further restriction that will be explained below: if there are any 2-cells from a non-discrete modality (such as an identity) to a discrete modality, then the arity of parametricity must be 1. This is the syntactic reason why -discrete-tconn, -discrete-cospatial, -discrete-ambiflector, and -discrete-ambiflection require arity 1, because of the reflector units 1 ⇒ △◇, 1 ⇒ ʃ, 1 ⇒ ♮, and 1 ⇒ △□ respectively; a semantic reason will be given in Semantics of modal parametricity.
Discrete function-types
If ○ : DomType → CodType is a tangible discrete modality, as in the mode theory -discrete-functor, then Br ((x :○| A) → B x) f₀ f₁ reduces to
(x :○| A) →⁽ᵖ⁾ Br B x (f₀ x) (f₁ x)
Note that the domain has not been degenerated: there is only one variable x, in place of the triple variable we get for a non-discrete modality
{x₀ :○| A} {x₁ :○| A} (x₂ :○| Br A x₀ x₁) →⁽ᵖ⁾ Br B x₂ (f₀ x₀) (f₁ x₁)
Note that an equivalence between these two types is exactly what we would expect if Br A is equivalent to eq A. In addition, in the codomain type Br B x (f₀ x) (f₁ x) the bridge argument x₂ is replaced by the point argument x; this is well-typed because the same principle applies to B : (x :○| A) → CodType, so that
Br B : (x :○| A) → Br CodType (B x) (B x)
Discrete units and arity 1
Now we can explain the arity-1 restriction on mode theories with a 2-cell from a non-discrete modality to a discrete one, at least from a syntactic perspective. Suppose in -discrete-tconn we have f : (x : X) (y :△◇| A) → B and (x : X) → A. Then we can form
(x ↦ f x (a x)) : (x : X) → B
where in giving a x as the second argument of f we implicitly apply the key 1 ⇒ △◇. The result is a non-modal function. If the arity were 2, then its degenerate version rel (x ↦ f x (a x)) would have type
{x₀ : X} {x₁ : X} (x₂ : Br X x₀ x₁) →⁽ᵖ⁾ Br B (f x₀ (a x₀)) (f x₁ (a x₁))
Thus rel (x ↦ f x (a x)), would have to compute to something in this type – but what? The obvious thing is an application of rel f, which has type
{x₀ : X} {x₁ : X} (x₂ : Br X x₀ x₁) (y :△◇| A) →⁽ᵖ⁾ Br B (f x₀ y) (f x₁ y)
and we can of course start with {x₀} {x₁} x₂ ↦ rel f x₂ ?, but what to put in the hole? We need an element of A, but we have two of them: a x₀ and a x₁, and no way to choose one consistently.
By contrast, if the arity is 1 then rel (x ↦ f x (a x)) has type
{x₀ : X} (x₁ : Br X x₀) →⁽ᵖ⁾ Br B (f x₀ (a x₀))
so it can (and does) compute consistently to {x₀} x₁ ↦ rel f x₁ (a x₀).
See Semantics of modal parametricity for further discussion of this restriction.
Discrete datatypes
The behavior of modal constructors annotated by discrete modalities can be deduced from that of modal function-types, by regarding constructors as functions. In particular, for the case of a positive modal operator:
def ○ (A :○| DomType) : CodType ≔ data [ circle. (_ :○| A) ]
we have circle. : (_ :○| A) → ○ A, and therefore for the bridge type we have a constructor
circle. : (x :○| A) →⁽ᵖ⁾ Br (○ A) (circle. x) (circle. x)
In other words, Br (○ A) is a datatype indexed by two copies of ○ A with one constructor of this type. Using this, it’s easy to prove that indeed Br (○ A) u₀ u₁ is equivalent to eq (○ A) u₀ u₁, in other words ○ A is discrete as defined above.
Discrete modalities can also be pellucid, transparent, or translucent. However, a discrete modality cannot currently be used as a window modality for a match against a higher-dimensional datatype. This is not a semantic restriction, but a limitation of the structure of contexts in Narya; it would be possible to work around but we haven’t done it yet.
In particular, the preferred replacement for the deprecated strictly discrete datatypes is now to use a two-mode theory with discreteness and work with ordinary datatypes at the Disc mode, under the discrete window △ when working at the Type mode. Thus, for instance, we can prove things at Type by induction over the Disc-natural-numbers ℕ using a △ window, and no higher-dimensional versions of ℕ appear even when recursing into higher dimensions.
Codiscrete records and codata
Similarly, the behavior of modal fields annotated by discrete sinister modalities can be deduced from that of modal function-types by regarding field projections as functions, although there are a few twists. Consider the negative modal operator in the -discrete-spatial mode theory:
def ♯ (A : Type) : Type ≔ sig ( (_ :♭| _) .unsharp : A )
Here the .unsharp projection can be considered a modal function of type (_ :♭| ♯ A) → A. Therefore, passing to bridges we see that its degenerate version has type
(x :♭| ♯ A) →⁽ᵖ⁾ Br A ((x :♭| ♯ A) .unsharp) ((x :♭| ♯ A) .unsharp)
However, this is nothing but x ↦ rel ((x :♭| ♯ A) .unsharp). In particular, it does not contain Br (♯ A) anywhere in its domain, and therefore it does not induce a field of Br (♯ A). That is, fields annotated by discrete modalities vanish when passing to higher-dimensional versions of a record or codatatype.
In the particular case of a negative modal operator such as ♯ where the only field is modal, this means that Br (♯ A) u₀ u₁ has zero fields, and therefore it is equivalent to the unit type ⊤. That is, ♯ A is codiscrete, the dual of discrete: all of its bridge-types are contractible (uniquely inhabited). Similarly, ∇ A is codiscrete in the -discrete-local mode theory, because □ is discrete (as it has a discrete target Disc).
There is no direct way to declare a modality to “be codiscrete”: codiscreteness only arises for right adjoints of discrete sinister modalities. But a codiscrete modality cannot commute with parametricity either, nor can it be discrete (unless the arity is 1, in which case discreteness and codiscreteness coincide). Thus, the modalities ♯ in -discrete-spatial, and ∇ in -discrete-local and -discrete-gwpt, are declared to be intangible, so that they do not admit positive modal operators or appear in modal function-types at all, as there is no consistent way to give behavior for such types. (Note that this means in -discrete-gwpt it is impossible to define a modal operator ∇◇ directly: one can only define ◇ positively and ∇ negatively. This is also why it has no single-mode version.)
If a modality is neither tangible nor sinister, like ♯ and ∇, then it cannot appear in function-types, datatypes, or record/codatatypes. Thus, whether or not it is discrete is undetectable to the theory. But for consistency, we call these modalities discrete when they have a discrete mode as their source or target.