7 ms·

Writing prettier Haskell with Unicode syntax and Vim

61 points by romes 3y ago

plaguepilled 3y ago
I think the applicability of using maths symbols in a program is highly domain dependent. It'd be reasonable to use it for a physics simulation. You probably should not use it for a banking application.
cryptonector 3y ago
Are there newer versions of Roboto Mono that support all these Unicode codepoints? [EDIT: No, I checked and there are not[0].] The one I have does not support ∃, ∈, and ∷, and probably others. I agree that this is very pretty, but font support is absolutely critical if you're going to do this. [0] https://fonts.google.com/specimen/Roboto+Mono/glyphs
felurx 3y ago
A few people have mentioned the compose key as a way to insert Unicode characters system-wide. I also really like Espanso[0]: You can use it to replace any typed string with anything else, it even supports forms and executing scripts / shell commands. There's tons of fancy stuff you can do with it, but just mapping something like \alpha or :a* to ɑ is easy too. (For greek characters, there's a package that uses a syntax like \alpha\) [0]: https://espanso.org/ https://espanso.org/
todd8 3y ago
Using the equals sign (=) for assignment is unfortunate. Mathematically, a=a+5 is confusing. Algol 60 (and its grandchild Pascal) are a bit better and represent this as a:=a+5, but this is an odd notation too. A left pointing arrow would be a better notation for the common assignment statement, at least to me. Does this mean I'm ready to embrace the use of mathematical notation via unicode glyphs in programming? No. I have a math degree and after dozens of university courses on math I've seen a lot of math notation. This notation uses a dizzying number of symbols across various mathematical disciples. LaTeX allows one to use any of 75 distinct kinds of arrows alone! Left, right, doubled, up, down, diagonal to the upper right, looped, long, bidirectional, harpooned, wiggly, maps-to, and so forth. That's just the arrows. Why does LaTeX allow typesetting with so many distinct arrows? Because mathematicians use them as distinct concepts. I count 160 relational symbols available for use with standard LaTeX: less-than, equal, equivalent, congruent, subset, parallel, similar, approximate, the list goes on and on. See [1]. Mathematicians don't even use these symbols consistently. Consider the ubiquitous lambda, appearing all over in functional programming. Surely, the use of a lower-case greek lambda is prettier than spelling out the word 'lambda', but it may in many contexts not stand for an anonymous function. It's use as a symbol can also mean: wavelength of any wave, number of offspring, radioactive decay constant, occurrence density within a time interval, eigenvalues, charge density, Lagrange multiplier, empty string, and so forth. Wikipedia lists 24 distinct uses for lambda, [2]. Why do mathematicians, engineers, and scientists use so many different symbols? Because they are doing something fundamentally different with them than programmers. They use the symbols as abbreviations that will be understood by their audience, which might be students watching a lecture, readers of a technical article, or even themselves at some time in the future. The context in all of these uses is very different than the context of a program. The program must be precise and unambiguous, and the program may be one hundred times longer than a published math paper. For this reason, spelled out identifiers and keywords using standard ASCII glyphs are wordier and less "pretty" but are far more practical. [1] https://www.cmor-faculty.rice.edu/~heinken/latex/symbols.pdf https://www.cmor-faculty.rice.edu/~heinken/latex/symbols.pdf [2] https://en.wikipedia.org/wiki/Lambda#:~:text=Lambda%20indicates%20the%20wavelength%20of,originated%20from%20Evolution%20strategy%20notation https://en.wikipedia.org/wiki/Lambda#:~:text=Lambda%20indica....
hole_in_foot 3y ago
Unicode in code is a footgun.
bojo 3y ago
While I do think these look nice (appropriate even), maintaining consistency across a large team of devs is where this type of stylization breaks down. Not everyone is using the same code editor, not everyone's configuration is the same. At the end of the day it's easier to write and maintain the long-hand word versions.
llimllib 3y ago
I got confused because I tried to use ctrl-k and wasn't getting any results; after reading the docs, at least on my system (neovim on mac), ctrl-K (uppercase) is the proper shortcut for entering digraphs when in insert mode. (:help digraph)
ufo 3y ago
On Linux I input special characters using the Compose key. Works everywhere, not just in Vim.
- pxc 3y ago
  I do this, too. I haven't yet found a solution that works very well for macOS— a few years ago, some mappings were not possible with the solutions I found.
  - fragmede 3y ago
    control-command spacebar brings up the emoji picker, and some of the symbols are in there, but like you said, not everything. ∀ ° ∫ Ω
    - pxc 3y ago
      I do really like modern emoji pickers in general. Compose keys are nice, but I love fuzzy filter interfaces that search as you type. Compared to compose sequences, they let you get up to a reasonable speed very quickly.
  - goerz 3y ago
    I got you covered: https://michaelgoerz.net/notes/the-us-international-scientific-keyboard-layout/ https://michaelgoerz.net/notes/the-us-international-scientif...
