Человеческое метапрограммирование

Пасаны, где вы всю эту CS выучили?

где вы всю эту CS выучили?

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

Можно перечислить множество систем обладающих свойствами правильности, полноты, непротиворечивости (в тех или иных комбинациях) в которых эта просьба не имеет смыла - можно начать с лямбда-куба, потом пройтись по линейным типам, по расширениям с подтипами.

Гм, нет, с чего вдруг? Из любого упомянутого класса систем можно выбрать сколько угодно таких систем, где с типом «5» все будет хорошо.

Про захардкоженность - в агде можно сделать postulate который может ломать систему типов (например, непротиворечивость), но сделать z : a : A : Set вообще нельзя

Это чисто синтаксическое ограничение. С семантикой оно никак не связано.

Я пока представляю это так - для всех уровней i для каждого универсума (категории-топоса) Set i есть эндо- точечный- коточечный- функтор Set i -> Set i как конструктор типа для операции цитирования «типа» (элемента : Set i), операция точечного функтора point это операция цитирования «терма» (элемента : T : Set i), операция коточечного функтора extract это операция подстановки цитированного «терма»:

Да нет, это то все очевидно и ненужно. Я говорил о том, какова форма возможных семантических правил - то есть какие типы могут быть у макросов?

Чем _более_ выразительна?

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

Можно какой-нибудь модельный пример?

Любой макрос в котором АСТ чуть сложнее обычного макровызова. Ну возьми, например, iterate из CL - там тип будет больше сотни строк :)

Хотя на такой системе iterate полностью будет реализовать невозможно все равно, т.к. эта система запрещает раскрытие внутренних форм во время раскрытия внешних. Ну и расширение тоже будет реализовать невозможно, т.к. для него надо уметь из макроса генерировать новые макросы. Или тот же match из Racket - тоже нельзя будет реализовать (а у обгрызенной реализации снова будет тип на сотню строк). То есть как мы попытаемся применить метапрограммирование именно для того, для чего оно нужно - такая система оказывается слишком слабой.

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

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

STLC с определением синтаксиса термов и типов, отношением типирования и тайпчекером, интерпретатором и доказательством правильности (в качестве бонуса - макросу это не необходимо) занимает в Coq/Agda пару экранов.

Не, ну давай не будет комедией заниматься? Тайпчекер для STLC занимает меньше сотни строк, но никому не нужна STLC, вот сколько занимает тайпчекер хаскеля, а? Все это работает только до тех пор, пока мы пробуем считать факториалы. Первая же реальная задача - слив.

У зависимых типов тоже есть довольно лаконичные формы (LF, формы из «simply easy» или «tutorial implementation»).

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

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

То есть «выразительность системы типов» = «выразительность средств доказательства корректности программы». Потому что формально система типов - это именно и есть не более чем средство доказательства корректности программы. Чем больше программ сможет допустить чекер (гарантируя их корректность, некорректные, естественно, пропускать не надо) - тем выразительнее система. Идеальная система, очевидно, позволяет допускать те и только те программы, которые корректны.

ЗЫ: под «программой» понимается программа без типов - то есть обычный нетипизированный терм, в котором типов нет, вообще в коде типов быть не должно.

А в динамической метасистеме они разве разные?

В динамической - всмысле в случае динамической типизации? Ну там вообще нет никакой системы типов. А ЯП - да, в каждой фазе может быть свой ЯП.

Нормальных систем типов вообще не может быть много (либо они будут эквивалентны друг другу)

Эквивалентность систем типов - это просто баззворд. Во-первых, чуть менее чем всегда когда говорят «система типов» понимается широкий КЛАСС СИСТЕМ. Например, каждая вершина лямбда-куба - это целый класс систем. Мы можем иметь много простых типизированных лямбд, которые неэквивалентны друг другу и применимы в той или иной ситуации. Аналогинчо для любого класса. Кроме того кроме самой системы типов есть еще и ее реализация - то есть как работает вывод, как определяются типы и т.п., что на практике тоже немаловажно.

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

Это не CS, это псевдонаучное бла-бла-бла. Ни один из отметившихся тут матанодрочеров никогда в жизни не напишет ни одной полезной софтины.

