Ex 9.9 in Paul Hudak's book
Antony Courtney
antony@apocalypse.org
Sun, 31 Mar 2002 16:23:10 -0500
This is a multi-part message in MIME format.
--------------050106010900040700080907
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Ludovic Kuty wrote:
> The exercise is short.
>
> First, he defines a "fix" function:
> fix f = f (fix f)
> Which has the type (a -> a) -> a
>
> Then the function "remainder":
> remainder :: Integer -> Integer -> Integer
> remainder a b = if a < b then a else remainder (a - b) b
>
> The function fix, has far as i understand the matter, has no base case.
> So if someone wants to evaluate it, it will indefinitely apply the function f
> to itself, leading the hugs interpreter to its end.
As a hint (but not a solution), attached are my own notes from when I
was puzzling through fixed points myself a few years ago. This is a
literate Haskell script that you can load into hugs and run. Note that
my 'y' is the same as your 'fix'. I use y to derive a factorial
function (fact) in terms of y that does terminate.
("Malkovich" is an obscure reference to the scene in the film "Being
John Malkovich" where Malkovich goes through his own portal... :-))
-antony
--
Antony Courtney
Grad. Student, Dept. of Computer Science, Yale University
antony@apocalypse.org http://www.apocalypse.org/pub/u/antony
--------------050106010900040700080907
Content-Type: text/plain;
name="Ynotes.lhs"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
filename="Ynotes.lhs"
A definition of the Y combinator in Haskell.
Valery calls this the "stupid" definition of the Y combinator since
it uses Haskell's recursion.
Of course, if it's the "stupid" definition, and it's not immediately
obvious to me why it works, well....there's only one conclusion.
Thankfully, however, I have other redeeming qualities. :-)
Here was Valery's original formulation:
y = \f -> let x = f x in x
But, of course, Paul pointed out that this definition of y
can be simplified to:
>
> y f = f (y f)
Now let's define a generator to test out y:
> factGen = \f -> \n -> if n==0 then 1 else n * f (n-1)
> fact = y factGen
Sure enough, if we run this under Hugs, it works:
Main> fact 3
6
Main>
Wow. mind-blowing.
Unfortunately, I don't have "stepper" for Haskell, so I better walk
through this myself to figure out what's going on.
First, some types:
y :: (a -> a) -> a
factGen :: (Integer -> Integer) -> Integer -> Integer
(Note, though, that since -> associates to the right, this is the same as:
(Integer -> Integer) -> (Integer -> Integer)
fact :: Integer -> Integer
which all makes sense.
Now let's trace through an evaluation like:
fact 3
==> (y factGen) 3
==> ((\f -> let x = f x in x) factGen) 3
==> (let x = factGen x in x) 3
(OK, I think this is the crucial step:
==> (let x = factGen x in (factGen x)) 3
==> (let x = factGen x in ((\f -> \n -> if n==0 then 1 else n * f (n-1)) x)) 3
==> (let x = factGen x in (\n -> if n==0 then 1 else n * x (n-1))) 3
==> let x = factGen x in (if 3==0 then 1 else 3 * x (3-1))
==> let x = factGen x in (3 * x (3-1))
==> let x = factGen x in (3 * x 2)
==> let x = factGen x in (3 * (factGen x) 2)
==> let x = factGen x in (3 * (factGen x) 2)
The above was with the original definition of y.
Of course, this should be easier to follow with Paul's definition:
fact 3
==> (y factGen) 3
==> (factGen (y factGen)) 3
==> ((\f -> \n -> if n==0 then 1 else n * f (n-1)) (y factGen)) 3
==> if 3==0 then 1 else 3 * ((y factGen) 2)
==> 3 * ((y factGen) 2)
which obviously works.
Ok, so what's going is this:
x is bound to (factGen x).
(factGen x) unfolds to: ((\f -> \n -> if n==0 then 1 else n * f (n-1)) x)
which reduces to: \n -> if n==0 then 1 else n * x (n-1)
but the "x" in the above will itself just unfold to (factGen x), yielding
yet another recursive call!
Note, too, that x has "type" Integer->Integer, although it is really a
name for a *computation* that produces such a function when evaluated.
mind-blowing.
Another way to think of it: If f is Malkovich, then:
x
<--> (Malkovich x)
<--> (Malkovich (Malkovich x))
<--> (Malkovich (Malkovich (Malkovich x)))
<--> (Malkovich (Malkovich (Malkovich (Malkovich ... (Malkovich x)))))
i.e. x unfolds to as many applications of "Malkovich" as we need to
eventually reach Malkovich's fixed point.
Of course, I used <--> just to indicate equivalence, not an actual
reduction sequence. In normal order evaluation, we only unfold x when
it's value is needed. But we'll keep doing that until we hit a fixed
point (or diverge).
--------------050106010900040700080907--