It should be possible to eliminate from Prop to a proof-irrelevant Set (e.g. a boxed Prop)

[guillaumebrunerie]

As the title says, it should be possible to pattern match on a Prop as long as the result is in a (definitionally) proof-irrelevant type, not only in a Prop. Examples of proof-irrelevant types that are not in Prop include in particular Box P : Set for P : Prop, or more generally any record for which all fields are proof-irrelevant, and also Pi-types whose codomain is proof-irrelevant, for instance (a : A) -> Box (P a).

[jespercockx]

In general, it seems quite hard to detect which types are 'proof-irrelevant'. It also seems counter-productive: isn't that exactly what we have Prop for?

For functions targeting Box P, you can make the pattern matching work by introducing the copattern .unbox. The same trick works for (a : A) -> Box (P a) after first introducing the variable a. So the motto is: if you want Agda to see that something is a Prop, you have to do sufficient (co)pattern matching to make that obvious to Agda.

[guillaumebrunerie]

I may be missing something but it seems quite easy to detect whether a type is proof-irrelevant or not. Just create two new metas of that type and check whether they are convertible. Eta for records and proof-irrelevance for Prop will imply that Box P is proof-irrelevant, and eta for functions will imply that (a : A) -> Box (P a) is proof-irrelevant as well.

I am aware of the copattern trick, but it doesn’t quite work for the case I have in mind. I would like to have a proof-irrelevant identity type but which lives in Set (because of the lack of Set/Prop polymorphism). It is easy to do that by simply Boxing the Prop-valued identity type, but then if I want to define ap I have to do it as follows:

ap : {A B : Set} (f : A → B) {a b : A} → a ≡ b → f a ≡ f b
unbox (ap f refl) = reflP

And the problem with this definition is that ap f refl no longer reduces to refl. I realize now that ap f refl is still definitionally equal to refl because of eta, but in my application I postulated a form of J for this identity type, together with a rewrite rule for the refl case (not sure if that’s safe…), and the rewrite rule doesn’t fire when applied to ap f refl. Maybe it should be an issue about rewriting not respecting eta instead.

But anyway, it still seems quite easy to me to just detect proof-irrelevant types.

[jespercockx]

I realize now that ap f refl is still definitionally equal to refl because of eta, but in my application I postulated a form of J for this identity type, together with a rewrite rule for the refl case (not sure if that’s safe…), and the rewrite rule doesn’t fire when applied to ap f refl. Maybe it should be an issue about rewriting not respecting eta instead.

That seems like it's a bug, can you please post it as a new issue?

But anyway, it still seems quite easy to me to just detect proof-irrelevant types.

I admit that it wouldn't be that hard to detect proof-irrelevant types. It still feels wrong somehow to do this, but I can't quite put my finger on why. I'll have to think about it some more.

[guillaumebrunerie]

I realize now that ap f refl is still definitionally equal to refl because of eta, but in my application I postulated a form of J for this identity type, together with a rewrite rule for the refl case (not sure if that’s safe…), and the rewrite rule doesn’t fire when applied to ap f refl. Maybe it should be an issue about rewriting not respecting eta instead.

That seems like it's a bug, can you please post it as a new issue?

See #3335 .

[andreasabel]

Prop is exactly the universe of proof-irrelevant Sets. Thus, I do not see why we should have another category of "things which are props but declared in Set".

The motivation seems to be the lack of sort polymorphism, see #3328. Maybe we should address this issue rather than adding some new heuristics.

[WolframKahl]

On Sun, Oct 28, 2018 at 06:05:52AM -0700, Jesper Cockx wrote:

I admit that it wouldn't be that hard to detect proof-irrelevant types. It still feels wrong somehow to do this, but I can't quite put my finger on why. I'll have to think about it some more.

My feelings are the other way around: I consider it counterproductive to be able to declare irreleveance, and even more counterproductive to have to do it for efficiency reasons, because that encourages premature optimisations. The compiler (including the type checker) should detect it whenever possible, and optimise it away as soon as possible.

[jespercockx]

My feelings are the other way around: I consider it counterproductive to be able to declare irreleveance, and even more counterproductive to have to do it for efficiency reasons, because that encourages premature optimisations. The compiler (including the type checker) should detect it whenever possible, and optimise it away as soon as possible.

Often the fact that a certain term is irrelevant is obvious to you as the Agda programmer but there's no way for Agda to figure this out from the code. If it's possible that you will use the term at any point in the future, Agda cannot (and should not) erase it. So any automatic detection of irrelevance would probably be very disappointing. (The alternative where Agda would eagerly erase things without asking and then complaining later when you try to use them is arguably worse). Another advantage of annotating irrelevant things, is that Agda can warn you when you use it accidentally in a non-erased position, instead of removing the irrelevance silently and causing hard-to-explain performance regressions.

On the other hand, maybe I'm wrong and it is possible to detect many proof-irrelevant types a such. On the top of my head, I can think of the following:

• The empty type
• The unit type
• Function types ending in a proof-irrelevant type
• Record types containing only proof-irrelevant fields
• Datatypes with disjoint constructor indices* where all non-forced constructor arguments are proof-irrelevant

Maybe you can think of more? It would be an interesting experiment to implement a check that detects all of these and replaces all terms of such types with 'dontCare' or such. Maybe this would significantly speed up typechecking time and make proofs easier, or maybe it would do nothing and all the extra work would end up slowing down typechecking. Either way would be interesting to know, though it probably depends a lot on the particular codebase.

(*) would need some extra checks for --without-K