Type Systems #4: STLC is not enough!

(This is part 4 in a series on type systems. You can find part 3 here .)

I have brought a fresh lambda term for you, but I forgot to type it! What do you think its type should be?

apply = λf. (λx. f x)

Not so easy, is it. It feels like applys type should depend on whatever function you pass in.. if you pass in plusOne, then apply plusOne should be a function Int → Int. But if you pass in not, then apply not should be a function Boolean → Boolean.

Or in other words, we would really like apply to be generic.

But if we recall the rules of simply typed lambda calculus, then we see that we have no way to express this genericity. Function parameters in STLC must be of a type that’s allowed by the language, and that’s either a base type (we chose Int, Boolean, String previously), or a function type like Int → Int.

That is to say, STLC will allow us to define concrete instances of apply, like these:

applyInt = λf: (Int → Int). λx: Int. f x
applyBool = λf: (Boolean → Boolean). λx: Boolean. f x

But we can’t define a generic apply that works for all types. This is the hard limit of STLC, and we will need to move to a more powerful type system to express these kinds of functions.

(This is part 4 in a series on type systems. You can find part 5 here .)