Why does the recursive `let` make space spectacular?

Question

I found this expression while studying functional reactive programming, from "Fixing a Space Leak with an Arrow" by Hai Liu and Paul Hoodak (page 5):

Suppose we wish to define a function that repeats its argument indefinitely: 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 

The difference here seems small, but it extremely suggests the effectiveness of space. Why and how is this happening? The best guess I made was to evaluate them manually:

  r = \x -> x: rx r 3 -> 3: r 3 -> 3: 3: 3: ........ -> [3,3,3,......] 

As above, we will need to create endless new thunks for this recursion. Then I try to evaluate the second:

  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 

In the second form, xs appears and can be divided between all the places it encounters, so I assume that we can use only the spaces O(1) , not O(n) . But I'm not sure if I'm right or not.

BTW: the keyword "shared" comes from the same page 4:

The problem is that standard on-demand evaluation rules cannot recognize that a function:

 f = λdt → integralC (1 + dt) (f dt) 

matches with:

 f = λdt → let x = integralC (1 + dt) x in x 

The previous definition makes the job repeat in a recursive call to f, whereas in the latter case, the calculation is general.

Answer 1

The easiest way to understand photos:

• First version

   repeat x = x : repeat x 

  creates a chain of constructors (:) ending in thunk, which will replace itself with a large number of constructors as they appear. Thus, the O (n) -space.

  

• Second version

   repeat x = let xs = x : xs in xs 

  uses let to "bind the node", creating a single constructor (:) that references itself.

  

Answer 2

Simply put, variables are common, but functional applications are not. AT

 repeat x = x : repeat x 

it is a coincidence (in terms of language) that a (co) recursive call is repeated with the same argument. This way, without additional optimization (called static argument conversion), the function will be called again and again.

But when you write

 repeat x = let xs = x : xs in xs 

no recursive function calls. You take x and plot the cyclic value of xs using it. All sharing is explicit.

If you want to more formally understand this, you need to familiarize yourself with the semantics of lazy evaluation, for example, Natural semantics for lazy evaluation .

Answer 3

Your intuition regarding xs is correct. Repeat the author’s pattern in terms of repetition, not the whole, when you write:

 repeat x = x : repeat x 

the language does not recognize that repeat x on the right matches the value expressed by the expression x : repeat x . If you write

 repeat x = let xs = x : xs in xs 

you explicitly create a structure that when evaluated looks like this:

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