RFC: changed _/_ and _%_ to use irrelevant instance arguments

[MatthewDaggitt]

Can't believe how nicely this worked. No real hitches anywhere, all just sailed through. Definitely one of the most satisfying refactors I've done. As it's a proof of concept I've only done the refactoring for naturals and integers at the moment, with just the minimal necessary changes to the rational proofs. Those should massively simplify as well when we get round to it.

The one small design flaw exposed is that because the NonZero predicate ultimately falls back to the unit type, we have to import Data.Unit everywhere to get it to work. You can't seem to import instances publicly, so I think the best thing to do is actually to lift the predicates up to their own datatypes with the constructors declared as instances. That can be left for another time though.

On the Agda side, I would also kind of like to have proper anonymous instance arguments so we can write {{NonZero}} instead of {{_ : NonZero}}...

[gallais]

I agree with the motivations and the overall design, my only question is
wrt the specifics of achieving proof irrelevance. Should we use:

1. judgmental irrelevance like in this proposal (i.e. .)
2. or Prop
3. or an encoding that is guaranteed to be proof irrelevant (propositionally only)
   ?

I seem to remember that we were not too keen on adopting more "exotic"
features of Agda for the sake of more judgmental equalities on account of
not everyone being a maximalist when it comes to the base theory. Cf. #645

Option 3 could be achieved by mixing the current approach with a record
wrapper to make instance resolution work:

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit

isSuc : Nat → Bool
isSuc (suc _) = true
isSuc _ = false

data ⊥ : Set where

isTrue : Bool → Set
isTrue true = ⊤
isTrue _ = ⊥

record NonZero (n : Nat) : Set where
  field isNonZero : isTrue (isSuc n)

variable n : Nat

instance
  nonZero : NonZero (suc n)
  nonZero = record { isNonZero = tt }

f : {{NonZero n}} → ({{NonZero n}} → Nat) → Nat
f g = g

f' : {{NonZero (3 + n)}} → ({{NonZero (3 + n)}} → Nat) → Nat
f' g = g

f'' : ((n : Nat) -> {{NonZero n}} → Nat) → Nat
f'' g = g 2

Of course we would not have judgmental equality anymore but we
could still prove proof irrelevance.

[gallais]

Wait, I got confused by talks of "constructors" for NonZero but AFAICT
it's already computing to unit/empty. So we already have most of the machinery.
I guess my only suggestion then is to use the record wrapper & maybe ditch the
judgmental irrelevance. The wrapper should fix the problem with re-exporting
instances too.

[jespercockx]

Another benefit of defining the types for instance arguments locally is that it typically makes for much nicer error messages when instance search fails.

[MatthewDaggitt]

@gallais So you're suggesting something like the following?

private
  NonZero' : ℕ → Set
  NonZero' zero    = ⊥
  NonZero' (suc x) = ⊤

record NonZero (n : Nat) : Set where
  field isNonZero : NonZero' n

instance
  nonZero : NonZero (suc n)
  nonZero = record { isNonZero = tt }

I wonder if we can somehow avoid having the private definition...

[MatthewDaggitt]

@gallais one advantage of using judgemental irrelevance that's just occurred to me is that instance search doesn't have to be unique for judgementally irrelevant arguments. For example we could define instances as follows:

instance
  gcd≢0ˡ : ∀ {m n} .{{_ : NonZero m}} → NonZero (gcd m n)
  gcd≢0ˡ {m@(suc _)} {n} = ≢-nonZero (gcd[m,n]≢0 m n (inj₁ λ()))
  
  gcd≢0ʳ : ∀ {m n} .{{_ : NonZero n}} → NonZero (gcd m n)
  gcd≢0ʳ {m} {n@(suc _)} = ≢-nonZero (gcd[m,n]≢0 m n (inj₂ λ()))

lcm : ℕ → ℕ → ℕ
lcm zero        n = zero
lcm m@(suc m-1) n = m * (n / gcd m n)

This wouldn't work with your scheme right?

[gallais]

I wonder if we can somehow avoid having the private definition...

