?

Log in

No account? Create an account

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

Aug. 27th, 2013

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

Previous Entry Share Next Entry

Comments:

From:Valentin Budaev
Date:August 27th, 2013 10:09 pm (UTC)
(Link)
> Мне кажется, метапрограммирование достаточно нетривиально для того, чтобы его реализовывать в стиле "тяп-ляп и в продакшен". Примеры Скалы и Агды это неплохо доказывают. Поэтому, на мой взгляд, здесь нужна какая-то научная база.

Это очевидно. Но я думаю, оно в данный момент просто недостаточно развито для формализации (_особенно_ для метапрограммирования в статике, тут кроме немерлей (которых почти никто не знает) и скалы (в которой оно сейчас на уровне "все может фундаментально поменяться в любой момент", как я понимаю) я ничего больше и не припомню). Сейчас тот уровень, когда все пытаются сделать что-то как-то по наитию (весьма хаотично), уровень первоначального накопления фактов. Со временем это дело выкристаллизуется, тогда и станет понятно - как, зачем и почему.

А сейчас даже такие банальные вещи, как формальное определение гигиены - это какой-то непонятный рокет саенс. Больше непонятный, чем рокет, что и плачевно.

Так что нам на данный момент требуется просто много разных проработанных макросистем - плохих, хороших, выразительных или нет - не так важно, главное, чтобы разных и как-то работающих. И потом уже по этому делу можно "агрегировать". Вот вы сами какие-то общие недостатки уже фиксируете - вот оно начало.

> Почему-то считается, что интересными являются только статически типизируемые генераторы кода

Так ниже ответ:

> науку интересуют проблемы _теоретически красивого_ МП

ЗЫ: А можете, кстати, несколько подробнее описать указанные в ОП-посте проблемы? А то по краткому описание не понятно, в чем суть.

Edited at 2013-08-27 10:12 pm (UTC)
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 27th, 2013 10:13 pm (UTC)
(Link)
В Немерле особо и формализации-то нет, т.к. народ не заморачивался насчет работ на серьезных конференциях. А у нас вообще нет ничего работающего кроме низкоуровневой макросистемы на ручной тяге, поэтому Скала вообще не считается :)
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 27th, 2013 10:31 pm (UTC)
(Link)
Ну вот. Откуда возьмется формализация, когда нечего формализовывать? :)

А немерлисты со своим немерле 2 вообще ушли не в те степи. Изначальная идея (объединить экспанд с тайпчеком) вроде и годна, но в результате у них получается какой-то ОБЧР с пиу-пиу лазерами из глаз и торчащим во лбу тентаклем, а не макросистема.

Вот на вас, выходит, вся надежда - если скала и ее макры будут успешны, то идея может пойти в массы (будут появляться другие языки с выразительными статическими макросистемами), будет материал для работы.

А на текущем уровне не ясно, в какую сторону идти. Никто никуда и не идет :)
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 27th, 2013 10:41 pm (UTC)
(Link)
Будем стараться! Вот буквально сейчас думаем над тем, как именно прикрутить гигиену. Есть несколько вариантов - как минимум пути Схемы, Немерле и Темплейт Хаскелла. Плюс, еще есть вариант на ручной тяге, но его не считаем. У всех есть свои трейд-оффы и свои сложности в реализации, поэтому поступало даже предложение забить на гигиену, но сейчас не время для малодушия :)
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 27th, 2013 11:29 pm (UTC)
(Link)
> Вот буквально сейчас думаем над тем, как именно прикрутить гигиену.

