From the Introduction section of Homotopy Type Theory book:

Type theory was originally invented by Bertrand Russell ... It was later developed as a rigorous formal system in its own right(under tha name "$\lambda$-calculus").

Can anyone explain me this sentence? I'm having trouble seeing $\lambda$-calculus as a type system.

(also in the same paragraph, $\lambda$-calculus called as "Church's type system")

  • $\begingroup$ While it may not seem obvious, the book "Types and Programming Languages" by Benjamin C. Pierce explains this in detail by going from lambda calculus up to a simple typed programming language. See: cs.stackexchange.com/q/9548/268 $\endgroup$ – Guy Coder Aug 12 '13 at 10:11

In the very next paragraph of that book (see HoTT, p. 2) they give an informal characterization of what qualifies a language system (or logic) as a type system, namely that: in it all terms are typed.

By "Church's type system" they're referring to the simply typed lambda calculus (introduced in 1940).

In 1930s, in particular while preparing his negative solution to the decision problem, Church had introduced a system of untyped lambda calculus. This, of course, was not a type theory.

The 1940 system, however, is a type theory, because in it all terms are typed (see, for example (T&S), Section 1.2 for how exactly this is done). By "lambda-calculus as a type system" they're referring to this second, simply typed version of lambda calculus.

(T&S) Troelstra, A.S. & Schwichtenberg, H. Basic Proof Theory, 1996.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.