[Agda] Status of Prop

[Conor McBride]

Hi Andreas

On 5 Sep 2008, at 09:10, Andreas Abel wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hi Conor,
>
> is not extensionality for singleton types missing here to make your
> example work?
>
>> data TT : Prop where
>>   tt : TT
>>
>> moo : TT -> Set
>> moo tt = Nat
>>
>> boo : {x : TT} -> moo x
>> boo = zero -- goes wrong
>
> If you have eta for TT, then you know that x is definitionally  
> equal to
> tt, and then moo x = Nat, definitionally.

But that's exactly the problem. The flag --proof-irrelevance PI gives us
exactly the definitional equation you want, but boo doesn't typecheck
because pattern matching on TT is strict.

The message:
   It's not enough to /decree/ an eta-law (eg, PI) by adding it to
   type-directed quotation/conversion. You must also ensure
   that computation respects it by being suitably lazy.

Consequence: eta-laws are good for negative types like (x : S) -> T,
and records, but less good foor positive types. That's why eta-laws
for datatypes --- which are positive --- are bad news in general,
even if a few also happen to have negative encodings.

Of course, if I'd made moo lazy by writing

   moo x = Nat

we'd have been ok. And for record types, one can always translate
patterns into projections: that's what would have to be done to make
record patterns work. It looks like quite a job to implement that
translation, especially if there are more patterns in the fields of
the record. I'm guessing that's why it hasn't been done yet --- it
would be nice, but it's not vital.

But here's a function which is a little harder to make lazy.

   data ILove : Nat -> Prop where
     fave : ILove (suc (suc (suc zero)))

   data _^_ (X : Set) : Nat -> Set where
     [] : X ^ zero
     _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n

   infixr 40 _::_

   happy : {n : Nat} -> ILove n -> Nat ^ n
   happy fave = zero :: suc zero :: suc (suc zero) :: []

It's possible to get over this problem. My point is just that the price
of proof irrelevance is laziness, and laziness takes hard work.

All the best

Conor