[Agda] Pattern matching on irrelevant data

[Andreas Abel]

On 04.10.11 5:13 PM, Dan Doel wrote:
> 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.

More formally,

   Squash (A \times B) \cong Squash A \times Squash B.

> 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.

I agree, this is why irrelevant matching on the inductive \top is now 
experimental with little hope of survival.

>> 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.

What use is in .\bot if you cannot eliminate it?

Formally elimination it is justified by

    Squash \bot \cong \bot

Nothing changes when you squash an empty set.

The question is whether erasure of irrelevant abstractions is so useful 
in the end.  I talked to Pierre Letouzey, who has done Coq's erasure, 
and he said he eta-expands stuff rather than eta-contracting it.  He 
retains dummy abstractions to preserve termination in a cbv language.

>> 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.

Indeed.  We need a second notion of "external irrelevance", which is 
justified by a closed term model, and allows us to do proof irrelevance 
for the identity type and stuff alike it.

> 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.

What is implemented in Agda currently is not EPTS, but .A is simply an 
internal version of the squash type.  That's the way to think about it. 
  This is the model behind Pfenning/Reed style irrelevance.

I have not understood the interplay between parametricity and typed 
equality.  If someone does, tell me, that could be the basis of a 
valuable new Agda feature!

> 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.

I am trying to move towards EPTS, but I still have not found a model 
that integrates EPTS-style irrelevance with typed equality.  Working on 
it, but I find it quite difficult.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/