В прошедший уикенд я читал лекции в CS-клубе при ПОМИ РАН по выводу типов в системе Хиндли-Милнера и компиляторе GHC (https://compsciclub.ru/courses/types/2019-spring/). Утром второго дня я получил от Amazon'а письмо, начинавшееся со слов «Hello Vitaly Bragilevsky,
Are you looking for something in our Computers & Technology Software Books department? If so, you might be interested in these items».

В теме письма при этом значилось «Types and Programming...», а в списке были настолько близкие к тематике курса книги, что я решил начать лекцию с зачитывания полученного списка. Честно говоря, я был удивлён качеством рекомендации. Разумеется, я все эти книги прекрасно знаю, но получить такую подборку от искусственного интеллекта было очень приятно. Чаще приходится месяцами наблюдать рекомендации относительно покупки чайника сразу после приобретения чайника, ведь всем известно, что люди всегда покупают по два чайника.

Один из слушателей попросил меня продублировать список здесь, что я с удовольствием и делаю.

1) Types and Programming Languages, Benjamin C. Pierce
Азбука нашего дела. Здорово, что есть (замечательный!) русский перевод (http://newstar.rinet.ru/~goga/tapl/), в котором мне в числе прочих выписана благодарность, которой я очень горжусь.

2) Purely Functional Data Structures, Chris Okasaki
Приятная книга, помогающая понять все сложности и интересности работы со структурами данных в чисто функциональном программировании. В книге примеры на ML, но есть приложение с реализациями на Haskell. Есть и русский перевод, я был его редактором: https://dmkpress.com/catalog/computer/programming/functional/978-5-97060-233-1/

3) Basic Category Theory for Computer Scientists, Benjamin C. Pierce
Как признаётся сам автор, ему захотелось изучить теорию категорий, поэтому он и написал эту книжку. Написана она почти 30 лет назад, Пирс тогда был совсем молодым. Книжка очень тонкая (всего 114 страниц), что очень приятно.

4) The Little Typer, Daniel P. Friedman, David Thrane Christiansen
Приятный (несколько игровой) способ изучить зависимые типы. Предисловие от Боба Харпера и послесловие от Коннора МакБрайда говорят сами за себя. Книжка новая, вышла в сентябре 2018 года.

5) Structure and Interpretation of Computer Programs, Harold Abelson, Gerald Jay Sussman, Julie Sussman
Ну, тут всё ясно, классика. Есть русский перевод: http://newstar.rinet.ru/~goga/sicp/sicp.pdf. Кстати, у книг 1, 2, 5 есть один общий переводчик — замечательный Георгий Бронников, мы все должны быть ему благодарны.

6) Practical Foundations for Programming Languages, Robert Harper
Актуальная библия теории типов. Текст сложный: этой осенью я участвовал в семинаре, в рамках которого делались доклады по этой книге. Так вот студенты всячески пытались с неё свинтить, заменяя на более простые источники. Ну, действительно сложно.

7) The Art of Computer Programming, Volumes 1-4A, Donald E. Knuth
Тут искусственный интеллект немного лопухнулся, но книжка всё равно важная!

8) Type Theory and Formal Proof: An Introduction, Rob Nederpelt, Herman Geuvers
Неплохой современный учебник по теории типов (2014 год) от Cambridge University Press, достаточно высокий уровень, но написано относительно просто.

9) The Little Prover, Daniel P. Friedman, Carl Eastlund
Индуктивные доказательства во всей красе и снова в игровом стиле. Предисловие от Маттиаса Феллайзена, тоже не последний человек, зря рекомендовать книгу не будет.

Внезапно оказалось, что я смотрел только часть письма, а внизу была ссылка на полный список рекомендаций. В полном списке также нашлись Type-driven Development in Idris от Эдвина Брейди (тоже с благодарностью мне!), Compilers: Principles, Techniques, and Tools от Ахо, Лэм, Сети и Ульмана, и почему-то Рефакторинг от Мартина Фаулера. Перестарался искусственный интеллект всё-таки, зря хвалил.