Inferring the types of the Combinator Birds
Combinatory logic is explained using the interesting analogy of birds living in an enchanted forest in the book To Mock a Mockingbird. In it, classical combinators are mapped to bird names (S = starling, K = kestrel, etc.). These are useful mnemonics for classical combinators.
Chris Rathman has a very useful list of all of the combinator birds, and their implementations as combinators, in the SK calculus, and in the lambda calculus. This list has been indispensible to me for understanding the relationship between combinatory logic and the lambda calculus, as well as the relationship between the Haskell semantics and types and Cat semantics and types.
I’ve just finished implementing a large number of the classical combinators with full type checking in Cat, that can be viewed here. As with any Cat program the type annotation serves only as a sanity check, the types are always inferred by the compiler. The only type signature which is clearly wrong is the W combinator, while a couple of other types have a slight bugs, but are still compatible. These bugs should be ironed out in the next major release of Cat.
In case it isn’t immediately obvious the Cat types have a trivial mapping to ML/Haskell style types as follows:
In Cat:Â
S : ( -> ((’a  -> (’b -> ‘c)) -> ((’a -> ‘b) -> (’a -> ‘c))))
K : ( -> (’a -> (’b -> ‘a)))
In Haskell
S : (a -> b -> c) -> (a -> b) -> a -> cÂ
K : (a -> b -> a)
You may notice if you look at the file, the fact that the S and K combinators are implemented using Cat’s new lambda expression notation:
define S { \a.[\b.[\c.[c b A c a A A]]] }
define K { \a.[\b.[a]] }
The “A” combinator, is the function application operation. It is the same as “apply” but only accepts unary functions. In languages like Scheme/Lisp function application is denoted by ”(f, x)” whereas in ML and Haskell function application is simply the juxtaposition of terms, such as “f x”. In C style languages function application is denoted by “f(x)”. In Cat function application is explicit: “x f apply” or “x f A”.
Sidebar: you can override “(” and “)” in order to achieve C style function application notation using Cat, you simply define “(” as “noop” and “)” as “swap A”.
This work is a major step forwards toward my current goal of Scheme to Cat translator, which should allow me to infer types for Scheme programs.
On a related note, the Cat type system is currently being discussed at Lambda-the-Ultimate.org.