Notation criticisms

Stream: general

[Kind Bubble]

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]

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

What do you mean by this?

[Trebor Huang]

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

[Ruben Van de Velde]

But what about the cos?

[Kind Bubble]

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]

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]

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

[Sky Wilshaw]

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]

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]

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]

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

[Sky Wilshaw]

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

[Eric Wieser]

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]

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

[Sky Wilshaw]

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

[Sky Wilshaw]

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

[Eric Wieser]

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]

Yeah, absolutely.

[Eric Wieser]

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

[Sky Wilshaw]

I think that would be nice to be honest

[Sky Wilshaw]

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]

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

[Sky Wilshaw]

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]

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

[Sky Wilshaw]

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

[Sky Wilshaw]

Almost like a Sigma' where both types are Props

[Eric Wieser]

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]

But maybe that's already the case for ×?

[Kind Bubble]

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]

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