Unit testing Agda code, redux

[pozorvlak]

My post about unit-testing Agda code using elisp was posted to the dependent types subreddit (of which I was previously unaware). There, the commenter stevana pointed out that you could achieve the same effect using the following Agda code:

test1 : 2 + 1 == 3
test1 = refl

test2 : 3 + 0 == 3
test2 = refl

If your test fails, you'll get a compile-time error on that line. Aaaaaaaargh. I do wish someone had told me that before I spent a week mucking about with elisp. Well, that's not quite true - I learned a lot about Emacs, I had some fun writing the code, I learned some things about Agda that I might otherwise not have done, I got some code-review from aaroncrane, and I had a chance to try out using darcs and patch-tag for a collaborative project (the experience, I'm afraid, didn't measure up well against git and GitHub).

What I'd failed to realise, of course, is that the == type constructor describes computable equality: a == b is inhabited if the compiler can compute a proof that a is equal to b. "They both normalise to the same thing" is such a proof, and obviously one that the compiler's smart enough to look for on its own.

Ordinarily, a testcase is better than a compile-time assertion with the same meaning, because you can attach a debugger to a failing test and investigate exactly how your code is broken. This doesn't mean that types are stupid - types draw their power from their ability to summarise many different testcases. But in this case, I don't think there's much reason to prefer our approach to stevena's: the slight increase in concision that agda-test allows is balanced out by its inability to coerce both expressions to the same type, which often means the user has to type a lot more code. Stevena's approach does not suffer from this problem.

This also makes me more positive about dependent typing: if simple testcases can be incorporated into your type-system so easily, then maybe the "types are composable tests" slogan has some truth to it.

But seriously, guys, macros.

Comments

<lj user=pozorvlak>, написавший систему юнит-тестов на Лиспе дл

[pingback-bot.livejournal.com]

User thesz referenced to your post from pozorvlak, написавший систему юнит-тестов на Лиспе для Agda2... (http://thesz.livejournal.com/1186365.html) saying: [...] ...продолжил экспедицию в мир тестирования в зависимых типах [...]

[andrewducker]

You've ended up on HN:
http://news.ycombinator.com/item?id=2245960

Such as finding aliens in the United States United Kingdom

[(Anonymous)]

Useful information and excellent design, you came here! I want to thank you for sharing your thoughts and your things into the release time! Great work!

Meble dla dzieci - Meble dla dziecka

[(Anonymous)]

Obmyslajac umeblowanie pomieszczenia w meble dla dzieci trzeba zwrocic uwage na pare waznych kwestii, ktore pojawia sie w przyszlosci w zwiazku z dojrzewaniem dziecka. [url=http://www.meble-dla-dzieci-meble-dla-dziecka.com.pl]meble dla dzieci[/url] Nowo narodzony bobas potrzebuje bliskosci mamy bardziej niz osobistego pokoju, natomiast przedszkolak potrzebuje juz wiecej, chocby lozeczka, do ktorego sie przyzwyczai. Szkolnemu uczniowi potrzebne bedzie biurko, natomiast mlodzieniec wymaga mebli, ktore zapewnia mu przechowywanie plyt i rynsztunku sportowego. Wyposazenie pokoju powinno nadazac za rozkwitem i wzrastajacymi potrzebami dziecka. [url=http://www.meble-dla-dzieci-meble-dla-dziecka.com.pl]meble dla dziecka[/url] bardzo roznia sie od mebli dla osoby dojrzalej pod wieloma wzgledami. Wynika to w glownej mierze z odmiennych potrzeb dziecka. Nade wszystko meble dzieciece powinny byc w pelni bezpieczne. Budowa takich sprzetow powinna byc trwala.

meble dla dzieci (http://www.meble-dla-dzieci-meble-dla-dziecka.com.pl)
meble dla dziecka (http://www.meble-dla-dzieci-meble-dla-dziecka.com.pl)