Метапрограммирование в Агде и немного философии
На днях просмотрел паперу Dependent Type Providers [1] и магистерскую диссертацию Reflection in Agda [2], которые используют средства рефлекшена, предоставляемые Агдой, для метапрограммирования
( Read more... )
Достижения на фронте макро-языков с динамической типизацией весьма впечатляют, но собратья со статической типизацией на спешат перенять передовой опыт. Почему-то считается, что интересными являются только статически типизируемые генераторы кода (т.е. такие генераторы, которые гарантированно производят код, корректный с точки зрения типов). Возьмем, к примеру, MetaML/MacroML, последние новшества в Template Haskell, вот тот же quoteTerm в Agda или примеры из последней главы магистерской диссертации, приведенной выше. На средства написания таких генераторов бросаются неслабые силы, а все остальное либо игнорируется (как в MacroML), либо оставляется в недоделанном состоянии.
Получается замкнутый круг. Для практичного МП в языках со статической типизацией нужна научная база, но науку интересуют проблемы теоретически красивого МП, который довольно далек от практики.
Reply
Это очевидно. Но я думаю, оно в данный момент просто недостаточно развито для формализации (_особенно_ для метапрограммирования в статике, тут кроме немерлей (которых почти никто не знает) и скалы (в которой оно сейчас на уровне "все может фундаментально поменяться в любой момент", как я понимаю) я ничего больше и не припомню). Сейчас тот уровень, когда все пытаются сделать что-то как-то по наитию (весьма хаотично), уровень первоначального накопления фактов. Со временем это дело выкристаллизуется, тогда и станет понятно - как, зачем и почему.
А сейчас даже такие банальные вещи, как формальное определение гигиены - это какой-то непонятный рокет саенс. Больше непонятный, чем рокет, что и плачевно.
Так что нам на данный момент требуется просто много разных проработанных макросистем - плохих, хороших, выразительных или нет - не так важно, главное, чтобы разных и как-то работающих. И потом уже по этому делу можно "агрегировать". Вот вы сами какие-то общие недостатки уже фиксируете - вот оно начало.
> Почему-то считается, что интересными являются только статически типизируемые генераторы кода
Так ниже ответ:
> науку интересуют проблемы _теоретически красивого_ МП
ЗЫ: А можете, кстати, несколько подробнее описать указанные в ОП-посте проблемы? А то по краткому описание не понятно, в чем суть.
Reply
Reply
А немерлисты со своим немерле 2 вообще ушли не в те степи. Изначальная идея (объединить экспанд с тайпчеком) вроде и годна, но в результате у них получается какой-то ОБЧР с пиу-пиу лазерами из глаз и торчащим во лбу тентаклем, а не макросистема.
Вот на вас, выходит, вся надежда - если скала и ее макры будут успешны, то идея может пойти в массы (будут появляться другие языки с выразительными статическими макросистемами), будет материал для работы.
А на текущем уровне не ясно, в какую сторону идти. Никто никуда и не идет :)
Reply
Reply
Не забудьте сразу подумать об удобных путях обхода и средствах "обхода гигиены без ее нарушения" (http://www.schemeworkshop.org/2011/papers/Barzilay2011.pdf), оно покрывает большую часть юзкейсов обхода.
Вот с этой статьей знакомы, кстати: http://www.ccs.neu.edu/home/dherman/research/papers/esop08-hygiene.pdf ?
И более подробно в диссертации: http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf
В nemerle, кстати, вполне схемная гигиена, конкретно - как в Racket (привязка идентификатора к контексту). И это единственный правильный путь, на мой взгляд. Вариант с TH (а также явные ренейминги и т.п.) кажется ограниченным - непонятно, как лифтануть идентификатор из контекста в контекст. Хотя может я просто плохо знаю TH.
Reply
Reply
Reply
Reply
Например, это используется в Racket в паттерн-матчинге по структурам - форма (struct struct-name ...) связывает со struct-name статическую информацию о свойствах структуры (гетеры, ацессоры, базовая структура и т.п.), потом когда мы делаем (match x [(struct-name ...) ...]), то match проверяет (статически, во время экспанда) - действительно ли struct-name структура, и, если да, то разбирает ее с помощью указанных в полученной информации геттеров.
Но тут все делается на ручном приводе, ага :)
А если сумеем трекать биндинги - то сможем автоматически туда-сюда гонять.
Reply
Мне пока не приходит в голову ничего умнее, чем запоминать: 1) весь исходный файл (только один файл, не весь проект), в котором определена квазицитата, 2) позицию квазицитаты в исходнике.
Reply
Про алгоритм гигиены я ниже рассказал, ну там надо просто потыкать в экспандере и будет все понятно :)
А вот именно с тем как привязывается к идентификаторам лексический контекст и как с ним работают (в частности, как работают let-формы, partial-expand в internal definitions и т.п.) - это какое-то страшное колдунство. По идее, можно самому руками устанавливать связывания (и реализовывать let-формы низкоуровнево, то есть связывать переменные, не раскрывая макрос в define/let-форму), но в доках описано мало и криво. Я все собирался порыться в исходник и разобраться, что да как - но так руки и не дошли.
> 2) позицию квазицитаты в исходнике.
В racket работают с source object - который, в частности, имеет source location. Вам в любом случае нужно будет рано или поздно этот source location для квазицитат (и подобъектов) устанавливать - иначе будет большая беда с обработкой ошибок в макрах.
Что до контекстов - как я понимаю, там просто во время экспанда, когда видим let-форму, то создаем контекст, который содержит связанные переменные (когда видим define - добавляем идентификатор в контекст модуля), контексты могут друг в друга вкладываться, сами идентификаторы содержат ссылки на контекст, соответственно. По крайней мере, глядя на ихнее АПИ, все должно примерно так быть.
Или вы про сериализацию контекстов? А зачем оно?
Reply
Reply
Reply
Reply
Reply
Leave a comment