38
$\begingroup$

I don't know anything about type theory and I would like to learn it.

I'm interested to know how we can found mathematics on it. So, I would be interested by any text about type theory whose angle is similar to the one of Russel and Whitehead in the Principia, or similar to the one of Bourbaki (for instance).

But, I am also interested by any nice presentation of type theory (without any special focus on foundation of mathematics) that would help me to get the best of it.

Books, texts, articles, links are welcomed.

I am interested by any type theory (Martin-Löf's, homotopic, etc.).

PS: If it can help, in a way, by "foundation of mathematics", I mean "total formalization of mathematics", as in Bourbaki for instance.

PPS: I have asked another related question there, a little bit more general.

Improve this question
$\endgroup$
7
  • $\begingroup$ Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)? $\endgroup$
    – Andrej Bauer
    May 6, 2019 at 20:29
  • 3
    $\begingroup$ Also, this should be a wiki question. $\endgroup$
    – Andrej Bauer
    May 6, 2019 at 20:29
  • 2
    $\begingroup$ @AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc. $\endgroup$
    – Colas
    May 6, 2019 at 21:17
  • 3
    $\begingroup$ If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation. $\endgroup$
    – Andrej Bauer
    May 6, 2019 at 22:08
  • 1
    $\begingroup$ You may be interested in github.com/jozefg/learn-tt. $\endgroup$
    – wchargin
    May 7, 2019 at 7:11

8 Answers 8

Reset to default
8
$\begingroup$

It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !

You will find everything from here: https://homotopytypetheory.org/

Improve this answer
$\endgroup$
15
  • 3
    $\begingroup$ @NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification. $\endgroup$
    – Andreas Blass
    May 6, 2019 at 20:15
  • 5
    $\begingroup$ @NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory. $\endgroup$
    – Andreas Blass
    May 6, 2019 at 21:30
  • 3
    $\begingroup$ @Colas This may be somewhat less technical than what you're looking for, but you might look at the book Foundations of Mathematics by William Hatcher. It has a chapter on type theory, describing both predicative (Russell-Whitehead-style) type theory and simplified type theory. $\endgroup$
    – Andreas Blass
    May 6, 2019 at 21:36
  • 4
    $\begingroup$ When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea. $\endgroup$
    – Ali Caglayan
    May 6, 2019 at 22:27
  • 3
    $\begingroup$ If you want to read more about type theory as a logic (in the sense of lambda calculi) then I would recommend "Lectures on the Curry-Howard Isomorphism" by Sorensen and Urzyczyn. They do a pretty good job of laying out the development and study of the subject. There is a lot of work on how these ideas relate to (more) classical ideas of logic too. $\endgroup$
    – Ali Caglayan
    May 6, 2019 at 22:32
16
$\begingroup$

Here are some resources:

  1. UniMath school teaching materials, and in particular:

  2. Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics

  3. Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions. $\endgroup$
    – Ivan Di Liberti
    May 6, 2019 at 20:09
  • 2
    $\begingroup$ @IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit. $\endgroup$
    – Andrej Bauer
    May 6, 2019 at 20:28
13
$\begingroup$

I am far from being an expert. I will make a few suggestions.

  1. Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984

  2. T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.

  3. Andre Joyal. Notes on Clans and Tribes.

  4. Michael Shulman. Homotopy type theory: the logic of space.

  5. Thorsten Altenkirch. Naïve Type Theory.

Improve this answer
$\endgroup$
7
  • 11
    $\begingroup$ Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible. $\endgroup$
    – Andrej Bauer
    May 6, 2019 at 19:53
  • $\begingroup$ Does one of these references emphasize on foundations of mathematics? $\endgroup$
    – Colas
    May 6, 2019 at 20:00
  • 1
    $\begingroup$ @Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/… $\endgroup$
    – Ivan Di Liberti
    May 6, 2019 at 21:06
  • $\begingroup$ @IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks $\endgroup$
    – Colas
    May 6, 2019 at 21:26
  • 2
    $\begingroup$ @AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro) $\endgroup$
    – Izaak Meckler
    May 7, 2019 at 1:16
7
$\begingroup$

If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:

  1. Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
  2. Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
  3. The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.

There are some disadvantages to this approach.

  1. The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
  2. Another disadvantage is that they might be a bit more geared to those who are CS literate.

I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.

It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.

Improve this answer
$\endgroup$
5
$\begingroup$

I was going to write how I was surprised that nobody recommened Girard's book "Proofs and Types" yet, when I discovered that it actually had been disrecommended by someone.

Even though Girard tends to be a bit sloppy at times, he still manages to explain the core logical concepts much more lucently than for example "Programming in Martin-Löf's Type Theory".

It mainly does what the title suggests, namely explain the relation between proofs and types, i.e. the Curry–Howard correspondence. It also helps in familiarizing yourself with various bits of logic like the significance of cut-elimination. This should certainly be useful information if you're a mathematician trying to learn about the field.

P.S.: Here's also a list by Daniel Gratzer of various references on the subject.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Proofs and Types was the first bite of the apple for me, and set me on the road towards becoming a type theorist (having previously had a good grounding in classical logic and set theory, but no type theory at all). I found it compelling and inspiring, and while in hindsight I can see its many idiosyncrasies (which others in the thread have criticised), they didn’t get in the way of either enjoying it at the time or coming around to more standard presentations of type theory later. $\endgroup$
    – Peter LeFanu Lumsdaine
    Aug 7, 2019 at 10:41
3
$\begingroup$

Dan Grayson's paper An introduction to univalent foundations for mathematics is an exceptionally clear exposition. The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence. The second half (on univalence) is even better.

Improve this answer
$\endgroup$
0
1
$\begingroup$

This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm

Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.

I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps

This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf

Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf

There is a ton of stuff on ncatlab.org.

Improve this answer
$\endgroup$
0
$\begingroup$

As in Jason's answer, I recommend starting with an implementation like agda.

I like the presentation in Diviánszky Péter - Agda tutorial and Wadler, Wen Kokke, and Siek - Programming Language Foundations in Agda.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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