- gylterud 3y ago
  Came here to mention this exactly. I have a quick intro to the compose key on my website [0] and an intro for how to use Unicode with Latex[1], and there are other resources around the web if you are looking. The idea of a compose key for Unicode originated in Plan 9, as far as I know. [0]: https://hakon.gylterud.net/tutorials/unicode.html https://hakon.gylterud.net/tutorials/unicode.html [1]: https://hakon.gylterud.net/tutorials/latex-maths-unicode.html https://hakon.gylterud.net/tutorials/latex-maths-unicode.htm...
- cryptonector 3y ago
avgcorrection 3y ago
Unicode in code might be what pushes people to consider variable-width font. Just look at the simple arrow in a text editor (hopefully the text filter on this website thinks this symbol is OK): → (U+2192 RIGHTWARDS ARROW). It’s tiny. And I notice that the author uses plain `->`. You do need at least an “em” width for that kind of symbol. But I wouldn’t want a normal variable-width font where colons are tiny and at-signs are gigantic. I read a programming email list in my regular webclient and it can be quite tiring. :)
- proc0 3y ago
  It seems we're really close to making language specific fonts. Haskell would certainly be a prime candidate for this.
  - int_19h 3y ago
    Fonts with "programming ligatures" have been a thing for some time now, and those ligatures tend to favor certain language families in practice.
    - proc0 3y ago
      Right, but they are general purpose monospace fonts. I would think something like a Haskell font or Python font would go beyond that and provide tailored designs for those languages. I wouldn't be surprised if those exist, but haven't seen them.
  - NikkiA 3y ago
    APL would say 'hi' using both its custom EBCIDIC code page(s) and its dedicated selectric ball.
  - pxc 3y ago
    Is Hasklig not already such a font? https://github.com/i-tu/Hasklig https://github.com/i-tu/Hasklig
- todd8 3y ago
  Another problem with using unicode in code is the handling of Unicode equivalence, compatibility, and normalization[1]. The same glyph can be produced in multiple ways. How is the reader, vim or emacs, and the compiler supposed to handle these cases? [1] https://en.wikipedia.org/wiki/Unicode_equivalence https://en.wikipedia.org/wiki/Unicode_equivalence
OkayPhysicist 3y ago
My favorite solution to this problem comes from the Julia community, where it's really, really nice to have your code representation of a mathematical formula look like the actual formula (because you need to work with scientists and engineers who know the formulas as math, and using the appropriate symbols makes reading it at a glance much, much easier): LaTeX. I type \Beta, press TAB, and boom, β.
- HappyPanacea 3y ago
  This is also how it works in Lean and in VSCode with the Lean extension it will also show you overlay saying how to type the symbol if you are unfamiliar with it. I'm not sure who came up with this feature first but it seems emacs has something similar so it probably came from there. (Edit: Someone else here thinks it originated in Plan 9) It works quite well. However, there is still a room for improvement: 1. Like was mentioned elsewhere in this thread on copy we could convert the symbol to how it is typed in order to support text (or even ASCII) only tools. 2. Better Integration with the browser and development tools like git so they get prettified when possible.
ctenb 3y ago
You can also insert unicode using XCompose (WinCompose on windows). The benefit is that this ability carries to other applications as well, which is pretty nice. I for one like to communicate about math over text channels like discord.
- cryptonector 3y ago
  TIL about WinCompose. Thanks!
- WorldMaker 3y ago
  Relatedly, I appreciate that most Unicode math symbols are in the built-in Windows emoji IME opened with Win+. or Win+; whichever feels more comfortable. Unicode math stuff is under the Omega (Ω) tab. The biggest shortcoming is that emoji themselves have type-to-search, but math/international symbols don't and you either get to mouse through it or arrow/tab/enter through it. But the nice advantage is that it has been built-in for several Windows versions now and you can count on it to work nearly everywhere.
