Древесные оптимизации нарушают семантику

[Mazdaywik]

Введение. Гарантии для равенства замыканий

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

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

Например:

Eq {
  t.Eq t.Eq = True;
  t.X t.Y = False;
}

F {
  e.X = <Eq (e.X) (e.X)>;
}

Функция F всегда должна возвращать True.

Ещё есть неявная аксиома — повторные s-переменные должны сопоставляться за константное время. В учебнике Турчина говорится, что открытые переменные, повторные t- и e-переменные скрывают за собой рекурсию, следовательно, виды сопоставлений рекурсию не скрывают, т.е. сопоставляются за константное время.

Рефал-5λ поддерживает вложенные функции в результатных выражениях. Во время выполнения для вложенных функций порождаются замыкания — значения типа «символ» (сопоставимые с s-переменными), которые можно вызывать как функции. Замыкания могут захватывать контекст.

Возникает вопрос: как сравниваются на равенство два замыкания? Для Простого Рефала в manul.pdf были определены следующие ограничения:

1. Экземпляры функций, как и другие атомы, копируются за константное время.
2. Передача управления на указатель на функцию выполняется за константное время.
   Передача управления на замыкание может выполняться как за константное время, так и за время пропорциональное размеру контекста. Последнее возможно, если в поле зрения присутствует несколько копий данного замыкания, поэтому для вызова каждого из экземпляров требуется своя копия контекста — такова списковая реализация. 〈…〉
3. Два экземпляра функции, полученные путём копирования одного атома, равны.
4. Два замыкания, построенные из текстуально разных функциональных блоков, не равны.
5. Два замыкания, имеющие разное содержимое элементов контекста, не равны.
6. Указатели на функцию равны тогда и только тогда, когда они указывают на одну и ту же функцию.

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

То, что не описано выше, намеренно не определено. В частности, если замыкание с одним и тем же контекстом из одного и того же текстуально блока создаётся в разные моменты времени, то равенство не определено. Простейший пример:

F1 { = { = } }
F2 { e.X = { = e.X } }

Eq { 〈см. выше〉 }

Test {
  e.X
    = <Prout <Eq <F1> <F1>>>
      <Prout <Eq <F2 e.X> <F2 e.X>>>
}

Функция F1 создаёт замыкание с пустым контекстом, а для таких случаев вместо объекта замыкания создаётся просто указатель на неявную глобальную функцию (&F1\1). Поэтому первый вызов распечатает True. Так было сделано с самой первой реализации вложенных функций в Simple Refal.004.

Второй вызов по умолчанию распечатает False, поскольку два вызова <F2 e.X> создадут два объекта замыкания, которые сравнятся по ссылке. Но если функции F2 и Eq прогнать (или даже встроить), то мы получим <Prout True>. Реализованный алгоритм обобщённого сопоставления с образцом допускает повторные переменные любого типа, причём сопоставление считается успешным, если значения этих переменных текстуально совпадают (если не совпадают и тип переменной не s — результат не определён). Поэтому здесь сопоставление будет успешным.

Далее, мы рассмотрим три примера. Один с мнимым нарушением семантики, два других — с реальным.

Воспроизведение ошибки

Пример 1. Мнимое нарушение семантики при прогонке

$ENTRY Go {
  e.X
    = <Eq <Clo e.X> <Clo e.X>> : False
    = /* пусто */
}

$INLINE Clo, Eq;

Clo { e.X = { = e.X } }

Eq {
  s.X s.X = True;
  s.X s.Y = False;
}

Скачать: closures-neq-drive.ref.

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

Пример 2. Реальное нарушение семантики при прогонке

$ENTRY Go {
  e.X
    = <Eq <Dup { = e.X }>> : True
    = /* пусто */
}

$INLINE Dup;

Dup { e.X = e.X e.X }

Eq {
  s.X s.X = True;
  s.X s.Y = False;
}

Скачать: closures-eq-drive.ref.

Здесь встраивается вызов Dup, в результате чего Eq вызывается с аргументом

<Eq {{ &Go\1 e.X }} {{ &Go\1 e.X }}>

Во время выполнения создаются два одинаковых объекта замыкания. Но, поскольку замыкания сравниваются по ссылке, они оказываются не равны.

Пример 3. Реальное нарушение семантики при специализации

$ENTRY Go {
  e.X = <S { = e.X }>;
}

$SPEC S s.STAT;

S {
  s.X = <Eq s.X s.X> : True = /* пусто */;
}