Из любого упомянутого класса систем можно выбрать сколько угодно таких систем, где с типом «5» все будет хорошо.

Для всех возможных Nat -> z можно выделить классы частичных и тотальных функций исходя из структуры Nat, как это сделать для 5 -> z? Какая структура у терма : 5? Я могу сделать паттерн-матчинг по терму : Nat, а по терму : 5? Гарантировать что паттерн-матчинг полный?

Я говорил о том, какова форма возможных семантических правил - то есть какие типы могут быть у макросов?

Я привёл пример - такие же как и у всех других функций, но с конструкторами ⟪⟫ вокруг цитируемых типов. Соответственно, выразительность сигнатур макросов как утверждений и реализаций как доказательств должна быть та же что и у обычных функций (исходя из ⟪ A ⟫ → ⟪ B ⟫ ≅ ⟪ A → B ⟫ и подобных свойств).

Если система выразительна, то мы для широкого класса программ можем доказать корректность. Если невыразительна - этот класс уже.

Я там попросил привести примеры программ которые не пишутся на языках которые, по-твоему, уже.

Тут вспоминаются споры из ru_lambda на тему того что динамика всегда просто выражается в статике (можно кинуть ссылкой на статью Пирса на эту тему), но не наоборот. И недавний разговор про нетипизированный ассемблер тоже.

Ну возьми, например, iterate из CL - там тип будет больше сотни строк :)

Ну так iterate же не нужен нигде кроме CL. Получаются либо макросы заменяемые ленивыми функциями (или лучше - возможностью задать нужную стратегию вычисления функциям), либо ненужные монстры вызванные нежеланием/невозможностью использовать нормальное ФП (кстати, iterate же не умеет list/data fusion, что-то подобное умел не попавший в стандарт series, а вот «нормальное ФП» умеет).

Или тот же match из Racket

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

То есть одобная система была бы интересна исключительно с теоретической точки зрения - практического применнеия она бы не нашла.

Это, конечно, так.

Не, ну давай не будет комедией заниматься? Тайпчекер для STLC занимает меньше сотни строк, но никому не нужна STLC, вот сколько занимает тайпчекер хаскеля, а?

Как будто каждый раз, каждым макросом, нам нужно реализовать что-то уровня хаскеля. В моём представлении всякий полезный compile-time транслятор как раз не очень сложен в смысле верификаций.

Первая же реальная задача - слив.

Еще раз - все интересное метапрограммирование заключается в написании _сложных_ макросов.

Пока что - iterate, match, которые нет необходимости писать (чисто практически). Что ещё?

но сложные будут писаться на порядок сложнее.

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

Для всех возможных Nat -> z можно выделить классы частичных и тотальных функций исходя из структуры Nat, как это сделать для 5 -> z? Какая структура у терма : 5? Я могу сделать паттерн-матчинг по терму : Nat, а по терму : 5? Гарантировать что паттерн-матчинг полный?

Считай, что 5 - это синоним для S S S S S Zero.

Я привёл пример - такие же как и у всех других функций, но с конструкторами ⟪⟫ вокруг цитируемых типов.

А если, например, в сигнатуре в каком-то месте будет тип (or A B)? А если этот тип функционально зависит от типа в другом месте сигнатуры? А как указать внутри типа ввод новых переменных? То есть все самое интересное ты упустил.

Я там попросил привести примеры программ которые не пишутся на языках которые, по-твоему, уже.

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

Тут вспоминаются споры из ru_lambda на тему того что динамика всегда просто выражается в статике (можно кинуть ссылкой на статью Пирса на эту тему), но не наоборот.

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

Ну так iterate же не нужен нигде кроме CL.

Нужен. Это удобный дсл для итераций.

Получаются либо макросы заменяемые ленивыми функциями (или лучше - возможностью задать нужную стратегию вычисления функциям), либо ненужные монстры вызванные нежеланием/невозможностью использовать нормальное ФП

Ну лучше написать ДСЛ, чем кучу лапше-кода, которую будет представлять «нормальное ФП». Эти «монстры» - как раз и есть суть метапрограммирования. То есть вместо той же фп-лапши мы делем простой в использовании и поддержке дсл.

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