pierrebai 3y ago
I think the fact that the author somehow thinks that Greek letters are prettier and easier to understand hints at an enormous bias. Many people would not know their names, most people are probably unfamiliar to Greek letters beyond beta or gamma, with some exceptions for pi, which has the dubious property of being confusingly ambiguous if the constant is meant or a simple high-brow variation on a variable named p. It's my conviction that there are a lot of things in computing that are made harder than they necessarily need to be by bad naming and chief amongst them is the insistence on borrowing mathematical notations and jargon. In my mind, it is mostly a question of elitism and exclusion.
- OkayPhysicist 3y ago
  Code should be easy to read to the relevant parties. If you're doing scientific code, the relevant parties know the math, and coming up with your own creative name merely obfuscates the meaning. It's not like programming is completely devoid of terms of the art already. What's a Class? or an Object? or a Map? Etc. Etc.
- whateveracct 3y ago
  I find this sort of thing mostly for fun. Sometimes your code is your code so who cares.
- jlg23 3y ago
  That "enormous bias" could also simply be that someone is using polar coordinates a lot. It's hard to not encounter rho and theta in literature about it... That's just one example, Greek letters have been used in science for a very long time and I personally find code that uses the same notation used in literature easier to reason about and much more pleasant to read.
texuf 3y ago
I’d like to voice the contrarian opinion that, as someone who isn’t a mathematician, these symbols make the code look like gibberish to me. I had to squint to even see the circle on the end of the lollipop symbol, no way I’m not mistaking that for a hyphen. I don’t know the names for these symbols, so my brain has to 1) learn new images, 2) pattern match them throughout the code. I would be totally lost. If the code used full names I could at least look them up and learn what they mean.
- jandrese 3y ago
  IMHO the mathematical language is an impediment for learning math for exactly this reason. It's chock full of cryptic symbols with no obvious meaning that make it incomprehensible to anyone who has not taken years to learn it and also surprisingly difficult to enter into a computer. Math is hard to read because quill pens were difficult to use and much of the syntax was made up on the spot by people who were better at thinking mathematically than communicating ideas. But so many people have spent the effort to learn it that nobody wants to create a "dumbed down" version that a layman might understand. It is kind of like everyone in the 60s decided that APL was the one true computer language and all interest in other languages died off entirely and when anybody complains about the syntax they are told that they just need to go to school for 4 years and they'll appreciate the beauty.
  - xchkr1337 3y ago
    If you open any reasonable math textbook (except for maybe logic related ones), chances are, you won't see the ∀ symbol anywhere at all. It's often considered bad taste to write a symbol like this when you can just write "for all". The main obstacle in learning math comes from not understanding the background material enough and basically never from not understanding the notation.
    - skydhash 3y ago
      And the notation are introduced to you gradually. Even books that do not have a chapter on the notation used, will have a reference page. If not, you’re not reading introductory material and some background is assumed.
dendodge 3y ago
Possibly a better way to achieve a similar level of prettiness would be (ab)use of vim's conceal feature. Through its judicious use, the author can have "forall" appear to them as ∀, "alpha" as α, etc., without imposing these symbols on their colleagues.
- gleenn 3y ago
  Agree, there is definitely a trade-off, I certainly don't know how to input those characters quickly even if the author states it is faster in Vim and I am not a Vim newbie. Also, if you get a stacktrace in a log file, do they still print nicely? Do they still print nicely if I'm viewing that stacktrace on a build server's web interface? There are probably some number of utilities that this code is "viewed" by that don't correctly handle non-ascii unicode and the usability would suffer at the expense of the beauty/terseness. They do look pretty though.
  - WJW 3y ago
    Well the article mentions Ctrl-k+FA to put in the ∀ symbol, but it should be fairly easy to make it output "forall" instead and then use the concealing feature to turn it into ∀. That would get you the best of both worlds, no?
  - OkayPhysicist 3y ago
    Honestly, I would have had this concern ~10 years ago, but it's 2023. Unicode is ubiquitous, to the point that you'd need to pretty aggressively go out of your way to find things breaking due to it.
    - cryptonector 3y ago
      Roboto Mono doesn't support all the math glyphs, even some of the ones TFA uses: https://news.ycombinator.com/item?id=36438765 https://news.ycombinator.com/item?id=36438765
    - jcparkyn 3y ago
      It's still much more annoying than it should be to input Unicode characters in most operating systems and text editors, though.
pacaro 3y ago
I use vim digraphs pretty extensively, but typically for comments, and not code. It's nice to be able to concisely document anything mathematical this way, it's also cute to be able to use the box drawing characters
omgmajk 3y ago
It looks pretty but in all honesty I would quit my job if someone forced me to do this.
- wryoak 3y ago
  Well, at least it’s pretty: that’s a step above standup and sprint planning meetings and you don’t quit your job over those do you?

