Live data from Hacker News

Rust, Macros, λ-calculus/Church numerals, oh my

github.com

21–30 of 82 posts

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#21
post #2

While it's definitely cute and amusing, this is exactly why languages that specify their source code in non-ascii encodings are a bad idea. Fully 92.6% of working programmers have no idea how to produce a λ or γ on their input device of choice. Maybe a third of those could eventually find it with a character picker tool. Java started this (in the unicode era anyway -- yeah yeah, APL). The community quite sanely rejec…

Maybe it’s time for a plugin that does this (or maybe it already exists?): You press the backslash key, enter the name of the symbol, then press enter, and the symbol will show up in your buffer. Something like: \lambda -> λ \Lambda -> Λ \\ -> \ et cetra.

Relatively easy in Vim with digraphs (:h digraph)

Ctrl-K l* produces λ

Ctrl-K L* produces Λ

Unsurprisingly, Emacs also supports this when programming in Agda (\lambda) i'm not sure if it's a builtin feature or part of the Agda plugin.

In Agda using Unicode identifiers is widely accepted, even in the standard library: https://github.com/agda/agda-stdlib/blob/master/src/Relation...

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#22

Earlier quoted context omitted.

Maybe it’s time for a plugin that does this (or maybe it already exists?): You press the backslash key, enter the name of the symbol, then press enter, and the symbol will show up in your buffer. Something like: \lambda -> λ \Lambda -> Λ \\ -> \ et cetra.

A dedicated global compose key solves this problem very elegantly. Hitting the ◆ compose key (right alt for me) followed by a series of intuitive characters inserts the corresponding character. For example: ◆ - - - produces an em dash (—) ◆ - - . produces an en dash (–) ◆ ' e produces é ◆ | c produces the cent symbol (¢) Usually, you can just guess the combination and be right 3/4 times. Otherwise, it's fairly easy t…

> Some distros of Linux have this built-in […]

Some? Nearly all of them do — usually it just needs to be activated in the desktop environment.

I used a … and an — in this post using the compose key without even thinking twice.

> Usually, you can just guess the combination and be right 3/4 times.

¾ even. Just guessing that it was 3 4.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#24
post #2

While it's definitely cute and amusing, this is exactly why languages that specify their source code in non-ascii encodings are a bad idea. Fully 92.6% of working programmers have no idea how to produce a λ or γ on their input device of choice. Maybe a third of those could eventually find it with a character picker tool. Java started this (in the unicode era anyway -- yeah yeah, APL). The community quite sanely rejec…

Because people in non-English-speaking countries are perfectly within their rights to name source code entities in their native language instead of either having to mangle words into ASCII representations (possibly even leading to ambiguities in case of near-homonyms that have identical ASCII bastardizations!) or being forced to awkwardly translate domain terminology into English which is a task that may be any of the following: a) against organization policy, b) not what programmers are paid to do, c) lead to ambiguous or outright misleading translations, d) require good English skills from anyone touching the code, e) make documentation more difficult, f) present unnecessary hurdles when onboarding new people to work on the code.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#25
post #11

Earlier quoted context omitted.