Я говорю о полноценном паттерн-матчинге. Как мне сделать паттерн-матчинг по произвольному предикату? А action-pattern? А как мне расширить синтаксис этого матчинга? Никак. Потому что то что в том же хаскеле - это совсем не паттерн-матчинг, а кривой огрызок от него. Ну и что на счет того, когда в ЯП понадобится что-то, чего в него НЕ захардкожено? Или как джавабляди - объявлять все, чего нет, ненужным и соглашаться с нужностью как только это что-то добавят в ЯП?

Как будто каждый раз, каждым макросом, нам нужно реализовать что-то уровня хаскеля.

Нет, коненчо, но значительно сложнее простой типизированной лямбды.

Пока что - iterate, match, которые нет необходимости писать (чисто практически). Что ещё?

Я могу сотни примеров приводить - но мне в ответ будет сказано, что «нет практической необходимости», ведь то же самое _можно сделать_ при помощи обычных функций. Или даже на брейнфаке. Согласно подобной логике ни в чем нету никакой практической необходимости, так что и говорить об этом смысла никакого нет. Для меня практическая необходимость в инструменте, который позволяет удобно реализовывать и использовать абстракции, очевидна. Ну для кого-то - нет, кто-то больше любит программировать на низком уровне - перекладывать байтики, комбинировать комбинаторы, а абстракций боится. Дело вкуса.

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

Но зачем? Какой в этом практический смысл?

анонимус, ты мне интересен как

1. оппонент, защищающий динамическую типизацию — сложно найти достаточно грамотного человека с такими взглядами

2. человек, имеющий некоторые use cases для макросов

у тебя есть контакты? мейл, джаббер там?

хотя на самом деле мне от тебя больше всего был бы интересен именно набор use cases для макросов; ты бы мог его в таких спорах цитировать, и с помощью него проверять качество предлагаемых средств для метапрограммирования

скажем, вместо абстрактного «макроса В который разворачивается по-другому внутри макроса А» нужны конкретные примеры; ну например (высосано из пальца) макрос А это define-iterator или define-function, а макрос В должен разворачиваться в зависимости от этогов в yield или в return

опять же может быть наоборот, когда define-iterator-or-function разворачивается в разный код в зависимости от того, присутствует ли в его теле yield или только return

и так далее

далее, ты правильно идентифицировал проблемы в подходе вольфхаунда — назовем их

1. необходимость верификации макросов

2. необходимость верификации системы типов

однако чересчур долго разжевывал их

В данном случае у нас есть вся информация, чтобы выдать пользователю очень подробный отчет об ошибке, с которым он может пойти бить автора языка.

автора языка тебе не жалко?

а что будет, если по ошибке будет записано:

typing
{
  assert Cond.Type == #Bool;
  assert Type <= ThenExpr.Type;
  assert Type >= ElseExpr.Type;
}

очевидно, это будет работать для одинаковых типов в ветвях if, и даже для разных в отношении дед-внук, но *внезапно* сломается, и тут Н2 не защищает автора языка от битья

... а ведь мог бы защищать, если скажем аналогичные условия были бы выписаны для cond и происходило бы их сопоставление с if-овскими

предыдущее сообщение — это ответ на Человеческое метапрограммирование (комментарий) т.е. wolfhound-у

далее, ты правильно идентифицировал проблемы в подходе вольфхаунда — назовем их

:))) Он даже не понял о чем говорил.

Но что еще ждать от человека, который с тайпчекером борется...

автора языка тебе не жалко?

Жалко. Именно поэтому и делаю такую систему.

Ибо сейчас в случае ошибки автора языка компилятор говорит «я сломался».

И пойди, разбери, где именно он сломался.

На днях подкинул Владу ошибку в компиляторе немерле. Он её два дня ловил. А в случае с данной системой ему бы сказали, в какой строке косяк и он бы его за 5 минут исправил.

Лисп тут ваще в пролете.

а ведь мог бы защищать, если скажем аналогичные условия были бы выписаны для cond и происходило бы их сопоставление с if-овскими

Чего? cond это просто выражения типа bool. Ничего другого про него не известно.

В любом случае может быть конструкция, для которой данное правило адекватно.

Вообще первое правило Н2: не навязывать автору языка систему типов. Ибо системы типов на все случаи жизни не существует.

