Homoiconic C

Лол, как ты сообрался оптимизировать потоки управления на уровне, когда у тебя никаких потоков управления еще нет, а есть только AST? Завязывай с веществами, AST раскладывается в граф управления, и все оптимизации выполняются на нём.

Еще один, с нулевым багажом знаний, но раздутым самомнением.

Найди CFG в лиспегах, лошарик.

Это как раз я не знаю, зачем тебе надо информацию о синтаксических структурах (for) на этапе control flow analysis, когда уже никаких этих структур нет.

Идиот. Этот самый control flow analysis в первую очередь восстанавливает как раз таки информацию о структурных конструкциях - циклах, if-ах и тому подобном. И на хера это делать, если эта информация у тебя уже есть?

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

И, кстати, я тебе говорил про семантику массивов vs. указатели, куда ты со своим CFG-то лезешь в калашный ряд?

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

только типы тут не при чем» — а я скажу «только динамические ЯП тут ни при чём». В хаскеле оно так работает, то есть _не только_ и _не столько_ за счёт модулей, например:

Как раз только за счет модулей оно и работает. Доказать это легко - уберем из хаскеля типы. Можно ли написать некорректный ИО-код? Нет, нельзя. Раскроем коснструктор IO. Можно ли написать некорректный код? Можно. Ч.Т.Д.

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

То есть даже _без_ модулей и сокрытия _вообще_ — уровни всё равно окажутся разделены

А, ты про это. Ну уровни разделены - но типы опять не при чем. Они разделяются просто за счет интерфейса. У тебя просто НЕТУ функций, которые могли бы смешать эти уровни. Если такие ф-и есть (интерфейс перестает быть безопасен), то все смешивается и ломается. И, смотри - ни на каком шаге не используется никаких типов!

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

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

Это ты так думаешь.

Не-а, не зря. Натурально не были бы нужны. Вместе со всем хаскелем, т.к. от IO никуда не денешься :)

Это не «система типов», это «любая compile-time хрень вообще».

Нет, система типов.

А так как макросистема эквивалентна по вычислительной части самому языку — она тоже «неразрешима»

С чего вдруг? Есть же вполне конкретный алгоритм экспанда.

Я говорю про структуры данных и алгоритмы имеющие отношение к предметной области, то есть про AST, функции проверки типов и т.п. — если их написать, можно будет потом спокойно и в макрос обвернуть.

Так и я о том же. Более того - надо не только существующие типы и т.п. использовать а в том числе и алгоритмы. То есть тут дело не в том чтобы обернуть в макрос.

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

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

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

При чем тут дублирование функциональности? Я хочу модульности, хочу чтобы у меня не было ядро языка засрано всякими forами и т.п.

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

Ну а почему бы тогда любому пользователю не раскрывать свои макросы в примитивный for?

Потому что макрос работает как-то по-другому и его нельзя раскрыть в примитивный for? Или это просто в данном случае неудобно?

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

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

а все оптимизации делаются на уровне структурного AST

На АСТ это не то, что сложно - на уровне АСТ это практически невозможно.

а потом развешивают на этот самый CFG обратно информацию от loop analysis (то есть, восстанавливают исходную семантику циклов).

То есть ЛЛВМ как раз и делает то, о чем я говорю. Сперва раскрываем, потом навешиваем хинты бекенду.

control flow analysis в первую очередь восстанавливает как раз таки информацию о структурных конструкциях - циклах, if-ах и тому подобном

Он «восстанавливает информацию» в виде, пригодном для понимания оптимизатором, а не на уровне твоих быдло-for-ов.

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

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

Хватит демонстрировать твоё незнание матчасти уже.

При чем тут дублирование функциональности? Я хочу модульности, хочу чтобы у меня не было ядро языка засрано всякими forами и т.п.

Или твой backend оптимизирует for, и, соответственно, засран им по самые яйца, или у тебя есть модульность, for реализован как макрос, и он ни хера не оптимизируется. С чего тред и начинался - я говорил, что макросы удобны разработчику языка, и полное говно для пользователей этого языка.

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

Ты тупой. Если эту информацию понимает твой backend, то в нем уже есть поддержка for. На кой хер тебе макрос?

Потому что макрос работает как-то по-другому и его нельзя раскрыть в примитивный for? Или это просто в данном случае неудобно?

А в семантически эквивалентные этому самому for-у «хинты» раскрывать типа удобнее? Ну-ну.

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

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

