[Agda] Performance issues and code structure.

[Dan Doel]

On Monday 28 September 2009 5:52:29 am Nils Anders Danielsson wrote:
> > [...] --proof-irrelevance [...]
> 
> I believe that --proof-irrelevance is broken and should not be used.
> Ulf, can you verify this? If this is true, then the flag should be
> disabled.

Well, at the very least, it has some oddities. For instance...

  data _==_ {A : Set} (x : A) : x -> Prop where
    refl : x == x

Without proof irrelevance, the following doesn't work:

  K : {A : Set} {x : A} {P : x == x -> Set} (p : x == x) -> P refl -> P p
  K p Pr = Pr

You must match against p (which is refl, of course). With --proof-irrelevance, 
though, the above is accepted (which is, perhaps, not surprising). You can 
also write the more general:

  foo : {P : Prop} {Q : P -> Set} {p q : P} -> Q p -> Q q
  foo Qp = Qp

However, if you also turn on --type-in-type, the above K goes back to not 
working, and you must match against p for it to work. So --type-in-type seems 
to turn off --proof-irrelevance (assuming I'm specifying them right; putting 
them both, space separated, in an OPTIONS pragma). :)

I guess that's because Prop becomes Set when --type-in-type is used. For 
instance, it enables you to write:

  data _<=_ : Nat -> Nat -> Prop where
    z<= : {k : Nat}   -> zero <= k
    s<= : {m n : Nat} -> m <= n -> suc m <= suc n

Which normally isn't allowed, even with non-proof-irrelevant Prop, because the 
constructors contain members of a Set-typed type (which is a bummer; inductive 
relations like that are a bit more luxurious to use (in Agda) than their 
recursive brethren).

If it's really broken, I suppose I won't use it though. I was mainly 
interested in it because lots of categories appear to be shaping up as having 
objects/morphisms involving records of values and (equality) proofs about 
those values, and I wasn't relishing proving things like 'trans (cong f foo) 
(trans bar refl) == bar', but instead just getting (the equivalent of) that as 
a given. :)

-- Dan