How `fix f = let {x = f x} in x` is evaluated?

Question

fix f = let {x = f x} in x

Talking about let, I thought that let P = Q in R would evaluate Q -> Q' then P is replaced by Q' in R, or: R[P -> Q'].

But in fix definition the Q depends on R, how to evaluate then?

I imagine that this is about lazy evaluation. Q' becomes a thunk, but I can't reason this in my head.

As a matter of context, I'm looking at Y combinator, it should find a fixed point of a function so if I have this function, one x = 1, then fix one == 1 must hold, right?

So fix one = let {x = one x} in x, but I can't see how 1 would emerge from that.

Angeli

Answer 1

Talking about let, I thought that let P = Q in R would evaluate Q -> Q' then P is replaced by Q' in R, or: R[P -> Q'].

Morally, yes, but P is not immediately evaluated, it is evaluated when needed.

But in fix definition the Q depends on R, how to evaluate then?

Q does not depend on R, it depends on P. This makes P depend on itself, recursively. This can lead to several different outcomes. Roughly put:

• If Q can not return any part of its result before evaluating P, then P represents an infinitely recursing computation, which does not terminate. For example,

  let x = x + 1 in x     -- loops forever with no result
  -- (GHC is able to catch this specific case and raise an exception instead,
  -- but it's an irrelevant detail)
  

• If Q can instead return a part of its result before needing to evaluate P, it does so.

  let x = 2 : x in x
  -- x = 2 : .... can be generated immediately
  -- This results in the infinite list 2:2:2:2:2:.....
  
  let x = (32, 10 + fst x) in x
  -- x = (32, ...) can be generated immediately
  -- hence x = (32, 10 + fst (32, ...)) = (32, 10+32) = (32, 42)
  

I imagine that this is about lazy evaluation. Q' becomes a thunk, but I can't reason this in my head.

P is associated with a thunk. What matters is whether this thunk calls itself before returning some part of the output or not.

As a matter of context, I'm looking at Y combinator, it should find a fixed point of a function so if I have this function. one x = 1, then fix one == 1 must hold, right?

Yes.

So fix one = let x = one x in x, but I can't see why 1 would emerge from that

We can compute it like this:

fix one
 = {- definition of fix -}
let x = one x in x
 = {- definition of x -}
let x = one x in one x
 = {- definition of one -}
let x = one x in 1
 = {- x is now irrelevant -}
1

Just expand the definitions. Keep recursive definitions around in case you need them again.

Vicinage

Amazing, thank you so much,. This was equational reasoning? I need to practice that – Angeli

@Angeli Yes, that's equational reasoning. Keep in mind that GHC might not follow those steps exactly (its runtime system is rather complex, using a ton of optimizations), but it is guaranteed to lead the the same result. – Vicinage

(I was too hasty in posting my answer before seeing the ending of your post... :)) – Oliana

Q does not depend on R, it depends on P. this is still gray to me, can you explaing more about it? To me P is like a label to Q' in R – Angeli

@Angeli Consider let x = f x in g x. f x depends on x, not on g x. – Vicinage

Hmmmmm, I think I get it let x' = f x in g x''. Supposing that all x are the same, I just mark it with ' to speak of each one. Now f depends on x, x' depends on f x and x'' depends on x' and g depends on x'' is this right? – Angeli

@Angeli Yes. To be pedantic I would say that f x depends on x, not that f depends on x. You say the latter only because you know that f is applied to x, so you mention f but you are thinking of f x. – Vicinage

Oh, sure f x depends on x, my bad. The only thing that doesn't fit in my head is, where the first x (in f x) is coming from. In fix definition for example, I can't see where x is coming from. In another language I would claim that x is undefined – Angeli

@Angeli It is a recursive definition, so you use it before it's fully defined. In imperative procedural languages you can write a function def x(): if ... then use x() else ... which calls itself. In Haskell, you can do that even for non-functions (because Haskell is lazy). – Vicinage

@Vicinage oh, now make sense, thank you chi, is really hard to get this lazy evaluation in head after years using strict languages – Angeli