Hacker News Reader

Comment by lelf | Hacker News Reader

I like to show you the immense beauty of the Agda standard library: http://agda.github.io/agda-stdlib/html/README.html (all clickable and…you'd better have proper unicode fonts).

View on HN

Even something as mundane as Data.Bool is beautiful, defining False in terms of bottom.

I love to look at unicode, but is it a pain to type it in practice, even given emacs?

I don’t use Agda, but for most mathy Unicode input, I use C-\ (toggle-input-method) and choose TeX mode. Then you can type “\forall\alpha. \alpha \to \alpha” and get back “∀α. α → α”, which is pretty good. There is also C-x 8 RET if you want to type a particular Unicode character by name or code point number.

Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0]

[0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...

Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are.

What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like

    theorem1 : T (1 - 1 == 0)

which is somewhat interestingly different from

    theorem2 : 1 - 1 = 0

in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).

Reply on news.ycombinator.com