[Agda] Records and irrelevant fields

[Dan Doel]

On Tuesday 21 September 2010 3:13:18 am Andreas Abel wrote:

> However, I think there is no problem with Squash, because there is
> always exactly one match, whereas with equality types there is at most
> one match, and it has a side information that two things are
> declaratively equal.

Having thought about this some more, I came to the conclusion that it is 
indeed just another statement that double-irrelevance is the same as 
irrelevance, or that Squash is a monad. It makes the following equivalent:

  Squash A => B
  Squash A -> B
         A => B

at least in the non-dependent cases. And that first case is also the same as

  Squash (Squash A) -> B

I'm willing to bet that this case is sound. The question then becomes: how 
does one decide when it's safe (Squash) and when it isn't (equality)? Or are a 
couple special cases (Squash and Unit alikes) enough?

----------

On an unrelated note, I studied a bit more of Pfenning's modal type theory in 
the paper I mentioned earlier. I can find no difference in the context reset 
rules between his proof irrelevant modality and the modality in EPTS. The 
difference between the two theories has to do with some of the type formation 
rules. For instance, Pfenning gives pi formation as:

  G |- A * Type   G , x * A |- B : Type
  --------------------------------------
        G |- (Pi x * A. B) : Type

where * stands in for any particular modality. In an EPTS, it's:

  G |- A :r Type  G , x :r A |- B :r Type
  ---------------------------------------
         G |- (Pi x * A. B) :r Type

* again standing in for either :r or :c, to similarize the notation.

I don't actually know how different this makes the two theories, but the 
irrelevant modalities in either are going to be pretty similar. The EPTS 
thesis states that the difference between the two is their desire to treat 
erasability as extrinsic to to the type, while Pfenning's models intrinsic 
erasability---for instance, x must be erasable from the type of B in 
Pfenning's system (and the judgment of the type of A has a corresponding 
modality), whereas it's relevant in the EPTS.

I guess that might mean that EPTSes are quite close to the LiCS stuff you 
mentioned earlier.

----------

I've also come to a tentative conclusion that weakness of elimination is kind 
of important to the abstraction guarantees of, say, modules. We might have a 
signature like:

  mod : exists T : Set.
          T * (T -> T) * (forall R. R -> (R -> R) -> T -> R)

and a key aspect of the abstraction is that T must always be opaque outside of 
the definition of 'mod', even if we happen to know what the definition of mod 
is, I think (that is, mod is some particular definition, not some variable 
we've quantified over). Even if we are only able to project out T at compile 
time, if (proj1 mod) isn't opaque, then we are no longer required to program 
to the interface exposed by the module.

In this sense, inductives with irrelevant fields are kind of like units of 
erasure. We can't project the A out of an Exists A P, except as a Squash A, 
because it's already been erased, to enforce the abstraction above. Of course, 
I can see this not necessarily being what is always desired. You may sometimes 
want a compile/runtime devide where compile time things are always transparent 
at compile time. Perhaps it's possible to incorporate both.

-- Dan