We could stick to using T instead of NonZero': T (not (n ≡ᵇ 0)).

This wouldn't work with your scheme right?

Correct.

[gallais]

Alternatively we could just define the NonZero view:

open import Agda.Builtin.Nat

data NonZero : Nat → Set where
  suc : (n : Nat) → NonZero (suc n)

instance
  nonZero : ∀ {n} → NonZero (suc n)
  nonZero = suc _

[JacquesCarette]

@gallais 's "I agree with the motivations and the overall design, my only question is
wrt the specifics of achieving proof irrelevance." is 100% my position too. I'm even Ok with instance arguments for this purpose, even though their pervasive use is quite dangerous (for performance and predictability).

On the various alternatives presented here: I have a slight bias towards using well-debugged features, especially for something so close to the core of the library (as Data.Nat is). That bias can be overcome by ergonomics. So 1) not having to write down the proofs when "it's obvious", 2) having the proofs never matter when deciding equality, 3) having multiple proofs around doesn't break things, are all powerful ergonomic factors that would sway me towards a solution that has all of them.

[MatthewDaggitt]

Hmm okay, so I've carried out several experiments and here are my thoughts:

1. Prop needs to be explicitly turned on, and therefore including it in the standard library would require everyone to turn it on so I think that's a no-go.

2. @jespercockx's point that defining the type locally results in more meaningful error messages is correct, but all the suggested approaches are doing that anyway. Whether we use a record/datatype/standard definition using ⊤ and ⊥ doesn't affect the error messages in any way. In the latter case, this is because if instance search fails then by definition it can't reduce NonZero n to ⊤ in the error message.

3. I don't think @gallais's other suggestion of using a record wrapper with a single constructor in order to get propositional proof irrelevance gets us anywhere. Even when using a record-wrapper Agda can only tell that the two instances are equal if the proof reduces, i.e. when n is in the form of suc n-1. However in this case the existing definition of NonZero reduces to tt anyway so there's no advantage over the current definition. If any of the found instances don't reduce, e.g. when we're proving the result of a function is non-zero, then Agda can't prove the two results are propositionally equal and therefore throws an error. Same story when considering equality.

So in summary, I think we should stick with the current simple definition of NonZero. The one remaining choice is then whether to use judgemental irrelevance where we consume NonZero proofs? Without it, we only have @JacquesCarette 2nd and 3rd criteria in a very limited set of circumstances. With it, we have them all the time.

In my honest opinion, I would vote in favour of using it.

As to whether people will be happy with judgemental irrelevance being used in the library, I only had a single query via the Agda mailing list on the proposed use of judgemental equality, and once the asker understood what it did they were fine with it being included.

Furthermore, the people who tend to be very concerned with the exact base theory they are using (looking at Martín Escardó/Andy Pitts et al.) do not use the standard library anyway. Martín has recently being asking on Zulip for the ability to cut down the Agda base theory even further, which suggests that he's not even happy with default Agda. So the chances of even the existing standard library fulfilling his criteria are pretty slim I would guess.

I guess the other argument is that we're the "standard" library and therefore using the features of "standard" Agda to improve the usability of the library should be fair game!

What are people's thoughts?

[JacquesCarette]

The argument "standard" Agda => "standard" library doesn't really move me: there are examples (even in Haskell) of standard features that end up not being used because they turn out to be a bad idea after all, even if they were loudly asked for.

Having said that: I think this particular experiment is worth doing 'in production'. All the signs are that this is going to work and help.

[MatthewDaggitt]

Okay, so it turns out a record-based definition does have one advantage. It means we don't have to have tt from Data.Unit in scope everywhere. This is actually a huge advantage, as otherwise either 1) the user has to import Data.Unit everywhere where they use proofs of non-zeroness or 2) we have to re-export tt from Data.Nat/Integer/Rational etc. which opens the path to conflicts with tt from Data.Unit.Polymorphic.

Therefore I've switched back to the record-based definition.

[MatthewDaggitt]

Okay, I'm happy with this in it's current state. If no one comments by tomorrow, I'll merge it in and start working on extending it to the rationals.