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?

  • $\begingroup$ 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. $\endgroup$
    – Petr
    Dec 11, 2012 at 10:14

1 Answer 1


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.

  • $\begingroup$ I never thought of the $\mathbf{S}$ combinator as acting over a Monad! Is that so? $\endgroup$ May 13, 2012 at 10:27
  • $\begingroup$ Actually, I've been pointed out that $\mathbf{S}$ corresponds to the <*> operator of Applicative Functors, and pure the $\mathbf{K}$. $\endgroup$ May 13, 2012 at 10:41
  • $\begingroup$ $\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$. $\endgroup$ May 13, 2012 at 14:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.