61 points by romes 3y ago

I think the applicability of using maths symbols in a program is highly domain dependent. It'd be reasonable to use it for a physics simulation. You probably should not use it for a banking application.

cryptonector 3y ago

Are there newer versions of Roboto Mono that support all these Unicode codepoints? [EDIT: No, I checked and there are not[0].] The one I have does not support ∃, ∈, and ∷, and probably others. I agree that this is very pretty, but font support is absolutely critical if you're going to do this. [0] https://fonts.google.com/specimen/Roboto+Mono/glyphs

felurx 3y ago

A few people have mentioned the compose key as a way to insert Unicode characters system-wide. I also really like Espanso[0]: You can use it to replace any typed string with anything else, it even supports forms and executing scripts / shell commands. There's tons of fancy stuff you can do with it, but just mapping something like \alpha or :a* to ɑ is easy too. (For greek characters, there's a package that uses a syntax like \alpha\) [0]: https://espanso.org/ https://espanso.org/

todd8 3y ago

Using the equals sign (=) for assignment is unfortunate. Mathematically, a=a+5 is confusing. Algol 60 (and its grandchild Pascal) are a bit better and represent this as a:=a+5, but this is an odd notation too. A left pointing arrow would be a better notation for the common assignment statement, at least to me. Does this mean I'm ready to embrace the use of mathematical notation via unicode glyphs in programming? No. I have a math degree and after dozens of university courses on math I've seen a lot of math notation. This notation uses a dizzying number of symbols across various mathematical disciples. LaTeX allows one to use any of 75 distinct kinds of arrows alone! Left, right, doubled, up, down, diagonal to the upper right, looped, long, bidirectional, harpooned, wiggly, maps-to, and so forth. That's just the arrows. Why does LaTeX allow typesetting with so many distinct arrows? Because mathematicians use them as distinct concepts. I count 160 relational symbols available for use with standard LaTeX: less-than, equal, equivalent, congruent, subset, parallel, similar, approximate, the list goes on and on. See [1]. Mathematicians don't even use these symbols consistently. Consider the ubiquitous lambda, appearing all over in functional programming. Surely, the use of a lower-case greek lambda is prettier than spelling out the word 'lambda', but it may in many contexts not stand for an anonymous function. It's use as a symbol can also mean: wavelength of any wave, number of offspring, radioactive decay constant, occurrence density within a time interval, eigenvalues, charge density, Lagrange multiplier, empty string, and so forth. Wikipedia lists 24 distinct uses for lambda, [2]. Why do mathematicians, engineers, and scientists use so many different symbols? Because they are doing something fundamentally different with them than programmers. They use the symbols as abbreviations that will be understood by their audience, which might be students watching a lecture, readers of a technical article, or even themselves at some time in the future. The context in all of these uses is very different than the context of a program. The program must be precise and unambiguous, and the program may be one hundred times longer than a published math paper. For this reason, spelled out identifiers and keywords using standard ASCII glyphs are wordier and less "pretty" but are far more practical. [1] https://www.cmor-faculty.rice.edu/~heinken/latex/symbols.pdf https://www.cmor-faculty.rice.edu/~heinken/latex/symbols.pdf [2] https://en.wikipedia.org/wiki/Lambda#:~:text=Lambda%20indicates%20the%20wavelength%20of,originated%20from%20Evolution%20strategy%20notation https://en.wikipedia.org/wiki/Lambda#:~:text=Lambda%20indica....

hole_in_foot 3y ago

Unicode in code is a footgun.

bojo 3y ago

While I do think these look nice (appropriate even), maintaining consistency across a large team of devs is where this type of stylization breaks down. Not everyone is using the same code editor, not everyone's configuration is the same. At the end of the day it's easier to write and maintain the long-hand word versions.

llimllib 3y ago

I got confused because I tried to use ctrl-k and wasn't getting any results; after reading the docs, at least on my system (neovim on mac), ctrl-K (uppercase) is the proper shortcut for entering digraphs when in insert mode. (:help digraph)

ufo 3y ago

On Linux I input special characters using the Compose key. Works everywhere, not just in Vim.

pxc 3y ago
I do this, too. I haven't yet found a solution that works very well for macOS— a few years ago, some mappings were not possible with the solutions I found.
- fragmede 3y ago
  control-command spacebar brings up the emoji picker, and some of the symbols are in there, but like you said, not everything. ∀ ° ∫ Ω
  - pxc 3y ago
    I do really like modern emoji pickers in general. Compose keys are nice, but I love fuzzy filter interfaces that search as you type. Compared to compose sequences, they let you get up to a reasonable speed very quickly.
