[ refactor ] enforce definitional proof-irrelevance of `Decidable`/`Recomputable` (in)equational hypotheses where possible

[jamesmckinna]

#2939 is yet another refactoring for one special case (plus knock-ons), but we should probably try to go through and systematically strengthen lemmas to take definitionally proof-irrelevant arguments of the form m ≤ n etc. where possible.

Issues:

• probably v3.0/breaking for such a large-scale overhaul?
• a lot of this (unfortunately; you live and learn ;-)) involves reverting changes previously made by me to insist on pattern matching on such proofs, even where unnecessary (and expensive: see comments on Why we should revert stdlib to --without-K instead of using --cubical-compatible #2792 about suppressing noUnsupportedIndexedMatch warnings)
• knock-on cost in eg. need for eta-expansion to ensure irrelevant arguments are consumed by functions presuming relevance
• @JacquesCarette 's comment about the pattern of matching-on-implicits which seems to be the only sensible way to do this
• codifying the change as a style-guide policy?

[JacquesCarette]

I'm actually against this change -- not that it is not the correct design, but rather that Agda's implementation of proof-irrelevance seems too shaky. Doing work with proof irrelevance "at scale" seems to always fail, in my experience. Plus some of the UX is sub-optimal.

[jamesmckinna]

Can you say a bit more about what "irrelevance 'at scale'" means? And how it fails?

[JacquesCarette]

Old and new experiences. Old: copumpkin's agda-categories stopped typechecking at some point, and it was in part because it used irrelevance pervasively. Now, the place that could not be repaired also involved with and heterogeneous equality, so it is hard to pinpoint what caused the actual problem. I spent days debugging, to no avail.

New: twice now with Conor, we used irrelevance in some medium-sized codes, because that is what we wanted to say. In both cases we had to keep turning on options (like irrelevant projections) to make some progress. And Agda blocked us on pattern-matching even if a data type had a single constructor, which destroyed our use of those to instruct Agda about type-level information that would otherwise disappear under computation. All of these only showed up 'much later', i.e. once we'd gotten very far with our development, were now in the middle of doing very complicated, and then basic machinery got in our way. Now we've removed irrelevance but try quite hard to be disciplined and never peek at things we should not have access to, no matter how tempting. I could try to do some archeology in the git history to be more precise.

My conclusion is that irrelevance has not been used enough, and there are some areas where it is not properly integrated. stdlib's use is very basic. But I am fearful that expanding its use will hit those rough patches. Furthermore, there is likely not a lot of pressure to fix irrelevance as a standalone feature because the equivalent feature in cubical works very well.

[Taneb]

Something to note about Data.Nat._≤_ in particular: it's heavy (defined as unary), it's thin (two values of type m ≤ n are equal), and it's recomputable (there is a function .(m ≤ n) -> m ≤ n. So, it's operationally useful to make it irrelevant, and we can get it back easily enough if we need it

[jamesmckinna]

Thanks @JacquesCarette for chapter-and-verse, and I can see that such experience might leave you feeling burnt.

But thanks also to @Taneb , who I think puts their finger on something I hadn't managed to say at the start: actually all of the relational hypotheses I had had in mind are Recomputable, usually a fortiori by dint of being Decidable. I'm sure that trying to make things irrelevant throughout stdlib would lead to problems, but here, with Nat and the other numerical datatypes, I think there are opportunities to leverage recomputability to good effect.

Separately, and I should return to this, I had been on a long kick about exploring the Recomputable space in order to recast old results about proof theory of classical PA in terms of intuitionistic HA. Nothing so fancy here, but an inkling that, where we can prove something to be propositionally Irrelevant, then (morally) we ought also to be able to posit, and exploit, it as being computationally irrelevant.

[JacquesCarette]

@Taneb 's argument fully convinces me: for Recomputable properties, we can make them irrelevant.

And the discussion also brought out something important (that I had not yet seen): my two negative experiences with irrelevance were both for desired irrelevance, i.e. irrelevance as an a priori desiderata, rather than irrelevance because it is a provable mathematical truth that these are irrelevant. So I can happily reverse my position and be for irrelevance here. And now I better understand exactly where I'm still not keen on it.

Success!

[jamesmckinna]

I've just closed two related Data.Fin.Base PRs until we had an agreed position to move forward with, which seems as though we have from the above discussion, but I think at the moment too many other things are going on, so I'd like to return to this issue, and subsequent PRs, at a later date.

[JacquesCarette]

I'm told that if we use Prop, we do get definitional proof irrelevance, based on sound theory. And that using it only for Decidable properties is a very sane thing to do. [Along with an opinion that fixing current modal irrelevance might never happen.]

[jamesmckinna]

I think that if we are to move stdlib to be based on Prop... that's a much wider design decision which would touch many many parts of the library, and so we should discuss that as a separate issue/Discussion topic... ;-)

Happy to not try to progress related PRs for the time being, but also to leave this issue open as well.

[JacquesCarette]

Certainly agree it is a bigger decision.

[jamesmckinna]

And #2998 , if it eventually lands, may signpost a/the way forward.