предположения называют типовой средой. Для выражения e, чьё типовое предположение в среде Γ равно τ, запись будет выглядеть как:
Γ ⊢ e:τ
Пример:
Рассмотрим выражение 1. В языке, который мы проектируем, числа будут иметь тип int. Следовательно, тип этого выражения будет записан как:
1: int
Теперь рассмотрим тип переменной. Если типовая среда {x: τ} указывает, что переменная x имеет тип τ, то это будет записано как:
{x: τ} ⊢ x: τ
Типовая среда Γ, содержащая x: τ, будет записана как:
Γ ⊢ x: τ
Новая запись для правил:
Для описания правил типизации в книге будет использоваться следующая запись. Если выполняются условия A1, A2, …, An, то выполняется правило A0. Это будет записано как:
A₁, A₂, …, Aₙ
A₀
С помощью этой записи мы будем определять типовые правила для различных выражений в нашем языке.
Определение правил типизации
Теперь давайте определим правила типизации для нашего собственного языка программирования.
Если в типовой среде Γ выражение e1 имеет тип int, а выражение e2 имеет тип int, то тип выражения a + b также будет int. Это можно записать следующим образом:
Γ ⊢ e1:int Γ ⊢ e2:int
Γ ⊢ e1+e2: int
Аналогично, для выражения e1 – e2 тип также будет int:
Γ ⊢ e1:int Γ⊢e2:int
int Γ ⊢e1 – e2: int
Для умножения e1 * e2
Γ ⊢ e1:int Γ⊢e2:int
Γ ⊢ e1 ∗ e2: int
Для деления e1 / e2
Γ ⊢ e1:int Γ⊢e2:int
Γ ⊢ e1 / e2: int
Теперь рассмотрим оператор сравнения на равенство. Мы будем использовать оператор == для проверки равенства целых чисел, и его тип будет bool. Это можно записать так:
Γ ⊢ e1:int Γ⊢e2:int
Γ ⊢ e1 == e2: int
Таким образом, мы можем типизировать основные выражения для арифметики и сравнения.
Пример:
Предположим, что у нас есть выражение x == (1 +2). Типовое заключение будет следующим:
1. Выражение 1 имеет тип int.
2. Выражение 2 имеет тип int.
3. В типовой среде Γ переменная x имеет тип int.
4. Выражение 1 + 2 имеет тип int.
5. Следовательно, выражение x == (1 + 2) будет иметь тип bool.
Это можно записать как (пример 1):
пример 1
Типизация с выводом типов
Типизация с выводом типов (type inference) – это процесс, при котором типы, явно не указанные в выражении, выводятся на основе контекста и других выражений.
Это позволяет уменьшить количество явных указаний типов в программе, что делает код короче и чище.
В качестве примера рассмотрим язык Standard ML, который известен своей мощной системой вывода типов. Рассмотрим определение функции для сложения:
fun add a b = a + b;
Когда эта функция вводится в интерпретатор Standard ML of New Jersey (SML/NJ) [3], система типов автоматически выводит, что функция add принимает два аргумента типа int и возвращает значение типа int.
val add = fn: int -> int -> int
Это означает, что функция add принимает два аргумента типа int и возвращает значение типа int. В Standard ML функции каррируются, то есть, int -> int -> int эквивалентно int -> (int -> int).
Этот вывод типов позволяет понять, как система типов может автоматически определить типы аргументов и результата, даже если они явно не были указаны в коде.
Вопрос для размышления:
Хотя человеку достаточно просто понять, как работает вывод типов, как именно компьютер выполняет этот процесс и какие алгоритмы используются для вычисления вывода типов в таких языках, как Standard ML?
Вывод типов
Основной подход в выводе типов заключается в том, чтобы заменить неизвестные типы переменными типов и решить типовые уравнения.
Унификация – это процесс, при котором для двух терминов s и t находится такая замена, что, применяя её к этим терминам, мы получаем одинаковые термины.
1.1.3 Унификация
Одним из ключевых инструментов для реализации системы вывода типов является алгоритм унификации, предложенный Джоном А. Робинсоном в 1965 году [5]. Этот алгоритм играет центральную роль в определении типов переменных и выражений, позволяя находить наименьшую общую подстановку (унификатор) для двух выражений или устанавливать, что такая подстановка невозможна. Он стал основой для логического программирования, например, в языке