Replace irrelevance with Prop

[jespercockx]

As discussed in agda/agda#8557, I made an attempt at replacing the use of irrelevance for the definition of the empty type with Prop. It seems to work rather nicely, with the main disadvantage being that --prop needs to be enabled in basically every file (I haven't yet checked which ones exactly, just enabled it globally for now). On the other hand, this would allow the standard library to adopt the --no-irrelevance flag once agda/agda#8575 is merged.

I'm curious to hear what the standard library developers think of this potential change, in particular @MatthewDaggitt @jamesmckinna @fredrikNordvallForsberg

[jespercockx]

One annoyance when implementing this change is that I could not simply use ⊥ = Irrelevant Empty but had to define Empty as a datatype in Prop instead. It is possible to make things work with the old definition but it requires a bunch of auxiliary definitions so I decided to go for the simpler version instead. It would be possible to go back to defining ⊥ = Irrelevant Empty if/when agda/agda#8548 gets merged.

[Taneb]

Thanks for looking into this! It looks like CI is failing because the README files are a separate Agda library, and also will need --prop enabled throughout. The .agda-lib file is at doc/standard-library-doc.agda-lib.

In addition to Data.Empty, we also use irrelevance for types like NonZero and Positive in Data.Nat, Data,Integer, Data.Rational.Rational, especially in instances. How does instance search interact with Prop? It's not something I've ever taken the time to play with.

As a further point of discussion, do we want to mark things that are provably but not necessarily "obviously" propositional, like _<_ in Data.Nat, as Prop? But that doesn't need to (and probably shouldn't) happen in this PR

[shhyou]

@Taneb Make _<_ live in Prop is similar to asking all _<_ uses be marked as irrelevant (but better), regardless of whether it's stdlib code. I'd argue that this is a huge burden on the clients of _<_ because they can't match on _<_ and have to manually match both indices first.

[jespercockx]

So for other uses of irrelevance for NonZero and Positive and such, I didn't touch them yet because they don't break with my proposed fix for agda/agda#8557. But if we want to migrate the standard library from irrelevance to Prop fully then I agree we should also consider them. There are a few options to migrate them:

• The least invasive change would be to simply replace every function type of the form .A -> B (and .{{x : A}} -> B etc) with Irrelevant A -> B (and {{Irrelevant A}} -> B etc.). This should be a drop-in replacement for irrelevant functions as long as you don't mind the extra verbosity.
• Another possible change would be to update the definition of types such as NonZero and Positive to already include the Irrelevant in their definition. It's less syntactic noise on the use site but you lose the flexibility to not use irrelevance for arguments of this type.
• The third possibility is to actually buy into Prop for user-facing code as well and define NonZero and friends to live in Prop themselves. In some way this is the most elegant (no need to bother with Squash and Irrelevant type wrappers) but you have to deal with the fact that Prop is not Set and many existing functions will not work with it and so need to be duplicated. This is why the Rocq people have been working hard to implement sort polymorphism. Since we don't have that (yet) in Agda I would not recommend this course of action, but I'm mentioning it for completeness' sake.

[jespercockx]

Regarding instance search for Prop: it should work exactly the same as instance search for irrelevant arguments, with the same caveats around it possibly discarding the wrong instances when there are multiple overlapping candidates.

[JacquesCarette]

Doesn't Data.Empty.Polymorphic need the same surgery?

[jespercockx]

Doesn't Data.Empty.Polymorphic need the same surgery?

I don't see any direct use of irrelevance in that file, so I don't think so?

[JacquesCarette]

Oh right, I forgot that that one came from before Empty was made irrelevant.

[JacquesCarette]

So the removal of this function seems to be the biggest change, as far as 'breaking changes' go. Though if this is new to v2.4, it is fine, since that is as-yet unreleased.

[shhyou]

It's 2.2. https://agda.github.io/agda-stdlib/v2.2/Relation.Nullary.Recomputable.html#1532

[JacquesCarette]

And, of course, the build failed because test-stdlib failed. Maybe --prop can't be compiled, so that's the problem?

[gallais]

I'd like to hear from people like @martinescardo on whether they're using the stdlib
and whether buying into Prop would be a no-go for them.

We may need to go back to a bot that's only propositionally irrelevant.

[martinescardo]

I'd like to hear from people like @martinescardo on whether they're using the stdlib and whether buying into Prop would be a no-go for them.

We may need to go back to a bot that's only propositionally irrelevant.

I confirm that I am not using stdlib and that Prop is a no-go for me, and so is irrelevance. But because they can be disabled, they don't bother me.

[jamesmckinna]

@jespercockx I think that there are two things at stake here:

• the main agda development resolving the issues around irrelevance
• fixing stdlib's deployment of this technology

I think for the time being, the minimally invasive reversion would simply be to remove/deprecate (or else put in an unsafe module) both Data.Irrelevant.recompute (and its re-exports elsewhere), and its single use in (re-)defining Data.Irrelevant._>>=_.

As far as I understand, the use of Data.Irrelevant in defining ⊥ = Irrelevant Empty (which doesn't need irrelevant-projections; specifically, ⊥-elim-irr remains definable, unless you're saying that even that definition is unsafe?) is otherwise harmless (and hence all the uses, via contradiction, contradiction-irr) in Relation.Nullary.Negation and Relation.Nullary.Decidable), and nowhere else do we make non-trivial use of irrelevant-projections, IIUC/IIRC.

The move to Prop is such a large-scale change that I think we'd want to discuss this at length before proceeding...

[jespercockx]

@jamesmckinna All right, that makes sense to me. I agree that removing irrelevance or replacing it with Prop is a major change and one that shouldn't be rushed. If the other library developers are fine with this, I can prepare an alternative PR that just puts recompute and _>>=_ in a separate (unsafe) module and keeps the rest of the irrelevance usage intact for now.

[jespercockx]

I'm converting this to a draft for now, feel free to close it and/or use it as the basis for future experiments with Prop in the standard library.