Naïm Camille Favier on Nostr: I recently discovered that Agda's @0/Erased modality for runtime irrelevance (see the ...

I recently discovered that Agda's @0/Erased modality for runtime irrelevance (see the docs, or Danielsson 2019 for a more detailed treatment) is an open modality (in the sense of Modalities in homotopy type theory, corresponding semantically to open subtoposes).

That is, one can prove (assuming function extensionality) that Erased A is equivalent to the function type Compiling → A, where Compiling is the following inductive type:

data Compiling : Type where
@0 compiling : Compiling


(and, over this equivalence, if A : Erased Type then Erased A is equivalent to the dependent function type (c : Compiling) → A c).

This is because Agda considers clauses that match on erased constructors as erased, so that pattern matching on the erased constructor compiling is equivalent to copattern matching on the erased field of the Erased record type.

I think this is pretty neat, because we get a bunch of theory for free: for instance, every open modality ○ has an associated closed modality ●, which we can define in Cubical Agda as the following higher inductive type:

data ●_ (A : Type ℓ) : Type ℓ where
η● : A → ● A
@0 tip : ● A
@0 cone : (a : A) → η● a ≡ tip


Whereas ○ A trivialises A's runtime information, one can think of ● A as the complementary operation that glues all of A together at compile time but leaves the runtime part unchanged.

I've formalised these things here, as well as proved an "Artin gluing" theorem that says that any type A can be reconstructed from its compile-time part ○ A and its runtime part ● A in a suitable sense.

This seems pretty closely related to some of the synthetic Tait computability stuff by nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0). In particular in Logical relations as types a similar open modality is used to express some kind of phase distinction between static and dynamic things. I wonder how precise the relationship can be made.

I am also wondering if there is a nice semantic place in which to make sense of all this. For example, it seems like we could interpret Compiling in a category of assemblies as the assembly with singleton carrier and no realisers, but this is disallowed by the definition of assemblies which requires every element to have at least one realiser. Is there a good reason for this restriction? (nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq42pdf0hluzkf9tygejlmwhf7aqalk70tp0jczdu7xfyhwn5mlc2qwtr8sr (nprofile…r8sr) do you know?)

Also pinging nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4sqchszg (nprofile…hszg) because of some of your comments here: maybe this suggests that a suitable axiomatisation of computational erasure (at least of the kind under discussion here) is simply a proposition C, possibly such that ¬¬C holds if we want ⊥ to be modal (corresponding to the ability to pattern match on erased arguments of the empty type).

(Sorry for the long post 😅)