⊢ 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]. Этот алгоритм играет центральную роль в определении типов переменных и выражений, позволяя находить наименьшую общую подстановку (унификатор) для двух выражений или устанавливать, что такая подстановка невозможна. Он стал основой для логического программирования, например, в языке Prolog, а также для автоматических систем вывода в искусственном интеллекте, и может быть полезен при проектировании нашего собственного языка.
Как работает алгоритм унификации?
Алгоритм унификации Робинсона анализирует два терма (выражения или типовые конструкции) и пытается найти такую