Notation for Pi type

Stream: general

[Filippo A. E. Nuccio]

In this line the notation

(x : α) → β x

is described to be a short version for the Pi type Π x : α, β x, and this affects the way the infoview renders terms of a pi type. What was the point of that notation? To me, it seems quite odd from a type-theoretic point of view, since the definition 'Pi type' is well documented and people landing on mathlib with no knowledge of its jargon but knowledgeable about (dependent) type theory would know what Π x : α, β x represents. I might be wrong, but the disappearance of the Π symbol does not look very intelligible to me. At least in the infoview, I would prefer the Π to survive, is it unreasonable?

[Patrick Massot]

Mathlib will make you happy if you ask nicely.

[Riccardo Brasca]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Add.20pi.20notation.20back.20.3F

[Riccardo Brasca]

And I agree that at least in mathlib we want this.

[Patrick Massot]

import Mathlib.Util.Delaborators

variable (α : Type) (β : α → Type)

#check (x : α) → β x -- (x : α) → β x : Type

#check Π (x : α), β x -- (x : α) → β x : Type

open scoped PiNotation

#check (x : α) → β x -- Π (x : α), β x : Type

[Patrick Massot]

As long as you import that file, Lean understands what you mean. If in addition you open the scoped notation then you will understand what Lean means.

[Patrick Massot]

Importing this file is pretty cheap since it is imported by Data.Set.Basic.

[Filippo A. E. Nuccio]

Patrick Massot said:

Mathlib will make you happy if you ask nicely.

Do you mean my question above was rude? I did not mean it to be so, so my apologies are in order if it felt it was.

[Patrick Massot]

No, it wasn't rude!

[Patrick Massot]

I wrote that to keep you hopeful when I was cooking up the code snippet I posted two minutes later.

[Filippo A. E. Nuccio]

Ah, so the "nicely" refer to the way I should ask mathlib, not the way I asked here...

[Patrick Massot]

Nicely means make sure you import at least Data.Set.Basic (importing any math file will be enough), and type that open scoped line.

[Patrick Massot]

The opened scoped requirement is a concession. If I were the only user of Mathlib I would have make it the default.

[Filippo A. E. Nuccio]

Well, it would be the case also if we were the only two users of mathlib :smile:

[Patrick Massot]

And of course I should also write that Kyle Miller wrote the corresponding delaborator, I only PRed it to Mathlib.

[Mario Carneiro]

Why not liberate Π too if we are liberating λ? This letter has other meanings in mathematics as well, most notably for actual products

[Patrick Massot]

This is an actual product. Mathematicians would be very happy to use the same symbol for this and for Finset.prod.

[Filippo A. E. Nuccio]

Well, as a matter of fact, I find the disappearance of λ quite annoying as well...

[Mario Carneiro]

Patrick Massot said:

This is an actual product. Mathematicians would be very happy to use the same symbol for this and for Finset.prod.

Right, but by using it for one we can't use it for the other. This is not a product in the sense of Finset.prod, it returns a type not a value

[Kyle Miller]

(If someone were to remove "scoped" from this line then it would become global.)

[Patrick Massot]

Filippo, if you insist I can write to the math department of St Etienne that you need to be reminded of the importance of having λ available, hence you should teach only linear algebra and eigenvalues for a couple of years.

[Filippo A. E. Nuccio]

Should we rename this entry to

fun _ => _ Calculus

:smirk:

[Mario Carneiro]

fun calculus sounds good

[Eric Wieser]

Why would we use U+03A0 Π greek capital letter pi for actual products when we already have and use U+220F ∏ n-ary product?

[Filippo A. E. Nuccio]

Patrick Massot said:

Filippo, if you insist I can write to the math department of St Etienne that you need to be reminded of the importance of having λ available, hence you should teach only linear algebra and eigenvalues for a couple of years.

I'll think about it...

[Mario Carneiro]

IMHO naming mathematical concepts after the random letters chosen to denote them is a terrible practice

[Kyle Miller]

Lean 4 put the fun back into formalizing mathematics

[Eric Wieser]

Patrick Massot said:

The opened scoped requirement is a concession. If I were the only user of Mathlib I would have make it the default.

Prefferably before mathport removed all the pi notations from our source code...

[Filippo A. E. Nuccio]

Mario Carneiro said:

IMHO naming mathematical concepts after the random letters chosen to denote them is a terrible practice

I certainly agree, in general. I just find that we live in a world where some practices are established and it does not make it easy for people coming from outside to understand what we mean if we start using our own language. But I did not want to open a Pandora's vase.

[Mario Carneiro]

Eric Wieser said:

Prefferably before mathport removed all the pi notations from our source code...

note that this was a technical restriction: lean 3 did not differentiate ∀ and Π at all, it forgets which one you wrote immediately

[Mario Carneiro]

lean 4 internally now universally refers to this as the "forall type", "Pi" no longer appears anywhere

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

Patrick Massot said:

Filippo, if you insist I can write to the math department of St Etienne that you need to be reminded of the importance of having λ available, hence you should teach only linear algebra and eigenvalues for a couple of years.