Eq {
  s.X s.X = True;
  s.X s.Y = False;
}

Скачать: closures-neq-spec.ref.txt.

Причина похожа на предыдущую — строятся два одинаковых экземпляра замыкания вместо копирования одного. Только теперь путём размножения значения статической переменной. Специализированная функция S@1 выглядит так:

S@1 {
  e.X#1 = <S=1 <Eq {{&Go\1 (e.X#1)}} {{&Go\1 (e.X#1)}}>>;

  e.X#1 = <S@0 {{&Go\1 (e.X#1)}}>;
}

Решение

А вот однозначного решения тут пока не видно — везде есть компромиссы.

• Запретить сравнивать на равенство замыкания — останавливать аварийно программу при таком сравнении. Решение слишком контринтуитивное — программа будет падать «на ровном месте» с точки зрения пользователя. При написании повторных переменных придётся задумываться: а не могут ли там оказаться замыкания?
• Отказаться от принципа, что значения, созданные копированием, равны. Тоже контринтуитивное решение, да и прогонка повисает без серьёзных оснований.
• Усложнить прогонку и специализацию — придумать «фокусы», которые отслеживали бы равные ссылки во время преобразований.
• Сравнивать замыкания по значению. Это отказ от сравнения s-переменных за константное время. В принципе, отказ не такой страшный, поскольку для замыканий и вызов функции не выполняется за константу (копируется контекст).
• Вообще отказаться от символов-замыканий. Можно сделать замыкания t-переменными, скрестив их с абстрактными скобками. Решение красиво тем, что существенно упрощает и семантику языка, и реализацию компилятора. Недостаток — слишком большое изменение.

Приемлемыми мне видятся только последние три варианта. А может даже, последние два.

Буду думать летом после завершения #260, #256, #252, #253.

[Mazdaywik]

Варианты с запретом на сравнение замыканий и нарушением аксиоматики отбрасываем. Рассмотрим приемлемые варианты.

Научить прогонку и специализацию не нарушать семантику

Тут возможны два пути: сужения и расширения.

Путь сужения — не генерировать опасные конструкции

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

Нечто похожее уже делается — в прогонке запрещены сужения в замыкания, а в специализации построенные функции проверяются на «осмысленность». Цель одна и та же — не дать замыканиям просочиться в образец, что синтаксически некорректно.

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

Путь расширения — усложнить логику для сохранения семантики

Требуется, чтобы при размножении в правых частях замыканий они всё равно считались равными. Значит, им нужно добавить некий «ключ», равенство которого соответствует семантическому равенству двух объектов.

Правая часть вида

<F {{ &G\1 (e.X) }}> <H {{ &G\2 (e.Y) }}>

будет неявно преобразовываться к виду

$genkey : s.k1, $genkey : s.k2, <F {{ &G\1 s.k1 (e.X) }}> <H {{ &G\2 s.k2 (e.Y) }}>

Здесь $genkey генератор ключа, ключи добавляются в объекты замыканий и используются для сравнения на равенство. Теперь, если функции F и H имеют вид

$INLINE F { s.X = s.X '+' s.X }

$SPEC H s.STAT;
H { s.X = s.X '*' s.X }

то правая часть преобразуется в

$genkey : s.k1,
$genkey : s.k2,
{{ &G\1 s.k1 (e.X) }} '+' {{ &G\1 s.k1 (e.X) }} <H@1 s.k2 e.Y>
…
H@1 {
  s.k2 e.Y = {{ &G\2 s.k2 (e.Y) }} '*' {{ &G\2 s.k2 (e.Y) }};
}

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

Заметим, что в этом случае оптимизация сохраняет поведение и для «зеркального» случая: когда в разные моменты времени создаются два замыкания с одинаковым контекстом.

Пример:

F { e.X = <G e.X> <G e.X> }

$INLINE G { e.X = { = e.X } }

После рассахаривания получим:

F { e.X = <G e.X> <G e.X> }

$INLINE G {
  e.X = $genkey : s.k, {{ &G\1 s.k (e.X) }};
}
G\1 { s.k (e.X) = e.X }

После встраивания получим:

F {
  e.X = $genkey : s.k1, $genkey : s.k2, {{ &G\1 s.k1 (e.X) }} {{ &G\1 s.k2 (e.X) }}
}

Ключи будут разные, а значит, объекты замыканий также будут не равны.

