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.

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.