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