Tue May 11 08:50:46 EDT 2010

S K combinators and the Reader monad

The S and K combinators form a complete set of combinators that can
encode all lambda terms.  The proof consists of a mechanised
transformation T explained in [1].  The trick is in the process of
abstraction elimination in rules 5 and 6.

  5. T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)
  6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

Abstractions provide a means to access values passed in by
applications in "outer shells" of a lambda term using their name.

The S combinator works the other way around, it can be interpreted to
operate on binary trees that correspond to applications, propagating
values to branches of a binary tree.  I.e. the S combinator passes
some values "under water".

Starting from lambda terms, this binary tree is created by the T
transform, where each application creates a fork point.  Rule 5 makes
sure that each abstraction is directly followed by an application, and
rule 6 eliminates the abstraction by representing it as an S

Short: all abstractions can be represented by passing values down
branches of a binary expression tree.

From this perspective it is not surprising that S and K pop up as
(<*>) and return from the Reader (environment) monad.

newtype Reader e a = Reader { runReader :: (e -> a) }

instance Monad (Reader e) where
    return a         = Reader $ \e -> a
    (Reader r) >>= f = Reader $ \e -> (runReader $ f (r e)) e

Compare these to S and K.

The K combinator is a non-tagged version of Reader's return.

k :: a -> e -> a
k x e = x

The S combinator is a non-tagged version of Reader's (<*>)

s :: (e -> a -> b) -> (e -> a) -> e -> b
s x y e = (x e) (y e)

(<*>) :: (Applicative f) => f (a -> b) -> f a -> f b

[1] http://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis
[2] http://en.wikipedia.org/wiki/SKI_combinator_calculus