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 :)