Priorities of × and ≃

Stream: general

[Yury G. Kudryashov]

Hi, currently α × β ≃ γ is parsed as α × (β ≃ γ) while it seems more natural to interpret it as (α × β) ≃ γ.

[Mario Carneiro]

I realize this looks odd, but type constructors deliberately have low precedence. The × symbol has approximately the same precedence as ∧, because they are used to put together basic types. This is below =, which is near ≃, and * lies above that

[Mario Carneiro]

Consider also α → β ≃ γ

[Scott Morrison]

That one is just clearly ambiguous and needs parentheses.

[Scott Morrison]

(because neither interpretation would be "dumb")

[Yury G. Kudryashov]

For → this order makes sense because it is often used in the sense "implies".

[Mario Carneiro]

α × (β ≃ γ) also makes sense if you want to produce two things

[Scott Morrison]

then you should have defined a structure with named fields, so people didn't need to listen to .1 and .2 :-)

[Yury G. Kudryashov]

/me wonders if it's possible to require explicit parentheses in some cases.

[Mario Carneiro]

Sadly no

[Mario Carneiro]

although we can certainly try to impose a convention

[Yury G. Kudryashov]

Conventions don't help newbies.

[Floris van Doorn]

There is no reason that ≃ has a precedence near =.
≃ only acts on types, so it makes sense for it to have lower precedence than (some) type formers. This is not the case for =, which should (almost) never be used on types, so it should have a precedence higher than all type formers.

[Floris van Doorn]

In the Lean 2 HoTT library the precedence of ≃ was 25, compared to × having 35 and = having 50.
https://github.com/leanprover/lean2/blob/master/hott/init/equiv.hlean#L304
https://github.com/leanprover/lean2/blob/master/hott/init/reserved_notation.hlean#L145-L208

This results in some nice statements, like

definition prod_equiv_prod [constructor] (f : A ≃ A') (g : B ≃ B') : A × B ≃ A' × B'

https://github.com/leanprover/lean2/blob/master/hott/types/prod.hlean#L215

I do not recall ever running into issues/confusion because of these conventions.

[Floris van Doorn]

Note: → did (and should) have a lower precedence than ≃, and you still require parentheses for them. This can cause confusion, but that's no reason to have the (in my opinion) wrong order for × and ≃. Example :

definition arrow_equiv_arrow_right' [constructor] (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B')

(the parentheses in the type of f1 are only for readability)
https://github.com/leanprover/lean2/blob/master/hott/types/arrow.hlean#L51

[Floris van Doorn]

I think we should change the precedence of ≃ to 25. I have also run against this issue before (maybe with two different tokens). This is only a mathlib change, not a core change.

[Mario Carneiro]

Oh, if it's a mathlib-only change then go ahead. I agree that the precedence in equiv.lean feels consistently the wrong way around