Precedence of negation and sigma/exists syntax

[MatthewDaggitt]

As pointed out by @jamesmckinna when trying to update PFLA to use v1.7 of the library (analysis below is his), currently you can't use ¬_ from Relation.Nullary and ∃[ A ] B syntax (i.e. ∃-syntax) from Data.Product without bracketing because the precedences are the wrong way around:

agda-stdlib/src/Relation/Nullary.agda

Line 23 in ed8efad

infix 3 ¬_

agda-stdlib/src/Data/Product.agda

Line 78 in ed8efad

infix 2 ∃-syntax

So you can't write ¬ ∃[ A ] B. The reason that it broke from v1.3 to v1.7 is that the fixity of the ∃-syntax was first added by @Taneb in a0b06ba

So it looks like we need to switch the precedences somehow (Σ-syntax included). Anyone have any thoughts? We should probably have a look at what else has precedences in at the 2/3/4 level...

[jamesmckinna]

@wenkokke You remarked on Monday that PLFA was now up-to-date with std-lib. How did you resolve/deal with this particular issue?

[wenkokke]

We added parentheses, e.g., we now write ¬ (∃[ A ] B) and ∃[ A ] (¬ B). Not great, but better than staying in the past.

[jamesmckinna]

Just did a quick Friday-afternoon experiment: changing the precedence of negation to

infix 2 ¬_

incurs only one knock-on change, namely in Data.Fin.Properties.¬∀⟶∃¬-smallest, with type

∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                 ¬ (∀ i → P i) → ∃ λ i → (¬ P i) × ((j : Fin′ i) → P (inject j))

(we now need brackets around (¬ P i) in addition to the ((j : Fin′ i) → P (inject j)) of the original)
while the examples of

example1 : (A : Set a) → (A → Set b) → Set (a ⊔ b)
example1 A B = ¬ Σ[ x ∈ A ] B x

example2 : (A : Set a) → (A → Set b) → Set (a ⊔ b)
example2 A B = Σ[ x ∈ A ] ¬ B x

example3 : (A : Set a) → (A → Set b) → Set (a ⊔ b)
example3 A B = ¬ Σ[ x ∈ A ] ¬ B x

shows that we have 'what we want' (or: what I/we think we might want).

But it (perhaps) feels a fragile move to have ¬, Σ (and _×_) all at the same precedence level. Thoughts?

[jamesmckinna]

Oh, and moving Σ and _×_ etc. to level 3 (and negation to level 2) breaks way too many things... there's the fragility... :-(

[JacquesCarette]

I'm pretty sure we'd have to move everything up a level if you want negation to have its own. That's a mighty big change. I think there was discussion of allowing fractional levels?

[jamesmckinna]

AFAIU, fractional levels were implemented. But moving "everything up a level" actually breaks things, with negation at 2, products at 3 etc. So the only workable (but yes, horrible?) solution that I found was to have negation at the same level. Hence the 'Friday afternoon' nature of the experiment. Not one I would pursue in earnest.

That said, @Taneb was there a(nother) reason for choosing the precedences which you didin the first place?

[JacquesCarette]

I thought the the breakages were because things now at level 3 would need to go to 4, and so on, so that if negation was at level 1.5, things would not break so much?

[Taneb]

@jamesmckinna

That said, @Taneb was there a(nother) reason for choosing the precedences which you didin the first place?

My only reasoning was to match Σ-syntax's fixity.

[jamesmckinna]

Suggest we close this for v2.0, and re-open a more general issue about precedences?
Else consider the matter closed entirely, with the PLFA niggle... just that?

[MatthewDaggitt]

Hmm so fractional levels are fine and implemented in Agda for exactly this use case. @jamesmckinna would using a fractional precedence work in your experiment?

[jamesmckinna]

Re: fractional precedence? I honestly don't know, and TBH think it is more hassle than it is worth, compared to eg the PLFA-authors' workaround. Plus we now have good symbols for negated existentials, so maybe the better solution would be to give those good syntax declarations as well?