flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Чистота означает «без изменения на месте», а не «без выделения памяти»

Частый вопрос: зачем чистому функциональному языку память, если в лямбда- исчислении её нет?

Лямбда-исчисление — модель на бумаге. Там нет памяти, потому что нет и времени: вычисление это переписывание символов. Как только программа идёт на настоящем процессоре, промежуточные значения надо где-то держать.

Парадокс: чистые языки выделяют памяти больше обычных. Вместо «изменить элемент списка» делается «создать новый список».

Сборщик мусора есть у всех. Lisp его изобрёл, у Haskell он есть, Coq работает на OCaml с его сборщиком. Единственное интересное исключение — Lean 4: там не сборщик, а подсчёт ссылок, память освобождается сразу, как только на значение никто не смотрит. Паузы предсказуемее, цена платится на каждой операции.

Для flang подсчёт ссылок доказуемо корректен — проверено, а не предположено: грамматика значений замкнута, вычисление строгое, пусть не рекурсивен, изменяемого состояния нет, значит цикл построить нечем. Найдена цена, которой нет в литературе: у строки в 32-байтном значении нет свободного слота под указатель на владельца (у списка есть — поле grow), то есть либо расширение до 40 байт (+25 % на каждое значение), либо особая схема для строк.

Связано: memory-per-category-is-regions, games-and-video-are-not-our-case