Книги для теории систем начального типа

Я хочу изучить теорию систем типов. Я не имею никакого фона в теории систем типов, поэтому я более или менее начинающий (за исключением статей, которые я прочитал по этому вопросу и которых я нахожу устрашающим из-за используемой нотации). Какие хорошие книги могут помочь мне начать? Я смотрел книгу Бенджамина К. Пирса "Типы и языки программирования". Это подходит для новичка или это слишком сложно? Если это слишком сложно, что еще я могу использовать для начала моего исследования?

Ответы

Ответ 1

Я думаю, что типы и языки программирования будут хорошим выбором.

Когда я впервые прочитал TaPL, я тоже был новичком в теории типов, и мне не было слишком трудно понять.

В статьях, которые вы видели, вы увидите много обозначений, но нотация будет объяснена до его использования, поэтому это не должно быть проблемой. На самом деле нет ничего пугающего в обозначении, если вы знаете, что это значит ¹.

¹ Это довольно часто случается с этими вещами. Иногда я думаю, что большая часть математики и формальной компьютерной науки состоит в том, что они изобретают страшные представления о простых вещах, поэтому необразованные массы не понимают, насколько легко все это на самом деле.

Ответ 2

TAPL - это трудная книга для понимания и нацелена на выпускников (и, возможно, кандидатов на пост phd). Это конечно не для новичков. Вместо этого я рекомендовал бы Джон К. Митчелл книгу "Понятия на языках программирования", нацеленную на студентов, чтобы сначала ознакомиться с основами.