haskelllambdalambda-calculuscombinatorscombinatory-logic

What does this combinator do: s (s k)


I now understand the type signature of s (s k):

s (s k)  :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

And I can create examples that work without error in the Haskell WinGHCi tool:

Example:

s (s k) (\g -> 2) (\x -> 3)

returns 2.

Example:

s (s k) (\g -> g 3) successor

returns 4.

where successor is defined as so:

successor = (\x -> x + 1)

Nonetheless, I still don't have an intuitive feel for what s (s k) does.

The combinator s (s k) takes any two functions f and g. What does s (s k) do with f and g? Would you give me the big picture on what s (s k) does please?


Solution

  • Alright, let's look at what S (S K) means. I'm going to use these definitions:

    S = \x y z -> x z (y z)
    K = \x y   -> x
    
    S (S K) = (\x y z -> x z (y z)) ((\x y z -> x z (y z)) (\a b -> a)) -- rename bound variables in K
            = (\x y z -> x z (y z)) (\y z -> (\a b -> a) z (y z)) -- apply S to K
            = (\x y z -> x z (y z)) (\y z -> (\b -> z) (y z)) -- apply K to z
            = (\x y z -> x z (y z)) (\y z -> z) -- apply (\_ -> z) to (y z)
            = (\x y z -> x z (y z)) (\a b -> b) -- rename bound variables
            = (\y z -> (\a b -> b) z (y z)) -- apply S to (\a b -> b)
            = (\y z -> (\b -> b) (y z)) -- apply (\a b -> b) to z
            = (\y z -> y z) -- apply id to (y z)
    

    As you can see, it's just ($) with more specific type.