6.1 Functional programming
Lambda calculi are prototype programming languages. Just as with imperative programming languages, some of which are untyped (machine code, assembler, Basic) and some typed (Algol-68, Pascal), systems of lambda calculi exist in untyped and typed versions. There are also other differences in the various lambda calculi. The one introduced in Church (1936) is the untyped λI-calculus in which an abstraction λx.M is only allowed if x occurs among the free variables of M. Nowadays, ‘lambda calculus’ refers to the λK-calculus developed under the influence of Curry, in which λx.M is allowed even if x does not occur in M. This book treats the typed versions of the λK-calculus. Of these, the most elementary are ...