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.
Morally, yes, but
P
is not immediately evaluated, it is evaluated when needed.Q
does not depend onR
, it depends onP
. This makesP
depend on itself, recursively. This can lead to several different outcomes. Roughly put:If
Q
can not return any part of its result before evaluatingP
, thenP
represents an infinitely recursing computation, which does not terminate. For example,If
Q
can instead return a part of its result before needing to evaluateP
, it does so.P
is associated with a thunk. What matters is whether this thunk calls itself before returning some part of the output or not.Yes.
We can compute it like this:
Just expand the definitions. Keep recursive definitions around in case you need them again.