Unicode normalization

Stream: general

[Mario Carneiro]

In the Bonn meeting in January I spoke with Makarius, and I asked him about why Isabelle uses a custom encoding of special characters rather than something like Unicode. He brought up the issue with Unicode normalization, and I didn't really have a good response. The basic problem is that Unicode allows for multiple encodings of characters that are nevertheless to be treated as equal in all contexts; the main example of this is a letter followed by a combining mark like e + ◌́ = e◌́ = é. Should lean be aware of this process? That is, if I make a definition étale and later use e◌́tale should these be considered the same constant? I am curious what community consensus is on issues like this.

[Andrew Ashworth]

They should be equal iff NFC(x) = NFC(y), where NFC is unicode normal form C

[Andrew Ashworth]

however for maximum laziness we could just do whatever Lean 4 does when it compares symbols for equality

[Mario Carneiro]

I assume that is the same thing as what lean 3 currently does which is nothing

[Mario Carneiro]

Unicode has a pretty unambiguous answer to what the correct thing to do is here. The question is mostly about the tradeoff between implementation complexity and accurate handling of unicode characters

[Andrew Ashworth]

I vote for inaccurate handling and simple implementation complexity because it doesn't seem like a pressing problem right now

[Andrew Ashworth]

hashtag procrastinate issue until next major version

[Andrew Ashworth]

most unicode is entered using vscode short codes so it's unlikely to be a big issue. If it can't be entered using a short code I don't think most people bother

[Andrew Ashworth]

there are lots of people with ascii keyboards and making people type graves and accents when there's perfectly good romanization / ascii schemes lying around...

[Mario Carneiro]

To be fair, I think in isabelle they also use short codes for input

[Mario Carneiro]

My personal stance is that unicode causes more problems than it solves, but it is an easy way to achieve okayish results in a variety of viewing media (vscode, html docs, github)

[Mario Carneiro]

Andrew Ashworth said:

there are lots of people with ascii keyboards and making people type graves and accents when there's perfectly good romanization / ascii schemes lying around...

This is just an argument for straight ASCII though, not the current halfsie unicode used in lean 3/4

[Mario Carneiro]

it's also kind of english-centric

[Andrew Ashworth]

爲什麽代碼都是用英文來寫的，將來會有中文寫代碼的那天嗎？

[Andrew Ashworth]

I wouldn't get hung up on preferring Latin-ascii for most code. Just by choosing the latin alphabet to represent words you're excluding a lot of the world

[Mario Carneiro]

I saw a demo of that once from some CMU student

[Mario Carneiro]

it was made up to look like a traditional chinese text

[Gabriel Ebner]

Unicode allows for multiple encodings of characters that are nevertheless to be treated as equal in all contexts

I don't remember this ever being an issue in practice (and Lean doesn't do any kind of Unicode normalization as far as I'm aware of). I think the appropriate response is "identifiers are byte strings, equality is byte string equality". This is also how file names are handled on sane operating systems (and windows).

[Kenny Lau]

Andrew Ashworth said:

爲什麽代碼都是用英文來寫的，將來會有中文寫代碼的那天嗎？

I can't tell if this is translated. the translations engines are getting scarily stronger day by day

[Kenny Lau]

but I'll go with yes just because people who speak Chinese are statistically more likely to use Simplified Chinese (because Simplified Chinese is used in China)

[Mario Carneiro]

The related problem of many visually indistinguishable but distinct definitions is definitely an issue though

[Kenny Lau]

but I as a Hongkonger appreciate the representation of Traditional Chinese

[Shing Tak Lam]

Andrew Ashworth said:

爲什麽代碼都是用英文來寫的，將來會有中文寫代碼的那天嗎？

https://en.wikipedia.org/wiki/Easy_Programming_Language

這個算嗎？

[Kenny Lau]

we need Google to translate Cantonese

[Mario Carneiro]

a proprietary programming language? Eww

[Gabriel Ebner]

In case anybody wonders how it looks like:
etx_9.jpg

[Johan Commelin]

Why do they use those foreign { } characters?

[Mario Carneiro]

Why is it a proportional font? This is doubly baffling considering that the language is already monospace

[Shing Tak Lam]

I guess "祖國你好" is like the Chinese equivalent of "Hello World"?

[Mario Carneiro]

not sure about the shades of meaning here but it sounds very nationalistic

[Shing Tak Lam]

Mario Carneiro said:

Why is it a proportional font? This is doubly baffling considering that the language is already monospace

There are two sets of punctuation used in Chinese computer text. Full width which is monospace (全角) so ， for example, and Half width (半角), ,. And they made the design decision to use the half width set (ie. the ASCII set of punctuation).

Dunno why they used a proportional font though

[Mario Carneiro]

The code looks like they are using ascii, not halfwidth, for the ascii characters

