Почему рекурсивный `let` делает пространство эффектным?

Я нашел это выражение при изучении функционального реактивного программирования, от "Закрепление космического утечка со стрелкой" Хай Лю и Поля Худака (страница 5):

Suppose we wish to deﬁne a function that repeats its argument indeﬁnitely:

    repeat x = x : repeat x

or, in lambdas:

    repeat = λx → x : repeat x

This requires O(n) space. But we can achieve O(1) space by writing instead:

    repeat = λx → let xs = x : xs
                  in xs

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

    r = \x -> x: r x
    r 3

    -> 3: r 3 
    -> 3: 3: 3: ........
    -> [3,3,3,......]

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

    r = \x -> let xs = x:xs in xs
    r 3

    -> let xs = 3:xs in xs
    -> xs, according to the definition above: 
    -> 3:xs, where xs = 3:xs
    -> 3:xs:xs, where xs = 3:xs

Во второй форме появляется xs и может делиться между всеми местами, которые он встречает, поэтому я предполагаю, что мы можем использовать только пробелы O(1), а не O(n). Но я не уверен, прав я или нет.

BTW: ключевое слово "shared" происходит из той же страницы 4:

Проблема заключается в том, что стандартные правила оценки по требованию не могут распознать, что функция:
f = λdt → integralC (1 + dt) (f dt) 
совпадает с:
f = λdt → let x = integralC (1 + dt) x in x
Предыдущее определение заставляет работу повторяться в рекурсивном вызове к f, тогда как в последнем случае вычисление является общим.

Ответы

Ответ 1

Легче всего понять фотографии:

Первая версия
```
repeat x = x : repeat x
```
создает цепочку конструкторов (:), заканчивающихся в thunk, который заменит себя большим количеством конструкторов по мере их появления. Таким образом, O (n) -пространство.
Вторая версия
```
repeat x = let xs = x : xs in xs
```
использует let для "связывания узла", создавая единственный конструктор (:), который ссылается на себя.

Ответ 2

Проще говоря, переменные являются общими, но функциональные приложения - нет. В

repeat x = x : repeat x

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

Но когда вы пишете

repeat x = let xs = x : xs in xs

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

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

Ответ 3

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

repeat x = x : repeat x

язык не распознает, что repeat x справа совпадает с значением, выражаемым выражением x : repeat x. Если вы пишете

repeat x = let xs = x : xs in xs

вы явно создаете структуру, которая при оценке выглядит следующим образом:

{hd: x, tl:|}
^          |
 \________/