[Agda] Pattern matching on irrelevant data

[Dan Doel]

On Tue, Oct 4, 2011 at 4:20 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> On 03.10.11 10:51 PM, Dan Doel wrote:
>>
>> I'd also add: the irrelevance in Agda seems to be mixing two different
>> things. The reducing of irrelevant arguments to _ during type checking
>> seems motivated by the EPTS and similar stuff, which is tracking
>> parametricity of arguments, and supports checking-time erasure. The
>> matching-on-irrelevant stuff, including this new addition, but also on
>> ⊤, ⊥, and the like,
>
> Here, I guess, we need to differ!  There are three different things:
>
> 1. Matching on irrelevant records (includes \top).
> 2. Matching on empty types (includes \bot).
> 3. Matching on one-constructor-slices on inductive families (the new stuff).
>
> 1. is justified by eta-equality for records.  Take
>
>  stone : A \times B
>
> then definitionally
>
>  stone = proj\_1 stone , proj\_2 stone : A \times B
>
> so clearly we can match (x , y) against stone, be it irrelevant or relevant.
>  There is no information gained by the match.

Frankly, I'm kind of wary of justifying things by "information [being]
gained," unless that means something more formal to you than it does
to me.

Anyhow, in the 1 case, if you want to justfiy record matches by the
fact that they aren't matches at all, then that's okay, I guess. But
I'd also wonder about the inductive ⊤ as well. 'f tt = ...' does not
translate to 'f _ = ...' in that case, it translates to an inductive
eliminator, and such eliminators are questionable in their having
certain irrelevant arguments, due to the indexed case.

> 2. Matching against an empty type also yields no new information.
> Squashing an empty set leaves it empty.  Thus, absurd matching against
> irrelevant empty types is fine.

It's not necessarily fine, depending on what you care about. Allowing
absurd matching adds some junk terms that wouldn't otherwise be
admissible to certain types. I think Mishra-Lingers example is
something like:

    .⊥ → S

Without irrelevant empty elimination, the erasures of terms of this
type are exactly the erasures of S. With empty elimination, there is
an (many?) additional inhabitant, which we see as λ() and the like.

I'm not sure how critical this is, but it may be a useful property to have.

> 3. As you pointed out with your refl-example, irrelevant matching against a
> data type with just one constructor does yield new information in some
> cases.  This indeed makes my enterprise questionable (the new stuff I pushed
> yesterday).

But it is proof irrelevant, or can be made so if you don't care about
homotopy type theory. And you haven't really responded to that. I
really do think some of the issues here are that we're trying to cram
two things into one modality. The EPTS and similar stuff, at least in
retrospect, is built toward capturing parametricity in the naive, "I
don't do any case analysis or applications of this," sense. But the
stuff about ⊤, ⊥ and ≡ have to go into justifications about, 'I do
case analysis, but it doesn't matter at the end of the day.'

For ⊤, you can somewhat justify it, in that eta equality (if you have
it) means that any case analysis you do isn't case analysis at all.
But the others genuinely depend on doing the case analysis for their
results, and declaring them parametric by virtue of the type's
structure manifestly doesn't work in some cases (at least with regard
to erasure and whatnot). So it seems to me that it may make sense to
actually recognize that they aren't the same thing.

Perhaps I'm wrong, though. I should get around to writing my personal
implementation of this stuff to experiment, and put my money where my
mouth is.

-- Dan