Причём ключом может являться сам указатель на объект замыкания. Операция $genkey создаёт «пустое» замыкание. Операция создания замыкания смотрит, пустое ли оно. Если пустое, ему присваивается контекст. Если не пустое — то ничего не делается. Фактически, на замыкание можно смотреть как на динамический ящик, который создаётся пустым, и которому можно присвоить только один раз.

Сейчас Рефал-5λ поддерживает только безымянные вложенные функции. Предлагаемая реализация с разделением создания замыкания на две фазы позволяет реализовать и именованные взаимно-рекурсивные вложенные функции.

Сравнивать замыкания по значению

Самый простой в реализации подход к решению этой проблемы. Минимальные правки рантайма.

Недостаток — быстродействие. Но, с другой стороны, пока на Рефале-5λ никто не использует стиль программирования, требующий сравнения замыканий на равенство. Приравниваются обычно пассивные значения (или глобальные функции как метки АТД-скобок), функции обычно только вызываются.

Отказаться от символов-замыканий

Почему замыкания представляются s-переменными? Потому что так было в Рефале-7 s-переменная — это значение, которое невозможно при помощи сопоставления с образцом разбить на составные части.

Замыкание состоит из указателя на глобальную функцию и контекста в виде объектного выражения определённого формата. При этом глобальная функция ожидает именно такого формата от контекста. Если дать возможность пользователю манипулировать содержимым замыкания, то он может нарушить инварианты. Поэтому для скрытия реализации замыкания считаются s-переменными. В общем, как-то так это рационализируются. На самом деле, я списал из Рефала-7, когда делал вложенные функции в Простом Рефале.

Но Рефал-5λ допускает и другую форму инкапсуляции — АТД-скобки. Получить доступ к содержимому можно только записав имя функции после открывающей квадратной скобки.

Если имя АТД-терма не будет доступно пользователю (вроде F\1), то инкапсуляция также будет обеспечена. Замыкания будут просто скобочными термами, поэтому приравниваться по значению будут совершенно естественным образом. Копироваться они будут за линейное время, при этом явно. Вызов будет осуществляться за константное время.

Также потребуется определить семантику для вызова АТД-термов. Тут возможны два варианта:

1. <[Func e.X] e.Y> → <Func e.X e.Y>
2. <[Func e.X] e.Y> → <Func [Func e.X] e.Y>

Какой из них предпочесть, пока неясно.

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

Недостаток — существенная переделка языка и компилятора.

Что выбрать?

Не знаю.

[Mazdaywik]

В задаче #160 рассматривается вариант, когда после специализации замыкания у него не остаётся контекста (#160 (comment)). Для такого замыкания можно или строить вырожденный объект замыкания, или заменять на указатель на функцию.

В случае замены на указатель на функцию в #160 (comment) рассматривается слабое изменение поведения программы — функция Type возвращает не тип замыкания, а тип указателя на функцию. Но есть и более сложная проблема в контексте настоящей задачи.

Рассмотрим программу:

$ENTRY Test {
  e.X
    = { e.Y = e.X e.Y } : s.Func
    = <Eq s.Func <S s.Func e.X>>;
}

$SPEC S s.FUNC e.ARG;

S {
  s.F e.X = s.F <D e.X>;
}

$DRIVE D;

D {
  'abc' = ;
  'a' e._ = ;
  e._ = ;
}

Eq {
  s.Eq s.Eq = True;
  s._ s._ = False;
}

После специализации, прогонки и специализации замыкания мы получим следующую функцию S:

S@1 {
  'abc' = &Test=1\1@1;  /* № 1 */
  'a' e.X = {{ &Test=1\1@2 (e.X) }};  /* № 2 */
  e.X = {{ &Test=1\1 (e.X) }};  /* № 3 */
}

* Неспециализированная функция
Test=1\1 {
  (e.X) e.Y = e.X e.Y;
}

Test=1\1@1 {
  e.Y = 'abc' e.Y;
}

Test=1\1@2 {
  (e.X) e.Y = 'a' e.X e.Y;
}

В неоптимизированной программе замыкание формируется один раз — в функции Test, затем оно «просеивается» через S, откуда возвращается неизменным. Функция Eq вернёт True.

В оптимизированной программе присваивание встроится — конструкторы одного и того же замыкания будут находиться в аргументах Eq и S. Функция S проспециализируется, конструктор упадёт в неё. А там размножится в результате прогонки.

В трёх ветвях функции S@1 мы будем строить для замыкания:

• указатель на глобальную функцию (№ 1),
• специализированное замыкание (№ 2),
• неспециализированное замыкание (№ 3).

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

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