- goerz 3y ago
  I got you covered: https://michaelgoerz.net/notes/the-us-international-scientific-keyboard-layout/ https://michaelgoerz.net/notes/the-us-international-scientif...
gylterud 3y ago
Came here to mention this exactly. I have a quick intro to the compose key on my website [0] and an intro for how to use Unicode with Latex[1], and there are other resources around the web if you are looking. The idea of a compose key for Unicode originated in Plan 9, as far as I know. [0]: https://hakon.gylterud.net/tutorials/unicode.html https://hakon.gylterud.net/tutorials/unicode.html [1]: https://hakon.gylterud.net/tutorials/latex-maths-unicode.html https://hakon.gylterud.net/tutorials/latex-maths-unicode.htm...
cryptonector 3y ago

avgcorrection 3y ago

Unicode in code might be what pushes people to consider variable-width font. Just look at the simple arrow in a text editor (hopefully the text filter on this website thinks this symbol is OK): → (U+2192 RIGHTWARDS ARROW). It’s tiny. And I notice that the author uses plain `->`. You do need at least an “em” width for that kind of symbol. But I wouldn’t want a normal variable-width font where colons are tiny and at-signs are gigantic. I read a programming email list in my regular webclient and it can be quite tiring. :)

proc0 3y ago
It seems we're really close to making language specific fonts. Haskell would certainly be a prime candidate for this.
- int_19h 3y ago
  Fonts with "programming ligatures" have been a thing for some time now, and those ligatures tend to favor certain language families in practice.
  - proc0 3y ago
    Right, but they are general purpose monospace fonts. I would think something like a Haskell font or Python font would go beyond that and provide tailored designs for those languages. I wouldn't be surprised if those exist, but haven't seen them.
- NikkiA 3y ago
  APL would say 'hi' using both its custom EBCIDIC code page(s) and its dedicated selectric ball.
- pxc 3y ago
  Is Hasklig not already such a font? https://github.com/i-tu/Hasklig https://github.com/i-tu/Hasklig
todd8 3y ago
Another problem with using unicode in code is the handling of Unicode equivalence, compatibility, and normalization[1]. The same glyph can be produced in multiple ways. How is the reader, vim or emacs, and the compiler supposed to handle these cases? [1] https://en.wikipedia.org/wiki/Unicode_equivalence https://en.wikipedia.org/wiki/Unicode_equivalence

OkayPhysicist 3y ago

My favorite solution to this problem comes from the Julia community, where it's really, really nice to have your code representation of a mathematical formula look like the actual formula (because you need to work with scientists and engineers who know the formulas as math, and using the appropriate symbols makes reading it at a glance much, much easier): LaTeX. I type \Beta, press TAB, and boom, β.

HappyPanacea 3y ago
This is also how it works in Lean and in VSCode with the Lean extension it will also show you overlay saying how to type the symbol if you are unfamiliar with it. I'm not sure who came up with this feature first but it seems emacs has something similar so it probably came from there. (Edit: Someone else here thinks it originated in Plan 9) It works quite well. However, there is still a room for improvement: 1. Like was mentioned elsewhere in this thread on copy we could convert the symbol to how it is typed in order to support text (or even ASCII) only tools. 2. Better Integration with the browser and development tools like git so they get prettified when possible.

ctenb 3y ago

You can also insert unicode using XCompose (WinCompose on windows). The benefit is that this ability carries to other applications as well, which is pretty nice. I for one like to communicate about math over text channels like discord.

cryptonector 3y ago
TIL about WinCompose. Thanks!
WorldMaker 3y ago
Relatedly, I appreciate that most Unicode math symbols are in the built-in Windows emoji IME opened with Win+. or Win+; whichever feels more comfortable. Unicode math stuff is under the Omega (Ω) tab. The biggest shortcoming is that emoji themselves have type-to-search, but math/international symbols don't and you either get to mouse through it or arrow/tab/enter through it. But the nice advantage is that it has been built-in for several Windows versions now and you can count on it to work nearly everywhere.

pierrebai 3y ago

