Jakie są dobre książki wprowadzające na temat teorii typów?

Odpowiedzi:

28

Software Foundations autorstwa Benjamina C. Pierce'a byłoby dobrym miejscem do rozpoczęcia. Byłby dobrym prekursorem jego rodzajów i języków programowania . Istnieją również teoria typów i programowanie funkcjonalne Simona Thompsona oraz dowody i typy Girarda .

Steven Shaw
źródło
10
Proponuję najpierw przygotować Typ i Języki Programowania Peirce'a, a dopiero potem podstawy oprogramowania, które są bardziej zaawansowane. Dla kogoś, kto chce zacząć powoli, coś takiego jak rachunek Lambda-Calculus i kombinatory Hindleya i Seldina to delikatne wprowadzenie.
Martin Berger,
4
Tak, TAPL jest książka. Jako uzupełnienie dostępne są również „Tematy zaawansowane w typach i językach programowania” Pierce'a.
Huck Bennett,
@MartinBerger, spojrzałem na spis treści dla Lambda-Calculus i Combinators i wydaje się to trochę zniechęcające. Czy na pewno jest to bardziej wprowadzające niż TAPL lub SF?
Steven Shaw,
1
@StevenShaw Hindley / Seldin zaczyna się od podstaw i postępuje naprawdę powoli, ale kompleksowo. Część teoretyczna typu nie robi nic szczególnego. Być może podstawowa teoria prostych typów Hindleya jest również odpowiednia. Jednak nigdy nie trzymałem tego w swoich rękach.
Martin Berger
10

Barendregts Lambda Calculi z typami jest bardziej zaawansowany, ale obejmuje kilka ważnych tematów w „klasycznej” teorii typów.

cody
źródło
Dzięki @cody, zapomniałem wspomnieć o Barendregt w mojej kolekcji zasobów na ten temat .
Steven Shaw,
9

Książka Roberta Harpera Praktyczne podstawy dla języków programowania (dostępna w wersji online: http://www.cs.cmu.edu/~rwh/plbook/book.pdf ) jest nieco bardziej intensywną alternatywą dla typów i języków programowania.

Chris Martens
źródło
5

Bardziej dotyczy podstaw matematycznych, a mniej informatyki, ale książka Homotopy Type Theory: Univalent Foundations of Mathematics jest dostępna bezpłatnie w formie pdf na licencji CC.

David Eppstein
źródło
6
Podoba mi się temat i książka, ale najwyraźniej nie jest tak, że nie zakłada się, że znasz już zasady abstrakcji lambda, redukcji itp. OP, pochodzący z używania Haskella i teraz ciekawy teorii typów, będzie zaskoczony interpretacją teorii homotopii za pomocą typów tożsamości, 80 stron. :)
Nikolaj-K
1
Zgadzam się z @NikolajK, że książka Hott jest zbyt zaawansowana dla początkującego w teorii typów. Dobrą drogą dla programisty Haskell jest najpierw nauka Agdy . Agda to (nieco upraszczając) Haskell z typami zależnymi i został użyty do sformalizowania Hott.
Martin Berger,
1
Nie wprowadzono :)
Steven Shaw