I'll think about it...

In the meantime I can also drop a line in Orsay, telling them that both x and y can be useful and should not be freezed just to mean that some misunderstanding is probably taking place :angel:

[Mario Carneiro]

this is also the strategy I used in #leantt, I just use ∀ for this type constructor and Π does not appear (except in the section on the proof-split language, which has both ∀ and Π and they mean different things)

[Filippo A. E. Nuccio]

Let me try to put the discussion back on the track I initially meant, which is: suppose you are somewhat new to mathlib and/or lean4 (at least, new enough not to be willing to go looking so deep ). Wouldn't it be nice to have some hint telling you that

1. This notation is meant to be something that you might know
2. Adding this open scoped PiNotation might be a useful thing to do?

[Filippo A. E. Nuccio]

Kyle Miller said:

(If someone were to remove "scoped" from this line then it would become global.)

@Kyle Miller I guess that you are not suggesting that someone opens a PR, right?

[Kyle Miller]

I guess I'm not not suggesting it either

[Patrick Massot]

Filippo A. E. Nuccio said:

Let me try to put the discussion back on the track I initially meant, which is: suppose you are somewhat new to mathlib and/or lean4 (at least, new enough not to be willing to go looking so deep ). Wouldn't it be nice to have some hint telling you that

1. This notation is meant to be something that you might know
2. Adding this open scoped PiNotation might be a useful thing to do?

That's a good point. We should at least mention it in #mil but I'm not sure we ever discuss dependent products specifically. Could you create an issue in the mathematics_in_lean_source repo?

[Filippo A. E. Nuccio]

Patrick Massot said:

Filippo A. E. Nuccio said:

Let me try to put the discussion back on the track I initially meant, which is: suppose you are somewhat new to mathlib and/or lean4 (at least, new enough not to be willing to go looking so deep ). Wouldn't it be nice to have some hint telling you that

1. This notation is meant to be something that you might know
2. Adding this open scoped PiNotation might be a useful thing to do?

That's a good point. We should at least mention it in #mil but I'm not sure we ever discuss dependent products specifically. Could you create an issue in the mathematics_in_lean_source repo?

Sure!

[Patrick Massot]

Kyle means that you won't be able to constructively prove that he didn't suggest you shouldn't refrain to not propose this PR. Or the other way around.

[Filippo A. E. Nuccio]

Kyle Miller said:

I guess I'm not not suggesting it either

Although the "not not suggesting" is great, the "I guess" at the beginning of your sentence is unbeatable!

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

Patrick Massot said:

Filippo A. E. Nuccio said:

Let me try to put the discussion back on the track I initially meant, which is: suppose you are somewhat new to mathlib and/or lean4 (at least, new enough not to be willing to go looking so deep ). Wouldn't it be nice to have some hint telling you that

1. This notation is meant to be something that you might know
2. Adding this open scoped PiNotation might be a useful thing to do?

That's a good point. We should at least mention it in #mil but I'm not sure we ever discuss dependent products specifically. Could you create an issue in the mathematics_in_lean_source repo?

Sure!

Done here [BTW Is there a way to reference to an issue in a repo different from mathlib?)] As mentioned there, I wonder if the right place for the comment is not Theorem Proving in Lean (or both).

[Kyle Miller]

I think to reference an issue you just include the full issue link? (edit: oh, for some reason I thought you meant linking from inside github rather than from here on zulip)

[Mario Carneiro]

We have linkifiers for general repos as well: avigad/mathematics_in_lean_source#149

[Filippo A. E. Nuccio]

Thanks! And I ended up doing a small Swiss tour with @Kyle Miller opening #8047 :flag_switzerland: (I wished 4810 was still available... :snowy_mountain: )

[Richard Copley]

Patrick Massot said:

Filippo, if you insist I can write to the math department of St Etienne that you need to be reminded of the importance of having λ available, hence you should teach only linear algebra and eigenvalues for a couple of years.

Alas:

variable (λ : Nat) -- unexpected token 'λ'; expected '_' or identifier

[Filippo A. E. Nuccio]

Richard Copley said:

Patrick Massot said:

Filippo, if you insist I can write to the math department of St Etienne that you need to be reminded of the importance of having λ available, hence you should teach only linear algebra and eigenvalues for a couple of years.

Alas:

variable (λ : Nat) -- unexpected token 'λ'; expected '_' or identifier

Oh well, but eigenvalues are complex numbers, not natural, right?! :face_with_hand_over_mouth:

[Junyan Xu]

variable (Π : Type*) produces a different error: expected token (without importing PiNotation). What's the mechanism behind this? I'm checking other Greek letters. λ is still used for functions, and Σ is for sigma types, these I know. But what's Ι (\Iota) used for? (same error as λ and Σ.)

[Patrick Massot]

Recall that Type* is a Mathlib thing.

[Patrick Massot]

So you cannot test what comes from Lean alone if you use Type*.

[Patrick Massot]

In Mathlib Iota is defined as a notationin Data/Set/Intervals/UnorderedInterval.lean.