I disagree. I looked through the source code to Principia a while back, and it makes really effective use of Greek script, black-letter script, math symbols, etc for implementing a physics engine. (It's a mod for Kerbal Space Program that implements n-body gravitation.) It's really well written and used just enough to make things more understandable. (They've got a great units system too; it's worth reading the code…

Greek letters are good for transcribing equations that were written with Greek letters. The equations were written like that because you only get one letter per variable and you need more than 26 variables across multiple equations, which you want to be consistent. You only get one letter per variable because on paper you write down each equation about fifty times as you work with it, so it's kept short as much as po…

But because you learn physics and maths on paper, you learn the equations this way. And once you've spent 10 years practicing physics with Greek letters, it's really annoying to be forced out of it when you program.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#26
post #24
post #2

While it's definitely cute and amusing, this is exactly why languages that specify their source code in non-ascii encodings are a bad idea. Fully 92.6% of working programmers have no idea how to produce a λ or γ on their input device of choice. Maybe a third of those could eventually find it with a character picker tool. Java started this (in the unicode era anyway -- yeah yeah, APL). The community quite sanely rejec…

Because people in non-English-speaking countries are perfectly within their rights to name source code entities in their native language instead of either having to mangle words into ASCII representations (possibly even leading to ambiguities in case of near-homonyms that have identical ASCII bastardizations!) or being forced to awkwardly translate domain terminology into English which is a task that may be any of th…

Sure, everybody has 'rights' but if I were to come across a workplace in my country where programmers were using much of our native language in the code I would consider it a red flag and I would expect to find amateurish practices in other places as well. The thing is that English is the lingua franca of programming and that ASCII is the lingua franca of source files. The highest quality manual that you are going to find is in English and stack overflow will answer your questions in English. Also, various tools are going to respond to non-ASCII characters in various ways which may not always be the most pleasant. You are bound to get yourself some problems that you would not have gotten otherwise.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#27
post #2

While it's definitely cute and amusing, this is exactly why languages that specify their source code in non-ascii encodings are a bad idea. Fully 92.6% of working programmers have no idea how to produce a λ or γ on their input device of choice. Maybe a third of those could eventually find it with a character picker tool. Java started this (in the unicode era anyway -- yeah yeah, APL). The community quite sanely rejec…

Agda[0] and Coq and other languages for formalising mathematics (they are also programming languages) make a lot of use of Unicode to make the mathematical statements readable. Here is an example: > ∑-+-distribute : ∑ (A + B) C ≃ (∑ A (C ∘ left)) + (∑ B (C ∘ right)) This is quite readable and would be understandable to someone who did not know Agda or the library in particular, but who understood the subject material…

This is true but it is still a choice. In my spare time coq project I use ascii exclusively in my source files. Same thing for my PhD thesis in theoretical physics that was in LaTeX.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#28
post #26
post #24

Earlier quoted context omitted.

Because people in non-English-speaking countries are perfectly within their rights to name source code entities in their native language instead of either having to mangle words into ASCII representations (possibly even leading to ambiguities in case of near-homonyms that have identical ASCII bastardizations!) or being forced to awkwardly translate domain terminology into English which is a task that may be any of th…

Sure, everybody has 'rights' but if I were to come across a workplace in my country where programmers were using much of our native language in the code I would consider it a red flag and I would expect to find amateurish practices in other places as well. The thing is that English is the lingua franca of programming and that ASCII is the lingua franca of source files. The highest quality manual that you are going to…

Sure, you could consider it unprofessional, but I'd wager that the large majority of all professional programming is done in languages other than English. The tooling issue is an "is vs. ought" problem. In 2019 full UTF-8 compatibility is not a feature anymore; on the contrary, a lack of support is a bug.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#29
post #2

While it's definitely cute and amusing, this is exactly why languages that specify their source code in non-ascii encodings are a bad idea. Fully 92.6% of working programmers have no idea how to produce a λ or γ on their input device of choice. Maybe a third of those could eventually find it with a character picker tool. Java started this (in the unicode era anyway -- yeah yeah, APL). The community quite sanely rejec…

> Fully 92.6% of working programmers have no idea how to produce a λ or γ on their input device of choice

I can imagine a simple remedy for this. Have the IDE suggest symbol replacements whenever the use types the name of the symbol. 'lambda' causes λ to be suggested.

Re: Rust, Macros, λ-calculus/Church numerals, oh my

#30

Earlier quoted context omitted.

Greek letters are good for transcribing equations that were written with Greek letters. The equations were written like that because you only get one letter per variable and you need more than 26 variables across multiple equations, which you want to be consistent. You only get one letter per variable because on paper you write down each equation about fifty times as you work with it, so it's kept short as much as po…

100% this. To understand code written with Greek letters you'd also need to understand the author's intentions for using said letters. Is mu an average or coeff of friction? Why should I lean on a crutch of context for a casual skim of code? It doesn't help readability and it surely isn't enjoyable to write.

It all depends on context. Short identifiers absolutely help readability. I feel like some people absolutely go too far with overly verbose variable names, especially in Java or C#.

Notation matters. What if I told you that to add two numbers you had to write it out as plus(number, number)? Clearly you'd riot. The reason people complain about short IDs is because they're not used to it, but there are a lot of domains (math, science) where using traditional notation enhances understanding. Hell, even in programming if someone wrote sequenceIndex instead of i when iterating over the indices of an array I'd think they were trying to troll.

Post reply on HN