¿Cuáles son algunos buenos libros introductorios sobre teoría de tipos?

Respuestas:

28

Fundamentos de software de Benjamin C. Pierce sería un buen lugar para comenzar. Sería un buen precursor de sus Tipos y Lenguajes de Programación . También está la teoría de tipos y la programación funcional de Simon Thompson y las pruebas y tipos de Girard .

Steven Shaw
fuente
10
Sugeriría preparar los lenguajes de programación y tipo de Peirce primero antes de las bases de software, que es más avanzado. Para alguien que quiere comenzar lentamente, algo como Lambda-Calculus y Combinators de Hindley y Seldin es una introducción amable.
Martin Berger
44
Sí, TAPL es el libro. También hay "Temas avanzados en tipos y lenguajes de programación" de Pierce como seguimiento.
Huck Bennett
@ MartinBerger, eché un vistazo a la tabla de contenido de Lambda-Calculus y Combinators y parece un poco desalentador. ¿Estás seguro de que es más introductorio que TAPL o SF?
Steven Shaw
1
@StevenShaw Hindley / Seldin comienza con lo más básico y continúa muy lentamente, pero de manera integral. La parte teórica tipo no hace nada elegante. Quizás la teoría básica simple del tipo de Hindley también sea apropiada. Sin embargo, nunca lo he tenido en mis manos.
Martin Berger
9

El libro de Robert Harper Fundamentos prácticos para lenguajes de programación (disponible como borrador en línea: http://www.cs.cmu.edu/~rwh/plbook/book.pdf ) es una alternativa algo más intensa que los Tipos y lenguajes de programación.

Chris Martens
fuente
5

Se trata más de fundamentos matemáticos y menos de informática, pero el libro Homotopy Type Theory: Univalent Foundations of Mathematics está disponible de forma gratuita en formato pdf bajo una licencia CC.

David Eppstein
fuente
66
Me gusta el tema y el libro, pero claramente, no es que no asuma que ya estás familiarizado con las reglas de abstracciones lambda, reducciones, etc. El OP, que proviene del uso de Haskell y ahora tiene curiosidad por la teoría de tipos, estará desconcertado por la interpretación de la teoría de la homotopía a través de los tipos de identidad, 80 páginas. :)
Nikolaj-K
1
Estoy de acuerdo con @NikolajK en que el libro de Hott es demasiado avanzado para un principiante en teoría de tipos. Una buena ruta para un programador de Haskell es aprender Agda primero. Agda es (simplificando un poco) Haskell con tipos dependientes, y se ha utilizado para formalizar Hott.
Martin Berger
1
No introductorio :)
Steven Shaw