Не забудьте сразу подумать об удобных путях обхода и средствах "обхода гигиены без ее нарушения" (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) (Parent) (Thread) (Expand)
[User Picture]
From:xeno_by
Date:August 27th, 2013 10:43 pm (UTC)
(Link)
А что там с тентаклем? Я, если честно, особо не следил за последними событиями в N2. Есть ли там что-то новое, что вы имеете ввиду, или же вам в целом не нравится предложенный фреймворк для тайпчека?
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 27th, 2013 11:16 pm (UTC)
(Link)
Мне не нравится универсальность, которой они хотят добиться, сделать вроде как "фреймоврк для разработки типизированных ЯП". Понятно, что в достаточно выразительной макросистеме можно навернуть все что угодно поверх хост-языка - но обычно эта возможность больше теоретическая и на практике стоит больших трудозатрат. А когда постулируется что "наша система удобно решает любую задачу", то это на практике значит, что она все задачи решает одинаково неудобно. Но, конечно, может и что-то удачное получиться вы итоге - заранее тут не скажешь.
(Reply) (Parent) (Thread)
[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)
[User Picture]
From:xeno_by
Date:August 27th, 2013 10:37 pm (UTC)
(Link)
Кстати, в Template Haskell все в порядке с гигиеной. Переменные, которые биндятся к глобальным определениям, реифицируются как fully qualified ссылки на эти определеня, а переменные, которые биндятся к локальным определениям, переименовываются (см. страницу 25 презентации https://github.com/scalamacros/scalamacros.github.com/blob/master/paperstalks/2012-09-10-CandidacyExamSlides.pdf?raw=true).

Единственная проблема, что там у всех квазицитат биндинги должны ресолвиться статическим образом, т.е. [| f $p = x + y |] работать не будет.
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 27th, 2013 11:34 pm (UTC)
(Link)
Конечно же в TH все в порядке - делать макросистему со статическими гарантиями корректности и без гигиены было бы, как минимум, странно :) Речь шла о формальном определении гигиены. На интуитивном уровне всем понятно, что это за зверь, и реализации гигиены - есть, но вот нормального формально строгого определения - нет. Я выше кинул ссылку на статью по этой теме как раз.

ЗЫ: посмотрел обход гигиены в TH на 19 странице слайдов - это, конечно, тихий ужас. Взять и переложить ответственность на пользователя макроса - архигениальное решение.

Edited at 2013-08-27 11:44 pm (UTC)
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 28th, 2013 05:59 am (UTC)
(Link)
Вы имеете ввиду $(dyn "it") на страничке, на которой справа-снизу написано 26?
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 28th, 2013 11:17 am (UTC)
(Link)
Ага, его.

Ну TH вообще в целом как макросистема на мой взгляд предельно неудобен.
(Reply) (Parent) (Thread) (Expand)
From:Valentin Budaev
Date:August 27th, 2013 11:58 pm (UTC)
(Link)
Да, еще, на счет примера с Racket:

(require syntax/parse/define)

(define-simple-macro (aif cond:expr then:expr else:expr)
#:with it (datum->syntax #'aif 'it)
(let ([tmp cond]
[it cond])
(if it then else)))

(define-simple-macro (aunless cond:expr then:expr else:expr)
(aif (not cond) then else))


не работает, конечно, зато вот


(define-simple-macro (aif cond:expr then:expr else:expr)
#:with it (syntax-local-introduce #'it)
(let ([tmp cond]
[it cond])
(if it then else)))

(define-simple-macro (aunless cond:expr then:expr else:expr)
(aif (not cond) then else))

работает вполне. Это и есть правильный обход, syntax->datum - это низкоуровневый инструмент для конструкции идентификаторов, его надо использовать весьма осторожно.

Edited at 2013-08-28 12:00 am (UTC)
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 28th, 2013 05:58 am (UTC)
(Link)
Я этот сниппет с datum->syntax брал из паперы http://www.schemeworkshop.org/2011/papers/Barzilay2011.pdf. Можете, пожалуйста, объяснить, в чем разница между datum->syntax и syntax-local-introduce?

