Zulip Chat Archive

Stream: general

Topic: Priorities of × and ≃


view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 20:23):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 20:33):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 20:34):

Consider also α → β ≃ γ

view this post on Zulip Scott Morrison (Jul 05 2019 at 20:35):

That one is just clearly ambiguous and needs parentheses.

view this post on Zulip Scott Morrison (Jul 05 2019 at 20:35):

(because neither interpretation would be "dumb")

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 20:35):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 20:36):

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

view this post on Zulip Scott Morrison (Jul 05 2019 at 20:36):

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

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 20:36):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 20:37):

Sadly no

view this post on Zulip Mario Carneiro (Jul 05 2019 at 20:37):

although we can certainly try to impose a convention

view this post on Zulip Yury G. Kudryashov (Jul 05 2019 at 20:49):

Conventions don't help newbies.

view this post on Zulip Floris van Doorn (Jul 08 2019 at 18:58):

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.

view this post on Zulip Floris van Doorn (Jul 08 2019 at 19:01):

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.

view this post on Zulip Floris van Doorn (Jul 08 2019 at 19:05):

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

view this post on Zulip Floris van Doorn (Jul 08 2019 at 19:09):

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.

view this post on Zulip Mario Carneiro (Jul 08 2019 at 19:25):

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


Last updated: May 14 2021 at 03:27 UTC