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

https://github.com/nixpulvis/lalrpop-lambda/blob/master/src/encode/numerals.rs

by nixpulvis • 7 years ago

121 76 7 years ago

ajross• 7 years ago

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 rejected it as a matter of style. I have no idea why it hasn't been killed dead in new designs.

chewbacha• 7 years ago

Sure but this is a macro that’s user defined and not in the rust source code. Here’s the macro def:

https://github.com/nixpulvis/lalrpop-lambda/blob/master/src/...

I think it’s important to allow Unicode for developers to be more inclusive of other languages and cultures. This is at the forefront of the community of Rust.

As for keywords, yes, I’m with you there.

llamathrowaway• 7 years ago

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.

penteract• 7 years ago

https://github.com/JunoLab/atom-latex-completions is one that does this.

_emacsomancer_• 7 years ago

xcompose does something like that. (as does TeX for that matter, in a different fashion.)

frosted-flakes2• 7 years ago

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 to look it up, or create it if it doesn't exist yet.

Some distros of Linux have this built-in, but I use WinCompose[1] on Windows.

[1]https://github.com/samhocevar/wincompose

xiphias2• 7 years ago

Atom in Julia Pro does this (with autocomletion), and I've been using it in practice to clarify math in my code. It's great in practice.

danidiaz• 7 years ago

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...

dan-robertson• 7 years ago

Emacs has this plugin (well not a plugin because it’s built in). One can select an input mode. Some translate directly (e.g. a Greek input mode where typing a gives an alpha). There is also a TeX mode like what you describe and another mode which is more concise (e.g. &a for alpha, where the means Greek). The difference from what you described is that instead of some escape sequence for these special prefixes, they are just never converted if they don’t match and you move the point away.

tomjakubowski• 7 years ago

this is exactly why languages that specify their source code in non-ascii encodings are a bad idea.

Seems like your problem isn't that the source has a specified encoding, but that the syntax allows for non-ascii characters in identifiers, which is actually an unstable feature of Rust, only available with nightly compiler builds. See the feature flag: https://github.com/nixpulvis/lalrpop-lambda/blob/master/src/...

Specifying ASCII for the source code, as your post suggests is better, would leave everyone stuck using \uxxxx escapes for non-ASCII data in string literals. That's unnecessary when you instead specify UTF-8.

x3ro• 7 years ago

I like to look at it from a different perspective:

Programming has mostly looked the same since we moved away from punchcards, and it seems worthwhile exploring different approaches (eg visual programming) and augmentations to the existing system. Now that we have UTF-8, it's trivial to represent all sorts of characters and use them for coding, and it's only natural that some people try.

Now, while I personally haven't seen a convincing application of using non-ascii beyond comments, that doesn't mean they don't exist. And if people come up with such a way, and a large number of people decide it's a good idea, then tooling in whatever form will follow and make using this new style of coding easy.

I feel like arguing that this should never be done because people don't know where to find the symbols is a bit like arguing we shouldn't build electric vehicles because we don't have a charger network on highways yet..

nixpulvis9• 7 years ago

I've been clear to make things work just fine with `\` (parsed with LALRPOP), `abs!`, and `app!`.

I've only been pasting in a few in READMEs and standard constants for brevity.

db48x6• 7 years ago

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 just for that.) Here's a random selection: https://github.com/mockingbirdnest/Principia/blob/master/phy...

Like anything else, it can certainly be misused. That doesn't mean it's never worth using though.

whatshisface• 7 years ago

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 possible.

Unless you speak Greek, I can't think of any other reasons for Greek letters to wander in to code.

orbital-decay• 7 years ago

Here's a random selection: https://github.com/mockingbirdnest/Principia/blob/master/phy...

I don't think r² as a variable name is a good idea. It may look natural for some (including myself), but for others it implies a function while not being one.

nurettin• 7 years ago

I did not know how to produce greek letters until I read your comment and thought: why not just add the greek keyboard layout and press l, p and g?

improbable222• 7 years ago

My tip: on recent macs, if you have two keyboard layouts, there's an easy option to make caps lock switch them. (Great so long as you got a mac with a real escape key too...)

gylterud• 7 years ago

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. If the characters were replaced by words the overhead would be big.

The Plan9 operating system invented the compose key, which makes writing unicode characters easy enough for anyone to use them. Unfortunately, it requires a bit of setup to make the compose key work in X on Linux or *BSD (I have described th process here[1]). Agda and Coq therefore use special input modes for Emacs and other editors.

I also use Unicode in my Latex documents to make them more readable. [2]

[0] https://agda.readthedocs.io/en/latest/getting-started/quick-...

[1] https://hakon.gylterud.net/tutorials/unicode.html

[2] https://hakon.gylterud.net/tutorials/latex-maths-unicode.htm...

cjfd2• 7 years ago

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.

