-- 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 beed 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
-}