Tuple vs. Anon Ctor

Stream: lean4

[Mac]

I am curious as to why the tuple syntax (a,b,*) isn't used for the anonymous constructor instead of the esoteric ⟨a,b,*⟩. Currently, the tuple syntax is used for constructing a Prod, but the anonymous constructor can also build Prod. There is also the specific use case where the expected type is unknown and one wants a Prod. But that could also be covered by having the anonymous constructor syntax default to Prod in such cases. Thus, there seems to be immense benefit in having the tuple syntax just be the anonymous constructor syntax.

[Kevin Buzzard]

I often use ⟨a⟩ and ⟨⟩ which would be problematic with round brackets ()

[Mac]

Kevin Buzzard said:

I often use ⟨a⟩ and ⟨⟩ which would be problematic with round brackets ()

The () is already is another special syntax (for constructingPUnit) that could also be replaced with the anonymous constructor (since it can also construct PUnit and could default it in the case of an unknown expected type).

[Mac]

The (a) is somewhat of a concern. However, there are already places in Lean where (a) is distinct from a, so it could still represent the anonymous constructor. However, for the same reason, it could cause clashes. Thus, alternatively, I would propose that could be the one place where the esoteric ⟨⟩ brackets are keep (i.e., leave it as ⟨a⟩), since that is something of a special case.

[Mario Carneiro]

Rust uses (a,) for 1-tuples

[Mac]

Mario Carneiro said:

Rust uses (a,) for 1-tuples

Oh yeah, I've seen that before! With that solution, the tuple syntax could be use for anonymous constructors of any size without much trouble.