а ведь мог бы защищать, если скажем аналогичные условия были бы выписаны для cond и происходило бы их сопоставление с if-овскими

Чего? cond это просто выражения типа bool. Ничего другого про него не известно.

сорри, s/cond/match/

Лисп тут ваще в пролете.

это да; тот анонимус совершенно необъяснимо к нему привязан

>> Пока что - iterate, match, которые нет необходимости писать (чисто практически). Что ещё?
> Я могу сотни примеров приводить

Хотя бы 5-10 примеров поближе к практическим задачам интересно услышать - для представления уровня абстракции / сложности.

скажем, вместо абстрактного «макроса В который разворачивается по-другому внутри макроса А» нужны конкретные примеры;

Чаще всего такая ситуация - дсл вводит какие-то макросы, внутри дсл они имеют смысл, вне дсл - не имеют (ну как какой-нибудь collect в loop). Соответственно, нам бы хотелось, чтобы при использовании вне контекста было выведено адекватное сообщение об ошибке, ну что-то вроде «collect: loop construction used out of context» вместо «collect: undefined». Собственно, это широко распространенная ситуация, можно даже скзаать - некий паттерн. Более интересный пример - допустим, мы хотим сделать дсл для реактивного программирования. Тогда любая переменная должна быть узлом нашей сети и представляет из себя де-факто некоторую структуру (node ...) в которой лежит все интересное, что нам нужно, для распространения сигнала. Нам бы хотелось, чтобы мы могли использовать эту переменную в обычном коде - в этом случае эта переменная просто вернет текущее значение узла (соответственно, вне каких-либо макросов «x» раскрывается в имя соответствующей «скрытой» переменной, которая это значение и содержит), нам бы хотелось, чтобы мы могли обратиться через эту переменную напрямую к структуре (node ...) - то есть в каком-нибудь (get-node x) «х» трансформируется в «скрытую» переменную содержащую структуру. И нам бы хотелось, чтобы внутри специальной формы (make-node body ...) (body - произвольный код) «х» раскрывалась в специальный макрос, который передает «вверх» всю нужную для создания нового узла статическую информацию. Т.о. переменная, обозначающая какой-либо узел, раскрывается тремя разными способами в зависимости от своего контекста.

опять же может быть наоборот, когда define-iterator-or-function разворачивается в разный код в зависимости от того, присутствует ли в его теле yield или только return

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

однако чересчур долго разжевывал их

Так что же поделаешь, если в ответ на указанные проблемы оказалось, что это и не проблемы никакие - ведь чудодейственный алгоритм йоба-тайпчека (которого правда еще нет) все сделает!

Лисп тут ваще в пролете.

Практика показывает обратное. Пока что под ваш н2 вообще никаких языков нет и самого н2 нет. А вот racket - есть, и языки под него пишут и никаких проблем.

А в случае с данной системой ему бы сказали, в какой строке косяк и он бы его за 5 минут исправил.

Да, да, мы уже знаем, что ваша система умеет читать мысли. За счет чего это реализуется, можно узнать? И когда нобелевку будете получать?

Хотя бы 5-10 примеров поближе к практическим задачам интересно услышать - для представления уровня абстракции / сложности.

Смотри, какая ситуация - у меня спрашивают, зачем нужны гвозди, я отвечаю - за тем, чтобы прибивать один объект к другому. Меня просят конкретные примеры - я привел в пример, допустим, табуретку и стол. Мне в ответ «да это же нинужно! я могу и на клей приклеить!». Какой мне смысл продолжать? Любой адекватный человек может сам прекрасно разобраться зачем что-то надо прибивать к чему-то и в каких случаях это может быть полезно, тем более, что несколько характерных примеров даны.

это да; тот анонимус совершенно необъяснимо к нему привязан

Я уже объяснял, почему лисп. Если речь идет о системе метапрограммирования, то от нее требуется одно-единственое - как можно сильнее упростить написание сложных макросов. Больше требований нет. В этом случае лисп как хост-язык оптимален за счет гомоиконичности и динамической типизации.

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

Я могу сотни примеров приводить - но мне в ответ будет сказано, что «нет практической необходимости», ведь то же самое _можно сделать_ при помощи обычных функций.