Также, есть ли где-то гайд на эту тему? Я помню, что, когда разбирался с Ракетом, именно в этом направлении столкнулся с проблемами. Много разной документации, но совершенно непонятно как все вместе укладывается в большую картину.
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 28th, 2013 11:14 am (UTC)
(Link)
Для этого надо понимать алгоритм работы гигиены в Racket. С каждым идентификатором проассоциирован набор syntax marks's. Два одноименных идентификатора могут быть связаны друг с другом тогда и только тогда, когда их marks не отличаются, то есть актуальный биндинг идентификатора - последний биндинг, появившийся до расхождения набора marks. Во время каждого раскрытия макроса генерируется своя уникальная mark и применяется рекурсивно к syntax object'у, потом этот object обрабатывается трансформером (собственно, логика макроса) и дальше к результату опять применяется та же mark. При этом если к объекту два раза подряд применяется одна и та же mark, то они взаимоуничтожаются. Выходит, что у идентификаторов, которые пришли макросу на вход, mark остается тот же, а к идентификаторам, сгенеренным макросом, добавляется mark макровызова. На примере, допустим у нас есть такой макрос:

(define-syntax-rule (macro arg) (let ([x 1]) (+ x arg)))

и мы его вызываем:
(let ([x 2]) (macro x))

(дальше включите Dr.Racket, напишите эти две формы и запустите макростеппер, активируйте stepper -> view syntax properies и stepper->extra options->one term at time, теперь все описанное будет зрительно видно - биндинги стрелочками при наведении на идентификатор, наборы марок - цветами, тыкнув на объект можно посмотреть все его свойства в окне справа)

сперва раскрывается само тело определения макроса и устанавливаются биндинги внутри него (и в квазицитате (let ([x 1]) (+ x arg)))). В этой точке уже связан + и let (т.о. фиксируется, что это + и let из стандартной библиотеки), а х остается свободной (это делается в раскрытии 1 фазы, то есть в степере уже будет сделано, т.к. стоит "hide phase > 0").

далее мы раскрываем (let ([x 2]) (macro x)) и устанавливается связывание для х=2 (то же сделано т.к. стоит "hide library syntax", можете поубирать эти hide галочки потом и посомтреть эти этапы более подробно). Потом раскрываем (macro x), сгенерируется марк с каким-то номером, этот марк применится рекурсивно к форме #'(macro x), соответственно, к идентификаторам #'x и #'macro (второе в дальнейшем важно!). Дальше #'x (уже с маркой и связыванием) подставляется на место arg и запускается макрос. Формируется форма (let ([x 1]) (+ x x)) и к ней опять рекурсивно применяется та же марка, результат возвращается из макроса. Т.о. у нас марка стоит на let, +, x в [x 1] и первом х в (+ x x), на втором х в (+ x x) марки нет. let и + были связаны до появления марок и все ок, так что теперь раскрывается сам этот let, х в let и первый х имеют одинаковые наборы марок - и связываются, второй х марок не имеет - по-этому не связывается, так что остается со своим связыванием во внешней let-форме.

Собственно, (syntax-local-introduce #'x) делает ни что иное, как применяет текущую марку к х, т.о. если х введен макросом, то он "выводит" х из-под гигиены (то есть х в итоге окажется без марки вовсе). (syntax->datum #'x 'y) предназначен для того, чтобы передать весь лексический контекст с х на y (и кроме того еще может передавать source location, syntax properties и вообще все свойства, какие есть у syntax object). Почему "не композируется" вариант с syntax->datum? У нас сперва раскрывается макрос aunless, который вешает на aif свою марку, потом начинает раскрываться aif и когда в нем делаем (syntax->datum #'aif 'it) то на it ложится марка с aif, которая там из aunless. А на it в форме макровызова (aunless 1 it it) никаких марок нет - в результате unbound variable.

> Также, есть ли где-то гайд на эту тему?

Только Racket Reference, в разделе syntax model, если не ошибаюсь. Больше не видел.

> Я этот сниппет с datum->syntax брал из паперы

Как я понимаю, везде суют этот datum->syntax, т.к. это классическое схемное решение (syntax-local-introduce в схеме нет, это чисто ракетовская фишка, связанная именно с ракетовской гигиеной, ну то есть конкретно с ее алгоритмом).
(Reply) (Parent) (Thread) (Expand)