[Agda] Proof irrelevance and self-realizing formulas

[Conor McBride]

Hi Dan

You raise an interesting point.

On 29 May 2009, at 16:09, Dan Doel wrote:

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

There's room for both views. If we're in the business of
detecting/ensuring absence of computational content, we
can do so either when there is nothing to see, or when
we choose not to look.

It seems plausible, for example, to extend Prop with

Inhabited : Set -> Prop
witness : (x : X) -> Prf (Inhabited X)
exploit : (P : Inhabited X -> Prop) ->
          ((x : X) -> Prf (P (witness x))) ->
          (i : Inhabited X) -> Prf (P i)

P \/ Q then becomes Inhabited (Prf P + Prf Q) but,
crucially, one can only exploit inhabitation to
construct proofs, not values in sets. It's not clear
to me whether this is enough to cause the damage that
Shin managed to code up. Must try to find out: it
would be terribly interesting if the above is toxic.

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

Yes, there's a trend for this sort of thing: see also
work by Alexandre Miquel, by Bruno Barras and Bernardo,
and the odd bit of blogging by me and Edwin. I think
it's interesting to distinguish Pi-like quantification
from intersection-like quantification, in order to
support erasure, and hopefully, some sort of
parametricity.

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

Nathan and I had a chat about that rule at POPL 2008.
I'd been talking about some of Edwin's optimizations
and taking care to distinguish:
  (1) the information it's safe to throw away even
       when computing with open terms;
  (2) the information it's only safe to throw away
       when computing closed terms.
He then realised that the rule you refer to, which
performs the conversion check on open terms using
the erasure intended for runtime, brings disaster.
He fired up his typechecker and broke it.

Remember: when you compute with open terms, lies are
true. Nathan and Tim's erasure gets rid of equality
proofs at runtime, replacing subst by the identity
function, but if we extend that to open terms, any
false hypothesis allows us to break type safety,
e.g. by proving that Nat == Nat -> Nat, then casting
between them.

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

With a bidirectional type system, one should be able
to get away with just marking Pi: this gets pushed
into lambda, and inferred for functions in application.
Moreover, as any sensible compiler would perform
"nothing to see" erasure (for types, proofs, etc), one
need only bother to mark data that one is actively
choosing not to inspect at run time.

I think it could be a good thing to do, both as an
optimization, and as a potential source of parametricity.
It's not the same deal as smashing, because it permits
different observations in different phases: think vector
append, adding static lengths to get the length of the
result, but only needing to make nil-or-cons tests at
run time.

However, strictly fewer things are safe to erase for
open computation than are safe to erase at run time,
and proofs live in that gap. It takes something more
subtle to identify proofs judgmentally. Erasure
doesn't cut it. So that's a yes to

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

but no to the speculation about proof irrelevance at
the end.

One other thing, while the topic of "implicit" (ie
run-time erasing) Pi is in the air -- don't be tempted
to conflate this with "implicit" (argument inferring)
Pi (Agda's {x : S} -> T). There is no inclusion either
way between what is inferrable statically and what is
erasable dynamically. Not like in Hindley-Milner.

If you want to identify proofs judgmentally, there's
only one way to get it: laziness. Any strict evaluation
rules which demand a canonical proof to trigger
computation effectively discriminate between canonical
and non-canonical proofs. Note that absurdity elimination
has no such strict rules! If you want

  subst : (x y : X) -> x == y ->
          (P : X -> Set) -> P x -> P y

you had better not rely on

  subst _ _ refl _ p = p

for its evaluation behaviour (although you'd hope it
would still be true). This toxic mixture of proof
irrelevance and strictness is what was a wee bit broken
with Agda's experimental Prop (see archives). The same
bug can be found in Epigram 1 (must add it to the
collection of horror stories
http://strictlypositive.org/Ripley.pdf I started last
week). Once you can ensure that the form of a proof
has no influence on the course of open computation,
then you can identify proofs judgmentally: proof
irrelevance cannot just be decreed; it must be achieved.

Tread carefully

Conor