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 ...

Get Good Math now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.