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.[1]

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

That is, variable reference, abstractions, application, and constant. A variable reference is bound if it is inside of an abstraction binding . A term is closed if there are no unbound variables.

In comparison, the syntax of untyped lambda calculus has no such typing or term constants:

Whereas in typed lambda calculus every abstraction (i.e. function) must specify the type of its argument.

Typing rules

To define the set of well-typed lambda terms of a given type, one defines a typing relation between terms and types. First, one introduces typing contexts or typing environments , which are sets of typing assumptions. A typing assumption has the form , meaning has type .

The typing relation indicates that is a term of type in context . In this case is said to be well-typed (having type ). Instances of the typing relation are called typing judgements. The validity of a typing judgement is shown by providing a typing derivation, constructed using typing rules (wherein the premises above the line allow us to derive the conclusion below the line). Simply-typed lambda calculus uses these rules:

(1) (2)
(3) (4)

In words,

  1. If has type in the context, then has type .
  2. Term constants have the appropriate base types.
  3. If, in a certain context with having type , has type , then, in the same context without , has type .
  4. If, in a certain context, has type , and has type , then has type .

Examples of closed terms, i.e. terms typable in the empty context, are:

These are the typed lambda calculus representations of the basic combinators of combinatory logic.

Each type is assigned an order, a number . For base types, ; for function types, . That is, the order of a type measures the depth of the most left-nested arrow. Hence:


Intrinsic vs. extrinsic interpretations

Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, variously called intrinsic vs. extrinsic, ontological vs. semantical, or Church-style vs. Curry-style.[1][3][4] An intrinsic semantics only assigns meaning to well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. For example, the identity term on integers and the identity term on booleans may mean different things. (The classic intended interpretations are the identity function on integers and the identity function on boolean values.) In contrast, an extrinsic semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language. In this view, and mean the same thing (i.e., the same thing as ).

The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise. It is possible to define an extrinsic semantics on annotated terms simply by ignoring the types (i.e., through type erasure), as it is possible to give an intrinsic semantics on unannotated terms when the types can be deduced from context (i.e., through type inference). The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language. Most of the different semantic interpretations discussed below can be seen through either an intrinsic or extrinsic perspective.

Equational theory

The simply typed lambda calculus has the same equational theory of βη-equivalence as untyped lambda calculus, but subject to type restrictions. The equation for beta reduction

holds in context whenever and , while the equation for eta reduction

holds whenever and does not appear free in .

Operational semantics

Likewise, the operational semantics of simply typed lambda calculus can be fixed as for the untyped lambda calculus, using call by name, call by value, or other evaluation strategies. As for any typed language, type safety is a fundamental property of all of these evaluation strategies. Additionally, the strong normalization property described below implies that any evaluation strategy will terminate on all simply typed terms.

Categorical semantics

The simply typed lambda calculus (with -equivalence) is the internal language of Cartesian closed categories (CCCs), as was first observed by Joachim Lambek.[5] Given any specific CCC, the basic types of the corresponding lambda calculus are just the objects, and the terms are the morphisms. Conversely, every simply typed lambda calculus gives a CCC whose objects are the types, and morphisms are equivalence classes of terms.

To make the correspondence clear, a type constructor for the Cartesian product is typically added to the above. To preserve the categoricity of the Cartesian product, one adds typing rules for pairing, projection, and a unit term. Given two terms and , the term has type . Likewise, if one has a term , then there are terms and where the correspond to the projections of the Cartesian product. The unit term, of type 1, is written as and vocalized as 'nil', is the final object. The equational theory is extended likewise, so that one has

This last is read as "if t has type 1, then it reduces to nil".

The above can then be turned into a category by taking the types as the objects. The morphisms are equivalence classes of pairs where x is a variable (of type ) and t is a term (of type ), having no free variables in it, except for (optionally) x. Closure is obtained from currying and application, as usual.

More precisely, there exist functors between the category of Cartesian closed categories, and the category of simply-typed lambda theories.

It is common to extend this case to closed symmetric monoidal categories by using a linear type system. The reason for this is that the CCC is a special case of the closed symmetric monoidal category, which is typically taken to be the category of sets. This is fine for laying the foundations of set theory, but the more general topos seems to provide a superior foundation.

Proof-theoretic semantics

The simply typed lambda calculus is closely related to the implicational fragment of propositional intuitionistic logic, i.e., minimal logic, via the Curry–Howard isomorphism: terms correspond precisely to proofs in natural deduction, and inhabited types are exactly the tautologies of minimal logic.

Alternative syntaxes

The presentation given above is not the only way of defining the syntax of the simply typed lambda calculus. One alternative is to remove type annotations entirely (so that the syntax is identical to the untyped lambda calculus), while ensuring that terms are well-typed via Hindley–Milner type inference. The inference algorithm is terminating, sound, and complete: whenever a term is typable, the algorithm computes its type. More precisely, it computes the term's principal type, since often an unannotated term (such as ) may have more than one type (, , etc., which are all instances of the principal type ).

Another alternative presentation of simply typed lambda calculus is based on bidirectional type checking, which requires more type annotations than Hindley–Milner inference but is easier to describe. The type system is divided into two judgments, representing both checking and synthesis, written and respectively. Operationally, the three components , , and are all inputs to the checking judgment , whereas the synthesis judgment only takes and as inputs, producing the type as output. These judgments are derived via the following rules:

[1] [2]
[3] [4]
[5] [6]

Observe that rules [1]–[4] are nearly identical to rules (1)–(4) above, except for the careful choice of checking or synthesis judgments. These choices can be explained like so:

  1. If is in the context, we can synthesize type for .
  2. The types of term constants are fixed and can be synthesized.
  3. To check that has type in some context, we extend the context with and check that has type .
  4. If synthesizes type (in some context), and checks against type (in the same context), then synthesizes type .