А ты приведи такой пример, из которого будут ясны преимущества написания именно макроса. Этому топику сильно не хватает хороших примеров.

а ведь мог бы защищать, если скажем аналогичные условия были бы выписаны для cond и происходило бы их сопоставление с if-овскими

Чего? cond это просто выражения типа bool. Ничего другого про него не известно.

сорри, s/cond/match/

Аналогичные условия для match естественно выписаны. Именно благодаря этому компилятор скажет при раскрытии if с разными типами, что все плохо.

Те даже вариант дед/внук не пройдет. Ибо if выведет отца. А match после раскрытия деда. После чего компилятор выведет подробный отчет о том, что, где и как навернулось.

Вся разница со статическим анализом это то, что нужно макрос на исполнение запустит. Это конечно недостаток, но далеко не всё так плохо как аноним пытается вещать. А по сравнению с лиспом который вообще ничего не ловит так ваще супер система.

Теоритически в некоторых простых случаях это можно сделать до запуска макроса на исполнение. Но толку от этого будет мало. Ибо случаи очень простые. И скорей всего этот анализ ничего не поймает.

Кстати насчет анонима. Я на 99% уверен, что это он http://rsdn.ru/Account/Info/100482

Я уже объяснял, почему лисп. Если речь идет о системе метапрограммирования, то от нее требуется одно-единственое - как можно сильнее упростить написание сложных макросов. Больше требований нет. В этом случае лисп как хост-язык оптимален за счет гомоиконичности и динамической типизации.

не согласен

1. то, что делается макросами, вроде внедрения всякой фигни в лексический контекст — безусловно нужно, но должно делаться не макросами (как — это отдельный разговор; будет тот чеклист с макросами, который я тебе предлагаю сделать — тогда я проверю на нем свои идеи)

2. динамическая типизация?

если у вольфхаунда есть условно говоря гарантии, что хотя бы та часть макроса, что мутирует AST (и наверно проверяет предусловия), хоть как-то дохромает до победного конца (предполагаю, что хотя бы NPE не будет... но в бесконечном цикле оно имеет полное право зависнуть), то у вас в лиспе с динамической типизацией даже этих условно говоря гарантий *НЕТ*

кстати, можно было бы подумать о более сильной системе типов, делающей AST rewrite тотальным (но не тьюринг-полным)

еще кстати — я так и непонял, нафига языку для AST rewrite-ов совпадать с переписываемым языком (как он там называется — целевым или хост-языком?)

А ты приведи такой пример, из которого будут ясны преимущества написания именно макроса. Этому топику сильно не хватает хороших примеров.

Тут уже приводился тот же match или iterate - в ответ пришло «мне клеем клеить удобнее».

Считай, что 5 - это синоним для S S S S S Zero.

Так и есть, поэтому этот терм можно разобрать. Но если использовать его как тип, то как разобрать a : S S S S S Zero я не пойму. Индуктивные определения типов задают множество собираемых и разбираемых термов данного типа и помещают тип в универсум, можно сделать

f : {T : U(0)} → T → ...
f T₀ = ...
f T₁ = ...

но не

f : T₀ → ...
f ? = ...

так как ни индуктивное определение ни что-либо ещё не позволяют работать с T₀ как со _множеством_. Со всем остальным - с индуктивно заданными типами и растущими вверх универсумами можно работать как со множествами.

А если, например, в сигнатуре в каком-то месте будет тип (or A B)? А если этот тип функционально зависит от типа в другом месте сигнатуры?

Сумма типов и функциональный тип как и в обычной сигнатуре, в чём проблема? ⟪ A ⊎ B ⟫ ≅ ⟪ A ⟫ ⊎ ⟪ B ⟫ и ⟪ A → B ⟫ ≅ ⟪ A ⟫ → ⟪ B ⟫.

А как указать внутри типа ввод новых переменных?

Как нарушить гигиену? Можно делать ⟦ let var = $ val in $ expr ⟧ : ⟪ тип-expr ⟫, чтобы сделать ⟦ let $ var = $ val in $ expr ⟧ : ⟪ тип-expr ⟫ нужно ввести новый тип цитированных имён ⟪ Name ⟫ (примерно как в TH).

Ну из простых примеров - настоящий flatten

