[Agda] Pattern matching on irrelevant data

[Andreas Abel]

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.

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.

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

> is motivated by proof irrelevance, though, which
> supports only closed-term runtime erasure, hence the problem above.
>
> In some cases, it seems safe to do the former's erasure for the latter
> situation. But in general, they are different modalities, and if we
> try to jam them all into one, I think we'll end up with ad-hoc rules
> for how things work. For instance:
>
> data ⊤ : Set where
>    tt : ⊤
>
> foo : .⊤ → ℕ
> foo tt = 5
>
> If I normalize 'foo tt', I get 'foo _'. We might decide that it should
> evaluate to 5, and this is safe, but we cannot make a similar decision
> for the identity type, because it will cause my listing above to
> loop... unless we also keep track of what was 'erased' and use it to
> decide whether the irrelevant match in fact matches, and so on.

I agree, reduction should be closed under definitional equality.

Actually, I knew all this, I have been thinking about this 1,5 years 
ago, but I forgot.  Like the bear that keeps forgetting he will be stung 
when he goes for the honey.  The honey is just too tempting.

I think I will remove the new feature again and settle for the 
inconvenient truth that irrelevance on termination proofs has to be 
shown the hard way...

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/