Прикольно было увидеть как народ брутфорсит некоторые вещи (например, подмножество функциональности тайп провайдеров) просто за счет того, что в Агде более мощная система типов.
Но самое интересное было в том, что, несмотря на навороченность системы типов, в Агдовском рефлекшене наблюдаются примерно те же самые проблемы, с которыми мы боремся в Скале:
1) Низкоуровневость API синтаксических деревьев
2) Невозможность использовать квазицитирование для нетипизированных фрагментов кода
3) Отсутствие возможности создавать новые конструкторы данных во время компиляции
4) Протекание деталей реализации (например, [3])
На мой взгляд, это очень показательный факт для иллюстрации того, что удобное метапрограммирование не получается автоматически из факта продвинутости языка программирования. Для метапрограммирования необходим серьезный доменно-специфичный фундамент [4].
[1] https://groups.google.com/forum/#!topic/scala-internals/B9g31aAkebE
[2] http://igitur-archive.library.uu.nl/student-theses/2012-1030-200720/UUindex.html
[3] http://code.google.com/p/agda/issues/detail?id=466
[4] http://xeno-by.livejournal.com/85721.html