Подумай над тем, как ты будешь реализовывать loop fusion.

Лупы сфьюзяться при самом построении flow-графа. На самом графе уже и не надо будет фьюзить ничего. Так заебала твоя ебанутость.

Он «восстанавливает информацию» в виде, пригодном для понимания оптимизатором, а не на уровне твоих быдло-for-ов.

Он восстанавливает back edge, внутренние блоки, induction variables, exit edges с условиями и инкремент. То есть, ровно то самое, что записано в исходном синтаксисе for.

Хватит демонстрировать твоё незнание матчасти уже.

Смешно, когда абсолютно невменяемые и безграмотные ламеры разбрасываются такими предъявами. Мамку свою иди учить борщ варить.

Повторяю для тупых - абсолютно ничего из CFG для этих оптимизаций не нужно. А нужна информация о структурном control flow. Которая, представь себе, есть в исходном AST.

Приводят в CFG, а потом обратно в структурное представление только для того, чтобы на уровне CFG проделать SSA-преобразование. А оно нужно для того, чтобы вычислить induction variable и инкремент, и сделать constant folding (который может привести к изменениям в понимании loop bounds). Только вот в чем прикол - SSA-преобразование можно делать и без CFG. И получается оно быстрее и дешевле, чем на dominator tree.

В общем, напиши хотя бы пару-тройку оптимизирующих компиляторов, а потом уже имей мнение.

А в семантически эквивалентные этому самому for-у «хинты» раскрывать типа удобнее? Ну-ну.

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

Или твой backend оптимизирует for, и, соответственно, засран им по самые яйца, или у тебя есть модульность, for реализован как макрос, и он ни хера не оптимизируется.

Он оптимизирует код с соответствующими хинтами.

Ты тупой. Если эту информацию понимает твой backend, то в нем уже есть поддержка for.

В нем нету поддержки for, в нем есть поддержка ряда оптимизаций.

Или «трансформации» (с потерей возможности оптимизаций), или оптимизации одной большой вонючей кучи.

Я тебе уже по пунктам объяснил, как это все возможно вместе. Но ты же тупой.

Лупы сфьюзяться при самом построении flow-графа.

Чего?!? Ты об что стукнулся, гомосятина?!?

На самом графе уже и не надо будет фьюзить ничего.

На Нобелевскую премию претендуешь? Рассказывай, каким образом это циклы сами сольются, если для этого сначала необходимо убедиться в тождественности инкремента и bounds (и, соответственно, их необходимо или вычислить заново, или взять из исходного ast), и убедиться в независимости тел циклов.

Так заебала твоя ебанутость.

Смешно. Некомпетентная свинья пытается не просто высказывать абсолютно идиотское мнение, но и с пеной у рта его отстаивать. В этом весь ЛОР!

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

Ололо. Ты еще и irreducible CFG сюда пришить хочешь, свинья?

Он оптимизирует код с соответствующими хинтами.

Да я уже понял, ты назвал примитив «хинтом», и теперь, по гомосяцкой логике, он примитивом больше не является.

В нем нету поддержки for, в нем есть поддержка ряда оптимизаций.

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

Я тебе уже по пунктам объяснил, как это все возможно вместе. Но ты же тупой.

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

Повторяю для свиней: если в IR есть вся информация из исходного цикла, то раскрывать его на хер не нужно.

ровно то самое, что записано в исходном синтаксисе for

В исходном синтаксисе for может быть записана любая херня. Вон в Сях туда вообще можно навешивать произвольные выражения. Чтобы из какого-нибудь частного случая for(int i = 0, j = k; i < n; i++, j--) {какая_то_херня(i, j);} вывести induction variable, нужен аппарат анализа, сам по себе аналогичный анализу CFG. Зачем ты этот анализ собрался делать на уровне анализа конструкций ЯП - да хер его знает.

Приводят в CFG, а потом обратно в структурное представление только для того, чтобы на уровне CFG проделать SSA-преобразование. А оно нужно для того, чтобы вычислить induction variable и инкремент, и сделать constant folding (который может привести к изменениям в понимании loop bounds). Только вот в чем прикол - SSA-преобразование можно делать и без CFG. И получается оно быстрее и дешевле, чем на dominator tree.

А потом перед твоим компилятором возникает задача прожевать что-то вроде семантики Сишечки, и всё, soosnuli. Оптимизации должны работать в общем виде, а не в сладких мечтах о правильных AST-ах с правильной семантикой, допускающей только правильные оптимизации.

