tapl

Скажу сразу: эта книга пригодится далеко не всем программистам. В ней полно «матана», «формул» (таких, как правила типизации и вычислений) и упражнений с доказательством теорем. Так же как в научных статьях, количество полезной информации в одном предложении иногда просто зашкаливает — в начале главы/книги определяют кучу разных символов и дальше ими регулярно «обфусцируют» предложения без дополнительных объяснений. Но нас не напугать сложностью, ведь так?

Я давно слышал о существовании этой книги, но достал ее бумажный вариант лишь во время увлечения фунциональной парадигмой программирования и ковыряния языка F#. Взгляд на новую для меня парадигму и необычную (по сравнению с C#) систему типов заставил заинтересоваться в том, что еще интересного можно встретить в системах типов и чем те или иные решения отличаются. Без сомнения могу сказать, что «Типы в языках программирования» (далее TAPL) — это настольная книга для всех, кто интересуется теорией системам типов, разрабатывает компиляторы или инструментарий для языков программирования.

Чтобы хоть как-то понимать содержимое TAPL, придется разобраться в основах бестипового и типизированного лямбда-исчисления (главы I и II), изучить способ записи правил типизации и вычислений (эти страшные «формулы» гораздо проще, чем кажутся на первый взгляд!), а так же разобраться с синтаксисом ML-подобного языка. Без этого минимального «набора для выживания» половина книги будет казаться написанной на инопланетном языке, так что обязательно подготовьте теоретический минимум.

.NET-программистам будет больше всего может быть полезна глава III — «Подтипы», которая фактически описывает классическое объектно-ориентированное программирование, основанное на классах. Книга объясняет и причины появления подтипов, и отвечает на массу самых фундаментальных вопросов, о которых мы обычно совсем не задумываемся, например:

  • Что представляет собой тип Object и какого «противоположного» ему типа нет в таких языках как C#/Java? Как типизировать функцию, которая никогда не завершается (бросает исключение)?

  • Чем отличаются структурная и номинальная (или «именная») системы типов с подтипами? Почему, например, для успешной типизации JavaScript кода в языке программирования TypeScript выбрана структурная система типов?

  • Почему в ООП-языках существуют разные вида приведения типов, в чем назначение каждого из них?

  • Зачем применяют упаковку («боксинг») значений, для чего нужно универсальное представление значений в памяти?

  • Почему о подтипах можно думать как о множествах, но на практике используется другая семантика?

  • Чем традиционные классы в ООП отличаются от алгебраических типов данных (АДТ, применяемые в большинстве функциональных языков программирования), в чем приемущества и недостатки обоих средств?

  • Что такое типы-объединения и типы-пересечения, набирающие популярность сейчас в языках типа TypeScript, Scala (Dotty) и Ceylon, в каком виде эти типы-пересечения встречаются в C#/Java?

Ответы на эти и многие другие вопросы TAPL дает в предельно краткой форме, существенно отличающейся от типичной подачи ООП в книгах. Разбор императивного ООП-языка с подтипами с помощью моделирования на базе простого типизированного лямбда исчисления — это все равно что изучать язык высокого уровня с помощью декомпилятора байткода (уверен, многие программисты так делают, это отличный способ разобраться как что-то работает).

Я не склонен читать подобную литературу на русском языке, но благодаря замечательной работе, проделанной Георгием Бронниковым и Алексом Оттом (издательство «Лямбда пресс» & «Добросвет»), перевод TAPL — это исключение, можно совсем не беспокоиться об искажении смысла или терминов.