Типизация с выводом типов
Типизация с выводом типов (type inference) – это процесс, при котором типы, явно не указанные в выражении, выводятся на основе контекста и других выражений.
Это позволяет уменьшить количество явных указаний типов в программе, что делает код короче и чище.
В качестве примера рассмотрим язык Standard ML, который известен своей мощной системой вывода типов. Рассмотрим определение функции для сложения:
Когда эта функция вводится в интерпретатор 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 находится такая замена, что, применяя её к этим терминам, мы получаем одинаковые термины.
Одним из ключевых инструментов для реализации системы вывода типов является алгоритм унификации, предложенный Джоном А. Робинсоном в 1965 году [5]. Этот алгоритм играет центральную роль в определении типов переменных и выражений, позволяя находить наименьшую общую подстановку (унификатор) для двух выражений или устанавливать, что такая подстановка невозможна. Он стал основой для логического программирования, например, в языке Prolog, а также для автоматических систем вывода в искусственном интеллекте, и может быть полезен при проектировании нашего собственного языка.
Как работает алгоритм унификации?
Алгоритм унификации Робинсона анализирует два терма (выражения или типовые конструкции) и пытается найти такую подстановку, которая сделает их идентичными. Процесс выполняется пошагово следующим образом:
• Разбор на подвыражения: Алгоритм разбивает входные термы на их составные части, такие как функции, переменные и константы, чтобы сравнить их структуру.
• Пошаговая унификация: Алгоритм последовательно проверяет термы и переменные, начиная с их корневых элементов. Если термы имеют одинаковую структуру (например, оба являются вызовами функции с одинаковым именем), унификация продолжается для их аргументов.
• Применение подстановок: Если в одном терме встречается переменная, а в другом – конкретное значение, алгоритм заменяет переменную этим значением. Например, если у нас есть переменная X и значение a, подстановка X -> a применяется ко всем вхождениям Х.
• Проверка совместимости: Алгоритм оценивает, можно ли сделать термы идентичными с помощью подстановок. Если подстановка успешно приводит к равенству термов, унификация завершается успешно. Если же обнаруживается противоречие, процесс завершается с ошибкой.
Рассмотрим пример унификации двух термов:
