Читать книгу Введение в разработку собственного языка и компилятора. Создаем на Rust! - Андрей Невский - Страница 6

В проектировании языка концепция типов является крайне важной. Почти все языки программирования, которые приходят на ум, включают концепцию типов. Почему же эта концепция была введена и стала широко использоваться? Для более подробного объяснения можно обратиться к книгам, таким как «Введение в системы типов» [2], но здесь мы кратко рассмотрим концепцию типов.

Роль типов заключается в том, чтобы классифицировать значения, с которыми работает программа. В большинстве языков программирования значению 1 будет присвоен тип, означающий целое число, например, integer или int.

Типы также выполняют роль гарантии правильности вычислений, основываясь на этой классификации.

Например, результат сложения двух целых чисел всегда будет целым числом. Это гарантирует, что операция сложения, выполненная для двух целых чисел, всегда даст результат в виде целого числа. Если же попытаться сложить целое число и строку, то это будет некорректной операцией, и система типов сгенерирует ошибку (хотя в некоторых языках, таких как JavaScript, возможно явное или неявное преобразование типов).

Правила типов

Как же определяются правила типов?

Давайте рассмотрим, как можно определить правила для типов и какие типы присваиваются выражениям.

Запись и значение правил типов

Для записи правил типов в этой книге будет использоваться следующая запись если у выражения e тип τ, то это записывается как:

e:τ

Кроме того, для анализа типа выражений, которые содержат переменные, может потребоваться сделать предположения о типах этих переменных. Такие

предположения называют типовой средой. Для выражения 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 находится такая замена, что, применяя её к этим терминам, мы получаем одинаковые термины.