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

[xeno_by]

На днях просмотрел паперу Dependent Type Providers [1] и магистерскую диссертацию Reflection in Agda [2], которые используют средства рефлекшена, предоставляемые Агдой, для метапрограммирования

Comments

[ex_juan_gan]

Хм, концептуально это логично звучит; но это как бы выходит за пределы математики, и непонятно, как это формализовать-то.

[xeno_by]

На это мне пока что ответить нечего, к сожалению. Я предполагаю, что именно из-за этого никто особо из академиков не парится на эту тему.

[ex_juan_gan]

Но проблема-то от этого не исчезает, конечно. Метапроблема.

[ext_1178598]

> и непонятно, как это формализовать-то.

А это действительно плохо?

[xeno_by]

С научной точки зрения, думаю, да.

[ext_1178598]

Вопрос не такой праздный, как кажется. Нельзя понять, _как_ формализовать, если мы не знаем, _зачем_. И ответ: "плохо с научной точки зрения", очевидно, плохой ответ на вопрос: "зачем?". В плане - неконструктивный.

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

[xeno_by]

Мне кажется, метапрограммирование достаточно нетривиально для того, чтобы его реализовывать в стиле "тяп-ляп и в продакшен". Примеры Скалы и Агды это неплохо доказывают. Поэтому, на мой взгляд, здесь нужна какая-то научная база

[ext_1178598]

> Мне кажется, метапрограммирование достаточно нетривиально для того, чтобы его реализовывать в стиле "тяп-ляп и в продакшен". Примеры Скалы и Агды это неплохо доказывают. Поэтому, на мой взгляд, здесь нужна какая-то научная база

[xeno_by]

В Немерле особо и формализации-то нет, т.к. народ не заморачивался насчет работ на серьезных конференциях. А у нас вообще нет ничего работающего кроме низкоуровневой макросистемы на ручной тяге, поэтому Скала вообще не считается :)

[ext_1178598]

Ну вот. Откуда возьмется формализация, когда нечего формализовывать? :)

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

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

А на текущем уровне не ясно, в какую сторону идти. Никто никуда и не идет :)

[xeno_by]

Будем стараться! Вот буквально сейчас думаем над тем, как именно прикрутить гигиену. Есть несколько вариантов - как минимум пути Схемы, Немерле и Темплейт Хаскелла. Плюс, еще есть вариант на ручной тяге, но его не считаем. У всех есть свои трейд-оффы и свои сложности в реализации, поэтому поступало даже предложение забить на гигиену, но сейчас не время для малодушия :)

[ext_1178598]

> Вот буквально сейчас думаем над тем, как именно прикрутить гигиену

[xeno_by]

Про формализацию гигиены слышал, но пока что не добрался. Сейчас надо будет, конечно. Спасибо!

[ext_1178598]

Обратите внимание, что проблема важнее, чем кажется. Если мы научимся коректно трекать биндинги - то мы сразу научимся корректно распространять статическую информацию довольно произвольного вида, тем же путем. А это уже _намного_ интереснее.

[xeno_by]

А на эту тему есть какие-нибудь паперы? (Я имею ввиду про распространение произвольной статической информации)

[ext_1178598]

Была одна годная, но не могу сейчас найти, если найду, то дам ссылку.

Например, это используется в Racket в паттерн-матчинге по структурам - форма (struct struct-name ...) связывает со struct-name статическую информацию о свойствах структуры (гетеры, ацессоры, базовая структура и т.п.), потом когда мы делаем (match x [(struct-name ...) ...]), то match проверяет (статически, во время экспанда) - действительно ли struct-name структура, и, если да, то разбирает ее с помощью указанных в полученной информации геттеров.

Но тут все делается на ручном приводе, ага :)

А если сумеем трекать биндинги - то сможем автоматически туда-сюда гонять.