[Agda] Proof irrelevance and self-realizing formulas

[Dan Doel]

On Friday 29 May 2009 4:24:22 am Shin-Cheng Mu wrote:
> Hi,
>
> I've been eavesdropping this interesting discussion for 2 days,
> while building up courage to interrupt and ask novice questions
> again... :)
>
> Is what I say below correct?
>
> There are now at least 3 interpretations of "proof irrelevance"
> I have heard of:
> ...

If I may also interject, as I'm also far from an expert:

There seems to be a school of thought that argues that assigning "irrelevance" 
to certain _types_ is wrong-headed in general. Rather, the correctness of 
erasing certain terms from the computation (which is, correct me if I'm wrong, 
the point of irrelevance) is dependent on how they're used, not whether their 
types are in Prop or Set.

I'm thinking of Erasure and Polymorphism in Pure Type Systems [1], since 
that's the paper I've read, but I think I've seen the line of thought 
elsewhere. And I do realize that the main body of the paper isn't about proof 
irrelevance, but they do give a rule at the end for what it might be in their 
system, and needless to say, it has nothing to do with particular universes of 
types, and rather to do with their two sorts of typing judgments and such:

   M :r A (M is a runtime-relevant term with type A)
   M :c A (M is a term with type A whose value is computationally irrelevant)

So, I suppose my question is whether anyone here is familiar with approaches 
to proof irrelevance like this, and how well do they work? It seems like such 
an approach might let you use proofs involving disjunction, for instance, 
since if you go on to inspect such a proof in a way that matters to your 
computation, it necessarily becomes relevant, but if you don't, you can erase 
it just as well as anything else which would be considered irrelevant in some 
other system. However, perhaps I'm too optimistic about that, or perhaps the 
downsides to the approach are too great (for instance, having to annotate 
lambdas, pis and applications with their relevance; although perhaps there's 
some way to make that less arduous?).

Thanks,
-- Dan

1: http://web.cecs.pdx.edu/~sheard/papers/FossacsErasure08.pdf