[Agda] Proof irrelevance and self-realizing formulas

[Andreas Abel]

Hi Conor,

On May 30, 2009, at 1:32 PM, Conor McBride wrote:
> 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.

You make me curious.  I have read the Ripley cabinet and find myself  
already mentioned in an unglorious way [you are right, the non- 
transitive codata equality is implemented in MiniAgda].  I wish not to  
contribute again [why not? mistakes increase knowledge], so maybe you  
have a comment on the following proposal on how I want to achieve  
proof irrelevance for _==_ before I edge it into stone:

We consider proof-irrelevant equality with

   Gamma |- p, q : Id S s s'
   ---------------------------------- (eta)
   Gamma |- p = q : Id S s s'

and the abovementioned beta-rule for subst.  Now I am implementing NbE- 
style type-directed normalization. Here is the idea (boring equations  
omitted):

   nf {(x:S) -> T}  t = \x -> nf {[s/x]T} (t at s)    where s = up {S}  
x   (assume x fresh for t)
   nf {Id S s s'}    t = whnf t                             [results  
in * or refl if everything is welltyped]

   up {Id S s s'}   u = refl                               if  nf {S}  
s = nf {S} s
                               = *                                    
otherwise
   up {(x:S) -> T} u = Up {(x:S) -> T} u

   whnf (r s)                          = (whnf r) @ s
   whnf (subst _ _ refl _ p) = whnf p

   (\xt)@ s                    = whnf ([s/x]t)
   Up{(x:S) -> T} @ s = up {[s/x]t} (u (nf {S} s))

nf is supposed to compute a unique eta-long normal form. At function  
type it introduces a fresh variable which is immediately "reflected"  
via up.  up takes a neutral normal form u and eta-expands it.  At  
identity type Id S s s' it checks whether s and s' have the same  
normal form; in this case u is expanded to refl, otherwise to *.  The  
main idea, coming from NbE, is that up at function type delays the eta- 
expansion. Only when it is applied (last equation), eta-expansion  
continues.

nf can be used on open terms if all free variables x:S are replaced by  
(up {S} x) first.

So, indeed I am distinguishing between canonical and non-canonical  
proofs.  To be more precise, I am distinguishing between p : Id T t t  
and q : Id T t t' where t, t' have different normal forms. I am aware  
that this makes nf non-compositional, in particular, to compute nf(r  
s), the normal form of r is unusable.  For example:

   T = (x,y:S) -> Id S x y -> Id S x y
    t : T
    t x y p = p

   nf {T} t = \x\y\p.*

   nf {...} (t x x) = \p.refl

But since I only compute nf's to check for type equality, and throw  
them away afterwards, I think I am safe.

Indeed, there is some lazyness in my approach, but not in subst, but  
in eta-expansion (reflection/unquote).

Cheers,
Andreas