Steele, G., Sussman, J. The Art of Interpreter (pdf)
Комментарий @gabriel-fallen
На основе серии метациркулярных интерпретаторов рассматривается влияние некоторых языковых фич на возможность построения модульных программ. В частности, изучается взаимное влияние разных схем связывания имён переменных (динамическая и синтаксическая), изменяемого состояния и побочных эффектов в целом, а также идентичности объектов (object identity). В качестве модельных языков используются диалекты LISP.
Friedman, D., Wand, M. Essentials of Programming Languages
Комментарий от @ksromanov.
(Заинтересованному читателю не составит труда найти PDF в сети Интернет)
На основе серии интепретаторов подробно рассматриваются различные аспекты семантических особенностей разных языков, навеянных семейством ML (SML/OCaml/Haskell), правда полиморфизм почти не затрагивается. В качестве языка реализации используется обеднённый диалект Scheme (LISP), представленный в системе Racket (lang:eopl). Учебные языки намеренно делаются непохожими на Scheme, но авторы предоставили крайне удобную библиотеку-генератор лексеров/парсеров, по функциональности похожую на Antlr. Поэтому читатель может сконцентрироваться на абстрактном синтаксисе и семантике, изредка развлекаясь простыми конструкциями конкретного синтаксиса модельных языков. Сильной стороной книги являются чудесно проработанные главы про состояние и CPS (continuation-passing-style), чёткое разделение между Expressed Values и Denoted Values, ненавязчивое введение спецификаций (операционная семантика). Фактически, книгу можно использовать для овладения техникой CPS. Слабые стороны — это продолжение сильных: спецификации введены слишком расплывчато (после желательно прочесть статью Г. Хаттона, отзыв см. ниже), абстрактная семантика дана в открыве от конкретной (многочисленные примеры и того, и другого можно увидеть в Essentials of Compilation). Вывод типов значительно лучше дан в Static Program Analysis А. Мёллера (см раздел Статический и динамический анализ).
Shriram Krishnamurthi, Programming Languages: Application and Interpretation
Комментарий @gabriel-fallen
Текущее третье издание является пересмотром и развитием предыдущих двух, нескольких "сопутствующих" учебников (HtDP, DCIC) и большого количества курсов, много лет читавшихся и продолжающих читаться автором в университете.
Изложение построено вокруг реализации и последовательного расщирения простого учебного языка программирования. Автор начинает с простейших понятий и вычислений "на бумаге" при помощи подстановки, после чего переходит к компьютерной реализации, вводя представления о Дереве Австрактного Синтаксиса (Abstract Syntax Tree, AST) и вычислении арифметических выражений. Только после этого поднимается вопрос синтаксического разбора и расширения интерпретатора более сложными конструкциями, такими как условное выполнение и связывание локальных имён. Среди продвинутых фич рассматриваются макросы, включая вопрос гигиены, и ООП, как основанное на классах, так и на прототипах, вклюяая ссылки на себя, множественное наследование, миксины и трейты.
Несмотря на фокус на динамических языках и интерпретации, большой раздел посвящён статической проверке типов. На элементарных примерах автор вводит базовые понятия, механизмы и нотацию теории типов, разбирает вопросы безопасности (safety) и здравости (soundness) системы типов, вывод типов и гибридную типизацию (gradual typing).
Среди дополнительных вопросов рассматривается реализация реляционного программирования, ленивых вычислений, "реактивных" вычислений, и другие.
Я бы рекомендавал этот учебник начинающим без математической подготовки в качестве простого введения в предмет, дающий очень широкий обзор тем, проблем и методов, таким образом формирующий фундамент для более тщательного и формализованного изучения вопросов реализации языков программирования.
Graham Hutton, Programming Language Semantics, It’s Easy As 1,2,3
Комментарий @gabriel-fallen
Эта недлинная вводно-обзорная статья — 25 страниц — покрывает удивительно обширный спектр тем, и делает это предельно просто и понятно. Горячо рекомендую к прочтению как начинающим, так и там, кто уже в курсе — хотя бы для удовольствия.
Хаттон демонстрирует 5 способов задания семантики:
- денотационную
- малого шага
- контекстуальную
- большого шага
- абстрактные машины
И ещё между делом вводит понятие индукции по правилам вывода, которое используется не только в семантике языков программирования и Computer Science, но и в математике в целом, наряду с математической и структурной индукцией.
Главный "секрет", позволяющий покрыть такой объём материала — использование предельно простого модельного языка: арифметических выражений, состоящих только из чисел и сложения. Это же является и главным недостатком — в языке нет переменных, соответственно, всё разнообразие подходов к работе с ними, и вся сложность остаются "за бортом". Кроме того, сам автор указывает, что такой язык не позволяет продемонстрировать разницу между денотационной и семантикой большого шага: в данном случае они выглядят одинаково, а вот для более сложных языков могут сильно отличаться.
Впрочем, примитивность рассматриваемого языка с головой компенсируется обилием ссылок на классические и современные статьи по разным подходам к формализации семантики и связям между ними. Среди прочего даются ссылки на аксиоматическую, алгебраическую, теоретико-игровую семантики и некоторые другие. Лично меня более всего заинтересовали статьи самого же Хаттона с соавторами, демонстрирующие систематический последовательный способ получения абстрактных машин и компиляторов из той или иной формальной семантики.
Benjamin C. Pierce, Types and Programming Languages
Бенджамин Пирс, Типы в языках программирования
Комментарий @gabriel-fallen
(Заинтересованному читателю не составит труда найти PDF в сети Интернет)
TaPL является, вероятно, самым часто советуемым введением в теорию типов и алгоритмы проверки типов, и выступает в качестве основного учебника на курсах во многих университетах по всему миру. Вполне заслуженно, нужно сказать.
Изложение ведётся от самых основ, начиная с краткого обзора необходимых математических понятий и формализмов, и базового фундамента в виде нетипизированных (динамически типизированных) интерпретаторов арифметических выражений и λ-исчисления. Таким образом он является одновременно и вводным учебником в реализацию интерпретаторов на функциональных языках.
Далее Пирс последовательно объясняет все основные вопросы и расширения терии типов: Simply-Typed λ-calculus, типизация (изменяемых) ссылок (references), типизация исключений, подтипирование (subtyping), рекурсивные типы, (параметрический) полиморфизм, экзистенциальные типы и типы высших порядков.
Как уже упоминалось, каждая тема сопровождается рассмотрением программы на языке OCaml, реализующей проверку типов. Конечно же, существуют "переводы" TaPL и на другие языки программирования, в первую очередь Haskell. Учебник предлагает большое количество упражнений, в том числе на программирование, решение которых также можно найти на множестве языков.
Таким образом, данная книга вкупе со всеми дополнительными материалами и обсуждениями, которые можно найти в Интернет, может выступать как учебником для начинающих разработчиков языков и систем типов, так и справочником по базовым системам и алгоритмам для продолжающих.