Simply Typed Combinatory Logic?

Question

As there is an untyped lambda calculus, and a simply-typed lambda calculus (as described, for example, in Benjamin Pierce's book Types and Programming Languages), is there a simply-typed combinatory logic?

For example, it would seem that natural types for the combinators S, K, and I would be

S : (a -> b -> c) -> (a -> b) -> a -> c
K : a -> b -> a
I : a -> a

where a, b, and c are type variables ranging over some set of types T. Now, perhaps we could get started with a single base type, Bool. Our set of types T is then Bool along with whatever types can be formed using the three patterns

(a -> b -> c) -> (a -> b) -> a -> c
a -> b -> a
a -> a

where a, b, c in T.

There would be two new constants in the language.

T : Bool
F : Bool

So, this language consists of the symbols S, K, I, T, and F, along with parentheses. It has one base type Bool, and the "function types" that can be made from the S, K, and I combinator patterns.

Can this system be made to work? For example, is there a well-typed if-then-else construction that can be formed from only S, K, I, T, F?