?

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:32 pm (UTC)
(Link)
> и непонятно, как это формализовать-то.

А это действительно плохо?
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 27th, 2013 09:34 pm (UTC)
(Link)
С научной точки зрения, думаю, да.
(Reply) (Parent) (Thread)
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) (Expand)
[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) (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) (Expand)
From:ex_juan_gan
Date:August 28th, 2013 05:43 pm (UTC)
(Link)
Хм, что плохо? Что непонятно как формализовать? Не знаю; у меня более мелкие вещи вызывают уже раздражение - похожие чем-то - до хрена чего не получается просто из-за type erasure в jvm.
(Reply) (Parent) (Thread)
[User Picture]
From:xeno_by
Date:August 28th, 2013 05:44 pm (UTC)
(Link)
Erasure и в Хаскелле есть, например.
(Reply) (Parent) (Thread)
From:ex_juan_gan
Date:August 28th, 2013 09:01 pm (UTC)
(Link)
Хм. Я и не знал (и не ощущал).
(Reply) (Parent) (Thread)
From:Valentin Budaev
Date:August 29th, 2013 02:26 am (UTC)
(Link)
Ну в хаскеле и нельзя же что-то типа case x: List[Int] =>? Потому и не заметно.
(Reply) (Parent) (Thread)