## Stream: general

### Topic: Notation criticisms

#### Kind Bubble (Jan 10 2023 at 16:40):

Last week I used this notation:

notation "Σ" "(" x ":" X ")" ":" F => Σ' (x : X), F
notation "Π" "(" x ":" X ")" ":" F => forall (x : X), F
notation "λ" "(" x ":" X ")" ":" f => (fun (x : X) => f)
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "∀" "(" x ":" X ")" ":" p => ∀ (x : X), p
notation "∃" "(" x ":" X ")" ":" p => ∃ (x : X), p
notation "*" => Unit.unit
notation "⊛" => Unit
notation x "≡" y => Σ(_:x=y):⊛


I would like people to criticize it or appraise how difficult it would be to follow this.

I was a bit irked that the notation wasn't already symmetrical or more uniform but I might have to let that go since it takes a lot of effort to read the modifications.

#### Eric Wieser (Jan 10 2023 at 16:47):

I was a bit irked that the notation wasn't already symmetrical or more uniform

What do you mean by this?

#### Trebor Huang (Jan 10 2023 at 16:55):

Changing notations is the greatest sin, it is greater than the sum of all the sin possibly committed by bad notation.

#### Kind Bubble (Jan 10 2023 at 17:16):

e.g. on the left there is : where on the right there is either , or =>. On the left there is no Sigma' just Sigma. On the left everything is a symbol and there are no words of different length.

I'm convinced it's esoteric now though so it's gonna have to go.

#### Sky Wilshaw (Jan 10 2023 at 17:18):

These pieces of notation have different purposes. For example, : is used for type ascription and only type ascription, so whenever you see : you instantly know we have an expression of a particular type.

#### Sky Wilshaw (Jan 10 2023 at 17:19):

In your notation, : can mean the type of an expression or (for example) the body of a function binder.

#### Sky Wilshaw (Jan 10 2023 at 17:20):

Every other programming language I've used makes this kind of distinction to aid readability, so I don't think it can really be called esoteric.

#### Sky Wilshaw (Jan 10 2023 at 17:21):

Also note that your usage of notation is not what lean "wants" you to do - using Sigma' is in some sense a sign you should be making your own structures or inductives.

#### Eric Wieser (Jan 10 2023 at 17:22):

where on the right there is either , or =>

I also find this sllightly strange, but only because I've been trained on Lean 3 where it's , everywhere. Perhaps someone more familiar with lean4 has a good explanation for what makes fun binders special.

#### Sky Wilshaw (Jan 10 2023 at 17:23):

Using => and -> for functions matches most other programming languages. Lean 4 seems like a step in that direction.

#### Sky Wilshaw (Jan 10 2023 at 17:23):

∀ has no other-language equivalent, so presumably it's just spelled the mathematical way.

#### Eric Wieser (Jan 10 2023 at 17:24):

I guess the fair comparison is to use the new Lean4 notation

• (a : α) → P a not ∀ a, P a or forall a, P a
• (x : X) × F not Σ (x : X), F

and then the use of arrows is consistent (i.e. the commas are gone entirely)

#### Eric Wieser (Jan 10 2023 at 17:27):

∃ doesn't fit that model though; unless you write ∃ x, p x as Exists fun x => p x.

#### Sky Wilshaw (Jan 10 2023 at 17:27):

I guess we just need an infix operator for ∃ then!

#### Sky Wilshaw (Jan 10 2023 at 17:28):

The : syntax for function bodies is not without precedent, though - Python uses it. But notably, Python doesn't have (often) type ascriptions.

#### Eric Wieser (Jan 10 2023 at 17:29):

Python's type ascriptions were added as an afterthought after most of the notation was already allocated, so are not really a good example to compare to

#### Sky Wilshaw (Jan 10 2023 at 17:29):

Yeah, absolutely.

#### Eric Wieser (Jan 10 2023 at 17:30):

I do wonder if ∃ x, p x should be spelt ∃ x => p x for consistency

#### Sky Wilshaw (Jan 10 2023 at 17:30):

I think that would be nice to be honest

#### Sky Wilshaw (Jan 10 2023 at 17:34):

But then it's less consistent with ∀. Before I learned type theory, I thought that ∀ and ∃ were basically the same kind of object, and it was nice to have their syntaxes align.

#### Floris van Doorn (Jan 10 2023 at 17:36):

If Σ (x : X), F x is spelled (x : X) × F x then should ∃ x, p x be spelled (x : X) ∧ p x?

#### Sky Wilshaw (Jan 10 2023 at 17:36):

Kind Bubble said:

there are no words of different length.

I don't think this is really an issue. The expressions we're talking about are really fundamentally different objects, and there's no reason (other than aesthetics) that they need to have the same length.

#### Eric Wieser (Jan 10 2023 at 17:38):

(x : X) ∧ p x certainly sounds like notation that should exist, even if we choose not to prefer it in mathlib.

#### Sky Wilshaw (Jan 10 2023 at 17:39):

I do like it, but at least to me that notation suggests X : Prop

#### Sky Wilshaw (Jan 10 2023 at 17:39):

Almost like a Sigma' where both types are Props

#### Eric Wieser (Jan 10 2023 at 17:40):

Yes, I guess that would have the weirdness where (x : X) ∧ (y : X) ∧ p x y is legal but (x : X) ∧ (y : X) is not

#### Eric Wieser (Jan 10 2023 at 17:40):

But maybe that's already the case for ×?

#### Kind Bubble (Jan 10 2023 at 17:41):

Eric Wieser said:

I guess the fair comparison is to use the new Lean4 notation

• (a : α) → P a not ∀ a, P a or forall a, P a
• (x : X) × F not Σ (x : X), F

and then the use of arrows is consistent (i.e. the commas are gone entirely)

Oh I didn't know this works for dependent types.

#### Shreyas Srinivas (Jan 10 2023 at 18:56):

Since notation seems to allow all sorts of new syntactic statements, is it possible to confuse lean with ambiguities? Or is it the opposite, are there limitations around what is allowed inside notation

Last updated: Aug 03 2023 at 10:10 UTC