I think the fact that the author somehow thinks that Greek letters are prettier and easier to understand hints at an enormous bias. Many people would not know their names, most people are probably unfamiliar to Greek letters beyond beta or gamma, with some exceptions for pi, which has the dubious property of being confusingly ambiguous if the constant is meant or a simple high-brow variation on a variable named p. It's my conviction that there are a lot of things in computing that are made harder than they necessarily need to be by bad naming and chief amongst them is the insistence on borrowing mathematical notations and jargon. In my mind, it is mostly a question of elitism and exclusion.

OkayPhysicist 3y ago
Code should be easy to read to the relevant parties. If you're doing scientific code, the relevant parties know the math, and coming up with your own creative name merely obfuscates the meaning. It's not like programming is completely devoid of terms of the art already. What's a Class? or an Object? or a Map? Etc. Etc.
whateveracct 3y ago
I find this sort of thing mostly for fun. Sometimes your code is your code so who cares.
jlg23 3y ago
That "enormous bias" could also simply be that someone is using polar coordinates a lot. It's hard to not encounter rho and theta in literature about it... That's just one example, Greek letters have been used in science for a very long time and I personally find code that uses the same notation used in literature easier to reason about and much more pleasant to read.

texuf 3y ago

I’d like to voice the contrarian opinion that, as someone who isn’t a mathematician, these symbols make the code look like gibberish to me. I had to squint to even see the circle on the end of the lollipop symbol, no way I’m not mistaking that for a hyphen. I don’t know the names for these symbols, so my brain has to 1) learn new images, 2) pattern match them throughout the code. I would be totally lost. If the code used full names I could at least look them up and learn what they mean.

jandrese 3y ago
IMHO the mathematical language is an impediment for learning math for exactly this reason. It's chock full of cryptic symbols with no obvious meaning that make it incomprehensible to anyone who has not taken years to learn it and also surprisingly difficult to enter into a computer. Math is hard to read because quill pens were difficult to use and much of the syntax was made up on the spot by people who were better at thinking mathematically than communicating ideas. But so many people have spent the effort to learn it that nobody wants to create a "dumbed down" version that a layman might understand. It is kind of like everyone in the 60s decided that APL was the one true computer language and all interest in other languages died off entirely and when anybody complains about the syntax they are told that they just need to go to school for 4 years and they'll appreciate the beauty.
- xchkr1337 3y ago
  If you open any reasonable math textbook (except for maybe logic related ones), chances are, you won't see the ∀ symbol anywhere at all. It's often considered bad taste to write a symbol like this when you can just write "for all". The main obstacle in learning math comes from not understanding the background material enough and basically never from not understanding the notation.
  - skydhash 3y ago
    And the notation are introduced to you gradually. Even books that do not have a chapter on the notation used, will have a reference page. If not, you’re not reading introductory material and some background is assumed.

dendodge 3y ago

Possibly a better way to achieve a similar level of prettiness would be (ab)use of vim's conceal feature. Through its judicious use, the author can have "forall" appear to them as ∀, "alpha" as α, etc., without imposing these symbols on their colleagues.

gleenn 3y ago
Agree, there is definitely a trade-off, I certainly don't know how to input those characters quickly even if the author states it is faster in Vim and I am not a Vim newbie. Also, if you get a stacktrace in a log file, do they still print nicely? Do they still print nicely if I'm viewing that stacktrace on a build server's web interface? There are probably some number of utilities that this code is "viewed" by that don't correctly handle non-ascii unicode and the usability would suffer at the expense of the beauty/terseness. They do look pretty though.
- WJW 3y ago
  Well the article mentions Ctrl-k+FA to put in the ∀ symbol, but it should be fairly easy to make it output "forall" instead and then use the concealing feature to turn it into ∀. That would get you the best of both worlds, no?
- OkayPhysicist 3y ago
  Honestly, I would have had this concern ~10 years ago, but it's 2023. Unicode is ubiquitous, to the point that you'd need to pretty aggressively go out of your way to find things breaking due to it.
  - cryptonector 3y ago
    Roboto Mono doesn't support all the math glyphs, even some of the ones TFA uses: https://news.ycombinator.com/item?id=36438765 https://news.ycombinator.com/item?id=36438765
  - jcparkyn 3y ago
    It's still much more annoying than it should be to input Unicode characters in most operating systems and text editors, though.

pacaro 3y ago

I use vim digraphs pretty extensively, but typically for comments, and not code. It's nice to be able to concisely document anything mathematical this way, it's also cute to be able to use the box drawing characters

omgmajk 3y ago

It looks pretty but in all honesty I would quit my job if someone forced me to do this.

wryoak 3y ago
Well, at least it’s pretty: that’s a step above standup and sprint planning meetings and you don’t quit your job over those do you?