Simply typed lambda calculus

Common card · No. 453448

The simply typed lambda calculus (⁠ λ → {\displaystyle \lambda ^{\to }} ⁠), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (⁠ → {\displaystyle \to } ⁠) that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. The term simple type is also used to refer to extensions of the simply typed lambda calculus with constructs such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems that introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The simple types, except for full recursion, are...

Read on Wikipedia