xeno_by (xeno_by) wrote,
xeno_by
xeno_by

Categories:

Метапрограммирование в Агде и немного философии

На днях просмотрел паперу Dependent Type Providers [1] и магистерскую диссертацию Reflection in Agda [2], которые используют средства рефлекшена, предоставляемые Агдой, для метапрограммирования.

Прикольно было увидеть как народ брутфорсит некоторые вещи (например, подмножество функциональности тайп провайдеров) просто за счет того, что в Агде более мощная система типов.

Но самое интересное было в том, что, несмотря на навороченность системы типов, в Агдовском рефлекшене наблюдаются примерно те же самые проблемы, с которыми мы боремся в Скале:
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
Tags: macros, scala
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 75 comments