Неделю назад я пошутил, что статьи по принципам языков программирования POPL должны соответствовать критерию «интеллектуального запугивания», чтобы их принимали для публикации. Конечно, это неправда, но факт в том, что статьи по языкам программирования выглядят особенно устрашающе для специалистов-практиков (или академик действительно работает в другой области компьютерных наук!). Они битком набиты математическими символами и такими фразами как «суждения», «операционная семантика» и тому подобное. Там много тонких вариантов записи, но вы можете в основном уловить суть статьи, усвоив несколько базовых понятий. Так что вместо рассказа об очередной научной статье я подумал, что сегодня лучше напишу краткое практическое руководство по расшифровке научных статей на тему языков программирования. Здесь я следую книге Бенджамина Пирса «Типы в языках программирования» в качестве авторитетного источника.

Синтаксис


Начнём с понятного: синтаксис. Синтаксис говорит, какие предложения можно использовать в языке (т. е. какие программы мы можем писать). Синтаксис содержит набор термов, которые представляют собой строительные блоки. Возьмём следующий пример из Пирса:

  t ::= 
      true
      false
      if t then t else t
      0
      succ t
      pred t
      iszero t

Всюду, где встречается символ t, можно подставить любой терм. Если в статье упоминаются термы, то часто используется t с подстрочным индексом для различия между разными термами (например, $t_1$, $t_2$). Множество всех термов часто обозначается как $\tau$. Его не следует путать с символом $T$, который традиционно используется для обозначения типов.

В вышеприведённом примере обратите внимание, что сам по себе оператор if не является термом (это токен, в данном случае, keyword-токен). Термом является условное выражение if t then t else t.

Термы — это выражения, которые можно вычислить, и конечным результатом вычисления в правильно построенном окружении должно стать значение. Значения — это подмножество термов. В вышеприведённом примере значениями являются true, false, 0, а также значения, которые могут быть созданы путём последовательного применения операции succ к 0 (succ 0, succ succ 0, ...).

Семантика


Мы хотим придать какое-то значение термам языка. Это семантика. Существуют различные способы определить значение программ. Чаще всего вы встретите упоминания операционной семантики и денотационной семантики. Из них операционная семантика наиболее распространённая. Она определяет значение программы, устанавливая правила для абстрактной машины, которая вычисляет термы. Спецификации имеют форму набора правил вычисления — рассмотрим их чуть позже. В этом мировоззрении значение (смысл) терма t — это конечное состояние (величина), которого достигает машина, запущенная с t в её начальном состоянии. В денотационной семантике в качестве значения терма принимается некий математический объект (например, число или функция) в некоторой ранее существующей семантической области, а функция интерпретации соотносит термы языка с их эквивалентами в целевой области. Так что мы указываем, что представляет (или денотирует) терм в этой области.

Вы можете также столкнуться с тем, что авторы упоминают операционную семантику с малым шагом (small-step) и операционную семантику с большим шагом (big-step). Как следует из названия, это относится к тому, насколько большой скачок делает абстрактная машина с каждым применяемым правилом. В семантике с малым шагом термы переписываются постепенно, по одному маленькому шагу за раз, пока в конечном итоге не станут значениями. В семантике с большим шагом (она же «естественная семантика») мы можем перейти от терма к его окончательному значению за один шаг.

