?

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 09:40 pm (UTC)
(Link)
Вопрос не такой праздный, как кажется. Нельзя понять, _как_ формализовать, если мы не знаем, _зачем_. И ответ: "плохо с научной точки зрения", очевидно, плохой ответ на вопрос: "зачем?". В плане - неконструктивный.

Гвозди молотком вот мы тоже безо всякой формализации забиваем - и ничего :)

Edited at 2013-08-27 09:41 pm (UTC)
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 27th, 2013 09:52 pm (UTC)
(Link)
Мне кажется, метапрограммирование достаточно нетривиально для того, чтобы его реализовывать в стиле "тяп-ляп и в продакшен". Примеры Скалы и Агды это неплохо доказывают. Поэтому, на мой взгляд, здесь нужна какая-то научная база.

Достижения на фронте макро-языков с динамической типизацией весьма впечатляют, но собратья со статической типизацией на спешат перенять передовой опыт. Почему-то считается, что интересными являются только статически типизируемые генераторы кода (т.е. такие генераторы, которые гарантированно производят код, корректный с точки зрения типов). Возьмем, к примеру, MetaML/MacroML, последние новшества в Template Haskell, вот тот же quoteTerm в Agda или примеры из последней главы магистерской диссертации, приведенной выше. На средства написания таких генераторов бросаются неслабые силы, а все остальное либо игнорируется (как в MacroML), либо оставляется в недоделанном состоянии.

Получается замкнутый круг. Для практичного МП в языках со статической типизацией нужна научная база, но науку интересуют проблемы теоретически красивого МП, который довольно далек от практики.
(Reply) (Parent) (Thread)
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) (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) (Expand)