Теперь рассмотрим тип переменной. Если типовая среда {x: τ} указывает, что переменная x имеет тип τ, то это будет записано как:
Типовая среда Γ, содержащая x: τ, будет записана как:
Новая запись для правил:
Для описания правил типизации в книге будет использоваться следующая запись. Если выполняются условия A1, A2, …, An, то выполняется правило A0. Это будет записано как:
С помощью этой записи мы будем определять типовые правила для различных выражений в нашем языке.
Определение правил типизации
Теперь давайте определим правила типизации для нашего собственного языка программирования.
Если в типовой среде Γ выражение 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, который известен своей мощной системой вывода типов. Рассмотрим определение функции для сложения:
Когда эта функция вводится в интерпретатор Standard ML of New Jersey (SML/NJ) [3], система типов автоматически выводит, что функция add принимает два аргумента типа int и возвращает значение типа int.