[Haskell-cafe] Cute code [was: The C Equiv of != in Haskell miscommunication thread]

[David House]

On 29/05/07, Vincent Kraeutler <vincent at kraeutler.net> wrote:
> anyhow. if someone has a "pedestrian's guide to the fixed point
> operator" lying around, a link would be much appreciated.

Here's a paraphrased quotation from Pierce's "Types and Programming Languages":

Suppose we want to write a recursive function definition of the form h
= (body containing h) -- i.e., we want to write a definition where the
term on the right-hand side of the = uses the very function that we
are defining. The intention is that the recursive definition should be
"unrolled" at the point where it occurs; for example, the definition
of factorial would intuitively be

if n=0 then 1
else n * (if n-1=0 then 1
          else (n-1) * (if n-2=0 then 1
                        else (n-2) * ...))

This affect can be achieved using the fix combinator by first defining
g = \f. (body containing f) and then h = fix g. For example, we can
define the factorial function be

g = \fct n. if n == 0 then 1 else n * (fct (n-1))
factorial = fix g

Figure 5-2 shows what happens to the term factorial 3 during evaluation:

factorial 3
fix g 3
g (fix g) 3   --  Using fix f = f (fix f)
if 3 == 0 then 1 else 3 * (fix g 2)  -- Using the definition of g
3 * (fix g 2)
3 * (g (fix g) 2)
3 * (if 2 == 0 then 1 else 2 * (fix g 1))
3 * (2 * (fix g 1))
3 * (2 * (g (fix g) 1))
3 * (2 * (if 1 == 0 then 1 else 1 * (fix g 0)))
3 * (2 * (1 * (fix g 0))
3 * (2 * (1 * (g (fix g) 0)))
3 * (2 * (1 * (if 0 == 0 then 1 else 0 * (fix g -1))))
3 * (2 * (1 * 1)))
6

The key fact that makes this calculation work is that fix g n
evaluates to g (fix g) n. That is, fix g is a kind of
"self-replicator" that, when applied to an argument, supplies _itself_
and n as arguments to g. Wherever the first argument appears in the
body of g, we will get another copy of fix g, which, when applied to
an argument, will again pass itself and that argument to g, etc. Each
time we make a recursive call using fix g, we unroll one more copy of
the body of g and equip it with new copies of fix g that are ready to
do the unrolling again.

(Adapted from pp59-60, Types and Programming Languages, Benjamin C. Pierce.)

-- 
-David House, dmhouse at gmail.com