3 ms·

Which is why I think languages need UTF-8 identifiers and arbitrary UTF-8 operators. Most people working on webdev in the USA should never touch them and shoul

Which is why I think languages need UTF-8 identifiers and arbitrary UTF-8 operators. Most people working on webdev in the USA should never touch them and should feel free to ban them in their linters. But people who speak and write foreign languages with other alphabets and domain experts and people who just want to use π or µ or ∆v or whatever because they feel it makes their code clearer should be able to. Mathematicians who have PhDs should be able to write arbitrarily complicated heiroglyphical operators that I probably won't choose to understand in this lifetime. And that's okay, I don't need a language that attempts to guarantee that I can always read it, that is probably literally impossible and just constrains it unnecessarily.

schoen 3y ago
Coq has an interesting compromise, where the actual code passed to the compiler is in ASCII, but one can define sequences which have alternative renderings (usually to attempt to visually match existing math notation). For example, one could write Theorem demo: forall (x: nat), (exists y, x = S y) -> x <> 0. In many editors, this will get rendered as Theorem demo: ∀ (x: ℕ), (∃ y, x = S y) → x ≠ 0. This looks a lot nicer for mathematicians. (S here is Peano successor.) One minor nuisance is that, without an additional plugin, you can't actually write source code literally using the Unicode symbols (they're normally display-only, not part of a source file). The plugin to allow one to type them explicitly (with a Unicode-aware input method) does exist, but would make one's source code not portable for other users. Also, this is really specifically for math, not internationalization, and doesn't provide a helpful model for people wanting to type identifiers in non-ASCII-supported scripts.
silvestrov 3y ago
One case where UTF-8 identifiers are needed is (Danish) tax calculation and legal concepts which do not have an equivalent version in English. I.e. you have a name/concept which cannot be translated into English. If you enforce "all names must be English" then you end up with a made up word. If you are an English only speaker, try imagine that you were not allowed to use "w" in any variable name as it would be considered a "too weird" letter.

schoen 3y ago

Coq has an interesting compromise, where the actual code passed to the compiler is in ASCII, but one can define sequences which have alternative renderings (usually to attempt to visually match existing math notation). For example, one could write Theorem demo: forall (x: nat), (exists y, x = S y) -> x <> 0. In many editors, this will get rendered as Theorem demo: ∀ (x: ℕ), (∃ y, x = S y) → x ≠ 0. This looks a lot nicer for mathematicians. (S here is Peano successor.) One minor nuisance is that, without an additional plugin, you can't actually write source code literally using the Unicode symbols (they're normally display-only, not part of a source file). The plugin to allow one to type them explicitly (with a Unicode-aware input method) does exist, but would make one's source code not portable for other users. Also, this is really specifically for math, not internationalization, and doesn't provide a helpful model for people wanting to type identifiers in non-ASCII-supported scripts.

silvestrov 3y ago

One case where UTF-8 identifiers are needed is (Danish) tax calculation and legal concepts which do not have an equivalent version in English. I.e. you have a name/concept which cannot be translated into English. If you enforce "all names must be English" then you end up with a made up word. If you are an English only speaker, try imagine that you were not allowed to use "w" in any variable name as it would be considered a "too weird" letter.