Brandon.Si(mmons)

code / art / projects

Do Applicative Functors Generalize the S & K Combinators?

If the title hasn’t scared you off yet, here’s the story: I was hacking on someone else’s code on the plane and trying to wrap my head around some Applicative class code; in particular the code in question used the Applicative instance for ((->) a) i.e. functions. This turned my brain to cream-of-wheat and I had to take a break.

If you aren’t familiar with Applicative Functors, they are somewhere in between the familiar and simple Functor class and the Monad class; an abstraction for function application with a context. Check out here for more. Away from the computer I got out a pad of paper and went about trying to figure out how the <*> method was defined over functions. Here are the types:

The polymorphic type:

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

Substitute (x -> ...) for f to get the type for the functions instance:

(<*>) :: (x -> a -> b) -> (x -> a) -> (x -> b)

You can try defining the instance from the type definition; there seems to be only one sensical way. When I did it I was struck by something: the definition for the function above is the same as the S combinator in the SKI combinator calculus!

At that point I started looking for other connections to combinatory logic, and quickly noticed that the class method pure was essentially the K combinator!. Here is the actual instance definition:

instance Applicative ((->) a) where
            pure = const
            (< *>) f g x = f x (g x)

For those not familiar, the SK(I) Combinator Calculus is a formal system for modelling computation, much like the lambda calculus; one can express any computable function using only the three (actually only S and K are necessary) symbols and parentheses. I’ve written about and implemented the combinator calculus, and you can read more on the wikipedia page.

Exploring the Connection

It’s pretty astounding to me that the only two methods required to define an Applicative instance turn out to be sufficient (the details of haskell’s type system aside) to define a complete combinator base, capable of expressing any computable function.

At first I wondered whether this connection was the brainchild of some clever haskeller who defined the (->) instance, and therefore somewhat artificial. But it turns out that the definitions for pure and (< *>) fall out quit naturally from the type definitions. So naturally in fact that we can use djinn to automatically derive their definitions!:

Djinn> ? (<*>) :: (x -> a -> b) -> (x -> a) -> (x -> b) 
(<*>) :: (x -> a -> b) -> (x -> a) -> x -> b 
(<*>) a b c = a c (b c) 
Djinn> ? pure :: a -> (x -> a) 
pure :: a -> x -> a 
pure a _ = a

Observe how the function definitions above could have been pulled right from an explanation of the S and K combinators.

Now let’s play with this in GHCi. We’ll first define our S and K combinators as the Applicative methods (giving type hints to keep the typechecker happy), then define the I combinator in terms of S and K, then we’ll express a Church numeral:

Prelude> :m + Control.Applicative  
Prelude Control.Applicative> let s = (<*>) :: (x -> b -> c) -> (x -> b) -> (x -> c) 
Prelude Control.Applicative> let k = pure :: a -> (x -> a) 
Prelude Control.Applicative> let i = s k k 
Prelude Control.Applicative> let two = s (s (k s) k) i 
Prelude Control.Applicative> two ('x':) [] 
"xx"

In the last last line above we sort of “render” the church numeral by applying it to a function and value that will construct a list; remember that church numerals represent integers as n-fold function composition; in the lambda calculus the numerical represenatations are more straightforward: two = \f x-> f (f x), but the idea is the same.

Conclusion

It makes a lot of sense that a general type class meant to aid programming in an “applicative” style would have some similarity with the combinator calculus (in which even data is function application), but I thought it was pretty exciting to see such a fundamental computer science concept seemingly emerge naturally out of a library designed to solve a very high-level problem.

I have no idea whether these observations are novel or old and obvious, but would love to hear from anyone who has any thoughts on this.

EDIT: After taking a closer look at Conor McBride and Ross Paterson’s paper on Applicative Functor’s, I see now that he labels his ((->) a) instance methods with “S” and “K”, but does not explore the subject further. So I’m leaning towards obvious. Thanks for reading :)

Comments