Type Systems #3: Simply Typed Lambda Calculus

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

Okay so in previous posts we explored why we probably want to have types in our lambda calculus. The simply typed lambda calculus (STLC) gives the most basic type system we can slap on top of the untyped lambda calculus, and it solves both problems we discussed before: It prevents nonsensical programs like add true horse, and it prevents us from writing down terms that might not terminate, like (λx. x x) (λx. x x).

The type system itself is really really simple — we just need two things.

Base Types

First, we define a list of primitive types that our language supports. For example Int, Boolean, and String.

Our types also need inhabitants, so we add a few so-called “typing judgements” as well: For example, we define true and false to be Boolean; 0, 1, 2, ... to be Int, and so on.

Unlike in untyped lambda calculus, where everything is lambdas all the way down, our symbols true and false here are atomic, definition-less tokens that have no further structure — they just are. The list of base types and values are god-given if you will, you get to choose what you want your language to support.

One problem we run into here is that for example, we can never write down a function definition for if… I mean how would you do it? if = λbool. λthen. λelse. ??? — what goes in the body? We can’t pattern match on bool because we don’t have pattern matching in lambda calculus. We can’t check for equality either.

The solution is to treat if as a primitive as well, it’s a god-given function that just exists, and it works on booleans. Or rather, it’s not really a function is it, it’s more like… a syntactical construct.

We could say that the syntax is if b then x else y, and it reduces to x or y depending what b is.

(We could say that in addition to alpha/eta-conversion and beta-reduction, we add an extension to our language called if-reduction; this implies that STLC isn’t a single language per se, rather it’s whatever you want it to be.)

For our integers, we add a bunch more primitives like add, subtract, multiply, and so on, too.

Function Types

In the simply typed lambda calculus, every function parameter must be annotated with a type. Here’s an example not function operating on booleans:

not = λb: Boolean. if b then false else true

The syntax for typing should be familiar from typescript.

The type of not would naturally be Boolean → Boolean, meaning it takes a boolean and returns a boolean.

Boolean → Boolean is not part of our base types, but the “function type” rule allows us to build more complex types from base types, using arrows.

And that’s it! Given just these two extra bits, we can now typecheck any lambda term. Have a few more examples and decide whether they typecheck, and if so, what their type is.

Question 1: 
λx: Int. add x 1

Solution: Int → Int.

Question 2: 
λx: Boolean. add x 1

Solution: Does not typecheck, assuming that add expects two Ints.

Question 3: 
λx: Int. (λy: Int. add x y)

Solution: Int → (Int → Int).

Subtle syntactical point: We usually write this type as Int → Int → Int, since → is right associative. (This also means in particular that (Int → Int) → Int is different from Int → Int → Int.)

Question 4: 
(λf: (Int → Int). f 3) (λx: Int. add x 4)

Solution: 7, which is of type Int.

Explanation: The left function has type (Int → Int) → Int, and we feed an Int → Int into it. The result type of the left function is Int, so the whole term typechecks and has type Int.

We got types, nice!

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