[Agda] Pattern matching on irrelevant data

[Dan Doel]

On Tue, Oct 4, 2011 at 2:25 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> More formally,
>
>  Squash (A \times B) \cong Squash A \times Squash B.

This is easily justified by Squash being applicative.

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

You cannot eliminate it to produce relevant things. You can eliminate
it in irrelevant positions.

> Formally elimination it is justified by
>
>   Squash \bot \cong \bot
>
> Nothing changes when you squash an empty set.

This is not provable in the same way as the product record. In fact, I
don't think it's even possible to prove the weaker:

    ○ (○ ⊥ → ⊥)

without the same postulate that we take for irrelevant record projections.

So this is kind of like saying, "we can eliminate squashed empty
relevantly because we can." I can tentatively agree that this is safe
due to squashed empty being itself empty. But there's another question
of whether an algorithm should be able to look at an irrelevant,
static argument to determine whether it's allowed to just fail
(because the impossible happened). We're violating a phase separation
by allowing absurd matching on an irrelevant ⊥.

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

I don't know how useful it actually is.

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

Another issue, of course, is whether this covers things like
well-founded induction. You end up tying the knot through something
that's supposed to be irrelevant in that case, which makes things
difficult, I think.

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

Yeah, I know Agda doesn't have the full EPTS stuff yet. And I don't
know the solution to the problems.

The squash type here is just an internalization of the modality,
though. Agda's . isn't any more useful than a squash operator
currently, but you still have to decide how the modality works, and
whether it's shooting for parametricity or proof irrelevance. The two
blend together a lot, I think, so it can be hard to tell the
difference (Sheard and Mishra-Linger thought they could do proof
irrelevance with their stuff in earlier papers, but I think that
turned out to not quite be the case).

-- Dan