BEGIN 16_11_09_FixPointOperator.lhs

RECURSION VIA A FIX-POINT OPERATOR
==================================

Given a let-expression of the form:

    let x = <e1> in <e2>

if the expression <e1> does NOT contain free occurrences of the
variable x, then the preceding expression is sugar for:

     (\ x -> <e2> ) <e1>

For example, "let f = (\ z -> z + 3) in (f 2)" can be first
de-sugared into "(\ f -> (f 2))(\ z -> z + 3)", and the latter
expression can be evaluated using call-by-value or call-by-name
strategy.

When the let-binding in the let-expression is recursive:

     let f = <e1> in <e2>

i.e., when there are free occurrences of f in <e1>, we proceed 
differently. (I use "f" instead of "x" to suggest that the
let-binding defines a function, i.e., a higher-order value.)
We define the so-called fix-point operator as follows:

> fix :: (a -> a) -> a
> fix f = f (fix f)

We then transform the let-expression into:

     let f = fix (\ f -> <e1>) in <e2>
          
Note that, in the resulting let-expression, there are NO free
occurrences of f in "fix (\ f -> <e1>)". We de-sugar the
resulting let-expression by writing:

     (\ f -> <e2> ) (fix (\ f -> <e1>))

=================================

BEGIN EXAMPLE:

The following is a well-formed expression in Haskell:

> e = 
>     (let f = (\ x -> if x == 0 then 1 else x * f (x-1))
>      in  (f 3))

The let-binding in the expression e is recursive, because "f" appears
on both sides of "=" in the binding. So, we first transform e so that
its let-binding is not recursive -- we call e1 the resulting expression:

> e1 = 
>     (let f = fix (\ f -> (\ x -> if x == 0 then 1 else x * f (x-1)))
>      in  (f 3))

We finally de-sugar the let-binding in e1 to obtain e2:

> e2 =
>     (\ f -> (f 3)) (fix (\ f -> (\ x -> if x == 0 then 1 else x * f (x-1))))

You should convince yourself that e, e1, and e2 are all equivalent.

END EXAMPLE

==================================

BEGIN EXERCISE

Define 'mySucc' by restricting the library 'succ' to have type Int -> Int:

> mySucc :: Int -> Int
> mySucc = succ

The definition of 'foo' type-checks (why?):

> foo :: Int
> foo = (fix mySucc)

But if you try to print 'foo', you get back the error message:

    ERROR - Control stack overflow

Explain the reason for this behavior.

END EXERCISE

END 16_11_09_FixPointOperator.lhs