Unicode symbols

Stream: lean4

[Paul Chisholm]

Many operators in Lean 4 can be entered as ASCII characters or Unicode symbols. However, the operator => can only be added as an ASCII sequence; \=> produces the expected symbol but results in an error. Are there any plans to allow the Unicode symbol?

While on the topic, the symbols \N and \Z for Nat and Int also throw an error. How can I use these symbols such that they are associated with Nat and Int?

It just occurs to me these may be defined in mathlib which explains why I get an error. Even when mathlib is ported to Lean 4, it would be nice to have these symbols associated with the types without having to load mathlib.

[Mario Carneiro]

The symbols for \N and \Z are indeed defined in mathlib4

[Paul Chisholm]

In that case it is probably best to avoid them unless intending to use mathlib.

[Mario Carneiro]

It's not hard to define them yourself either: notation "\N" => Nat

[Mario Carneiro]

But I agree that it is annoying to not be able to use the notation in basic code examples where you don't want to add imports

[Paul Chisholm]

Ok, I haven't got to the notation part as I work my way through the docs. So that notation just creates an alias.

[Mac]

@Paul Chisholm I think the choice to make the => used for functions/matches/macros/etc. different from \=> was deliberate (there is even a commit in the Lean 4 repo a while back that specifically removed it).

I suspect the rational is to allow \=> (which generals means logical implication) to still be used as such in logic while reserving the ASCII art for its special uses in the Lean syntax.

[Mario Carneiro]

A notation is an additional parser rule, which generates the same expression under the hood as if you used Nat directly. It differs slightly from aliases defined with abbreviation since these create a different expression and can be handled differently by tactics

[Paul Chisholm]

Ok, thanks both for the info.

[Leonardo de Moura]

@Paul Chisholm We wanted to make sure Lean 4 can also be used as a regular programming language, and the notation was not too exoteric for regular software developers. We assumed that \N and \Z are mainly used in math applications, and all math users will use Mathlib 4 anyway.
@Mac is correct about \=>, we didn't want to "reserve" the unicode symbol, math users can use it for something else.

[Justus Springer]

Speaking about math users, I've noticed that the unicode symbol ≅ is reserved for heterogeneous equality. Is that here to stay? Because math users will probably want to use that for "isomorphism"...

[Leonardo de Moura]

@Justus Springer We will remove it.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/6fb2a2b47b4397b05e9e99346e713f81dace60d8

[Kevin Buzzard]

I don't know what the CS people use for this idea, but I had also noticed this and to be honest am rather pleased that it's gone! Thank you!

[Mario Carneiro]

@Leonardo de Moura Regarding \N and \Z, how about the compromise position: The notations are defined but not used at all in the lean core repo. That way programmers browsing the code won't be put off by overuse of unicode, and they can feel free to not use it at all in their own code, while math-oriented textbooks like TPIL can just use it exclusively in code examples etc.

[Leonardo de Moura]

Yes, I think math-oriented documentation is a good motivation for having them at least available in Init.
We currently avoid them in TPIL 4: https://leanprover.github.io/theorem_proving_in_lean4/
BTW, we also had to avoid references to the algebraic structure in TPIL4. It was not too bad.

[Leonardo de Moura]

@Mario Carneiro The notation \N and \Z will have to be scoped in Init. Otherwise, the messages produced by Lean will use them.

[Leonardo de Moura]

Not sure whether we will be making things more confusing or not.

[Leonardo de Moura]

BTW, @Chris Lovett is investigating how to support a new feature on the VS Code Lean 4 extension. The idea is to have the option to communicate with a server running Lean. Then, we would be able to run Lean programs using the VS Code browser version. The server would have Mathlib 4, and would enable complex examples that depend on big chunks of Mathlib. The dream is to support the new "." feature available on GitHub, where we can start VS Code in the browser by simply pressing "." in any file on GitHub.

[Mario Carneiro]

It's a good point about needing to scope the notations, else things ilke #check 1 -- 1 : \N will cause problems

[Mario Carneiro]

Unfortunately it has to do one thing or the other starting from an empty file so we can't please everyone

[Mario Carneiro]

I wish we had data about how much programmers vs mathematicians care about this. Probably taking a poll here will give skewed results

[Mario Carneiro]

But my general impression is that mathematicians care a lot about seeing \N and programmers are mostly ambivalent and don't really see the point

[Kevin Buzzard]

I definitely care a lot about seeing \N however I would not mind at all if I only see it in mathlib4. It is only very rarely I find myself looking at core Lean 3 files in practice. Now we have this policy of having Lean being the foundations and mathlib being the mathematics (which I think we all believe is great) the mathematicians aren't going to mind if the notation is in core lean or mathlib, as long as it's there somewhere :-)

[Mario Carneiro]

What I'm not sure about is to what extent we consider Init a good starting point for doing whatever. I don't know whether lean 4 is trying to be "batteries-included" or "absolute bare necessities" or (most likely) somewhere in between. What is the demographic that we are targeting here of people who can start up lean, import nothing and then do stuff?

[Mario Carneiro]

Certainly in mathlib / lean 3 community edition we have trended towards making core only be about absolute bare necessities, at the price of making no-import lean be less usable than it used to be