Чего?!?

Того, блять. Если ты даже таких очевидных вещей не знаешь, хули вообще с тобой разговаривать?

если для этого сначала необходимо убедиться в тождественности инкремента и bounds

и убедиться в независимости тел циклов.

Ну ты и тупой. Как раз сначала надо убедиться в независимости тел, после чего строятся ноды инкремента и bounds, которые при совпадении сливаются и циклы получается зафьюженым. А в незафьюженом виде их в CFG даже и не присутствовало.

На АСТ это не то, что сложно - на уровне АСТ это практически невозможно.

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

То есть ЛЛВМ как раз и делает то, о чем я говорю.

Так LLVM - говно.

Сперва раскрываем, потом навешиваем хинты бекенду.

Они это не от хорошей жизни делают. Им надо языки с потенциально irreducible cfg поддерживать. А если бы исходные языки были гарантированно всегда структурными, такого говна даром не надо было бы.

Как раз сначала надо убедиться в независимости тел, после чего строятся ноды инкремента и bounds, которые при совпадении сливаются и циклы получается зафьюженым. А в незафьюженом виде их в CFG даже и не присутствовало.

Придурок. На уровне CFG без хинтов ты даже не узнаешь, что basic block такой-то является частью тела такого-то цикла.

И еще, говна отрыжка, CFG строится задолго до того, как какие бы то ни было оптимизации будут делаться.

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

Ололо. Ты еще и irreducible CFG сюда пришить хочешь

Именно так.

Да я уже понял, ты назвал примитив «хинтом»

При чем тут примитив, ебанашка? Там даже близко может не быть твоего фора. Код вообще может не выражаться через фор.

Идиот. Эти оптимизации возможны только если for - полноценный примитив.

Нет.

если в IR есть вся информация из исходного цикла, то раскрывать его на хер не нужно.

При раскрытии внутренних макросов могут ВНЕЗАПНО появиться и другие хинты на термах в форе.

На уровне CFG без хинтов ты даже не узнаешь, что basic block такой-то является частью тела такого-то цикла.

Ты что, слепой, я не понимаю? Еще раз, для дебилов - это делается _при построении_ CFG.

Ты меня уже реально заебал своей тупостью и невежеством.

Вон в Сях туда вообще можно навешивать произвольные выражения.

А зачем делать как в сях? Говно не нужно.

А потом перед твоим компилятором возникает задача прожевать что-то вроде семантики Сишечки, и всё, soosnuli.

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

Оптимизации должны работать в общем виде,

В общем виде они не работают никогда. Задача об aliasing неразрешимая.

а не в сладких мечтах о правильных AST-ах с правильной семантикой, допускающей только правильные оптимизации.

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

Доказать это легко - уберем из хаскеля типы. Можно ли написать некорректный ИО-код?

Может, уберём тип IO, всё схлопнется в один уровень как в C++/Scala и будем писать readNumber() + 5?

Раскроем коснструктор IO. Можно ли написать некорректный код? Можно.

Вообще, unsafePerformIO не зачем быть реализованным именно unsafe.

Если такие ф-и есть (интерфейс перестает быть безопасен), то все смешивается и ломается.

Явно же смешивается. То есть

_>>_ : m a -> m b -> m b

а не

_;_ : a -> b -> b

во втором случае что угодно следует за чем угодно, в первом — m фиксирует слой, если m !~ m', то нужно явно вызвать функцию перехода на другой слой m a -> m' a (если такая вообще видна).

И, смотри - ни на каком шаге не используется никаких типов!

data Foo = Foo Int String

test = Foo "123" "123"

тут используются? Так и с кодом

foo :: IO ()
foo = do
  chan1 <- ...
  chan2 <- ...
  ...
  pass someFn chan1 chan2
  ...

atomically выброшен — будет обычная ошибка несовпадения типов.

Можно вернуть atomically, но и Foo (read «123») «123» тоже можно сделать.

Ну точно так же, в чем проблема?

А напиши пример, только без макросов и с compile-time проверками, разумеется — разделение уровней с/без переходами туда-сюда.

Нет, система типов.

И даже по Пирсу, ага. Но оно ещё что-нибудь может делать попутно, не относящееся к типам.

С чего вдруг?

Экспанд разрешим? Тайпчек — вполне.

Ты что, слепой, я не понимаю? Еще раз, для дебилов - это делается _при построении_ CFG.

Что ты называешь «построением» CFG, свинская отрыжка?

