Какие хорошие вводные книги по теории типов?

Ответы:

28

Фонды программного обеспечения Бенджамина С. Пирса было бы хорошим началом. Это было бы хорошим предшественником его типов и языков программирования . Есть также Теория типов Саймона Томпсона и Функциональное программирование и Доказательства и Типы Жирара .

Стивен Шоу
источник
10
Я бы посоветовал подготовить Peirce's Type и Programming Languages ​​в первую очередь до основания программного обеспечения, которое является более продвинутым. Для тех, кто хочет начать медленно, что-то вроде Lambda-Calculus и Combinators Хиндли и Селдина - это мягкое введение.
Мартин Бергер
4
Да, TAPL - это книга. Есть также «Продвинутые темы по типам и языкам программирования» Пирса в качестве продолжения.
Гек Беннетт
@MartinBerger, я взглянул на оглавление для Lambda-Calculus и Combinators, и это кажется немного пугающим. Вы уверены, что это более вводный, чем TAPL или SF?
Стивен Шоу
1
@StevenShaw Hindley / Seldin начинает с самых основ и продвигается очень медленно, но всесторонне. Теоретическая часть типа не делает ничего особенного. Может быть, Базовая Простая Теория Типа Хиндли также подходит. Я никогда не держал это в моих руках все же.
Мартин Бергер
9

Книга Роберта Харпера «Практические основы языков программирования» (доступна в виде черновика на сайте: http://www.cs.cmu.edu/~rwh/plbook/book.pdf ) представляет собой несколько более интенсивную альтернативу типам и языкам программирования.

Крис Мартенс
источник
5

Это больше о математических основах и меньше о компьютерных науках, но книга « Теория гомотопических типов: однолистные основы математики» доступна бесплатно в формате pdf по лицензии CC.

Дэвид Эппштейн
источник
6
Мне нравится тема и книга, но ясно, что она не предполагает, что вы уже знакомы с правилами лямбда-абстракций, сокращений и т. Д. ОП, исходящий из использования Haskell и теперь интересуемый теорией типов, будет сбит с толку интерпретацией теории гомотопий через типы идентичности, 80 страниц. :)
Николай-К
1
Я согласен с @NikolajK, что книга Хотта слишком продвинута для новичка в теории типов. Хороший путь для программиста на Haskell - это сначала изучить Agda . Agda (немного упрощает) Haskell с зависимыми типами и используется для формализации Hott.
Мартин Бергер
1
Не вступительный :)
Стивен Шоу