HList - hMapOut.

Ну и flatten это функция а не программа. Если ставить задачу в терминах пользовательского ввода и вывода программы, то написать можно что угодно.

Как мне сделать паттерн-матчинг по произвольному предикату?

Это guards?

action-pattern?

?

А как мне расширить синтаксис этого матчинга?

А чего конкретно не хватает? И потом, я сказал про _зависимый_ паттерн-матчинг он с обычным - как небо и земля.

Ну и что на счет того, когда в ЯП понадобится что-то, чего в него НЕ захардкожено?

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

Но зачем? Какой в этом практический смысл?

Такой же как ограничения на все остальные функции, которые накладывает статическая система типов.

Так что же поделаешь, если в ответ на указанные проблемы

Которые ты высосал из пальца.

оказалось, что это и не проблемы никакие - ведь чудодейственный алгоритм йоба-тайпчека (которого правда еще нет) все сделает!

Естественно сделает. Математика есть уже лет 20. Нужно только реализацию сделать. И как её делать я уже придумал.

Тут уже приводился тот же match или iterate

Примеры - это когда показывается макрос, его код и объясняются, почему все остальные способы реализации хуже. А просто отсылка к макросу $foo - это не пример.

Опять речь зашла об абстрактной теоретической возможности. На практике никого не интересует теоретическая возможность. Инструмент должен быть удобен, а не «теоретически достаточно мощен для решения данной задачи». Поскольку единственный тайпчекер который (чисто теоретически) мог бы быть аналогичен макросистеме и давать возможность работы с лексическим контекстом еще даже не доделан и находится на этапе мокрых мечтаний создателя - неясно, о чем вообще говорить.

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

Те даже вариант дед/внук не пройдет. Ибо if выведет отца.

с чего вдруг? там везде знаки включают равенство

Аналогичные условия для match естественно выписаны. Именно благодаря этому компилятор скажет при раскрытии if с разными типами, что все плохо.

а еще (предположу), что до запуска макроса можно вывести, что

1. условия, наложенные на настоящий if, в любом случае *достаточны* для условий, требуемых match-ем

2. условия, наложенные на кривой if, могут обломаться

... хотя выпиши-ка условия, требуемых match-ем, если они у тебя есть

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

Это гнилая отмазка. Ты тут сам жалуешься, что жабисты объявляют все, что жаба не умеет не нужным.

Но сам ведешь себя 1 в 1. Ты обосновываешь не нужность фичи по тому, что лисп так не умеет.

Это твоя единственная мотивация. Даже если ты сам себе в этом не признаёшься.

Примеры - это когда показывается макрос, его код и объясняются, почему все остальные способы реализации хуже.

Там далеко не 100 строк реализация, вы же все равно ее не поймете. Никто из здесь присутствующих (не поймет за разумное время, которое может затратить человек на форумный срач). Так же как никто не поймет типовую эквилибристику, которую даст в ответ quasimoto. Это будет натуральный спор глухого с немым. Если хотите - можете начать с изучение спеков:

http://docs.racket-lang.org/reference/index.html

Если закончите - можно будет вернуться к примерам. Через месяц-два.

Это гнилая отмазка. Ты тут сам жалуешься, что жабисты объявляют все, что жаба не умеет не нужным.

Для идиотов, которые не умеют читать, поясняю. Лисп так _умеет_. Более того, в том же racket есть специальные механизмы, которые смогут упростить обеспечение гарантий корректности специально для такого случая (к слову в том же н2 мало того что таких механизмов нет - но и вообще раскрыть внешнюю форму в зависимости от внутренней не выйдет).

Но если так _можно_ - не значит, что так _нужно_ делать каждый раз, как оно пришло в голову. не всегда первое решение, которое пришло в голлову - лучшее.

Примеры - это когда показывается макрос, его код и объясняются, почему все остальные способы реализации хуже.

Там далеко не 100 строк реализация, вы же все равно ее не поймете.

Я сказал «пример», а не «макрос из сурового продакшена».

http://docs.racket-lang.org/reference/index.html

Если закончите - можно будет вернуться к примерам. Через месяц-два.

«Я знал, что ты скажешь это» (ц)

Система метапрограммирования предназначена для работы с лексическим контекстом, система типов - для доказательства корректности программы. Это ортогональные вещи

