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.
Talking about let, I thought that let
P = Q in R
would evaluateQ -> Q'
thenP
is replaced byQ'
inR
, or:R[P -> Q']
.
Morally, yes, but P
is not immediately evaluated, it is evaluated when needed.
But in fix definition the
Q
depends onR
, 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
, thenfix one == 1
must hold, right?
Yes.
So
fix one = let x = one x in x
, but I can't see why1
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.