haskelllazy-evaluationevaluationfixpoint-combinators

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


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.


Solution

  • 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:

    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.