toLower and toUpper in Basic.lean are incomplete

[lovettchris]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

See ucase.cpp for full unicode consortium implementation of ucase_toFullLower.

Steps to Reproduce

#eval String.toUpper "α"

Expected behavior: [What you expect to happen]
Should return unicode value 913, which is the greek letter "Α"

Actual behavior: [What actually happens]
Instead returns unmodified string "α"

Reproduces how often: [What percentage of the time does it reproduce?]
100%

Versions

"leanprover/lean4:nightly-2021-10-22"

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[tydeu]

@lovettchris toUpper/toLower are just ASCII uppercase and lowercase, not full Unicode. While Lean does support Unicode symbols, it does so only at a byte level. It does not link to a Unicode library like ICU, and thus it has no information about what codepoints belong to which character categories or the like.

From what I can tell, the support mostly exists for allowing exoteric mathematical symbols in source code, not to do string processing or to support coding in foreign languages (e.g., #698). While there are many users from countries where English is not the primary language, they thus far seem to have decided to stick with English (see the Zulip thread on the question of translating the mathlib docs for an example). That is, there does not seem to be sufficient demand to support other languages at the moment to justify the cost needed to do so.

[lovettchris]

I'm just pointing out every other programming language that provides toUpper and toLower do it properly, for example, here's the Rust implementation .So it will confuse a lot of folks when they realize the Lean version isn't. So I would recommend either fixing it or removing it. Statically linking the official unicode library would not be hard to do. This also helps with "isWhitespace". So either Lean is trying to be a full programming language or it isn't... Sure the priority can be lower than other things right now, but I think it needs to get fixed at some point.

[tydeu]

@lovettchris I mean, the toupper/tolower in C doesn't either? (And even in C++, it still wouldn't uppercase Greek unless you were in a Greek supporting locale.) So, I do not think lack this feature inhibits it from being a "full programming language". Regardless, once Lean gets a proper the standard library (e.g., #528), things like proper Unicode support can be in there. But, as I understand it, that is not a priority for now. I do agree, however, that this is a desirable feature in the future.

[Kha]

So either Lean is trying to be a full programming language or it isn't... Sure the priority can be lower than other things right now, but I think it needs to get fixed at some point.

It definitely should be. The short answer is that "trying to be a full programming language" is not the main focus right now.

[leodemoura]

Regardless, once Lean gets a proper the standard library (e.g., #528), things like proper Unicode support can be in there. But, as I understand it, that is not a priority for now. I do agree, however, that this is a desirable feature in the future.

As @tydeu pointed out, this discussion should be part of the standard library design. I am closing this issue here since it is not blocking any Lean user.

[lovettchris]

Leo where are the "standard library design" issues kept then so I can move it there?

[leodemoura]

Leo where are the "standard library design" issues kept then so I can move it there?

We currently don't have a repo for the std library yet. It is not the current focus right now.

[leodemoura]

Note that it may not even be a single repo, but a collection of repos.