[Kevin Buzzard]

Certainly Patrick and my opinion on this was that if you're targetting mathematicians then they should use leanproject and not leanpkg to make a new project, and mathlib is then automatically set up as a dependency. In particular the instructions called "how to install lean" on the community website give you a fully working mathlib (with all the oleans) before the user even understands what's going on. I tell all my students to start every file with import tactic.

[Mario Carneiro]

For the first few chapters of TPIL, I think the point is to dig down to the basics, and for that purpose any dependencies are problematic. In fact you can almost do everything from a no-core starting point: prelude, no imports. (I probably wouldn't do this, just because that requires explaining what prelude is, though.)

[Mario Carneiro]

But I think most of it can be done in a comfortable foundation with import Mathlib.Init or something of that nature. If we are committed to making sure that mathematicians never use Init only, then it wouldn't be too much trouble to have notation "\N" => Nat out of init.

[Mario Carneiro]

It would be pretty cool if you could specify a custom init in the toml file or something, though, so that mathematicians can also get that init-only feel while also getting mathlib-specific init stuff

[Leonardo de Moura]

@Mario Carneiro

I don't know whether lean 4 is trying to be "batteries-included" or "absolute bare necessities" or (most likely) somewhere in between.

We don't want the Lean 4 repo to be "batteries-included". The default installation is supposed to provide a working programming language.
The near future goal is to have Mathlib 4 working.
The long-term goal/dream is to have something like Rust crate https://crates.io with many packages for software development. Disclaimer: we are not suggesting the Mathlib project should follow this path.

It would be pretty cool if you could specify a custom init in the toml file or something, though, so that mathematicians can also get that init-only feel while also getting mathlib-specific init stuff

This is feasible to implement. We are also considering "persistent" set_options.
BTW, @Mac 's Lake build system will replace leanpkg soon, and it will open many new possibilities.

[Mario Carneiro]

@Leonardo de Moura What is your position on the role of the Std library? It sounds like something that might want to be a bit more batteries-included than Init, but it is also in the lean 4 core repo, probably because it is a dependency of lean 4, which leads to many of the same problems / complications as rust's std crate. Right now I'm not sure where development on a batteries-included standard library for lean 4 programming applications should go. Rust uses a model with many small crates, and I think we will want to go in that direction eventually, but centralized maintenance is a big plus while the ecosystem is still small. Like you say, lake will help a lot here with adding more build flexibility.

[Leonardo de Moura]

@Mario Carneiro

What is your position on the role of the Std library?

Std is currently on hold. One of the ideas discussed is to have it in a separate repo that can be populated by the community. We have a GitHub issue for that: https://github.com/leanprover/lean4/issues/528
The part of the Std library that is needed to implement Lean would be renamed to StdCore, but we would still use the Std namespace there.
The nightly build would pack the Lean, Lake, and Std in a binary distribution package.
We are not assuming this Std package would be a "batteries included" one. The goal is to have many small packages like Rust. This is the "dream".
Here is the reality for the near future, we want the following:

• Mathlib 4 in a usable state
• Lean 4 official release (including the missing features)
• Lake distributed with Lean 4
• Zig distributed with Lean 4 as a standalone C compiler
• Lake support for compiling shared libraries for Mathlib (i.e., Mathlib tactics compiled in native code without having to set up plugins or complicated makefiles).
• Widgets for Lean 4
• Better installation story for Lean 4

[Mario Carneiro]

The part of the Std library that is needed to implement Lean would be renamed to StdCore, but we would still use the Std namespace there.

I was also thinking of something like that. Rust's core / std comes to mind

[Mario Carneiro]

I like the near term goals, I will help when I can. (Especially the one about getting away from complicated makefiles. For me this has been the biggest step down from lean 3 to lean 4, it feels like I'm driving a C compiler with all the attendant dependency nightmares, compared to the old lean --make syntax. I can't wait for lake :smile: )

[Mac]

Mario Carneiro said:

But my general impression is that mathematicians care a lot about seeing \N and programmers are mostly ambivalent and don't really see the point

You might be surprised at how finicky programmers can be! :laughing: For instance, I know the heavy use of Unicode symbols is a major hurdle for one of my colleagues who I have been trying to get to use Lean (and he was even a Computer Science / Math double major). I also know that the Unicode symbols were a major concern for me as well when I first started using Lean. I think I lot of programmers really like their ASCII art.

It still annoys me once in a while when I see a symbol while exploring GitHub Lean code and have no clue what its name is or how to type it, but I have mostly gotten use to it. However, I still do prefer the ASCII art for computer science related-symbols (and is one of the reasons I would still love to see the anonymous constructor syntax just use plain parentheses).

[Scott Morrison]

Hopefully after the mathlib4 port has stabilised we can start splitting out the "standard library" stuff, removing it from mathlib and putting it into something along the lines of Std (or multiple separate repositories). While I'm a big fan of a monolithic mathematics repository, it would be a disaster if programming users felt that they had to depend on mathlib to get access to basic "standard library" stuff. We've been able to ignore this in Lean3 / mathlib3 because performance issues were a bigger deal anyway.