# Is there a typed SKI calculus?

Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the simply typed lambda calculus. Does such thing exist? Where could one find information about it?

• You might be interested in The Reader Monad and Abstraction Elimination in The Monad.Reader, Issue 17. The Reader monad (or more precisely its applicative functor) is closely related to typed SKI. – Petr Dec 11 '12 at 10:14

The expressive completeness of the typed combinators compared to the simply typed lambda calculus has been demonstrated. For each untyped combinator, one needs a whole family of typed combinators. For example, one has

• $\mathbf{I}_{\alpha\to\alpha}$
• $\mathbf{K}_{\alpha\to(\beta\to\alpha)}$
• $\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\to\gamma))}$

for all combinations of simple types $\alpha,\beta$ and $\gamma$.

Alternatively, just think of the types as type schemes (or polymorphic types) and enter them into Haskell and voila: combinators.

• I never thought of the $\mathbf{S}$ combinator as acting over a Monad! Is that so? – Hugo Sereno Ferreira May 13 '12 at 10:27
• Actually, I've been pointed out that $\mathbf{S}$ corresponds to the <*> operator of Applicative Functors, and pure the $\mathbf{K}$. – Hugo Sereno Ferreira May 13 '12 at 10:41
• $\mathbf{S}$ is quite fundamental, so it could correspond to many things. $\mathbf{S}$ has the same type as the monad function $ap$ for functor $\Lambda X.\alpha\to X$. – Dave Clarke May 13 '12 at 14:40