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?

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.

StackExchange Computer Science Q#1816, answer score: 18