Modal parametric discreteness ============================= As remarked under :ref:`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 :ref:`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 :ref:`arity `, and their "discrete" modalities and modes (to be explained below) and potential "parametricity locker" modalities (to be explained in :ref:`Modally guarded parametricity`), are: .. csv-table:: Mode theories :widths: auto :header-rows: 1 :stub-columns: 1 "Command-line flag", "Base theory", "Arity", "Discretes", "Param. Locker" "``-discrete-functor``", "``-functor``", "any", "``○``, ``DomType``", "--" "``-discrete-coreflector``", "``-coreflector``", "any", "``♭``", "``♭`` (arity 1)" "``-discrete-comonad``", "``-comonad``", "any", "``♭``", "``△□``" "``-discrete-spatial``", "``-spatial``", "any", "``♭``", "--" "``-discrete-cospatial``", "``-spatial``", "1 only", "``ʃ``, ``♭``", "``♭`` (arity 1)" "``-discrete-ambiflector``", "``-ambiflector``", "1 only", "``♮``", "--" "``-discrete-coreflection``", "``-coreflection``", "any", "``△``, ``Disc``", "``△□`` (arity 1)" "``-discrete-adjunction``", "``-adjunction``", "any", "``△``, ``△□``, ``Disc``", "``△□``" "``-discrete-local``", "``-local``", "any", "``△``, ``△□``, ``Disc``", "--" "``-discrete-tconn``", "``-tconn``", "1 only", "``△``, ``△□``, ``△◇``, ``Disc``", "``△□`` (arity 1)" "``-discrete-gwpt``", "``-gwpt``", "any", "``△``, ``△□``, ``△◇``, ``Disc``", "``△□``" "``-discrete-ambiflection``", "``-ambiflection``", "1 only", "``△``, ``□``, ``△□``, ``Disc``", "--" Some discrete mode theories also differ from their base theories by having more :ref:`pellucid ` modalities: - ``△`` is pellucid in ``-discrete-coreflection``, ``-discrete-adjunction``, and ``-discrete-local``. - ``△`` is pellucid in ``-discrete-gwpt``, and in the :ref:`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 :ref:`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 :ref:`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 :ref:`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 .. code-block:: none (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 .. code-block:: none {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 .. code-block:: none 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 .. code-block:: none (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 .. code-block:: none {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 .. code-block:: none {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 .. code-block:: none {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 :ref:`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: .. code-block:: none def ○ (A :○| DomType) : CodType ≔ data [ circle. (_ :○| A) ] we have ``circle. : (_ :○| A) → ○ A``, and therefore for the bridge type we have a constructor .. code-block:: none 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 :ref:`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: .. code-block:: none 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 .. code-block:: none (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.