Was sind einige gute Einführungsbücher zur Typentheorie?

Antworten:

28

Software Foundations von Benjamin C. Pierce wäre ein guter Anfang. Es wäre ein guter Vorläufer für seine Typen und Programmiersprachen . Es gibt auch Simon Thompsons Typentheorie und funktionale Programmierung sowie Girards Beweise und Typen .

Steven Shaw
quelle
10
Ich würde vorschlagen, Peirces Typ und Programmiersprachen zuerst vor den fortgeschritteneren Software-Grundlagen vorzubereiten. Für jemanden, der langsam anfangen möchte, ist etwas wie Lambda-Kalkül und Kombinatoren von Hindley und Seldin eine sanfte Einführung.
Martin Berger
4
Ja, TAPL ist das Buch. Es gibt auch Pierces "Advanced Topics in Types and Programming Languages" als Follow-up.
Huck Bennett
@MartinBerger, ich habe mir das Inhaltsverzeichnis für Lambda-Calculus und Combinators angesehen und es scheint ein wenig entmutigend. Sind Sie sicher, dass es einführender als TAPL oder SF ist?
Steven Shaw
1
@StevenShaw Hindley / Seldin beginnt mit den Grundlagen und geht sehr langsam, aber umfassend vor. Der typentheoretische Teil ist nichts Besonderes. Möglicherweise ist auch die einfache Typentheorie von Hindley angemessen. Ich habe es aber noch nie in der Hand gehalten.
Martin Berger
9

Robert Harpers Buch Practical Foundations for Programming Languages ​​(verfügbar als Entwurf online: http://www.cs.cmu.edu/~rwh/plbook/book.pdf ) ist eine etwas intensivere Alternative zu Types und Programming Languages.

Chris Martens
quelle
5

Es geht mehr um mathematische Grundlagen und weniger um Informatik, aber das Buch Homotopy Type Theory: Univalente Grundlagen der Mathematik ist kostenlos im PDF-Format unter einer CC-Lizenz erhältlich.

David Eppstein
quelle
6
Ich mag das Thema und das Buch, aber es ist eindeutig nicht so, als ob Sie mit den Regeln für Lambda-Abstraktionen, -Reduktionen usw. bereits vertraut wären. Das OP, das von Haskell kommt und jetzt neugierig auf Typentheorie ist, wird durch die Interpretation der Homotopietheorie über Identitätstypen, 80 Seiten in verwirrt sein. :)
Nikolaj-K
1
Ich stimme @NikolajK zu, dass das Hott-Buch für Anfänger in der Typentheorie zu fortgeschritten ist. Ein guter Weg für einen Haskell-Programmierer ist, zuerst Agda zu lernen . Agda ist (ein bisschen vereinfacht) Haskell mit abhängigen Typen und wurde verwendet, um Hott zu formalisieren.
Martin Berger
1
Nicht einleitend :)
Steven Shaw