Teoría de tipos desde cero, primera recomendación de libro

Question

Básicamente tengo un gran problema para encontrar un recurso decente para aprender la teoría de tipos.

Me gustaría que me recomendaran algún tipo de recurso para aprender teoría de tipos en sentido matemático.

También quiero señalar que no tengo experiencia previa con ningún tipo de teoría de tipos (básicamente todo lo que sé sobre ella es que existe).

Así que, teniendo esto en cuenta, ¿a dónde puedo ir desde aquí?

Answer 1

Puede ver :

• Peter Andrews, Introducción a la Lógica Matemática y a la Teoría de Tipos : A la verdad a través de la demostración (1986)

• J. Roger Hindley, Teoría básica de tipos simples (1997)

• Fairouz Kamareddine y Twan Laan, Una perspectiva moderna de la teoría de tipos (2004).

---

También puede ver :

• William Farmer, Las siete virtudes de la teoría de tipos simple (2008).

Answer 2

Si tiene conocimientos sobre la teoría de las categorías, podría echar un vistazo a Lógica categórica y teoría de tipos por Bart Jacobs.

Al igual que tú no tenía experiencia con la teoría de tipos y me han dicho que la lea. Estoy lejos de terminarlo pero hasta ahora estoy bastante satisfecho.

Editar. Quizás valga la pena decir que el libro enfatiza el hecho de que no hay una teoría de tipos sino numerosas; básicamente una para cada fibración de Grothendieck sobre buenas categorías . Sólo la introducción y el primer capítulo me ayudaron a entender las diferencias entre la teoría de tipos simples y la teoría de tipos dependientes, por ejemplo.

Answer 3

Yo tuve el mismo problema cuando empecé a aprender sobre la teoría de tipos, así que empecé a recopilar una lista de recursos, que ha crecido (¿demasiado?). Está aquí: github.com/williamdemeo/TypeFunc .

En cuanto a buenos libros de texto, como alguien con más formación en matemáticas que en ciencias naturales, he encontrado que los dos libros más amenos y que parecen proporcionar una buena base para la teoría de tipos son

1. Mitchell's Fundamentos de los lenguajes de programación .
2. Crole's Categorías para los tipos .

A riesgo de simplificar demasiado, el primero de ellos parece más orientado a la cs (pero sigue siendo bastante riguroso y teórico), mientras que el segundo se lee más como un libro de matemáticas (pero con un enfoque en cosas que son útiles para la teoría de tipos).