# 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?

– Petr
Dec 11, 2012 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? May 13, 2012 at 10:27
• Actually, I've been pointed out that $\mathbf{S}$ corresponds to the <*> operator of Applicative Functors, and pure the $\mathbf{K}$. May 13, 2012 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$. May 13, 2012 at 14:40