Quels sont les bons livres d'introduction à la théorie des types?

Réponses:

28

Les fondations logicielles de Benjamin C. Pierce seraient un bon point de départ. Ce serait un bon précurseur pour ses Types et Langages de Programmation . Il y a aussi la théorie des types et la programmation fonctionnelle de Simon Thompson et les preuves et types de Girard .

Steven Shaw
la source
10
Je suggère de préparer les langages de type et de programmation de Peirce avant les fondations logicielles qui sont plus avancées. Pour quelqu'un qui veut commencer lentement, quelque chose comme Lambda-Calculus and Combinators de Hindley et Seldin est une introduction douce.
Martin Berger
4
Oui, TAPL est le livre. Il y a aussi les "Rubriques avancées sur les types et les langages de programmation" de Pierce.
Huck Bennett
@MartinBerger, j'ai jeté un œil à la table des matières pour Lambda-Calculus et Combinators et cela semble un peu intimidant. Êtes-vous sûr que c'est plus introductif que TAPL ou SF?
Steven Shaw
1
@StevenShaw Hindley / Seldin commence par les bases et se déroule très lentement, mais de manière globale. La partie théorique type ne fait rien d'extraordinaire. Peut-être que la théorie de type simple de base de Hindley est également appropriée. Je ne l'ai cependant jamais tenu entre mes mains.
Martin Berger
9

Le livre de Robert Harper Practical Foundations for Programming Languages ​​(disponible en version préliminaire en ligne: http://www.cs.cmu.edu/~rwh/plbook/book.pdf ) est une alternative un peu plus intense aux types et langages de programmation.

Chris Martens
la source
5

C'est plus sur les fondements mathématiques que sur l'informatique, mais le livre Homotopy Type Theory: Univalent Foundations of Mathematics est disponible gratuitement en format pdf sous une licence CC.

David Eppstein
la source
6
J'aime le sujet et le livre, mais clairement, ce n'est pas comme s'il ne supposait pas que vous connaissiez déjà les règles des abstractions lambda, des réductions, etc. L'OP, issu de l'utilisation de Haskell et maintenant curieux de la théorie des types, sera dérouté par l'interprétation de la théorie de l'homotopie via les types d'identité, 80 pages. :)
Nikolaj-K
1
Je suis d'accord avec @NikolajK que le livre de Hott est trop avancé pour un débutant en théorie des types. Une bonne voie pour un programmeur Haskell est d'apprendre d' abord Agda . Agda est (simplifiant un peu) Haskell avec des types dépendants, et a été utilisé pour formaliser Hott.
Martin Berger
1
Pas d'introduction :)
Steven Shaw