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

28

Ostatnio studiuję Haskell i języki programowania. Czy ktoś mógłby polecić jakieś książki na temat teorii typów?

soft-question pl.programming-languages type-theory

— qazwsx
źródło

5

Być może zainteresuje Cię moja kolekcja zasobów na temat teorii typów

— Steven Shaw,

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

4

Inną ciekawą książką, która splata teorię typów z programowaniem w języku funkcjonalnym, jest Używanie, rozumienie i odkrywanie języka OCaml przez Didiera Remy'ego .

— Radu GRIGore
źródło