The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () 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 extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which 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 still considered simple because the Church encodings of such structures can be done using only and suitable type variables, while polymorphism and dependency cannot. In this article, the symbols and are used to range over types. Informally, the function type refers to the type of functions that, given an input of type , produce an output of type . By convention, associates to the right: is read as . To define the types, a set of base types, , must first be defined. These are sometimes called atomic types or type constants. With this fixed, the syntax of types is: For example, , generates an infinite set of types starting with A set of term constants is also fixed for the base types. For example, it might assumed that a base type , and the term constants could be the natural numbers. In the original presentation, Church used only two base types: for "the type of propositions" and for "the type of individuals". The type has no term constants, whereas has one term constant. Frequently the calculus with only one base type, usually , is considered. The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. The term denotes that the variable is of type . The term syntax, in BNF, is then: where is a term constant.