Запрет на дублирование замыканий слишком жёсткий — не даёт специализировать такие функции, как Map. Можно придумать и более сложный анализ, который позволял бы и Map оптимизировать, и сохранять семантику. Для этого нужно при специализации функции передавать в неё и переменные из контекста, и указатель на замыкание, создаваемый вовне. При этом внутри функции нужно помнить, что эта s-переменная хранит уже известное значение. Для таких «заимствованных» замыканий специализация замыканий работать уже не должна. Но всё это дико сложно, особенно в рамках текущего формализма, поэтому рассматривать дальше этот вариант не будем.

[Mazdaywik]

Возможно, наилучший вариант — отказаться от инварианта, что все копии всегда равны. Для пассивных данных — равны. Если вступают в действия указатели на функции и агрессивные оптимизации — уже не определено. При этом при прогонке нужно подразумевать, что все копии всегда равны, семантика, вроде как, должна оставаться корректной.

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

[Mazdaywik]

Замыкания — типы значений, квадратные скобки?

В последнее время я склоняюсь к мысли реализовать замыкания как квадратные скобки, как в Модульном Рефале:

https://github.com/Mazdaywik/mrefal/blob/a0e62511207544ca6102a1e6b0fb94eee7c93681/Documentation/%D0%96%D1%83%D1%80%D0%BD%D0%B0%D0%BB/Changes.txt#L8413-L8534

Преимущества и недостатки:

