Haskell Schule des Ausdrucks fix Funktion

Question

So lese ich Paul Hudak Buch "The Haskell School of Expression" und bin auf einer Übung drin stecken.

Hier geht es

Angenommen Funktion fix als

fix f = f (fix f) 

Was ist der Haupttyp ist fix definiert ist. Das weiß ich, es ist b -> b -> b

Aber ich verstehe nicht die Art, wie Fix definiert ist, wird es nicht in eine unendliche Rekursion gehen?

lassen sich auch die Rest-Funktion definiert werden als

remainder :: Integer -> Integer -> Integer 
remainder a b = if a < b then a 
       else remainder (a - b) b 

Rewrite Rest fix mit, so dass es nicht rekursiv ist.

Answer 1

Zunächst wird der Haupttyp fix ist eigentlich (b -> b) -> b (denken Sie daran, dass nur b -> (b -> b) die gleiche wie b -> b -> b ist).

In einer strengen Sprache würde eine solche Definition in unendliche Rekursion gehen, aber weil Haskell faul ist, werden die Argumente für eine Funktion nur ausgewertet, wenn sie an irgendeinem Punkt benötigt werden. Zum Beispiel können Sie factorial definieren.

-- with recursion 
factorial :: Int -> Int 
factorial n = if n == 0 then 1 else n * factorial (n-1) 

-- with `fix` 
factorial' :: Int -> Int 
factorial' = fix (\f n -> if n == 0 then 1 else n * f (n - 1)) 

dem gleichen Muster folgend, sollten Sie in der Lage sein remainder zu definieren.

Answer 2

mit ihm spielen ein wenig gibt uns

fix f   = f (fix f)           -- definition 
fix f  a = f (fix f) a           -- eta expansion 
fix f  a b = f (fix f) a b          -- eta expansion 
remainder a b = if a < b then a else remainder (a - b) b    -- definition 
-- we want remainder = fix f:          -- equation 
fix f  a b = if a < b then a else (fix f) (a - b) b    -- substitution 
     = (\g -> if a < b then a else g   (a - b) b) (fix f) -- abstraction 
    = fix (\g -> \a b -> if a < b then a else g (a - b) b) a b  -- abstraction 

so

remainder = 
    fix (\g  a b -> if a < b then a else g (a - b) b)   -- eta reduction