до какой-то степени да

и «меняться» инструментами в данном случае (то есть метапрограммировать типами и доказывать корректность макросами) - это и с той и с той стороны использование микроскопа для колония орехов. Так уж просто случайно получилсоь, что работа с контекстом позволяет фиксировать некоторые варианты. И, наоборот, работа с типами позволяет обрабатывать в компайлтайме некоторую информацию.

в с++ практически единственный способо обработать в компайл-тайме нечто — это работа с типами; в классической скале, которая без макросов и не виртуализована — тоже; безусловно, это все извращения

с другой стороны, насчет лексического контекста я отнюдь не уверен — ведь лексический контекст функции это практически тип стекового фрейма функции

Так и есть, поэтому этот терм можно разобрать. Но если использовать его как тип, то как разобрать a : S S S S S Zero я не пойму.

В чем вы видите разницу? Для меня лично ее нет, ведь 5 - это рвоно ТО ЖЕ САМОЕ что S S S S S Zero. Они взаимозаменяемы.

Сумма типов и функциональный тип как и в обычной сигнатуре, в чём проблема?

Это не сумма, а объединение. Проблема в следующем - как задать произвольную функциональную зависимость?

Как нарушить гигиену?

Нет, гигиену нарушать не надо. Пример, вот такой макрос (yoba x) -> (define x 1). надо в типе yoba указать, что макрос вводит в контекст переменную x соответствующего типа (Int). Напишите тип для yoba.

HList - hMapOut.

