nLab simple type theory

Idea

Originally, “simple type theory” was the name of the type theory introduced by Church (1940) (therefore often and more informatively: “Church’s type theory” or similar). This type theory allowed (only) function type-type formation (therefore often: “simply typed lambda-calculus”) based on two elementary types (a kind of type of natural numbers and a type of propositions).

In mild generalization, if one admits in addition product type-type formation then [e.g. Gunter (1992)] these are the type theories whose categorical semantics is in cartesian closed categories [Lambek & Scott (1986), Part I], see also at relation between category theory and type theory.

More generally, the term “simple type theory” has come to refer to any type theory whose type formations are not indexed, in that the judgment that a type $A$ is well-formed has no other inputs, understood in contrast to:

• polymorphic type theory, where types depend on a context of type variables,

• dependent type theory, where types depend on a context of more general variables.

Related Pages

• pure type system

References

Original articles:

• Bertrand Russell, Mathematical Logic as Based on the Theory of Types, American Journal of Mathematics, Vol. 30, No. 3 (Jul., 1908), pp. 222-262

• Alonzo Church, §5 of: A Formulation of the Simple Theory of Types, The Journal of Symbolic Logic 5 2 (1940) 56-68 [doi:10.2307/2266170]

See also

• Alonzo Church: Schröder’s Anticipation of the Simple Theory of Types, Erkenntnis 10 (1976) 407-411 [doi:10.1007/BF00176047]

• Stanford Encyclopedia of Philosophy, Church’s Type Theory

Establishing the syntax/semantics relation between cartesian closed categories and simply-typed lambda calculi:

• Joachim Lambek, Philip J. Scott, Part I of: Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7 (1986) [ISBN: 0-521-24665-2, pdf]

Lecture notes:

• Jean-Yves Girard (translated and with appendiced by Paul Taylor and Yves Lafont), Proofs and Types, Cambridge University Press (1989) [ISBN:978-0-521-37181-0, webpage, pdf]

Textbook accounts:

• J. Roger Hindley, Basic Simple Type Theory, Cambridge University Press (1997, 2009) [doi:10.1017/CBO9780511608865]

• Carl A. Gunter, §2-3 in: Semantics of Programming Languages – Structures and Techniques, MIT Press (1992) [ISBN:9780262570954]

  (in a context of programming languages)

See also:

• W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267-286.

For a general framework for a class of simple type theories, in the philosophy of categorical algebra, see:

• Nathanael Arkor, Marcelo Fiore, Algebraic models of simple type theories: a polynomial approach, Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (2020) 88-101 [doi:10.1145/3373718.3394771, arXiv:2006.16949[