-- Recursive definitions in lambda-calculus
-- Recursion combinator Y

-- The polymorphic Mu type is a strategy to bypass the Haskell type
-- system to be able to define the Y combinator adapted from:
-- https://mail.haskell.org/pipermail/haskell/2006-September/018497.html
newtype Mu a = Id (Mu a -> (a -> a))
idd (Id x) = x

-- Defining factorial in pure lambda calculus

-- This expression (call it f) takes a function (call it g) and
-- returns a function that computes the factorial of a number.

f = \g -> \n -> if n == 0
                then 1
                else n * (g (n - 1))

-- What can we apply it to, to get the factorial function?

-- (f f) is not well defined: type of f is (Z->Z)->(Z->Z) 

-- (f i) is well defined:  it returns n * (n-1) (for n>0) but it
-- does not return the desired factorial function, e.g.:

i = \x->x

{--To test it:

((f i) 5)

-}

-- We want to find an expression x, such that (f x) is the factorial
-- function, and x behaves as factorial itself---notice that g itself
-- in the construction above is supposed to compute the factorial
-- function---, that is, we want to solve the fixpoint equation:

--                             (f x) = x


--- In the factorial example, the following lambda-expression does the
--- job:

x =     (\x -> (\g -> \n -> if n == 0
                            then 1
                            else n * (g (n - 1))) ((idd x) x))
    (Id (\x -> (\g -> \n -> if n == 0
                            then 1
                            else n * (g (n - 1))) ((idd x) x)))

{-- Test it with:

(f x) 5

x 5

(f (f x)) 5

--}

-- Such x can be defined in terms of the recursive function f as follows:

--                            x = y f

-- where y is the following recursion combinator (in normal order)

---the type of y is ((Z->Z->(Z->Z))->(Z->Z)
y :: ((t -> t) -> t -> t) -> t -> t

y = \f ->     (\x -> f ((idd x) x))
          (Id (\x -> f ((idd x) x)))

x' = y f

{-- Test it with:

(f x') 5

x' 5

-- notice that (y f) = (f (y f)) by the construction above.

(f (y f)) 5

(y f) 5

--}


-- thus, here is the "pure" lambda-calculus combinator computing factorial:
-- (assuming that lambda calculus has been extended with 0, 1, -, *, ==, if)

factorial = (\f ->     (\x -> f ((idd x) x))
                   (Id (\x -> f ((idd x) x))))
            (\g -> \n -> if n == 0
                         then 1
                         else n * (g (n - 1)))

{-- Test it with:

factorial 6

--}

-- Fortunately, in Haskell, we can more easily define recursive functions:

fact :: Integer -> Integer
fact 0 = 1
fact n = n * fact (n-1)

{-- Test it with:

fact 6

fact 100

-}