• ✔ Основная проблема была в том, что замыкание — ссылочный тип, создаваемый встроенной конструкцией языка. Из-за чего ссылочные типы входили в ядро языка и поэтому должны были учитываться при преобразованиях программы.

  Теперь ссылочные типы (в актуальной реализации их нет, кроме замыканий) могут создаваться только внешними функциями на Си, а проблем для значений, созданных внешними функциями, быть не должно (Разрешить аргументам прогоняемых функций быть активными #230). Результаты вызовов двух функций всегда считаются независимыми, даже если у них аргументы одинаковы.

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

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

• ✔ Упростится сам язык (в русле Удаление устаревших элементов языка и компилятора #318), на одно понятие в языке будет меньше. Абстрактные скобки сами станут активными объектами. Можно даже для симметрии разрешить вызов вида <(&F e.1) e.2> на уровне среды выполнения.

• ✔ В актуальной версии специализатора есть проблема, которая решается костылём.

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

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

  При замене замыкания на АТД-терм проблема растворяется сама собой: в образцах допустимы и естественны квадратные скобки.

• ✔ Можно реализовать именованные рекурсивные и даже взаимно-рекурсивные замыкания. Захваченные переменные замыкания, которое вызывает другое замыкание, включают в себя захваченные переменные этого замыкания. Следствие: два взаимно-рекурсивных замыкания захватывают одни и те же переменные. Синтаксис можно взять из Рефала-7.

• ❌ Проблема со специализацией замыканий (Специализация замыканий #160) остаётся нерешённой. Возможно, при условии Разрешить аргументам прогоняемых функций быть активными #230, специализация замыканий станет менее актуальной и её можно будет убрать.

• ❌ Обратная совместимость. Но она не актуальна, т.к. единственная программа на Рефале-5λ, не являющаяся программой на Рефале-5 (т.е. которая использует замыкания) — это сам компилятор Рефала-5λ.

Также потребуется определить семантику для вызова АТД-термов. Тут возможны два варианта:

1. <[Func e.X] e.Y> → <Func e.X e.Y>
2. <[Func e.X] e.Y> → <Func [Func e.X] e.Y>

Можно добавить и третий вариант:

<[Func e.X] e.Y> → <Func (e.X) e.Y>

Его преимущества: по сравнению с 1 не сливается содержимое терма с аргументом, по сравнению с 2 не требуется дополнительных аллокаций памяти.

[Mazdaywik]

Развитие идей предыдущего комментария

Про специализацию замыканий

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

Если «наивно» заменить (ClosureBrackets …) на (ADT-Brackets …), то специализация замыканий как таковая станет невозможной. Ведь квадратные скобки могут использоваться не только для представления замыканий компилятором, их может использовать программист для создания собственных типов данных. В качестве тега инкапсулирующих скобок может быть использована не только пустая функция, но и вообще любая локальная (а почему бы и нет?). Такие скобочные термы, очевидно, специализировать нельзя, т.к. пользователь будет немало удивлён.

Можно придумать и более изощрённые варианты, например, угадывать специализируемые квадратные скобки по суффиксу. Имена без суффиксов или с суффиксом ~N оптимизировать нельзя, остальные — можно.

Сложные случаи специализации замыканий

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

• Пример из комментария Древесные оптимизации нарушают семантику #276 (comment), дублировать его содержимое не буду.

• Следующий пример, описания очевидных функций опущены:

  F { e.X = { = e.X } }
  $SPEC F s.STAT;
  
  G {
    e.X = <Eq <F 'abc'> <F <gen_e__ 'abc'>>>
  }
  

  В случае актуальной реализации замыканий (символы-ссылки) замыкания будут неравны в неоптимизированной программе, в оптимизированной программе они будут иметь разные типы, т.к. первое замыкание будет без контекста.

  В предполагаемой реализации замыканий как квадратных скобок, защищённых невидимым именем безымянной функции, в неоптимизированной программе оба замыкания будут равны (замыкают равный контекст, построены из одного блока кода), в оптимизированной… А как они будут в оптимизированной? Наивный вариант, как мы поняли, не работает. Более изощрённый вариант проспециализирует и они станут не равны, в том числе по типам.

Из приведённых примеров можно сделать такой вывод: нельзя специализировать замыкания в экземплярах специализированных функций. Пример из #276 (comment) демонстрирует специализацию «чужого» замыкания, который попал внутрь экземпляра из сигнатуры. Второй пример демонстрирует специализацию «своего» замыкания (замыкания функции F\1).

$ENTRY F {
  (e.X) (e.Y) = <{ s.F = <Eq <s.F e.X> <s.F e.Y>> } { e.A = { = e.A } }> <D e.X>
}

$DRIVE D, Eq;

D {
  'abc' = 1;
  'a' e._ = 2;
  e._ = 3;
}

Eq {
  t.X t.X = True;
  t._ t._ = False;
}

$EXTERN F;

$ENTRY Go {
  /* пусто */
    = <Prout
        <F ('abc') ('abc')>
        <F ('abcd') ('abcd')>
        <F ('bcd') ('bcd')>
      >
}

Актуальная реализация в неоптимизированном варианте напечатает False 1 False 2 False 3, в оптимизированном — False 1 False 2 True 3. Предполагаемая реализация с абстрактными скобками без оптимизации выдаст True 1 True 2 True 3 с оптимизацией — False 1 False 2 True 3. Предполагаемая реализация с предполагаемой оптимизацией #322 может выдать и True 1 True 2 True 3. Но в более хитрых примерах и #322 не спасёт.

Но и в этом примере можно сказать, что выполняется специализация «чужого» замыкания — функции F\2\1 внутри функции F. «Родной» функцией для F\2\1 является функция F\2.

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

Со «своими» замыканиями всё проще:

$ENTRY F {
  e.X = { = e.X } <D e.X>
}

$DRIVE D;

D {
  'abc' = 1;
  'a' e._ = 2;
  e._ = 3;
}

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

В оптимизированной версии инварианты сохранятся. Актуальная реализация для <F 'abc'> будет возвращать один и тот же указатель на глобальную функцию, но это никто не запрещает. У предполагаемой реализации ссылочная прозрачность (в определении Андрея Климова) тоже сохранится.

Вызов <Type <F 'abc'>> в актуальной реализации меняет свой результат при оптимизации. В предполагаемой будет менять, если построение [F\1@1] будет сокращаться до &F\1@1.

Так что следует запрещать специализацию тех замыканий, стирание одного суффикса имени которого даёт имя, отличное от имени функции, внутри которой находится замыкание. Отдельный вопрос с замыканиями в условиях — тут мне пока не очевидно.

Однако обратное неверно. Можно привести пример, когда специализация «своего» замыкания опасна. (Это не комментарий сам себе противоречит, это моя мысль развивается в процессе написания.) Это слегка модифицированный первый пример:

$ENTRY F {
  e.X = <G { = e.X }> <D e.X>
}

$DRIVE G, D, Eq;

G {
  s.F = <Eq <S s.F> s.F>
}

D {
  'abc' = 1;
  'a' e._ = 2;
  e._ = 3;
}

Eq {
  t.X t.X = True;
  t._ t._ = False;
}

$SPEC S t.STAT;

S { t.F = t.F }

Вызов G раскроется, получится <Eq <S {{ &F\1 e.X }}> {{ &F\1 e.X }}> <D e.X>. Потом прогонится вызов D, сужения для e.X горизонтально распространятся. Прогонять нечего. Выполнится проход специализации. Сначала он построит экземпляры для S, а потом для замыкания F\1.

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

Вывод

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

Возможно, единственный вариант сохранить и семантику, и эту оптимизацию — хранить в замыканиях уникальные идентификаторы (см. $genkey в #276 (comment)) и при сравнении на равенство использовать их, а не ссылку на объект (как сейчас) или содержимое (как предполагается).

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

Скобки каррирования?

Рассмотрим случай, когда замыкания всё-таки станут типами-значениями. Семантика их вызова будет выглядеть так:

<[F e.X] e.Y> → <F e.X e.Y>

(поведение по аналогии с Apply)

Тогда квадратные скобки можно назвать каррирующими скобками. Ведь они действительно строят объект, который можно вызвать и связывают префикс входного формата — несколько входных параметров.

В этом дискурсе замыкание в квадратных скобках становится простым синтаксическим сахаром — компилятор неявно генерирует функцию и связывает часть её формата со значениями переменных контекста.

Однако, инкапсуляция при помощи квадратных скобок становится наоборот хаком, а синтаксические ограничения на квадратные скобки повисают в воздухе. Во-первых, неочевидным становится потребность разбирать каррированное значение в образце. Во-вторых, почему, если в переменной s.f или t.f находится функция, нельзя писать в результатном выражении [s.f e.a] или [t.f e.a]? В третьих, почему нельзя писать образцы вида [s.f e.a], почему известное имя функции обязательно?

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

[Mazdaywik]

Сегодня в ИПМ имени М.В. Келдыша онлайн проходил семинар — я читал доклад о проблеме и предложил два варианта решения:

https://mazdaywik.github.io/direct-link/2021-05-17-Konovalov-Closures-and-Optimizations-Refal-5-lambda.pdf

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

[Mazdaywik]

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

Предлагается (что-то похожее писалось выше) отделить конструирование замыкания от его использования. Вместо записи

RL {{ &F\1 CTX }} RR

(где RL и RR части выражения) писать

{{ &F\1 CTX }} : s.1, RL s.1 RR

«Условие» в этой записи понимается не как ограничение на предшествующий образец, а как льезонная форма записи.

Переменной s.1 в этом случае приписывается аксиома (её можно называть также рестрикцией)

<s.1 e.∀> ≡ <F\1 CTX e.∀>

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

При специализации функции в сигнатуру попадает и сама переменная s.1, и аксиома. Что-то вроде

<S s.1 e.2 t.3> / <s.1 e.∀> ≡ <F\1 t.3 e.4 e.∀> /* Внимание, t.3 повторяется! */

Соответственно, внутри экземпляров специализированной функции никаких специализаций замыкания быть не может. Сама функция F\1 специализироваться, конечно, может, если переменная s.1 оказалась после < и сработала аксиома.

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

$OPT D;
D {
  X = X;
  s._ = S;
  t._ = T;
  e._ = E;
}

F {
  e.X = { = e.X } <D e.X>;
}

Здесь функция F в промежуточной форме примет вид

F {
  e.X = {{ &F\1 (e.X) }} : s.1, s.1 <D e.X>;
}

F\1 { (e.X) = e.X; }

и она успешно прогонится, а F\1 — проспециализируется:

F {
  X = &F\1@1 X;
  s.1 = {{ &F\1@2 s.1 }} : s.2, s.2 S;
  t.1 = {{ &F\1@3 t.1 }} : s.2, s.2 T;
  e.X = {{ &F\1 e.X }} : s.1, s.1 E;
}

F\1 { (e.X) = e.X }
F\1@1 { = X }
F\1@2 { s.1 = s.1 }
F\1@3 { t.1 = t.1 }

Если при прогонке функции наружу всплывает конструктор замыкания, то он выносится в «условие-льезон»:

Dup { s.X = s.X s.X }
Make { e.X = { = e.X } }

Eq {
  s.X s.X = True;
  s._ s._ = False;
}

$DRIVE Dup, Make, Eq;

F {
  1 e.X = <Eq <Dup <Make e.X>>>;
  2 e.X = <Eq <Make e.X> <Make e.X>>;
}

После оптимизации функция F примет вид

F {
  1 e.X = {{ &Make\1 e.X }} : s.1, True;
  2 e.X = {{ &Make\1 e.X }} : s.1, {{ &Make\1 e.X }} : s.2, False;
}

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

В случае размножения замыкания:

{{ &F\1 e.X }} : s.1, s.1 s.1

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

Как-то так.

[Mazdaywik]

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