set image notation

Stream: mathlib4

[Sebastian Ullrich]

I'm happy to fix support for '' if there's consensus on that notation (at least for the time being)

[Shreyas Srinivas]

Richard Osborn said:

Would a unicode double quote work? Not sure which one would best

I would recommend against using unicode symbols that look an awful lot like ascii symbols. There would be debugging nightmares. You would have a cascade of errors if someone accidentally used the wrong kind of symbol in some critical part of mathlib for instance.

[Eric Wieser]

If fixing it is easy, we should stick with ''. The time to change the notation (if we are going to change it) is after the port, not during it

[Sebastian Ullrich]

Oh my god, I only just realized that ''' is valid syntax for the apostrophe Char

[Sebastian Ullrich]

I don't think that's intended though, let's fix that as well

[Shreyas Srinivas]

Sebastian Ullrich said:

I don't think that's intended though, let's fix that as well

What would the correct notation for the apostrophe Char be?

[Sebastian Ullrich]

'\'', which is in fact used by the character literal parser itself

[Sebastian Ullrich]

And probably most other languages with similar literal syntax

[Kevin Buzzard]

I've noticed that computer scientists are in general much more paranoid about "oh no two characters which look similar" than mathematicians. Number theorists use dvd everywhere and this is a weird symbol which looks like pipe but isn't, and things are fine, you just learn the gotcha early on and it's fine. You can't use the wrong symbol in any context because it's an immediate syntax error.

[Shreyas Srinivas]

I am not an expert on what the standard symbols are in specific areas of mathematics, but I would extreme caution in choosing apostrophes as symbol for anything other than chars and strings. The tooling (potentially syntax highlighting) could get messed up.

@Kevin Buzzard : We are paranoid for a good reason. Unlike in latex math, debuggability is important in programming, and anything that makes a piece of syntax less easy to read at a quick glance is harmful for debugging.

[Shreyas Srinivas]

So it is not enough that the compiler and tools show syntax errors (which depends as much on your text editor as your language).

[Notification Bot]

86 messages were moved here from #mathlib4 > data.set.basic by Eric Wieser.

[Sebastian Ullrich]

The tooling concern is not really changed between Lean 3 and 4 though, so I'm happy to give this rope to mathematicians

[Kevin Buzzard]

Sounds to me like we're still pushing for '', if it's not too much trouble.

[Shreyas Srinivas]

Sebastian Ullrich said:

The tooling concern is not really changed between Lean 3 and 4 though, so I'm happy to give this rope to mathematicians

Being tied to the reliability of specific tooling is not a good idea either.

[Kevin Buzzard]

I still personally think '' awful though, and that all that's happened is that we have been conditioned to get used to it. However I don't know of a better solution (I do like the idea of weird brackets though, it would be much closer to what mathematicians write on paper, and we are already using weird brackets for field extensions). Patrick's $f_*(S)$ is the best really, in terms of what we use in other contexts. I don't even know why we're talking about unicode, can't you just let us use LaTeX somehow and it all be displayed in VS Code?

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/1931

[Shreyas Srinivas]

A quick readability check :

1. This is <single quote><backslash><double quote>'\"
2. This is <single quote><backslash><single quote><single quote> '\''

[Shreyas Srinivas]

Kevin Buzzard said:

I still personally think '' awful though, and that all that's happened is that we have been conditioned to get used to it. However I don't know of a better solution (I do like the idea of weird brackets though, it would be much closer to what mathematicians write on paper, and we are already using weird brackets for field extensions). Patrick's $f_*(S)$ is the best really, in terms of what we use in other contexts. I don't even know why we're talking about unicode, can't you just let us use LaTeX somehow and it all be displayed in VS Code?

I thought the latex is converted to unicode

[Shreyas Srinivas]

In general I have the following suggestion: When choosing notation, ask yourself the following question: If this code were written in notepad, would you be able to read it and debug it quickly.

[Kevin Buzzard]

Right, which is a lot uglier than what we are used to seeing in the textbooks. Lean looks more like the textbooks than other ITPs (because other ITPs are dominated by the computer science community which has a far more cautious approach to these matters) and I've heard people say on several occasions that what has drawn them to Lean is that it looks more like mathematics than mathematics written in other systems, but LaTeX rendered the way LaTeX renders it would be better than these clunky unicode versions.

[Ruben Van de Velde]

But lean is an interactive theorem prover. Reading it in notepad is very much not an intended use case

[Kevin Buzzard]

Right -- that's the point. We read mathematics in pdf, not notepad. We're not computer scientists.

[Ruben Van de Velde]

In any case, if the notation already worked in lean4, we'd never consider changing it during the port

[Shreyas Srinivas]

Ruben Van de Velde said:

But lean is an interactive theorem prover. Reading it in notepad is very much not an intended use case

I am aware. Nevertheless, if you want to avoid debugging nightmares, it is safer to have to rely on fewer things working perfectly (in this case tooling).

[Shreyas Srinivas]

Further, tying your language design to one toolset is a bad idea. Then the language lives and dies with that toolset.

[Shreyas Srinivas]

Also, even within vscode, people use all sorts of themes for all sorts of reasons. These themes make font and styling changes which can also hinder readability if there are very similar looking symbols.

[Ruben Van de Velde]

I don't think I've got anything else to add to the discussion, so I'm going to disengage

[Eric Wieser]

if you want to avoid debugging nightmares

Debugging lean code without access to the lean server (via VSCode, vim, etc) is effectively impossible anyway. There's no way you can meaninfully do so in notepad

[Shreyas Srinivas]

Eric Wieser said:

if you want to avoid debugging nightmares

Debugging lean code without access to the lean server (via VSCode, vim, etc) is effectively impossible anyway. There's no way you can meaninfully do so in notepad

I would say I am using "notepad readability"as a metaphor for a situation where you need to debug something and the tools are not functioning properly or don't clearly tell you what is going wrong. Language designers are careful about potential readability issues for good reasons.

[Marc Huisinga]

Designing ITPs to function well without any tooling whatsoever is not reasonable. ITPs need to do much more than programming languages.

[Trebor Huang]

It would be desirable to have Monads be universe polymorphic regardless of what the set image notation is, right?

[Trebor Huang]

That way I can sell Haskellers with lines like "You can use f <$> xs to express the image of a set just like in Haskell, just that mathematicians don't like the notation".

[Eric Wieser]

Here's a discussion about changing the typeclasses to achieve that in Lean 3, and one about universe-polymorphic IO in Lean 4.