type Church a = (a -> a) -> a -> a

s :: (a -> b -> c) -> (a -> b) -> c
s x y z = x z (y z)

k :: a -> b -> a
k x y = x

succ :: Church a -> Church a
succ n f x = f (n f x)

{-
In order to convert actualSucc into a point-free combinator you need to abstract the lambdas from the inside out:
-}

succ = \n -> \f -> \x -> f (n f x)

{-
Here, we want to abstract \x -> f (n f x). This looks a lot like the definition of the s combinator.
The s combinator places the second argument as an argument to the first argument, using the s combinator
we would get something like x\ -> f x (n f x) so in order to drop the first x we can pre-compose f with k to
get \x -> k f x (n f x). This is identical to s (k f) (n f).
-}

succ = \n -> \f -> s (k f) (n f)

{-
Similarly, we see that the innermost lambda again looks like an s combinator but with an extra s preceding it.
Notice that in a simples lambda like \x -> f (g x) this is just composition. And we know that lambda evaluation
is left associative, so really, the above lambda could be \f -> (s (k f)) (n f). This now shows that the solution
is to pre-compose k with s as the first argument to a new s combinator:
-}

succ = \n -> s (s . k) n

{-
Now notice that \n -> s (s . k) n is the same as the point-free version s (s . k) and now all we need to do is
find what the combinator for composition is. Usually, the composition combinator is called b so:
-}

b :: (b -> c) -> (a -> b) -> a -> c
b f g x = f (g x)

{-
First, notice that k s simplifies to:
-}

k s = (\x y -> x) s
    = \y -> s
    = \y -> \a b c -> a c (b c)
    = \y a b c -> a c (b c)
    = \w x y z -> x z (y z)

{-
It basically just ignored the first argument and then applied the s combinator. If we then apply the s combinator
to this again we get:
-}

s (k s) = (\a b c -> a c (b c)) (k s)
    = \b c -> (k s) c (b c)
    = \b c -> (\w x y z -> x z (y z)) c (b c)
    = \b c -> \y z -> (b c) z (y z)
    = \b c -> \y z -> b c z (y z)
    = \a b c d -> a b d (c d)

{-
This may look like a mess, but the idea here was that applying s to k s brought the
argument (b c) in \a b c -> a c (b c) forward and dropped the c. If we have a way of ignoring that d argument
then this would just be \b c d -> b (c d) which is exactly the kind of lambda we need. We can do this with k.
-}

s (k s) k = (\a b c d -> a b d (c d)) k
    = \b c d -> k b d (c d)
    = \b c d -> b (c d)

{-
We can conclude that composition is:
-}

b = s (k s) k

{-
Finally, we can say that:
-}

succ = \n -> s (s . k) n
    = \n -> s (b s k) n
    = \n -> s (s (k s) k s k) n
    = s (s (k s) k s k)