yy.hs

yy.hs

{- |
REFERENCES:
https://gist.github.com/lukechampine/a3956a840c603878fd9f
https://rosettacode.org/wiki/Y_combinator#Haskell
https://mvanier.livejournal.com/2897.html

GOAL: Implement recursion in languages which do not support **Explicit recursion**
      Do so in an intuitive way

PREREQUISITES:
- Know what lambda calculus is
- Know Basic Haskell

TERMS USED:
- Explicit recursion:
  Calls the same function in its own body.
  E.g.
    f a = f (f a)

  f has explicit recursion since it is called in it's function body

- Static typing:
  Compile time types are checked

- Dynamic typing:
  Run time types are checked

- Strong typing:
  Every value mapped to a single type

- Weak typing:
  Every value can be mapped to multiple types

- Combinator:
  Lambda expression with no free variables.
  E.g
  Valid:
    \x -> x
    \x -> \y -> x
  Invalid:
    \x -> x y (y is unbound)
    \x -> x 1 (1 is unbound)

- Fixed point of a function:
  A value which maps to itself:
  f x = x

- Fixed point combinator:
  Higher-order function: returns a fixpoint of its argument function.
  fix f = x
        = f x
        = f (fix f)
-}

module Main where


type Natural = Integer

-- | Recursive definition
factorial :: Natural -> Natural
factorial n = if n == 0 then 1
              else n * factorial (n - 1)

-- | Removing factorial call in body to a function parameter
-- since we want to support languages without explicit recursion
-- here, we also note that the f we pass in has to be a factorial function!
almost_factorial :: (Natural -> Natural) -> Natural -> Natural
almost_factorial f n = if n == 0 then 1
                       else n * f (n - 1)

{- |
Let's examine how almost_factorial expands:
almost_factorial f 10 = 10 * f (10 - 1)
                      = 10 * (almost_factorial f (10 - 1))                  # 1) If we let f = almost_factorial f
                      = 10 * 9 * (almost_factorial f (9 - 1))
                      ...
                      = 10 * 9 * ... * 2 * 1 * (almost_factorial f (1 - 1))
                      = 10 * 9 * ... * 2 * 1 * (almost_factorial f 0)       # 2) Here f is ignored, since we have reached 0
                      = 10!

From the above expansion we can make some observations:

1) Since we can let f = almost_factorial f and get a solution,
   This shows that f is the fixpoint of almost_factorial.
   As such, we need a function that plugs this definition of f in, giving us a factorial function

2) As long as a function terminates with some value, we can make use of its fixpoint
-}

-- | Let's define such a function which 1 requires
-- Note that f can terminate, although fixpoint f can expand indefinitely,
-- only if n converges with succeeding applications and f terminates at some n.
--
-- Also note
-- In: f (fixpoint f) n
-- (fixpoint f) only becomes evaluated if necessary
-- , due to lazy evaluation (arguments of a function are not evaluated until needed)
fixpoint :: ((Natural -> Natural) -> (Natural -> Natural)) -> (Natural) -> (Natural)
fixpoint f = f (fixpoint f)

-- | We have an issue however! fixpoint still requires explicit recursion!
-- What can we do?

-- | We go back to the original function and change the shape of the arguments
-- That way we can simply pass in almost_factorial to itself, without any sort of explicit recursion
--
-- almost_factorial' :: (Natural -> Natural) -> Natural -> Natural
-- almost_factorial' f n = if n == 0 then 1
--                         else n * (f f) (n - 1) -- we added another f here
--
-- But it doesn't type check...
--
-- What exactly is the type of f?
-- f is the same type as almost_factorial'
-- f :: a -> a
--
-- for (f f) to typecheck, a ~ (a -> a).
--
-- How do we declare such a type?
--
-- Let's attempt to create such an equivalence:
newtype Mu a = Roll { unRoll :: Mu a -> a }

-- | With this newtype we attempt to redeclare almost_factorial'
almost_factorial' :: Mu (Natural -> Natural) -> Natural -> Natural
almost_factorial' f n = if n == 0 then 1
                        else n * g (n - 1) -- we added another f here
  where g = unRoll f f

-- | Parameterizing "g" and renaming f as self, we get
almost_factorial'' :: Mu (Natural -> Natural) -> Natural -> Natural
almost_factorial'' self = (\g n -> if n == 0 then 1
                                 else n * g (n - 1)) -- we added another f here
                          (unRoll self self)

fix :: (a -> a) -> a
fix = g <*> (Roll . g)
  where
    g = (. (>>= id) unRoll)

-- | Somehow this returns us our factorial??
factorial'' :: Natural -> Natural
factorial'' = fixpoint almost_factorial

main :: IO ()
main = print $ factorial'' 5