Неделю назад я пошутил, что статьи по принципам языков программирования POPL должны соответствовать критерию «интеллектуального запугивания», чтобы их принимали для публикации. Конечно, это неправда, но факт в том, что статьи по языкам программирования выглядят особенно устрашающе для специалистов-практиков (или академик действительно работает в другой области компьютерных наук!). Они битком набиты математическими символами и такими фразами как «суждения», «операционная семантика» и тому подобное. Там много тонких вариантов записи, но вы можете в основном уловить суть статьи, усвоив несколько базовых понятий. Так что вместо рассказа об очередной научной статье я подумал, что сегодня лучше напишу краткое практическое руководство по расшифровке научных статей на тему языков программирования. Здесь я следую книге Бенджамина Пирса «Типы в языках программирования» в качестве авторитетного источника.
Начнём с понятного: синтаксис. Синтаксис говорит, какие предложения можно использовать в языке (т. е. какие программы мы можем писать). Синтаксис содержит набор термов, которые представляют собой строительные блоки. Возьмём следующий пример из Пирса:
Всюду, где встречается символ
,
). Множество всех термов часто обозначается как
. Его не следует путать с символом
, который традиционно используется для обозначения типов.
В вышеприведённом примере обратите внимание, что сам по себе оператор
Термы — это выражения, которые можно вычислить, и конечным результатом вычисления в правильно построенном окружении должно стать значение. Значения — это подмножество термов. В вышеприведённом примере значениями являются
Мы хотим придать какое-то значение термам языка. Это семантика. Существуют различные способы определить значение программ. Чаще всего вы встретите упоминания операционной семантики и денотационной семантики. Из них операционная семантика наиболее распространённая. Она определяет значение программы, устанавливая правила для абстрактной машины, которая вычисляет термы. Спецификации имеют форму набора правил вычисления — рассмотрим их чуть позже. В этом мировоззрении значение (смысл) терма
Вы можете также столкнуться с тем, что авторы упоминают операционную семантику с малым шагом (small-step) и операционную семантику с большим шагом (big-step). Как следует из названия, это относится к тому, насколько большой скачок делает абстрактная машина с каждым применяемым правилом. В семантике с малым шагом термы переписываются постепенно, по одному маленькому шагу за раз, пока в конечном итоге не станут значениями. В семантике с большим шагом (она же «естественная семантика») мы можем перейти от терма к его окончательному значению за один шаг.
В записи семантики с малым шагом вы увидите что-нибудь такое:
, что следует читать так, что
вычисляется в
. (Вместо подстрочных индексов могут использоваться штрихи, например,
). Это также известно как суждение (judgement). Стрелка
представляет один шаг вычислений. Если вам встретится
, то это значит «после многократного применения одношаговых вычислений
в конечном итоге перешёл в
».
В семантике с большим шагом используется другая стрелка. Так что
означает, что терм
в результате вычисления перешёл в
. Если в одном и том же языке используется семантика с малым шагом и семантика с большим шагом, то
и
означают одно и то же.
Согласно конвенции, правила именуются ПРОПИСНЫМИ буквами. И если вам повезёт, то авторы добавят к правилам вычисления префикс ‘E-‘ как дополнительную подсказку.
Например:
if true then t2 else t3
t2 (E-IFTRUE)
Обычно правила вычисления задают в стиле правил вывода (inference rules). Пример (E-IF):
Это следует читать как «С учётом указанного в делителе мы можем сделать вывод о том, что находится в знаменателе». То есть в данном конкретном примере: «Если
выводится в
, то в этом случае
выводится в
.
В языке программирования не обязательно должна быть определённая система типов (он может быть нетипизированным), но у большинства она есть.
Двоеточие используется для указания, что данный терм принадлежит определённому типу. Например,
. Терм считается корректно типизированным (или типизируемым), если существует такой тип, для которого верно выражение
. Как у нас были правила вычисления, так здесь имеются правила типизации. Они тоже часто определяются в стиле правил вывода, а их названия могут начинаться с префикса ‘T-‘. Например (T-IF):
Такое следует читать как «Поскольку терм 1 принадлежит типу Bool, а термы 2 и 3 принадлежат типу T, то терм “if term 1 then term 2 else term 3” будет принадлежать типу T».
В функциях (лямбда-абстракциях) мы тоже следим за типами аргумента и возвращаемого значения. Можно аннотировать связанные переменные, указав их тип, так что вместо простого
можно написать
. Тип лямбда-абстракции (для функции с одним аргументом) записывается как
. Это означает, что функция принимает аргумент типа
и возвращает результат типа
.
В правилах вывода вы увидите знак выводимости — оператор в виде турникета
. Значит,
следует читать как «Из P можно вывести Q» или как «P подразумевает Q». Например,
означает «Из того факта, что x принадлежит типу T1, следует, что тип t2 принадлежит типу T2».
Следует отслеживать привязку переменных к типам для свободных переменных в функции. Для этого мы используем контекст типизации (окружение типизации). Представьте его как знакомое вам окружение, которое транслирует названия переменных в значения, но только здесь мы транслируем названия переменных в типы. Согласно конвенции, для указания контекста типизации используется символ гаммы (
). Он часто встречается в научных статьях без объяснений, по конвенции. Я запомнил его значение, представив виселицу, фиксирующую переменные с их типами, свисающими на верёвке. Но у вас может быть и другой способ! Это приводит к часто встречаемому тройственному соотношению в виде
. Его следует читать так: «Из контекста типизации
следует, что терм t принадлежит типу T». Оператор в виде запятой расширяет
путём добавления новой привязки справа (например,
).
Объединив это всё, вы получаете правила, которые выглядят как это (в данном случае, для определения типа лямбда-абстракции):
Расшифруем правило: «Если (то, что указано в числителе) из контекста типизации с ограничением x до T1 следует, что t2 принадлежит типу T2, то (часть, указанная в знаменателе) в том же контексте типизации выражение
принадлежит типу
».
Если бы Джейн Остин писала книгу о системах типов, наверное она бы назвала её «Продвижение и сохранение» (на самом деле я думаю, что можно написать много интересных эссе с таким названием!). Система типов считается «безопасной» (типобезопасной), если правильно типизированные термы никогда не оказываются в тупике в процессе вычисления. На практике это означает, что в цепочке правил вывода мы никогда не застрянем где-то без окончательного значения и в то же время без возможности применить правило для дальнейшего продвижения (вы увидите, что авторы употребляют фразы «застрять» и «оказаться в тупике» — именно это они имеют в виду). Для демонстрации, что правильно типизированные термы никогда не окажутся в тупике, достаточно доказать теоремы продвижения и сохранения.
Иногда вы увидите, что авторы говорят о продвижении и сохранении, не указывая явно, почему это важно. Теперь вы знаете, почему!
Вот ещё пару вещей, которые вам могут встретиться и о которых интересно знать:
На самом деле я просто заинтересованное постороннее лицо, которое наблюдает за тем, что происходит в сообществе. Если вы читаете это в качестве эксперта по языкам программирования, и знаете больше вещей, которые следует включить в шпаргалку практикующего специалиста, пожалуйста, сообщите в комментариях!
Синтаксис
Начнём с понятного: синтаксис. Синтаксис говорит, какие предложения можно использовать в языке (т. е. какие программы мы можем писать). Синтаксис содержит набор термов, которые представляют собой строительные блоки. Возьмём следующий пример из Пирса:
t ::=
true
false
if t then t else t
0
succ t
pred t
iszero t
Всюду, где встречается символ
t
, можно подставить любой терм. Если в статье упоминаются термы, то часто используется 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). Как следует из названия, это относится к тому, насколько большой скачок делает абстрактная машина с каждым применяемым правилом. В семантике с малым шагом термы переписываются постепенно, по одному маленькому шагу за раз, пока в конечном итоге не станут значениями. В семантике с большим шагом (она же «естественная семантика») мы можем перейти от терма к его окончательному значению за один шаг.
В записи семантики с малым шагом вы увидите что-нибудь такое:
В семантике с большим шагом используется другая стрелка. Так что
Согласно конвенции, правила именуются ПРОПИСНЫМИ буквами. И если вам повезёт, то авторы добавят к правилам вычисления префикс ‘E-‘ как дополнительную подсказку.
Например:
if true then t2 else t3
Обычно правила вычисления задают в стиле правил вывода (inference rules). Пример (E-IF):
Это следует читать как «С учётом указанного в делителе мы можем сделать вывод о том, что находится в знаменателе». То есть в данном конкретном примере: «Если
Типы
В языке программирования не обязательно должна быть определённая система типов (он может быть нетипизированным), но у большинства она есть.
«Система типов — это гибко управляемый синтаксический метод доказательства отсутствия в программе определённых видов поведения при помощи классификации выражений языка по разновидностям вычисляемых ими значений» — Пирс, «Типы в языках программирования».
Двоеточие используется для указания, что данный терм принадлежит определённому типу. Например,
Такое следует читать как «Поскольку терм 1 принадлежит типу Bool, а термы 2 и 3 принадлежат типу T, то терм “if term 1 then term 2 else term 3” будет принадлежать типу T».
В функциях (лямбда-абстракциях) мы тоже следим за типами аргумента и возвращаемого значения. Можно аннотировать связанные переменные, указав их тип, так что вместо простого
В правилах вывода вы увидите знак выводимости — оператор в виде турникета
Следует отслеживать привязку переменных к типам для свободных переменных в функции. Для этого мы используем контекст типизации (окружение типизации). Представьте его как знакомое вам окружение, которое транслирует названия переменных в значения, но только здесь мы транслируем названия переменных в типы. Согласно конвенции, для указания контекста типизации используется символ гаммы (
Объединив это всё, вы получаете правила, которые выглядят как это (в данном случае, для определения типа лямбда-абстракции):
Расшифруем правило: «Если (то, что указано в числителе) из контекста типизации с ограничением x до T1 следует, что t2 принадлежит типу T2, то (часть, указанная в знаменателе) в том же контексте типизации выражение
Типобезопасность
Если бы Джейн Остин писала книгу о системах типов, наверное она бы назвала её «Продвижение и сохранение» (на самом деле я думаю, что можно написать много интересных эссе с таким названием!). Система типов считается «безопасной» (типобезопасной), если правильно типизированные термы никогда не оказываются в тупике в процессе вычисления. На практике это означает, что в цепочке правил вывода мы никогда не застрянем где-то без окончательного значения и в то же время без возможности применить правило для дальнейшего продвижения (вы увидите, что авторы употребляют фразы «застрять» и «оказаться в тупике» — именно это они имеют в виду). Для демонстрации, что правильно типизированные термы никогда не окажутся в тупике, достаточно доказать теоремы продвижения и сохранения.
- Продвижение. Правильно типизированный терм не может быть тупиковым (либо это значение, либо он может проделать следующий шаг в соответствии с правилами вычисления).
- Сохранение. Если правильно типизированный терм проделывает шаг вычисления, то получающийся терм также правильно типизирован.
Иногда вы увидите, что авторы говорят о продвижении и сохранении, не указывая явно, почему это важно. Теперь вы знаете, почему!
Чёрч, Карри, Говард, Хоар
Вот ещё пару вещей, которые вам могут встретиться и о которых интересно знать:
- В определении языка по стилю Карри сначала мы задаём грамматику термов, затем определяем их поведение, и наконец добавляем систему типов, «отвергающую некоторые термы, поведение которых нам не нравится». Семантика возникает раньше, чем типизация.
- В определении языка по стилю Чёрча, типизация идёт прежде семантики, так что мы никогда не задаём вопрос, каково поведение неверно типизированного терма.
- Соответствие Карри — Говарда — это соответствие между теорией типов и логикой, в которой логические утверждения рассматриваются как типы в системе типов. (аналогия «утверждения как типы»). Это соответствие можно использовать для переноса результатов из одной области в другую (например, из линейной логикой в систему линейных типов).
- Логика Хоара или тройки Хоара относятся к выражениям вида {P}C{Q}. Такое следует читать как «Если предусловие P истинно, то выполняется команда C (и если она завершается), а постусловие Q будет истинным».
На самом деле я просто заинтересованное постороннее лицо, которое наблюдает за тем, что происходит в сообществе. Если вы читаете это в качестве эксперта по языкам программирования, и знаете больше вещей, которые следует включить в шпаргалку практикующего специалиста, пожалуйста, сообщите в комментариях!