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?

Answer 1

Quick note, I allow parametric polymorphism (System F) in this system so that S, K and I can work over all types.

Notice that without pattern matching, we can't write an if no matter what we do. We have absolutely no operations on booleans. There is no way to distinguish True from False. Instead try

true : a -> a -> a
true = \t -> \f -> t

false : a -> a -> a
false = \t -> \f -> f

Let's let Bool = a -> a -> a for clarity.

 if : Bool -> a -> a -> a
 if = \bool -> \a -> \b -> bool a b

Now it's just a matter of compiling some lambda calculus expressions to combinators, which is pretty trivial.

if : Bool -> a -> a -> a -- Or just Bool -> Bool
if    = I

true : a -> a -> a
true  = K

false : a -> a -> a
false = K I