Observe that the rules for synthesis are read top-to-bottom, whereas the rules for checking are read bottom-to-top. Note in particular that we do not need any annotation on the lambda abstraction in rule [3], because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules [5] and [6] as follows:

  1. To check that has type , it suffices to synthesize type .
  2. If checks against type , then the explicitly annotated term synthesizes .

Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations. And in fact, annotations are needed only at β-redexes.

General observations

Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term . Recursion can be added to the language by either having a special operator of type or adding general recursive types, though both eliminate strong normalization.

Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete.

Important results


  1. ^ a b Church, Alonzo (June 1940). "A formulation of the simple theory of types" (PDF). Journal of Symbolic Logic. 5 (2): 56–68. doi:10.2307/2266170. JSTOR 2266170. S2CID 15889861. Archived from the original (PDF) on 12 January 2019.
  2. ^ Pfenning, Frank. "Church and Curry: Combining Intrinsic and Extrinsic Typing" (PDF): 1. Retrieved 26 February 2022. ((cite journal)): Cite journal requires |journal= (help)
  3. ^ Curry, Haskell B (1934-09-20). "Functionality in Combinatory Logic". Proceedings of the National Academy of Sciences of the United States of America. 20 (11): 584–90. Bibcode:1934PNAS...20..584C. doi:10.1073/pnas.20.11.584. ISSN 0027-8424. PMC 1076489. PMID 16577644. (presents an extrinsically typed combinatory logic, later adapted by others to the lambda calculus)[2]
  4. ^ Reynolds, John (1998). Theories of Programming Languages. Cambridge, England: Cambridge University Press. pp. 327, 334. ISBN 9780521594141.
  5. ^ Lambek, J. (1986). "Cartesian closed categories and typed λ-calculi". Combinators and Functional Programming Languages. Lecture Notes in Computer Science. Vol. 242. Springer. pp. 136–175. doi:10.1007/3-540-17184-3_44. ISBN 978-3-540-47253-7.
  6. ^ Tait, W. W. (August 1967). "Intensional interpretations of functionals of finite type I". The Journal of Symbolic Logic. 32 (2): 198–212. doi:10.2307/2271658. ISSN 0022-4812. JSTOR 2271658. S2CID 9569863.
  7. ^ Statman, Richard (1 July 1979). "The typed λ-calculus is not elementary recursive". Theoretical Computer Science. 9 (1): 73–81. doi:10.1016/0304-3975(79)90007-0. ISSN 0304-3975.
  8. ^ Mairson, Harry G. (14 September 1992). "A simple proof of a theorem of Statman". Theoretical Computer Science. 103 (2): 387–394. doi:10.1016/0304-3975(92)90020-G. ISSN 0304-3975.
  9. ^ Statman, Richard (July 1979). "The typed λ-calculus is not elementary recursive". Theoretical Computer Science. 9 (1): 73–81. doi:10.1016/0304-3975(79)90007-0. ISSN 0304-3975.
  10. ^ Berger, U.; Schwichtenberg, H. (July 1991). "An inverse of the evaluation functional for typed lambda-calculus". [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science: 203–211. doi:10.1109/LICS.1991.151645. ISBN 0-8186-2230-X. S2CID 40441974.
  11. ^ Huet, Gerard P. (1 April 1973). "The undecidability of unification in third order logic". Information and Control. 22 (3): 257–267. doi:10.1016/S0019-9958(73)90301-X. ISSN 0019-9958.
  12. ^ Baxter, Lewis D. (1 August 1978). "The undecidability of the third order dyadic unification problem". Information and Control. 38 (2): 170–178. doi:10.1016/S0019-9958(78)90172-9. ISSN 0019-9958.
  13. ^ Goldfarb, Warren D. (1 January 1981). "The undecidability of the second-order unification problem". Theoretical Computer Science. 13 (2): 225–230. doi:10.1016/0304-3975(81)90040-2. ISSN 0304-3975.
  14. ^ Stirling, Colin (22 July 2009). "Decidability of higher-order matching". Logical Methods in Computer Science. 5 (3): 1–52. arXiv:0907.3804. doi:10.2168/LMCS-5(3:2)2009. S2CID 1478837.
  15. ^ Schwichtenberg, Helmut (1 September 1975). "Definierbare Funktionen imλ-Kalkül mit Typen". Archiv für mathematische Logik und Grundlagenforschung (in German). 17 (3): 113–114. doi:10.1007/BF02276799. ISSN 1432-0665. S2CID 11598130.
  16. ^ Friedman, Harvey (1975). "Equality between functionals". Logic Colloquium. Lecture Notes in Mathematics. Springer. 453: 22–37. doi:10.1007/BFb0064870. ISBN 978-3-540-07155-6.
  17. ^ Statman, R. (1 December 1983). "-definable functionals and conversion". Archiv für mathematische Logik und Grundlagenforschung. 23 (1): 21–26. doi:10.1007/BF02023009. ISSN 1432-0665. S2CID 33920306.
  18. ^ Plotkin, G.D. (1973). Lambda-definability and logical relations (PDF) (Technical report). Edinburgh University. Retrieved 30 September 2022.
  19. ^ Jung, Achim; Tiuryn, Jerzy (1993). "A new characterization of lambda definability". Typed Lambda Calculi and Applications. Lecture Notes in Computer Science. Springer. 664: 245–257. doi:10.1007/BFb0037110. ISBN 3-540-56517-5.
  20. ^ Loader, Ralph (2001). "The Undecidability of λ-Definability". Logic, Meaning and Computation: Essays in Memory of Alonzo Church. Springer Netherlands: 331–342. doi:10.1007/978-94-010-0526-5_15. ISBN 978-94-010-3891-1.