> докладчик делает логическую ошибку, когда говорит (момент 32:26), что из сохранения эквивалентности следует, что новая фича не привносит мощности (т.е., она выразима через существующие фичи).

Подозреваю, такую теорему тоже можно доказать. 😊

>  кто больше "сломал", тот и выразительнее.

Не, так нельзя. Новая базовая фича вообще может не нарушить эквивалентность, но быть очень "крупной". Автор работы приводит пример, когда добавляется целый отдельный язык.

> Подозреваю, такую теорему тоже можно доказать

Да нельзя ее доказать, т.к. она опровергается контр-примером.

Это Вы пытаетесь заданное формальное понятие натянуть на свою интуицию о том, "как должно быть". Не надо так! 😃
Нужно новое понятие воодить и формализовывать.

Каким?

Давайте я начну издалека. Интересно ознакомиться с историей проекта. Оказывается, этот MicroC родом из университетского курса. Курс вполне стандартный, но простенький компилятор там предлагалось строить на Ocaml. По мотивам автор блога решил сделать версию для Haskell. Как видно из github-статистики, работал он над своей версией в течение 2 лет.

На что сразу хочу обратить внимание. Здесь имеет место типичная история для современных bondage-and-discipline ("строгих"/"чистых"/etc) языков в духе Haskell или, например, Rust. Задача четко и формально определена, более того, уже есть ее решение. То есть весь вопрос в переписывании, с целью достижения каких-то новых качеств.

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

Автор активно пользуется готовыми библиотеками из Haskell для реализации парсера и порождения LLVM-представления, но при этом объем полученного кода на Haskell вполне сравним с chibicc (который реализует многое из C99 и генерирует x64-код)  на чистом Си.

Теперь кратко по отдельным разделам.

1. Очень хорошо, что автор привел сравнение lex/yacc-подобного инструмента и работы библиотеки комбинаторов парсеров. На мой взгляд, в данном случае убедительную победу завоевал заурядный генератор парсеров. К счастью, комбинаторы парсеров могут быть гораздо более выразительными, но, увы, не в данной Haskell-реализации.

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

3. Здесь, в основном, идет работа с готовой библиотекой поддержки LLVM. В какой-то момент автор срывается в описание свойств SSA и phi-функций, но не стоит его принимать всерьез -- на деле код будет сгенерирован самым обычным образом, в надежде на LLVM'овский mem2reg.

В целом, на мой взгляд, посредственная читаемость кода данного игрушечного компилятора проистекает, в первую очередь, из-за монадического подхода. Классический вариант на SML от того же Аппеля имеет гораздо более ясный код. Конечно же, я не говорю сейчас о том, что части компилятора сегодня можно писать на более высоком уровне, с помощью специальных нотаций/eDSL.

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

Но, Теорема 3.14 часть ii, что обратное не верно, доказывается в работе.

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

а что не так со вторым типизированным аст? это же обычный подход - провели десижн процедуру, зафиксировали инварианты в уточненной структуре

Ну Вы же помните, как было сделано в учебнике Аппеля? А еще можно, все-таки, ввести новый вариант IR, но сделать это изящно, без многословия, то есть как в Nanopass :)

а что там в нанопассе, кодировка черча?

Ну вот. А ведь я уже не первый год в этом чате пишу про Nanopass! Важное замечание — далеко не все полезное для практики компиляторописания выводится непосредственно из лямбда-исчисления или, скажем, теории категорий ;)
https://github.com/nanopass/nanopass-framework-scheme/blob/master/doc/user-guide.pdf

Т.е., следует сравнивать мощность выразительных средств в области построения встроенных компиляторов/интерпретаторов (в общем — трансляторов), так?

Причем, как я понимаю, транслятор DSL (т.е., транслятор подходящей нотации для решения задачи) должен встраиваться в сам исходный язык, верно?

Да, можно задать градацию "расширяемости" языка. Навскидку, среди конструкций можно вспомнить:

1. Цепочки методов в ООП-языках.
2. Типы и перегрузка операций.
3. ФВП (комбинаторы).
4. Макросы.
5. БНФ-подобные средства описания синтаксиса.
6. Развитые средства создания компиляторов.

Примеры ЯП не привожу -- но они полезны были бы :)

А какая разница между комбинаторами и ФВП?

git install typescript гы 😊

Действительно, только git install и нехватает...

Отражение (рефлексия, reflection) куда встанет в списке?  или, оно не важно?

Библиотеки комбинаторов — способ создания eDSL с использованием ФВП.

Тогда почему комбинаторы попали в выразительные средства языка вместо ФВП???