It makes the code look absolutely gorgeous, readable and it's very easy to type too. I use Emacs agda-mode so it just automatically replaces e.g. \r with → or \== with ≡ etc...
I don't use Agda for theorem proving, I make real life programs in Agda, I compile them to Haskell and compile with GHC to executables.
That's pretty cool. What kind of problems do you find yourself solving with your Agda code?
(Or, asked another way, what sort of stuff do your programs do?)
Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling.
Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.
Julia also allows Unicode characters, which I think is great for math-heavy programs. I love that about it. I always forget the keybindings for them though.
agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.
Pretty much, yes. It's not "required" required, but in order to use the stdlibrary (i.e. use Unicode chars) you need to use Emacs and Emacs mode is extremely useful to develop Agda code. You can still compile and type check using `agda` binary but that's pretty much the only thing you can do.
There's a full rune reference available at https://urbit.org/docs/reference/hoon-expressions/rune/, but tldr they're group into families, with the first character being broadly what it does. AST nodes that have to do with "conditionals" are ?:, ?., ?@, etc.
I don't think anyone uses non-ASCII diagraph fonts for them, but it wouldn't be a big jump.
Obviously it belies a very anglo-centric view of the computer engineering landscape, but frankly I think that's a good thing, as it allows easier exchange.
Comments
It's interesting to me to see these projects as alt-history, and see them as the dead-end technical choice that they were.
Has any programming language since then tried to use more than ASCII for its keywords?
I program in Agda pretty often and community usually uses Unicode characters for most things, so I do too.
The impl of AVL trees in stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Data/Tre...
Some basic properties of natural numbers: https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...
It makes the code look absolutely gorgeous, readable and it's very easy to type too. I use Emacs agda-mode so it just automatically replaces e.g. \r with → or \== with ≡ etc...
I don't use Agda for theorem proving, I make real life programs in Agda, I compile them to Haskell and compile with GHC to executables.
What font do you use for this? It looks weird with my defaults.
I once seriously considered trying to build something that included math symbols in the syntax. It's pretty cool to see that I don't have to.
Not currently on my computer with that setup but afair I use Inconsolata.
That's pretty cool. What kind of problems do you find yourself solving with your Agda code? (Or, asked another way, what sort of stuff do your programs do?)
Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling.
Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.
Julia also allows Unicode characters, which I think is great for math-heavy programs. I love that about it. I always forget the keybindings for them though.
agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.
I think Emacs is basically required to use Agda, right? To the point that the set of Agda users is a strict subset of the set of Emacs users.
Pretty much, yes. It's not "required" required, but in order to use the stdlibrary (i.e. use Unicode chars) you need to use Emacs and Emacs mode is extremely useful to develop Agda code. You can still compile and type check using `agda` binary but that's pretty much the only thing you can do.
Haskell's GHC compiler has a tiny UnicodeSyntax extension and some packages that explore the idea further.
UnicodeSyntax: https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...
Base Library Symbols: http://hackage.haskell.org/package/base-unicode-symbols
Containers Library Symbols: http://hackage.haskell.org/package/containers-unicode-symbol...
Mathematica does this, and they solve the keyboard problem with floating palettes of symbols.
They also have ESC symbolname ESC, with autocomplete.
The Z ("zed") notation -- but that is a non-executable specification language:
https://en.wikipedia.org/wiki/Z_notation
Racket uses λ for “lambda” and it’s pretty common in Racket code.
Urbit's programming language Hoon uses two character "runes" instead of keywords. Here's the standard library and compiler source, for example: https://github.com/urbit/urbit/blob/master/pkg/arvo/sys/hoon...
There's a full rune reference available at https://urbit.org/docs/reference/hoon-expressions/rune/, but tldr they're group into families, with the first character being broadly what it does. AST nodes that have to do with "conditionals" are ?:, ?., ?@, etc.
I don't think anyone uses non-ASCII diagraph fonts for them, but it wouldn't be a big jump.
Obviously it belies a very anglo-centric view of the computer engineering landscape, but frankly I think that's a good thing, as it allows easier exchange.