[Agda] Records and irrelevant fields

[Dan Doel]

On Tuesday 21 September 2010 3:13:18 am Andreas Abel wrote:
> Yeah, with the equality type there is an issue.  You cannot erase
> equality proofs at compile time because you still have to match
> against refl to prevent the bad stuff outlined below.  Also, if you
> want proof irrelevance for the identity type you need to eta-expand
> h : t == t  to refl : t == t, otherwise it is not true that the proof
> of t == t does not matter.
> 
> 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.

It may be okay. I haven't thought deeply on the issue, and have come up with 
objections in both directions.

One concern is that:

  Squash Bot

is (hopefully) empty, which seems to be part of the weirdness of equality 
types (i.e. they aren't always inhabited). And the thesis presents a case 
against empty type erasure, too.

On the other hand, erasing matches:

  foo (squash at bot) = ...

giving an irrelevant bottom value don't exactly seem comparable to allowing:

  foo@()

which empty type erasure would.

> This seems to be a different principle, namely that types themselves
> are irrelevant, meaning they contain at most one inhabitant (after
> erasure).  Along this kind of reasoning you could have
> 
>    g : (A -> Unit) -> Squash A -> Unit
>    g f (squash a) = f a
> 
> although in this kind one could argue that it is ok since the r.h.s.
> can be eta-exanded to the empty tuple
> 
>    g f (squash a) = ()

Yes, the effect of adding modal operators seems to be the ability to 
distinguish certain types as propositional (anything of the form <>T). And 
some types already are naturally, but might not be treated as such.

The alternate Squash eliminator is, of course, tied to Squash being a monad, 
which is added by fancier means in the proof irrelevant version of the theory, 
where you can add axioms nicely. Adding the alternate rule is a more 
conservative addition. On the other hand:

> Maybe more interesting would be the typing
> 
>    g : (A -> Empty) -> Squash A -> Empty

This is novel, even if Squash is a monad (and even in the presence of the 
above axioms). Squash Empty does not imply Empty unless empty type erasure is 
done, and the thesis argues against that, as mentioned.

-- Dan