Типизированные индексы де Брёйна для LLM

Классические индексы де Брёйна заменяют именованные переменные позиционными ссылками (λx.λy.x превращается в λ.λ.1). Вариант в Vera типизирует каждое связывание и ссылается на него по типу плюс обратной позиции: @Int.0 - это последний Int в области видимости, @Int.1 - предыдущий, @String.0 - последний String. Проблем с затенением не возникает, поскольку слот определяется типом: добавление нового Int не сдвигает то, на что указывает @String.0.

Мотивация здесь эмпирическая. README проекта Vera ссылается на исследование, показывающее, что LLM особенно уязвимы к ошибкам, связанным с именованием: выбору вводящих в заблуждение имён, некорректному повторному использованию имён и потере связи между именем и значением (см. arXiv:2307.12488). Все три сценария отказа исчезают в языке, где имён нет вовсе. Модели не нужно помнить, как именно она назвала пользовательский ввод: в области видимости есть всего одна @String или две, а ссылка на неё позиционная.

Чем приходится жертвовать

• Чтение коммутативных операций. @Int.0 + @Int.1 и @Int.1 + @Int.0 дают одно и то же значение, но визуально различаются, поэтому проверяющему-человеку приходится мысленно привязывать имя к каждому слоту, чтобы разобрать нетривиальную арифметику. В DE_BRUIJN.md из репозитория Vera это называется "ловушкой коммутативных операций".
• Когнитивная опора на самодокументируемые имена. Человек, читающий userBalance / pricePerToken, сразу видит предметный смысл. Выражение @Int.0 / @Int.1 этой информации не несёт - её приходится извлекать из контракта, имени функции или комментариев.

Расчёт строится на том, что в сценарии, где автором выступает LLM, такой компромисс оправдан: снижение уровня шума даёт больше выигрыша, чем потеря читаемости для человека создаёт издержек (человек проверяет контракт, а не выражение со слотами).

Где ещё это может применяться

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

• Позиции полей в конструкторе вместо именованных полей структур (некоторые языки уже поддерживают позиционное конструирование).
• Анонимные аргументы лямбда-функций - _1, _2 в некоторых стилях Scala/F#, та же идея в более узком масштабе.
• Операторы конвейера (|>), которые передают значение через цепочку преобразований без связывания с именем.

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

Перекрёстные ссылки

• vera - страница языка в каталоге инструментов.
• vamp-ai-frontend - смежная тема: неявность во фреймворках (VDOM, хуки, согласование) враждебна генерируемому ИИ коду, и явные конвейеры выигрывают по той же причине, по которой здесь проигрывают имена.
• clippy-stricter-config - противоположный подход: вместо переизобретения языка под агентов - ужесточение привычного языка линтерами.
• clean-code-coding-agents - экономика контекстного окна, заставляющая языки быть дешёвыми для ориентации.