Раскрытие структурных конструкций в метки и goto - это уже построение CFG.

Loop analysis - это тупо один из pass-ов над уже готовым CFG. И сам по себе, без SSA и constant folding он бесполезен.

Именно так.

Тогда никакие оптимизации и не работают.

При чем тут примитив, ебанашка? Там даже близко может не быть твоего фора. Код вообще может не выражаться через фор.

Если семантика не эквивалентна for-у, то оптимзации для for не работают, огрызок быдла.

При раскрытии внутренних макросов могут ВНЕЗАПНО появиться и другие хинты на термах в форе.

То есть, твой примитив еще и более сложный, чем макро-морда к нему. Поздравляю, сука, ты насрал в backend.

не переводится, т.к. в с++ нельзя перегрузить оператор ";"

а еще проблема в том, в с++ если и можно запретить частичную специализацию шаблона, то какими-то совсем уж заумными способами

з.ы. но тут нужны эффекты, а монады — это костыль

Экспанд разрешим?

Я под разрешимостью подразумевал наличие алгоритма, пусть и виснущего (иногда).

Может, уберём тип IO, всё схлопнется в один уровень как в C++/Scala и будем писать readNumber() + 5?

почему схлопнется? Не схлопнется. readNumber() будет возвращать числа, завернутое в IO, по-этому обычный плюс даст эррор, очевидно.

во втором случае что угодно следует за чем угодно, в первом — m фиксирует слой

Ну так m что с типами что без типов одинаково слой фиксирует.

тут используются?

Нет.

А напиши пример, только без макросов и с compile-time проверками, разумеется — разделение уровней с/без переходами туда-сюда.

#lang racket

(struct io (x))

(define return io)

(define (bind-io x f)
  (match x
    [(io x) (f x)]))

(define >>= bind-io)

Но оно ещё что-нибудь может делать попутно, не относящееся к типам.

Ну, условно говоря, любая достаточно сильная система может делать вещи, которые вполне следует считать «попутным» (вычисления в компайл-тайме) :)

Но сущностно мы имеем то же самое: nomalloc-выражение может состоять только из nomalloc-выражений; а «просто выражение» может состоять из «просто выражений» и nomalloc-выражений.

если так, то это система эффектов (и макросистема тут не обязательна; можно обойтись атрибутами как в яве или с++0х)

btw, тебе скорее всего еще захочется эффект-полиморфизм — эти страшные слова означают, что функция f(int x, int y, int (*g)(int), int z) является nomalloc если g — nomalloc, и не является в противном случае

Тайпчек — вполне.

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

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

Кстати, можно примеры реальных предметных областей?

Это скорее общее место — типы ЯП интерпретируются как логические утверждения, типы с элементами — истинные утверждения, без — ложные, сами элементы, то есть значения и программы — как доказательства-свидетели своих типов-утверждений. Если в ЯП есть полиморфизм и зависающая программа f() { return f(); } или (fix id), то её тип это полиморфный тип (forall (A : Type). A), то есть оно населяет любой тип — переводим в логическую плоскость и получаем логику в которой все утверждения истины, то есть совсем негодную логику. Вот, например, все системы лямбда куба обладают свойством строгой нормализации (все программы завершаются), также им соответствуют непротиворечивые логики, также известно, что верхней системе соответствует логическая система достаточная мощная математически — достаточно мощная чтобы её тащили в foundations, так что соответствующий ЯП-реализация, теоретически, может служить и ЯП и средством само-верификации одновременно.

Обратно — есть разные логические системы в которых справедлива cut-elimination theorem.

Проблема Тьюринг-полноты решается, конечно, монадами :) Тип fix id это (forall (A : Type). Inf A) где Inf — partiality monad без run, так что эта вещь уже не ломает ничего, но позволяет писать (или специфицировать) Тьюринг-полные программы.

Первая реализация не называлась не Shen.

Вся идея Shen - как раз в этом KL, минимальном наборе примитивов.

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

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

это не вывод, т.к. статически неизвесно — g nomalloc или нет

есть код

int f(int x, int y, int (*g)(int), int z) {
  int result = 0;
  for(int i=x; i<z; i+=y ) 
    result += g(i);
  return result;
}

запиши сигнатуру f

у тебя получится что-то вроде

template<NomallocEffect NE> NE int f(int x, int y, NE int (*g)(int), int z); 

А, дошло.

