Супер-синхронизм: мой конца февраля пост про DSL
"как нейронки агенты использовать, чтобы писать в 1000 раз компактный код (любые технологии фреймворки, не важно), и чтобы человек уровня миддл мог реализовывать проекты любой сложности, сохраняя её рост линейным."

А 4 марта выходит мощный пейпер "A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism" учёных четырёх европейских университетов (я уже говорил не раз, что все годы придерживаюсь подходов именно европейской школы computer science, она сегодня топчик). Это математическая теория для создания DSL, и при этом строго в рамках теории типов! В самой статье DSL не упоминается, это как-то слишком приземлённо, но разбирается именно это, просто на более высоких уровнях абстракции.

Конкретную программу пишем на DSL, и этот язык предметной области формально описывается мета-системой (GAT из статьи), которая описывается мета-мета-системой (Алан Кэй: "Lisp isn't a language, it's a building material").

И вот наконец данная работа развивает эту идею до математического абсолюта: GAT/CwF позволяют создавать языки с формально доказанными свойствами, и отсюда мы попадаем и в существенно облегчённую формальную верификацию, и суперпродуктивную работу с нейронками, которые так здорово понимают лингвистически формализованные бизнес-темы, генеря реально хороший код.

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

Пейпер добавляет к этому:
- система может математически доказать свою корректность;
- любой DSL, описанный в этом мета-языке, наследует все эти гарантии!

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

=

Сама статья даёт категорный взгляд на синтаксис и правила вывода, позволяющий строить т.н. "начальные" модели и доказывать их единственность через общую алгебраическую теорию (GAT) (в рамках MLTT например). "Начальные" - это по сути математический объект, где синтаксис языка (то, что пишет программист) однозначно соответствует его семантике (тому, что происходит при выполнении).

Обобщение многосортных алгебраических теорий: сорта и операторы могут иметь зависимые типы, позволяет описывать синтаксис и правила типизации как сигнатуру с уравнениями.

CwF (Category with Families): категориальная модель зависимых типов.
Индексация уровнями, уровни вселенных организуются как untyped cwf (явный полиморфизм). Вы же помните мой трек по HoTT? :)

Каждая теория представляется как GAT. Синтаксис -- это начальная модель. Категориальная абстракция устраняет зависимость от конкретных правил вывода. Связь с Second-Order Generalised Algebraic Theories, Quotient Inductive-Inductive Types, Logical Frameworks...

Метод применим вообще к любым формальным дедуктивным системам!!

=

Когда вы пишете DSL на Racket или Scala, RoR или Haskell, вы полагаетесь на свой опыт, тесты и code review, и всё. Даже в Template Haskell нету гарантий корректности.

Когда мы описываем DSL через GAT (как в статье), мы получаем
- математическую гарантию, что наш DSL корректен;
- автоматическую верификацию всех программ на этом DSL;
- наследование свойств через иерархию мета-уровней.

Это и есть та самая "meta-system" Алана Кэя, доведённая до логического и математического совершенства.