Coding style: `Π i, X i` vs `∀ i, X i` vs `(i : ι) -> X i`

Stream: mathlib4

[Yury G. Kudryashov]

Lean accepts all 3 of Π i, X i, ∀ i, X i, and (i : ι) -> X i. Do we have any official preference in Mathlib?

[Kyle Miller]

My preference:

1. If it's a proposition, use ∀ i, X i
2. If it's thought of as a product of types (like say you're working with the product of a family of groups), you can use Π i, X i
3. If you're writing a dependent function, use (i : ι) -> X i, it's more convenient, it's more clearly a function type, and it makes it easy to switch to and from being dependent.

There's also sigma types, with (i : ι) × X i and Σ i : ι, X i. I think the first is clearer, making it much more obvious that it's a pair, and it also is easy to switch it between a non-dependent product and a dependent product.

[Yury G. Kudryashov]

What about [∀ i, TopologicalSpace (X i)] vs [Π i, TopologicalSpace (X i)]?

[Yury G. Kudryashov]

Should we change it everywhere?

[Anatole Dedecker]

I agree that this one is trickier. Technically speaking it’s data, on the other hand I think using forall makes it closer to what one could say on paper.

[Jireh Loreaux]

Kyle's list also fits my exact preferences.

[Yury G. Kudryashov]

Should we add it to #style?

[Andrew Yang]

I thought Π i, X i was disallowed in lean4?

[Anatole Dedecker]

We added it back in Mathlib (I think ? Maybe earlier)

[Yaël Dillies]

(i : ι) -> X i is a weird non-mathematical notation, so I would be in favour of using it only when a type-ascription is necessary. It's otherwise unnecessarily wordy

[Yury G. Kudryashov]

@Kyle Miller What do you mean by "if you're writing a dependent function"? What's a good example?

[Yury G. Kudryashov]

@Yaël Dillies We use notation that isn't natural for mathematicians here and there (e.g., a linear algebra book would talk about $E \oplus F$, not $E \times F$)

[Yaël Dillies]

Regardless of mathematicality, it forces you to write out the type of the binder even when it can be inferred from context, which makes it a deal-breaker to me

[Eric Wieser]

(not with (i : _) -> X i, but obviously that's still uglier than either of the other two spellings)

[Kyle Miller]

Yury G. Kudryashov said:

What do you mean by "if you're writing a dependent function"?

I'm thinking about families of elements vs functions. They're the same thing, but mathematically we write the first as $s_i$ but the second as $s(i)$.

[Kyle Miller]

@Eric Wieser That made me think about whether (i :) -> X i would make sense to have. We already have (i :) is a typeless type ascription.

[Eric Wieser]

I don't think we want that; binders are not type ascriptions so there's no obligation to be consistent, and the notation itself seems pretty ugly anyway.

[Edward van de Meent]

The fact that they use the same symbol (:) suggests that they are similar, which (imho) should imply that they are consistent

[Edward van de Meent]

i suppose the notation being ugly suggests that (i :) shouldn't be used as a type ascription either...

[Notification Bot]

Sebastian Ullrich has marked this topic as resolved.

[Sebastian Ullrich]

What... I don't even know how I did that in the app

[Notification Bot]

Kyle Miller has marked this topic as unresolved.