Yesterday I had a nice chat with Matthieu about the upcoming Coq release that will have proof irrelevance. Proof irrelevance means that all objects of some proposition are equal (perhaps they are even convertible). The problem with proof irrelevance is that it can screw up fixpoint reduction when you have a proof of termination witnessed by something in Prop. The standard example of this is well-founded recursion where the recursion is over Acc.
Well-founded recursion is nice because it does structural recursion over a proposition. When extracting the program the proposition goes away and you are left with just the relevant computational parts. The problem occurs when well founded recursion is done inside an inconsistent context. Then the proof of termination may be based on false premises. If all the different termination proofs happen to be convertible, then the fixpoint can always unfold. Then you lose normalization.
What I vaguely understand is that the forthcoming version of Coq will have proof irrelevance. It will give you the choice between reducing these fixpoints and losing strong normalization, or not reducing these fixpoints and losing canonicity. Lack of canonicity would mean that there would be some natural numbers which don't begin with a constructor.
Up till now I had figured that Epigram 2 with its OTT logic would have everything I want: proof irrelevance, functional extensional equality, etc. Matthieu asked me what OTT loses. I said that it loses inductive types in Prop, but I figured that was no big deal. Then Matthieu asked me how to do well-founded recursion in OTT. The problem is that Acc is inductively defined. I had assumed that there would be some non-inductive replacement for it, but now it is not looking that way.
I believe I was told that all propositions in OTT are double-negation stable. I thought that maybe if I prove that Acc is stable, then I would get some insight into how to define it without induction. The problem is that I cannot prove that Acc is stable. This really surprised me. It is my first example of something that is proof irrelevant (assuming functional extensional equality), but not double negation stable.
Matthieu pointed me to the a lemma done by the Chalmers people that stability of Acc implies Markov's principle. I redid this proof in Coq to see the result for myself. Since Markov's principle isn't constructive, we cannot expect Acc to be stable. Since (i believe) that all props in OTT are stable, that means that Acc cannot be defined in Prop in OTT.
When squash types are added to OTT, then these new squashed propositions are not double negation stable. One one solution may be to define Acc in Type and then squash it into Prop. But I don't know what the reduction properties would be, or if this would even work.
I'm starting to think that the following four things are incompatible
- Well-founded recursion
- Proof irrelevance
By well-founded recursion, I mean being able to do structural recursion over propositions to product a value in type, such as recursion over Acc (of course if you put Acc in Type then everything works, but we don't want to do that because we want to strip Acc during program extraction). By proof irrelevance I mean that all proofs of the same proposition are equal (and maybe I mean that they are convertible). By canonicity I mean that all normalized inductive objects in the empty context begin with a constructor.
Coq currently leaves out proof irrelevance. The forthcoming version of Coq will leave out (at your choice) either canonicity or normalization (as I understand). Finally, OTT leaves out well-founded recursion (as I've defined it).
Perhaps OTT plus squash types will give all 4 properties, but I don't think I would bet on it.