[Mario Carneiro]

This issue is discussed a bit here. That was about lambda but the same thing is true for Pi

[Mario Carneiro]

it is explicitly excluded as an identifier character, even though it has since been removed as a token

[Mario Carneiro]

as far as I know Ι should work as an identifier (testing seems to agree)

[Junyan Xu]

In Mathlib Iota is defined as a notationin Data/Set/Intervals/UnorderedInterval.lean.

Thanks, indeed, I was importing too much.

[Gareth Ma]

Slightly unrelated, but what does \Iota look like for you all? Also, guess which is \Iota and which is I:
Screenshot-2023-10-31-at-04.34.57.png

[Kevin Buzzard]

The one with the red line under it is the one which isn't recognised as a token :-)

[Mario Carneiro]

For me I and Ι look identical. I don't know many fonts that differentiate them

[Mario Carneiro]

and it's a bit underhanded that mathlib is using capital iota as a notation

[Filippo A. E. Nuccio]

Just to understand: at the beginning of the survival guide I read that

Function notation changed from λ x, f x to fun x => f x or λ x => f x or fun x ↦ f x or λ x ↦ f x.

Does it mean that even in mathlib the λ-notation is accepted, or only the fun one is OK? Similar question for => vs ↦.

[Jireh Loreaux]

Only fun. Both arrows are accepted.

[Eric Wieser]

This is covered in #style

[Filippo A. E. Nuccio]

Oh, thanks. That's what I feared. I know it is too late (and not relevant), but I find it a pity.

[Yaël Dillies]

We can just start using λ again.

[Eric Wieser]

Obligatory link to the let's kill lambda thread where we never actually eliminated it

[Filippo A. E. Nuccio]

Indeed, what I see is that at the end of the day the notation is not deprecated in Lean4, but it is in mathlib (and the discussion pointed at by @Eric Wieser was indeed about Lean4). I cannot find the equivalent discussion for mathlib but it just seems to me to be a top-down directive that brings nothing. I do not want to claim it is better to use λ over fun, just that preventing users from using a symbol that the system accepts is weird. As far as uniformity is concerned, mathlib is allowing both => and ↦. Likewise, I guess that both fun x => x + 1 and (· +1 ) are accepted. What is the downside to the solution "every contributor can use whatever symbol they prefer" here as well?

[Eric Wieser]

I think there's a lot of value to picking one style and sticking to it; no one wants to read code like λ x => fun y => λ z => and have to try and work out whether the two different spellings genuinely mean different things.

[Eric Wieser]

Arguably this should apply to ↦ too, but that's a mess because there are lots of =>s in Lean that you can't replace with ↦...

[Filippo A. E. Nuccio]

I agree, but this seems to be a crazy contributor who likes to mix things up (and the PR review could go along the lines of "please pick one convention in your PR and stick to it").

[Eric Wieser]

That quickly becomes "please pick the convention in the rest of the existing files you touch", and well, that convention is fun because that's what we asked mathport to write

[Jireh Loreaux]

Three reasons from my perspective.

1. If mathlib uses λ, core will be less likely to abolish it.
2. λ is weird type theory notation that math users may be unfamiliar with. We should avoid this where possible.
3. As Eric said, consistent style.

Note that we will always have fun x ... because it can do things that (· + 1) can't, even though the latter is more pleasing. So, it's to be expected, and a user can choose here which they prefer since both will be allowed. As for => and ↦, I think the problem is that the community is rather split about which is preferred (and, as Eric mentioned, we will always have => in some places).

[Patrick Massot]

Mario told us that one day he will write a meta-program turning every λ x => ... into fun x ↦ ... in Mathlib. That's the only reason why we didn't do it by hand.

[Eric Wieser]

(That's a very good reason not to do it by hand)

[Filippo A. E. Nuccio]

OK, I see your points. My only concern is of inclusiveness: many people coming from type theory are used to the lambda notation and this goes against what they are used to. Had we at least gained in flexibility by freeing the symbol, or had it been impossible to let Lean work with both, I would understand the need of being strict. Like this, it just seems to put a preference on mathematicians over type-theorists and I am not that much happy about it. At any rate, I realise it was a well-thought-out decision and I do not want to make a fuss out of it.

[Jireh Loreaux]

I think λ is in a sense only for the type theorists (i.e., mathematicians and software engineers may not understand the reason for it's use, whereas fun is clear).

[Shreyas Srinivas]

As far as I know, non mathlib projects can still use \lambda. Further it also makes perfect sense for a mathematical library to have conventions that work for math, which could be linter enforced. The question is, what does removing it from core achieve?

[Jireh Loreaux]

Shreyas, allowing us to use it as a variable.

[Shreyas Srinivas]

Fwiw, type theorists probably don't use lean as it is. They construct a suitable DSL for their type theory.

[Patrick Massot]

We could remove from core the fact that λ cannot be used for anything else, and then define it as a scoped notation for people who want it.

[Eric Wieser]

Or just teach those people how to define the notation as a notation example, without actually doing it in Std or Mathlib