[Gabriel Ebner]

Ascii is half-width.

[Shing Tak Lam]

Half width doesn't mean half the width of a normal character. It just means ASCII. It's a term (I think) borrowed from Japanese, and is from typesetting prior to computers.

[Mario Carneiro]

it's a bit more than halfwidth in most fonts. Isn't there a dedicated halfwidth section of unicode?

[Mario Carneiro]

which is literally a half moji wide

[Gabriel Ebner]

But it is exactly the half width in monospace fonts.

[Mario Carneiro]

thank goodness for that, I suppose. I guess they just chose not to use such a font in the snippet

[Gabriel Ebner]

Terminals would be hell otherwise. It's already a problem that half-widthness changes with new Unicode versions...

[Sebastian Ullrich]

Mario Carneiro said:

it was made up to look like a traditional chinese text

You're probably thinking of https://github.com/wenyan-lang/wenyan/blob/master/README.md. It's beautiful.

[Sebastian Ullrich]

But as for the topic at hand, I agree with Gabriel. I'd much rather have a linter that forbids non-normalized/deceptive input than adding slow normalization to the parser itself.

[Johan Commelin]

"unicode normalization is an editor feature" — Ancient eastern wisdom

[Kevin Buzzard]

Mario Carneiro said:

My personal stance is that unicode causes more problems than it solves, but it is an easy way to achieve okayish results in a variety of viewing media (vscode, html docs, github)

I am convinced that unicode is one of the reasons that undergraduate mathematicians are interested. It has only dawned on me recently that computer scientists are not all familiar with notation like $\forall, \exists, \land, \lor, \lnot$. In maths degrees this notation is introduced literally on day 1 (by me, at Imperial, for example, in lectures 1 and 2) and it makes Lean code more readable for us.

[Mario Carneiro]

Weren't you the one who explained to me that most mathematicians never get exposed to logic?

[Kevin Buzzard]

They get exposed to precisely the truth tables for and, or, not in classical logic, and modus ponens, and contrapositive, and that's it.

[Mario Carneiro]

but once they are out of that class they never use those symbols again

[Mario Carneiro]

except maybe the quantifiers

[Kevin Buzzard]

You're right I don't see much and, or, not, but the quantifiers are everywhere in the analysis scripts I'm marking right now

[Kevin Buzzard]

in the questions as well as the student scripts

[Mario Carneiro]

Anyway I'm not saying using symbols is bad, I'm saying that unicode is not a very good solution

[Kevin Buzzard]

Probably after a while you don't see many of the quantifiers either, but they are just used as part of the vernacular, e.g. some people use the symbols in English sentences if they're taking notes

[Mario Carneiro]

I'm not proposing ascii art as an alternative

[Kevin Buzzard]

I'm saying symbols is essential for readability by mathematicians which is one of the many problems which the area had 5 years ago

[Mario Carneiro]

unicode is a specific implementation of the idea of symbols in code, and it's not a very good one

[Kevin Buzzard]

I can't comment on other possibilities, we don't care what is going on under the hood

[Mario Carneiro]

isabelle has a different implementation of the same idea

[Mario Carneiro]

isabelle doesn't use unicode but you still see all the fancy symbols when you pull it up in the various media

[Mario Carneiro]

and more besides - things that don't exist in unicode

[Mario Carneiro]

LaTeX is yet another implementation of symbols in code (well, typeset text) that is not related to unicode

[Mario Carneiro]

and frankly I think LaTeX addresses the symbolic needs of mathematicians far better than unicode, which is primarily aimed at representing international scripts

[Kevin Buzzard]

I agree that LaTeX would be better. There have been times when writing instructional Lean code where I have wished for LaTeX over what unicode can offer me.

[Jannis Limperg]

Kevin Buzzard said:

It has only dawned on me recently that computer scientists are not all familiar with notation like $\forall, \exists, \land, \lor, \lnot$. In maths degrees this notation is introduced literally on day 1 (by me, at Imperial, for example, in lectures 1 and 2) and it makes Lean code more readable for us.

These certainly appear very early in any CS degree. It's not like we do literally no math. ;) Unicode remains unpopular in programming languages because programmers like to use a variety of editors, not all of which can comfortably input Unicode. (Also, entrenched ASCII prejudice imo.)

[Sebastian Ullrich]

In practice, Isabelle's symbols can be a huge pain in the neck - they are pretty when you're in JEdit, but turn into an unreadable and unmanageable mess when you look at them with any other tool or on Github or...

[Kevin Buzzard]

And people post lean code on discord now

[Kevin Buzzard]

And It Just Works

[Mario Carneiro]

Oh wow, looks like this comes up in Python, where they use a fairly aggressive normalization: https://stackoverflow.com/questions/62256014/does-python-forbid-two-similarly-looking-unicode-identifiers