Quais são alguns bons livros introdutórios sobre teoria dos tipos?

Respostas:

28

As fundações de software de Benjamin C. Pierce seriam um bom ponto de partida. Seria um bom precursor para seus tipos e linguagens de programação . Há também a teoria dos tipos e a programação funcional de Simon Thompson e as provas e tipos de Girard .

Steven Shaw
fonte
10
Sugiro que você prepare primeiro as Linguagens de programação e tipo de Peirce antes das fundações de software, que são mais avançadas. Para alguém que quer começar devagar, algo como Lambda-Calculus e Combinators de Hindley e Seldin é uma introdução suave.
Martin Berger
4
Sim, TAPL é o livro. Há também os "Tópicos avançados em tipos e linguagens de programação" de Pierce como acompanhamento.
Huck Bennett
@ MartinBerger, dei uma olhada no índice para Lambda-Calculus e Combinators e parece um pouco assustador. Tem certeza de que é mais introdutório que TAPL ou SF?
Steven Shaw
1
@StevenShaw Hindley / Seldin começa com o básico e prossegue muito lentamente, mas de forma abrangente. A parte teórica do tipo não faz nada sofisticado. Talvez a teoria básica simples de tipos de Hindley também seja apropriada. Eu nunca segurei em minhas mãos embora.
Martin Berger
9

O livro de Robert Harper, Fundamentos práticos para linguagens de programação (disponível como rascunho on-line: http://www.cs.cmu.edu/~rwh/plbook/book.pdf ) é uma alternativa um pouco mais intensa aos tipos e linguagens de programação.

Chris Martens
fonte
5

É mais sobre fundamentos matemáticos e menos sobre ciência da computação, mas o livro Homotopy Type Theory: Univalent Foundations of Mathematics está disponível gratuitamente em formato pdf sob uma licença CC.

David Eppstein
fonte
6
Gosto do tópico e do livro, mas, claramente, não é como se não assumisse que você já conhece as regras de abstrações, reduções etc. de lambda. O OP, vindo de usar Haskell e agora ser curioso sobre a teoria tipo, será perplexo com a interpretação da teoria de homotopia via tipos de identidade, 80 páginas em :).
Nikolaj-K
1
Concordo com @NikolajK que o livro Hott é muito avançado para um iniciante em teoria dos tipos. Um bom caminho para um programador Haskell é aprender primeiro o Agda . Agda é (simplificando um pouco) Haskell com tipos dependentes e foi usado para formalizar Hott.
Martin Berger
1
Não :) introdutório
Steven Shaw