Lambda Calculus with Elementary Type Theory


The Lambda Calculus  that we have been looking at in Lambda Calculus and Combinatory Logic  has been the untyped Lambda Calculus. It is plenty interesting for sure, being able to provide a foundation for computability, programming languages, and many areas of linguistics and philosophy. But untyped Lambda calculus also has some features to be wary of; for example, some reduction sequences go on forever and never reduce the expression to a normal form. We wouldn't really want that happening unintentionally with an ordinary computer program running on an ordinary computer. Also Russell's paradox (considering 'the set of all sets which are not members of themselves' and asking whether that set is a member of itself— if it is, it isn't and if it isn't, it is) can be mimicked in the untyped Lambda Calculus, as can many other paradoxes and inconsistencies.

Church himself, the author of Lambda Calculus, presented a typed Lambda Calculus in his 1940 paper A Formulation of the Simple Theory of Types and this is a route we are going to follow. Simply Typed Lambda Calculus (STLC), at a basic conceptual level, is not that hard to understand (although type theory can ascend to the clouds and beyond).