Ну где реализация-то? Как мне сделать: `((1 2) «gdfg» (23 r #\q) (((5)))) -> `(1 2 «gdfg» 23 r #\q 5)? И почему она принимает два аргумента? Должен быть только один.

Если ставить задачу в терминах пользовательского ввода и вывода программы, то написать можно что угодно.

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

Это guards?

Да.

?

Ну например (app f pat) применяет любую функцию f и матчит относительно паттерна pat.

А чего конкретно не хватает?

Сейчас не знаю. Сейчас я пишу вам пост и мне вообще никакого паттерн-матчинга не надо.

Такой же как ограничения на все остальные функции, которые накладывает статическая система типов.

При чем тут ограничения? Речь шла о том, какая практическая польза от обсуждаемой системы метапрограммирования? Хотя выше вы сами уже сказали, что никакой - только поиграться с точки зрения теории. Собственон, продолжать дальше уже было и не нужно.

с чего вдруг? там везде знаки включают равенство

Это я затупил. Тут, конечно же, до раскрытия даже не дойдет. Ибо типизатор не сможет тип для if вывести.

хотя выпиши-ка условия, требуемых match-ем, если они у тебя есть

Что-то типа такого

syntax Match is Expr
parsing "match" "(" MatchExpr ")" "{" Cases "}"
{
  alias MatchExpr = Expr;
  alias Cases = MatchCase*;
}
typing
{
  foreach (case in Cases)
  {
    assert case.InType <= MatchExpr.Type;
    assert Type <= case.ResultType;
  }
}

Я сказал «пример», а не «макрос из сурового продакшена».

Макрос из сурового продакшена - это и есть самый хороший пример. Если не устраивает - прошу пояснить, какого же рода примеры нужны? Если привести маленький макрос - его легко будет заменить любой другой констуркцией, если привести полноценный дсл на сотни строк - опять будешь вопить о «мне не нужен макрос из продакшена». Хорошая макросистема как раз и нужна для написания полцноценных макросов из продакшена. Потмоу что она реализована для прктического удобства, а не для теоретических изсканий. Вот в опследнем случае как раз просто и хорошо пишутся всякие факториалы, а когда дело до суровог опродакшена доходит - отсос.

с другой стороны, насчет лексического контекста я отнюдь не уверен — ведь лексический контекст функции это практически тип стекового фрейма функции

Нет, конечно. Лексический контекст макроса (а не функции, при чем тут функция?) - это просто вся та компайл-тайм информация, к которой мы можем обратиться во время экспанда этого макроса.

Если закончите - можно будет вернуться к примерам. Через месяц-два.

давай по одному макросу в неделю? и по рукам!

Макрос из сурового продакшена - это и есть самый хороший пример. Если не устраивает - прошу пояснить, какого же рода примеры нужны?

Нужен краткий пример, демонстрирующий суть идеи. Если самый краткий пример - сотни строк и для понимания требует пары месяцев изучения Racket - об этом следует сказать прямо.

Вот в опследнем случае как раз просто и хорошо пишутся всякие факториалы, а когда дело до суровог опродакшена доходит - отсос.

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

Для идиотов, которые не умеют читать, поясняю. Лисп так _умеет_.

Настолько через зад автогеном, что это всё равно, что не умеет. А если случай чуть сложнее, то ты сам признал, что там начинается АД И ПОГИБЕЛЬ (С)

Более того, в том же racket есть специальные механизмы, которые смогут упростить обеспечение гарантий корректности специально для такого случая

Ссылку.

(к слову в том же н2 мало того что таких механизмов нет - но и вообще раскрыть внешнюю форму в зависимости от внутренней не выйдет).

Есть. В Н2 распространение информации такое что лиспу и не синилось.

Там не только макрос А может повлиять на вложенный макрос Б и в обратную сторону. Причем одновременно.

Но и макрос Б может повлиять на макрос Е который вложен в макрос Д вызванный рядом с макросом А.

А всё по тому, что есть специальная фаза типизации, на которой распространяется информация.

Но если так _можно_ - не значит, что так _нужно_ делать каждый раз, как оно пришло в голову. не всегда первое решение, которое пришло в голлову - лучшее.

Это банально удобно. Например, тот же yield return в C# так и работает.

Это не говоря про такие «мелочи» как вывод типов, который в общем случае должен разруливать циклические зависимости.

с другой стороны, насчет лексического контекста я отнюдь не уверен — ведь лексический контекст функции это практически тип стекового фрейма функции

Нет, конечно. Лексический контекст макроса (а не функции, при чем тут функция?) - это просто вся та компайл-тайм информация, к которой мы можем обратиться во время экспанда этого макроса.

а давай не будем путать понятия? именно, макрос как реализационное средство и макрос — как новая созданная пользователем конструкция языка, далее — Новая Конструкция

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

з.ы. хотя, конечно, это все имеет явный уклон не в тип данных, а в naming conventions & namespaces

Это я затупил. Тут, конечно же, до раскрытия даже не дойдет. Ибо типизатор не сможет тип для if вывести.

сможет, если звезды лягут удачно (или неудачно, как назвать)

IfType == Granfather

IfType <= Grandfather

IfType >= Grandson

но может и облом быть

IfType == ?

IfType <= Grandson

IfType >= Grandfather

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

з.ы. гы-гы, а как ты предлагаешь отлавливать такие ошибки? юнит-тестами?

другой анонимус.

Что-то мне сдается, что спор двух анонимусов зашел в тупик - каждый остался при своем. Наверное, сначала нужно h2 реализовать, а уж потом копьи ломать. Практика - критерий истины. А пока все выглядит умозрительным.

сможет, если звезды лягут удачно (или неудачно, как назвать)

Не сможет. Ибо он выведет сразу 3 подходящих типа и сообщит о неоднозначности.

з.ы. гы-гы, а как ты предлагаешь отлавливать такие ошибки? юнит-тестами?

А иначе они не отлавливаются. Ты вообще видел размеры тестов у серьёзных компиляторов?

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

Нужен краткий пример, демонстрирующий суть идеи.

Если привести «краткий пример», то скажут что он «чересчу рабстрактен и непонятен» или «да ведь это можно и с ФВП».

Если самый краткий пример - сотни строк

Макросистема нужна для написания дслей. Как вы видите написание дсл в десяток строк? Я могу приводить в пример те или иные аспекты (и приводил) и особенности макросистемы, которые, да, можно продемонстрировать коротко, но меня опять спросят «зачем это нужно? я и без этого обойдусь» - а оно нужно именно тогда, когда пишем сложные дсли.

и для понимания требует пары месяцев изучения Racket

Чтобы понимать код - надо понимать семантику ЯП и рантайма, очевидно. Это верно для любого ЯП. Конечно, с парой месяцев - это я загнул, но ведь тут никто и пару вечеров тратить не станет.

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

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