?

Log in

No account? Create an account

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

Aug. 27th, 2013

09:49 am - Метапрограммирование в Агде и немного философии

Previous Entry Share Next Entry

Comments:

[User Picture]
From:xeno_by
Date:August 27th, 2013 10:27 pm (UTC)
(Link)
1) В диссертации по рефлекшену автор пишет, что пришлось изобрести надстройку над API деревьев для того, чтобы было хоть как-то удобно их анализировать. Плюс, как я понимаю, переменные в деревянном API представляются голыми индексами де Брауна, что не очень-то удобно (голые имена, как у нас, тоже неудобные, конечно).

2) Из Agda 2.3.0 release notes (https://lists.chalmers.se/pipermail/agda/2011/003560.html): "...New keyword: quoteTerm... 1. The type of t is inferred. The term t must be type-correct...". К сожалению, на практике невероятно часто нужны квазицитаты, которые не типизируются по одиночке. На quoteTerm их не реализовать, поэтому придется использовать голые деревья. Мы в Скале проходили через точно то же самое.

3) Это из паперы про Dependent Type Providers. Местные тайп провайдеры не могут создать новые конструкторы данных - только типы, основанные на существующих конструкторах. Учитывая то, что Агда зависимо типизированная, это совсем неплохо (например, рекорды с динамически именуемыми полями можно эмулировать гетерогенными списками с ассоциированными метаданными, что, кстати, возможно и в Скале), но это не идеально.

4) Тут, я думаю, довольно понятно из ссылки: http://code.google.com/p/agda/issues/detail?id=466. Из-за того, что нет продуманного фундамента для МП, приходится использовать существующие в компиляторе механизмы в публичном API. Такие механизмы обычно не рассчитаны на публичное потребление в неожиданных контекстах, поэтому могут время от времени обламываться. Если что, это было про Скалу. Я совсем не знаком с внутренним устройством Агды, поэтому там ситуация может оказаться совсем другой, но вышеприведенная гипотеза мне кажется вполне правдоподобной.

Edited at 2013-08-27 10:28 pm (UTC)
(Reply) (Parent) (Thread)