Hacker News Reader

Comment by gnulinux | Hacker News Reader

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.

View on HN

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 use Emacs agda-mode

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.

Reply on news.ycombinator.com