почему схлопнется? Не схлопнется. readNumber() будет возвращать числа, завернутое в IO, по-этому обычный плюс даст эррор, очевидно.

Так мы выбрасываем типы или нет? Там у тебя был такой case + IO продолжало работать — как это ещё понять?

Нет.

То есть структура с полями int и string и инициализация её двумя int это не ошибка типов? А 1 + «2» где 1 : int, «2» : string и _+_ : int * int -> int?

(я тут подумал — а может ты вообще наплевал на всю эту статико-терминологию и вещаешь о чём-то своём? :)).

#lang racket

Я на elispe:

(defstruct io x)
(defun ret (x) (make-io :x x))
(defun bin (x f) (funcall f (io-x x)))
(defun good () (bin (ret 5) (lambda (x) (+ x 5))))
(defun bad () (bin 5 (lambda (x) (+ x 5))))
(good) ;=> RT: 10
(bad) ;=> RT: Debugger entered--Lisp error: (error "io-x accessing a non-io")

нифига же не работает, just as planned.

Так мы выбрасываем типы или нет? Там у тебя был такой case + IO продолжало работать — как это ещё понять?

Теперь понял — ты предлагал оборачивать значения в рантайме и там же всё проверять, хаскельная обвёртка newtype не сказывается никак на рантайме, она нужна только для проведения различий в во время компиляции (на уровне типов).

нифига же не работает, just as planned.

Не понял, что не работает? Вон же ошибка («io-x accessing a non-io»), слои не смешиваются.

Так мы выбрасываем типы или нет?

Выбрасываем.

Теперь понял — ты предлагал оборачивать значения в рантайме и там же всё проверять, хаскельная обвёртка newtype не сказывается никак на рантайме, она нужна только для проведения различий в во время компиляции (на уровне типов).

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

Теперь понял — ты предлагал оборачивать значения в рантайме и там же всё проверять, хаскельная обвёртка newtype не сказывается никак на рантайме, она нужна только для проведения различий в во время компиляции (на уровне типов).

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

Вон же ошибка

Во время выполнения.

Ахо,Ульман - говно? А что тогда читать?

P.S Почему LLVM - говно?

Во время выполнения.

Какая разница-то? Некорректной аппликации бинд не допустил же.

elisp - динамический ЯП же.

элементарный синтакс-чек прошел - идем в рантайм.

Ну в треде-то обсуждаются как раз системы, гарантирующие проверки в compile time. Началось обсуждение с недопустимости malloc в обработчике прерывания.

Так что elisp тут не в тему.

Изначально речь была про систему эффектов (да ещё и для ядра, то есть желательно без оверхеда). Разумеется со статическими проверками. anonymous стал утверждать, что типы не нужны и того же можно добиться в динамическом ЯП, как оказалось — без статических проверок (и с оверхедом в виде боксинга).

но ведь можно же.

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

Некорректной аппликации бинд не допустил же.

(bad) не нужен, вообще этой ветки выполнения быть не должно — такая хотелка.

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

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

В питоне между прочим такие вещи делаются очень изящно... мы щас как раз чем то подобным на нем и занимаемся;-)

а подробнее? что вы делаете — новый синтаксис? typecheck?

и в чем проявляется изящество?

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

Изящество - парсить ничего не надо, все делает интепретатор;-)

Перегонять код в AST и попуцтно преобразовывать <...> Изящество - парсить ничего не надо, все делает интепретатор;-)

и что — можно вытащить AST *полностью*?

я так предполагаю, что методика вытаскивания AST — это подсунуть exec-y правильный mapping object, чтобы вместо/во_время выполнения f(x,42) построилось соответствущее AST

но для этого нужно, чтобы перегружались не только функции, но и if-ы и прочие управляющие конструкции — питон это позволяет?

понятно, что если хочется всего лишь

exec "from(table1,table2).select(a,b,c).where(a=c).order_by(b)" in crafted_mapping_object

то управляющие конструкции перегружать не надо, но тогда и без AST вроде можно обойтись

и в чем будет отличие получившегося языка от питона? exec намекает на то, что отличие будет в том, что переменные будут за-bind-ены на что-то другое, чем в питоне — а на самом деле?

ACL2

что скажешь на тему ACL2 vs. agda или coq в разрезе без типизации vs. с типизацией? с одной стороны, для term rewriting типизация вроде и не нужна, с другой — я так глянул, там подозрительно как-то занимаются деструкцией cons-ов, что намекает на какие-то срезания углов или соглашения вместо человеческой типизации