Learn you an Agda (2011) | Hacker News Reader

Learn you an Agda (2011)

learnyouanagda.liamoc.net

80 pointsjxub8 comments

While this starts strong, a heads up: it peters out quick. There's only about an hour of material here, and the last of the three parts is unfinished, in the sense that there are gaps, not just an abrupt ending.

After finishing this I jumped over to wadler/kokke's programming language theory in AGDA:

https://wenkokke.github.io/sf/

Which is also unfinished, but generally more comprehensive and better motivated. It also stands a much greater probability of being continued.

Verified Functional Programming in Agda is the best Agda resource available, but studying Idris via Type-driven Development with Idris will net you very transferable insights. These are research languages, so the ideas are extremely interesting but not production ready. What I like about working in Agda is: proofs are verified by the compiler (so I know when I've proved enough), dependent types blurs the lines between types and values in a way that makes expressing complex typing relations no bother at all, and that mixfix operators let you create some really neat syntax. (Aspiring) computer scientists will be well of taking a look.

Why always Peano numbers? If it's doable, I'd love to see something like a web server with provable safety guarantees (e.g. eliminating any SQL injection risk), or a concurrent system with the compiler proving there are no races, even though the code is sharing memory. Or just proving that some simple business rules hold. Is stuff like that doable in a dependently typed language?

We start with Paeno numbers because they are probably the simplest inductive data type that set the scene for how we tend to proves things in dependently typed programming (inductive reasoning). Proving the things you want are probably doable (I can't say for certain, they are vaguely specified which does not fit with formal methods), but significantly more involved. Trying to take the reader from nothing to that in a single blog post or talk is beyond anyone's ability. Generally, this is because dependent types aren't quite ready for mainstream in terms of convenience.

That said, I'd read some of Edwin Brady's research, as he is actively trying to find the intersection of "business programming" and dependent types: https://edwinb.wordpress.com/publications/

It's not Agda, but you may be interested in this article by Foursquare about how they use Scala Phantom Types to ensure MongoDB queries are semantically well formed at compile time:

https://engineering.foursquare.com/going-rogue-part-2-phanto...

Yes, it's possible but might require a lot of effort. For example, my thesis was about creating a system where actors send messages to each other and the system guaranteed that you could not send messages with an unexpected type to another actor. Extending that, you could create a system where messaging has to follow an exact protocol, ensuring that there can be no deadlocks. You can read my work here: https://www.dropbox.com/s/lczrcqu2m9p6osv/Master_Thesis.pdf?... and the code is here: https://github.com/Zalastax/singly-typed-actors

You might like this talk [1] about building a better regex library using dependent type style features. It is really great! The regex is parsed at compile time and then can return better typed information about the capture groups to the lib user. There is also this interview I did with the author on it [2]

[1] https://thestrangeloop.com/2017/dependent-types-in-haskell.h...

[2] https://corecursive.com/015-dependant-types-in-haskell-with-...

Conor McBride's lecture series CS410 at Strathclyde is freely available on Youtube, and my team is watching that at lunchtimes - excellent gentle introduction to proofs-as-types and so forth, and it has turned me onto Agda as a theorem proving environment.

Reply on news.ycombinator.com