Good Math

Playing to Type

When Church designed typed λ calculus, his goal was to build a model that showed that λ calculus was consistent. What he was worried about was a Cantor-esque self-reference problem. In order to avoid that, he created a way of partitioning values into groups called types and then used that idea of types to constrain the language of λ calculus so that you couldn’t write an expression that did something inconsistent.

The main thing that typed λ calculus adds to the mix is a concept called base types. In a typed λ calculus, you have some universe of atomic values that you can manipulate. Those values are partitioned into a collection of distinct non-overlapping groups called the base types. Base types are usually named by single ...