[Agda] Proof irrelevance and self-realizing formulas

[Andrej Bauer]

On Thu, May 28, 2009 at 3:22 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
> I think the efficient compilation of Agda programs is an important and
> challenging question. However, I don't think we have to change the
> foundations to achieve this. And indeed proof-irrelevance (i.e. Prop) seems
> a good way to mark computationally irrelevant subterms.

Well, another point of my talk (oh my, I never put the slides up, here
they are now: http://math.andrej.com/2009/05/29/mathematically-structured-but-not-necessarily-functional-programming/
) was that the realizability interpretation automagically gives you
"thinned" types, i.e., it is possible to optimize away the boring
parts. This is good because the programer/logician does not have to
decide which things go into Prop and which into Set. I always thought
it was a bit strange that Coq wants me to tell which things are
computationally irrelevant--it should know by itself.

Isn't computational irrelevance an inherent property of a
proof/realizer/proposition? If so, then we shouldn't just go around
declaring things to be computationally irrelevant.

Perhaps, rather than thiking about adding a Prop to Agda, it would be
worthwhile thinking about having a "thinning" phase in Agda's
extractions, like RZ does. The idea is to chop off "boring" parts of
types and realizers/proofs. Essentially, the almost negative formulas
are boring (forall, false, true, and, and implication with boring
consequent). To get "interesting" code, you need sums and
disjunctions. Do you think such an idea would work? Perhaps Agda
and/or Coq already do this?

With kind regards,

Andrej