что нужно рассмотреть, это смысл вычислений.
Существует множество типов семантики для вычислений, такие как операционная [1] семантика и денотационная [1] семантика. Однако в нашем случае мы не будем углубляться в подробности этих подходов, а сосредоточимся на том, что означают базовые команды.
Начнем с вычислительных выражений. Мы будем реализовывать операции сложения (+), вычитания (-), умножения (*) и деления (/). Сравнение будет ограничено проверкой на равенство (==), которая проверяет, равны ли значения слева и справа.
Присваивание переменной означает, что в переменную записывается заданное значение.
Оператор if оценивает условие: если оно истинно, выполняется инструкция в ветке then, если ложно – инструкция в ветке else (если она есть).
Оператор print выводит результат вычисления заданного выражения.
Для этого вычисления мы ограничиваемся такими простыми определениями на уровне естественного языка. Более глубокое определение семантики будет рассмотрено в другой книге, и я буду рад, если в будущем появится возможность подробно изложить этот процесс.
1.1.2 Типы
В проектировании языка концепция типов является крайне важной. Почти все языки программирования, которые приходят на ум, включают концепцию типов. Почему же эта концепция была введена и стала широко использоваться? Для более подробного объяснения можно обратиться к книгам, таким как «Введение в системы типов» [2], но здесь мы кратко рассмотрим концепцию типов.
Роль типов заключается в том, чтобы классифицировать значения, с которыми работает программа. В большинстве языков программирования значению 1 будет присвоен тип, означающий целое число, например, integer или int.
Типы также выполняют роль гарантии правильности вычислений, основываясь на этой классификации.
Например, результат сложения двух целых чисел всегда будет целым числом. Это гарантирует, что операция сложения, выполненная для двух целых чисел, всегда даст результат в виде целого числа. Если же попытаться сложить целое число и строку, то это будет некорректной операцией, и система типов сгенерирует ошибку (хотя в некоторых языках, таких как JavaScript, возможно явное или неявное преобразование типов).
Правила типов
Как же определяются правила типов?
Давайте рассмотрим, как можно определить правила для типов и какие типы присваиваются выражениям.
Запись и значение правил типов
Для записи правил типов в этой книге будет использоваться следующая запись если у выражения e тип τ, то это записывается как:
e:τ
Кроме того, для анализа типа выражений, которые содержат переменные, может потребоваться сделать предположения о типах этих переменных. Такие
предположения называют типовой средой. Для выражения e, чьё типовое предположение в среде Γ равно τ, запись будет выглядеть как:
Γ ⊢ e:τ
Пример:
Рассмотрим