Ex 9.9 in Paul Hudak's book

[Antony Courtney]

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