saagarjha3• 7 years ago

The Plan9 operating system invented the compose key, which makes writing unicode characters easy enough for anyone to use them. Unfortunately, it requires a bit of setup to make the compose key work in X on Linux or *BSD

Does macOS have something similar to this?

Sharlin3• 7 years ago

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.

cjfd2• 7 years ago

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.

deogeo• 7 years ago

As a non-native-English-speaker, the idea of having invisible bugs in code due to lookalike characters terrifies me.

The allowed set of characters would have to be vetted very carefully before I'd consider non-ASCII.

Edit: A small taste of what we can expect: https://i.imgur.com/k8S00sM.jpg

rubber_duck• 7 years ago

I'm not disagreeing with you because sometimes it's just project requirements - but as a developer in a non-English-speaking country - the idea of writing code in a non-English language is ridiculous to me.

Programming languages and standard libraries are written in English, programming terminology is invented in English, the international community adopted english as a defacto standard, almost all third party APIs expose English interfaces.

Every time I've seen a project written in my native language it's been ridiculously hard to follow because the terminology is translated in various ways (there's no official or even widely used terms because hardly anyone uses native language in SW development and CS outside of academia) and it's a mish mash between languages since everything not written in the project (along with language keywords) is written in English.

I don't usually take a hardline stances on things but this is one thing where it would be 100% a dealbreaker for working on a project.

worldsayshi2• 7 years ago

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.

saagarjha3• 7 years ago

That is, if they know that “λ” is “lambda”, which honestly might not extend to many of the Greek letters, to say nothing of Unicode.

Zekio2• 7 years ago

on Windows you can simply type `Windows key` + `.` and easily find it there, tho if languages use such characters they really should also have alternatives

the84722• 7 years ago

that only opens the emoji picker, not a generic unicode picker.

magicalhippo• 7 years ago

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.

Clearly full Unicode-enabled source code is the future, just look at how amazing it can be: http://baldi.me/blog/emoji-in-sql

newen• 7 years ago

Oh man, I really like this but I can definitely imagine a whole lot of people who would hate this.

est312• 7 years ago

ASCII is typeable by everyone. I'm german. I know how to type äöüß they are native keys on my keyboard. I know how to type \lambda in LaTex. I don't know how to get the λ key. However, I can type ASCII. A russian knows how to type cyrillic letters, and while very likely also knowing their way around ASCII, probably can't type λ easily either. Like it or not, ASCII is the least common denominator. There is nothing gained by having your macro called λ instead of lambda. It's just a redundant gimmick that makes code harder to type.

I have no idea why it hasn't been killed dead in new designs.

Well there is the use case that someone can't or doesn't want to learn/use english and their native language instead. These people definitely should be able to do that. For me personally, I've arrived at the conclusion that I personally do not want to code in projects in my native tongue. Simply because then a) it's only visible to a limited community and b) I constantly have to translate english concepts/ideas into the native tongue or risk having a half-english/half-german mixup. Other people might arrive at other conclusions, that's their thing and therefore they should be able to code in their native tongue and script.

This "native speakers" question is different from the question of using λ instead of lambda in an otherwise english codebase, or using Chebyshev's cyrillic name vs an ASCII transliteration. And here my opinion is different: some people may benefit from being able to code in their native tongue, but nobody has any benefits from λ or suddenly having a set of cyrillic characters as function name.

If you check the lib.rs of the project, you can see that it opts-in to nightly features. Naming anything λ is not possible in stable Rust right now. This will change though whith a newly merged RFC [1]. Fortunately, great care had been put on preventing homoglyph and mixed script attacks. My biggest issue with the change is that it's not opt-in but some future compiler release will accept non-ascii idents by default. It's easy to see why they arrived at this outcome: the entire thread is full with political ideology. According to the people in the thread, it might make someone feel excluded if they had to put #![allow(non_ascii_idents)] to lib.rs or an analogon to Cargo.toml... Seriously...

The keywords etc. are all in english anyway, an additional #![allow(non_ascii_idents)] can't be such a big issue can it.

I hope, like in java, non-ascii idents in mostly english codebases will get rejected by the Rust community as bad coding style. Fortunately there will be an option at least to forbid non-ascii identifiers without needing additional tooling and I guess I'll enable it in all of my own codebases.

[1] https://github.com/rust-lang/rfcs/pull/2457

nixpulvis9• 7 years ago

You don't think λ-calculus deserves the symbol `λ!` in Rust? Anyone who is learning or interested in λ-calculus should be aware of what it means (that's the whole point).

I generally agree we should all be so fortunate as to be able to read the code put in front of us.

And you clearly know how to type a λ, you did it 6 times in your post.

threatofrain• 7 years ago

I think it reads fluently to anyone who is studying the lambda calculus in some way, but it's not fluent for the editor; or they use Latex. I suspect that's the motivation for Julia, Agda, and Coq also allowing unicode.