В записи семантики с малым шагом вы увидите что-нибудь такое: $t_1 \rightarrow t_2$, что следует читать так, что $t_1$ вычисляется в $t_2$. (Вместо подстрочных индексов могут использоваться штрихи, например, $t \rightarrow t'$). Это также известно как суждение (judgement). Стрелка $\rightarrow$ представляет один шаг вычислений. Если вам встретится $t_1 \rightarrow^{*} t_2$, то это значит «после многократного применения одношаговых вычислений $t_1$ в конечном итоге перешёл в $t_2’$».

В семантике с большим шагом используется другая стрелка. Так что $t \Downarrow v$ означает, что терм $t$ в результате вычисления перешёл в $v$. Если в одном и том же языке используется семантика с малым шагом и семантика с большим шагом, то $t \rightarrow^{*} v$ и $t \Downarrow v$ означают одно и то же.

Согласно конвенции, правила именуются ПРОПИСНЫМИ буквами. И если вам повезёт, то авторы добавят к правилам вычисления префикс ‘E-‘ как дополнительную подсказку.

Например:

if true then t2 else t3 $\rightarrow$ t2 (E-IFTRUE)

Обычно правила вычисления задают в стиле правил вывода (inference rules). Пример (E-IF):

$\frac{t_1\ \rightarrow t'_{1}}{\mathrm{if}\ t_1\ \mathrm{then}\ t_2\ \mathrm{else}\ t_3 \rightarrow \mathrm{if}\ t'_1\ \mathrm{then}\ t_2\ \mathrm{else}\ t_3}$


Это следует читать как «С учётом указанного в делителе мы можем сделать вывод о том, что находится в знаменателе». То есть в данном конкретном примере: «Если $t_1$ выводится в $t'_{1}$, то в этом случае $\mathrm{if}\ t_1 ...$ выводится в $\mathrm{if}\ t'_1 ...’$.

Типы


В языке программирования не обязательно должна быть определённая система типов (он может быть нетипизированным), но у большинства она есть.

«Система типов — это гибко управляемый синтаксический метод доказательства отсутствия в программе определённых видов поведения при помощи классификации выражений языка по разновидностям вычисляемых ими значений» — Пирс, «Типы в языках программирования».

Двоеточие используется для указания, что данный терм принадлежит определённому типу. Например, $t:T$. Терм считается корректно типизированным (или типизируемым), если существует такой тип, для которого верно выражение $t:T$. Как у нас были правила вычисления, так здесь имеются правила типизации. Они тоже часто определяются в стиле правил вывода, а их названия могут начинаться с префикса ‘T-‘. Например (T-IF):

$\frac{t_1:\mathrm{Bool}\ \ t_2:\mathrm{T}\ \ t_3:\mathrm{T}}{\mathrm{if}\ t_1 \ \mathrm{then}\ t_2\ \mathrm{else}\ t_3\ : \ \mathrm{T}}$


Такое следует читать как «Поскольку терм 1 принадлежит типу Bool, а термы 2 и 3 принадлежат типу T, то терм “if term 1 then term 2 else term 3” будет принадлежать типу T».

В функциях (лямбда-абстракциях) мы тоже следим за типами аргумента и возвращаемого значения. Можно аннотировать связанные переменные, указав их тип, так что вместо простого $\lambda x.t$ можно написать $\lambda x:\mathrm{T_1} . t_2$. Тип лямбда-абстракции (для функции с одним аргументом) записывается как $\mathrm{T_1}\ \rightarrow\ \mathrm{T_2}$. Это означает, что функция принимает аргумент типа $\mathrm{T_1}$ и возвращает результат типа $\mathrm{T_2}$.

В правилах вывода вы увидите знак выводимости — оператор в виде турникета $\vdash$. Значит, $P \vdash Q$ следует читать как «Из P можно вывести Q» или как «P подразумевает Q». Например, $x:\mathrm{T_1} \vdash t_2 : \mathrm{T_2}$ означает «Из того факта, что x принадлежит типу T1, следует, что тип t2 принадлежит типу T2».

Следует отслеживать привязку переменных к типам для свободных переменных в функции. Для этого мы используем контекст типизации (окружение типизации). Представьте его как знакомое вам окружение, которое транслирует названия переменных в значения, но только здесь мы транслируем названия переменных в типы. Согласно конвенции, для указания контекста типизации используется символ гаммы ($\Gamma$). Он часто встречается в научных статьях без объяснений, по конвенции. Я запомнил его значение, представив виселицу, фиксирующую переменные с их типами, свисающими на верёвке. Но у вас может быть и другой способ! Это приводит к часто встречаемому тройственному соотношению в виде $\Gamma \vdash t : \mathrm{T}$. Его следует читать так: «Из контекста типизации $\Gamma$ следует, что терм t принадлежит типу T». Оператор в виде запятой расширяет $\Gamma$ путём добавления новой привязки справа (например, $\Gamma, x:\mathrm{T}$).

Объединив это всё, вы получаете правила, которые выглядят как это (в данном случае, для определения типа лямбда-абстракции):

$\frac{\Gamma, x : \mathrm{T_1} \vdash t_2 : \mathrm{T_2}}{\Gamma \vdash \lambda x:\mathrm{T-1}.t_2 : \mathrm{T_1} \rightarrow \mathrm{T_2}}$


Расшифруем правило: «Если (то, что указано в числителе) из контекста типизации с ограничением x до T1 следует, что t2 принадлежит типу T2, то (часть, указанная в знаменателе) в том же контексте типизации выражение $\lambda x:\mathrm{T_1}.t_2$ принадлежит типу $\mathrm{T_1} \rightarrow \mathrm{T_2}$».

Типобезопасность


Если бы Джейн Остин писала книгу о системах типов, наверное она бы назвала её «Продвижение и сохранение» (на самом деле я думаю, что можно написать много интересных эссе с таким названием!). Система типов считается «безопасной» (типобезопасной), если правильно типизированные термы никогда не оказываются в тупике в процессе вычисления. На практике это означает, что в цепочке правил вывода мы никогда не застрянем где-то без окончательного значения и в то же время без возможности применить правило для дальнейшего продвижения (вы увидите, что авторы употребляют фразы «застрять» и «оказаться в тупике» — именно это они имеют в виду). Для демонстрации, что правильно типизированные термы никогда не окажутся в тупике, достаточно доказать теоремы продвижения и сохранения.

  • Продвижение. Правильно типизированный терм не может быть тупиковым (либо это значение, либо он может проделать следующий шаг в соответствии с правилами вычисления).
  • Сохранение. Если правильно типизированный терм проделывает шаг вычисления, то получающийся терм также правильно типизирован.

Иногда вы увидите, что авторы говорят о продвижении и сохранении, не указывая явно, почему это важно. Теперь вы знаете, почему!

Чёрч, Карри, Говард, Хоар


Вот ещё пару вещей, которые вам могут встретиться и о которых интересно знать:

  • В определении языка по стилю Карри сначала мы задаём грамматику термов, затем определяем их поведение, и наконец добавляем систему типов, «отвергающую некоторые термы, поведение которых нам не нравится». Семантика возникает раньше, чем типизация.
  • В определении языка по стилю Чёрча, типизация идёт прежде семантики, так что мы никогда не задаём вопрос, каково поведение неверно типизированного терма.
  • Соответствие Карри — Говарда — это соответствие между теорией типов и логикой, в которой логические утверждения рассматриваются как типы в системе типов. (аналогия «утверждения как типы»). Это соответствие можно использовать для переноса результатов из одной области в другую (например, из линейной логикой в систему линейных типов).
  • Логика Хоара или тройки Хоара относятся к выражениям вида {P}C{Q}. Такое следует читать как «Если предусловие P истинно, то выполняется команда C (и если она завершается), а постусловие Q будет истинным».

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