Also most programmers wouldn't care to implement toy projects on the lambda calculus as part of their job. This is like complaining that most doctors couldn't program their own MRI machine.

dwaite• 7 years ago

I see no problem with this outside of the set of core Rust technologies. If you were to require the average developer to type mathematic symbols it would be a barrier. However, libraries specifically targeting mathematicians would obviously not have that same barrier. Making mathematical equations clearer to read and easier to work with within that domain may certainly be worth using syntactic tricks and non-ASCII symbols.

I've seen plenty of code bases which are not in English, since the developers did not have English as their first language. This is usually a well-contemplated decision - for instance, the Ruby language source code is specifically written so that you don't require knowledge of Japanese to understand the core libraries or the C reference implementation.

hansdieter1337• 7 years ago

looking forward to the first homograph attack in rust

estebank• 7 years ago

If you look at the Unicode identifiers RFC's discussion[2] you'll see the steps we're taking to address and mitigate that and other problems. That being said if you look at the tracking issue[3] you would also see that we haven't had the man power to fully implement this feature, which is why it will remain opt-in, nightly only for the medium term.

[1] https://github.com/rust-lang/rfcs/blob/master/text/2457-non-...

[2] https://github.com/rust-lang/rfcs/pull/2457

[3] https://github.com/rust-lang/rust/issues/55467

db48x6• 7 years ago

Hmm. What would you attack? That is, if you were writing a crate that I was thinking of using in my program, how would homographs allow you to compromise my code?

saagarjha3• 7 years ago

Here’s a somewhat contrived “attack”: I write a crate with two functions that are named similarly, wait for you to integrate it, then file a pull request using the Unicode function name (and hence calling the malicious function) and be relatively assured that if you looked up the function you’d stop reading code at the ASCII one.

wyldfire• 7 years ago

The best attack is of an alias of a popular crate. Duplicate the functionality/behavior/version number but include a subtle backdoor.

tempodox• 7 years ago

Another source code that demonstrates how things that are easy to write, read and understand in FP languages are a nightmare in Rust. Maybe making functional code indecipherable is not the best example of what Rust may actually be good for.

nixpulvis9• 7 years ago

I'm actually finding the opposite. This is mapping very nicely to Rust. But of course not as nicely as it would if I could encode things as lambda terms in the language itself. I'm currently working on an impl of Fn for the Expression. Maybe it'll work out.

This code isn't really meant to be an easily digestible read. I don't make much effort to explain the church numerals for example, I just show that it works with a few tests.

I personally find a lot of good FP principles come into play in Rust quite frequently.

nixpulvis9• 7 years ago

Amazing, 46 comments, all about my choosing to use the correct symbol for the macro. It's not like I choose some super misleading Unicode characters, like for example, how macOS smart quotes might change "foo" into “foo”.

Again, technically correct... maybe programming languages should match these kinds of quotes too.

But this is all more or less beside the point. I can type `λ!{x.x}` easily, since I have a Greek keyboard on my system (and a λ on my wrist, and a cat named π).

It's even more of a small deal as I've included the equivalent `abs!{x.e}` and `app!(e1,e2)` macros. In fact `λ!` and `γ!` are just macro "aliases".

Also, given the prominence of α-renaming, β-reduction, and η-reduction, I'm very glad I can use these symbols in Rust.

rbonvall• 7 years ago

I agree, it's nice to use the same symbols you'd use on paper. I did something similar in Scala http://mez.cl/en/lambda-dsl/

nixpulvis9• 7 years ago

Very cool! I think you've inspired me to implement something like `Expression << Expression` much like your `$`.

I'm currently trying to determine the best way to implement `From<Expression> for u64` (or maybe `Option<u64>`...), so I can convert both to and from `u64` types as church encoded numerals. Eventually the goal is to `impl Into/From<Expression>` for all the types one might use, giving a horribly inefficient runtime for Rust ;)

nixpulvis9• 7 years ago

P.S. DrRacket (https://racket-lang.org/) let's you insert a `λ` with Ctrl+\.

buster• 7 years ago

My first thought is, that code should be plain ascii and preferably english. But ultimately it's fine and nice that the language supports Unicode. It should be a matter of code guidelines and of the particular project setting the preferred way beforehand.

It should not be a decision by people implementing the language but not all projects using that language.

nixpulvis9• 7 years ago

If you want to play with this, you can run `cargo run` from this: https://github.com/nixpulvis/lambash/ repository.

It currently does both with and without η-reduction, and generally should work similarly to http://lambda.jimpryor.net/code/lambda_evaluator/ a very cool online JS lambda evaluator.

boazbarak• 7 years ago

I wrote an implementation of the λ calculus in python as an appendix for my book https://nbviewer.jupyter.org/github/boazbk/nandnotebooks/blo...

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

Related Stories