![](https://habrastorage.org/getpro/habr/upload_files/70e/c8e/32b/70ec8e32b05b92b1b60da05835596cf7.png)
Если вы пишете свой язык программирования, то вы наверное слышали о type inference. В этом цикле статей, без лишней теории, мы наглядно разберем как это работает и реализуем свой на Rust.
Что такое type inference?
Type inference в контексте компиляторов - это стадия компиляции, в которой компилятор определяет типы для выражений. Type inference в основном присущ функциональным языкам, но и другие группы языков тоже могут его реализовывать.
Разбираем алгоритм
Дисклеймер: Здесь будет минимум теории и некоторые термины и определения могут быть не использованы.
Перед тем как производить анализ типов, нашему компилятору нужно спарсить наш исходник.
![](https://habrastorage.org/getpro/habr/upload_files/24b/1d6/7e9/24b1d67e92704d11b586b699bfe5f770.png)
Задача же type inference понять какие типы у выражений и name binding-гов в AST или HIR:
![](https://habrastorage.org/getpro/habr/upload_files/8ee/db3/6e6/8eedb36e679184fa1b9d0921e898643d.png)
В этой статье мы не будем напрямую представлять код в виде абстрактного синтаксического дерева (чтобы было проще понимать примеры), поэтому результат type inference мы будем визуализировать как-то так:
![](https://habrastorage.org/getpro/habr/upload_files/556/f28/49c/556f2849c31f96c4951f8d1883372297.png)
Представим, что у нас есть код на гипотетическом языке программирования, для которого мы хотим реализовать вывод типов:
![](https://habrastorage.org/getpro/habr/upload_files/2ed/72b/f39/2ed72bf39a0b71b4cc8d2fcf46441a2e.png)
Так как в сигнатуре функции типы не указаны, нам придется определять их самим. Первое, что нам нужно сделать это создать переменные типов:
![](https://habrastorage.org/getpro/habr/upload_files/94d/7ce/0ea/94d7ce0eadd614f26699a7c4561c5c06.png)
Переменная типа — в данном случае обозначает тип, которой мы еще не определили.
Для простоты и наглядности допустим что, сигнатура оператора +
это: (int, int) -> int
. Тогда, из a + 1
следует, что тип параметра a
должен быть int
и тип выражения 1
тоже должен быть int
. А так как a + 1
равно int
и является возвращаемым значением функции inc
, то возвращаемое значение функции это int
. Таким образом, мы получили информацию об взаимоотношениях между типами или type constraint-ы.
![](https://habrastorage.org/getpro/habr/upload_files/590/6bf/f27/5906bff2736c5525419833b2b4aaca69.png)
Type constraint - проще говоря, это способ записывать информацию о взаимоотношениях между типами.
Здесь мы используем равенство, но могли и использовать знаки неравенства, для обозначения других взаимоотношений между типами, например для численных типов (что мы в этой статье делать не будем).
Теперь когда мы имеем список этих самых взаимоотношений, мы можем узнать значения переменных типов, это называется - unification (унификация). Суть в том, чтобы из системы уравнений, которая является списком type constraint-ов получить так называемые замены (substitutions) - это как бы решения системы уравнений из type constraint-ов:
![](https://habrastorage.org/getpro/habr/upload_files/203/e65/c8e/203e65c8e24008818eda85d4bc46dfc7.png)
Таким образом подставляя значения переменных типов мы получим долгожданный результат!
У читателей мог возникнуть вопрос, что произойдет если у уравнения нет решения? Ответ прост - ошибка mismatched types. Например:
![](https://habrastorage.org/getpro/habr/upload_files/611/583/b05/611583b0531c7702b3af90ec49308746.png)
Так как String
не может быть равен int
, type constraint не соблюден и уравнение не имеет решений. Тогда мы можем увидеть ошибку mismatched types:
![Пример ошибки компилятора Rust-а - rustc Пример ошибки компилятора Rust-а - rustc](https://habrastorage.org/getpro/habr/upload_files/677/23b/7b0/67723b7b0e822c7a510aecccf97c160c.png)
Возьмем пример поинтереснее:
![](https://habrastorage.org/getpro/habr/upload_files/f8d/a3c/f88/f8da3cf887a038d21a084783a27b03b0.png)
Сначала, как в прошлом примере разметим переменные типов для имен и сигнатуры функции:
![](https://habrastorage.org/getpro/habr/upload_files/9b0/c0b/6df/9b0c0b6dff12f1f00144755d4d21a90f.png)
Теперь посмотрим на место где мы объявляем a
- мы создаем пустой массив. Мы можем использовать переменную типа, для того чтобы обозначать тип элементов массива:
![](https://habrastorage.org/getpro/habr/upload_files/0e3/8d8/59a/0e38d859affa9e01d99242bfd2d513b0.png)
Идем дальше:
![](https://habrastorage.org/getpro/habr/upload_files/afb/9e6/b6b/afb9e6b6ba0795e1ae7a554a31ddf142.png)
Предположим, что операторы <
и ++
работает только со значениями типа int
. Так, что у нас есть 3 новых constraint-а.
Продолжим:
![](https://habrastorage.org/getpro/habr/upload_files/7ef/3ac/42b/7ef3ac42bc5893678c699ca294706f78.png)
Для дженерика T
в метода списка insert
нам нужна еще одна переменная типа - ?6
.
И самое последнее:
![](https://habrastorage.org/getpro/habr/upload_files/0a9/640/0b1/0a96400b143c0d6c5de32327efcef96c.png)
Возвращаемое значение функции это a
, значит что ?3 = ?2
.
Таким образом получаем систему type constraint-ов:
![](https://habrastorage.org/getpro/habr/upload_files/6c2/f90/ec8/6c2f90ec88bcd0a32bbde450e9074c4a.png)
И снова, с помощью алгоритма унификации, мы можем решить данную систему уравнений и получить:
![](https://habrastorage.org/getpro/habr/upload_files/2c6/ccb/e0a/2c6ccbe0ade983ed91d81dd17185ea6c.png)
Подставив эти типы получим результат type inference:
![](https://habrastorage.org/getpro/habr/upload_files/462/163/9a7/4621639a72ffcbcb68df238e741de900.png)
Теперь возможно у читателя появился вопрос, как работает этот загадочный алгоритм унификации который решает систему уравнений из type constraint-ов? Сейчас мы это разберем!
Unification algorithm (Алгоритм унификации)
Сначала напишем представление типов в нашем языке:
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
enum Type {
Constructor(TypeConstructor),
Variable(TypeVariable),
}
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
struct TypeConstructor {
name: String,
generics: Vec<Arc<Type>>,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
struct TypeVariable(usize);
То есть:
int
этоTypeConstructor { name: "int", generics: Vec::new() }
.List<int>
этоTypeConstructor { name: "List", generics: vec![ TypeConstructor { name: "int", generics: vec![] } ] }
.?1
этоTypeVariable(1)
.
Теперь мы можем преступать к реализации алгоритма унификации:
fn unify(left: Arc<Type>, right: Arc<Type>,
substitutions: &mut HashMap<TypeVariable, Arc<Type>>) {
match (left.as_ref(), right.as_ref()) {
Если оба типа это type constructor-ы, то тогда проверяем то, что они равны и унифицируем их generic-и:
(
Type::Constructor(TypeConstructor {
name: name1,
generics: generics1,
}),
Type::Constructor(TypeConstructor {
name: name2,
generics: generics2,
}),
) => {
assert_eq!(name1, name2);
assert_eq!(generics1.len(), generics2.len());
for (left, right) in zip(generics1, generics2) {
unify(left.clone(), right.clone(), substitutions);
}
}
Например из:
Array<int> = Array<?1>
Следует, что:
int = ?1
Если же мы получаем два разных type constructor-а, то тогда у нас type mismatch:
Array<?2> != Option<?3>
Если обе стороны это равные переменные типов, то тогда все хорошо и мы ничего не делаем:
(Type::Variable(TypeVariable(i)),
Type::Variable(TypeVariable(j))) if i == j => {}
Если же нет, то тогда мы добавляем значение переменной в хранилище и, что важно проверяем не создали ли мы бесконечный тип.
(_, Type::Variable(v @ TypeVariable(..))) => {
if let Some(substitution) = substitutions.get(&v) {
unify(left, substitution.clone(), substitutions);
return;
}
assert!(!v.occurs_in(left.clone(), substitutions));
substitutions.insert(*v, left);
}
(Type::Variable(v @ TypeVariable(..)), _) => {
if let Some(substitution) = substitutions.get(&v) {
unify(right, substitution.clone(), substitutions);
return;
}
assert!(!v.occurs_in(right.clone(), substitutions));
substitutions.insert(*v, right);
}
Пример, случая когда мы пытаемся использовать бесконечный тип в Rust-е:
![Ошибка компилятора Rust-а - rustc Ошибка компилятора Rust-а - rustc](https://habrastorage.org/getpro/habr/upload_files/87e/d42/ce6/87ed42ce6f68fbc5a37c39063d8f2de1.png)
В данном примере generic в push - T
, его значение равно типу a.to_vec()
, то есть Vec<T>
. Получаем T = Vec<T>
. Единственное возможное решение для данного type constraint-а это: Vec<Vec<Vec<Vec<Vec<Vec<Vec<....>>>>>>>
. Конечно есть языки которые это позволяют, но в данном случае для простоты и во избежании проблем, такие типы мы не будем принимать.
Реализуем occurs_in
, который проверяет присутствует ли тип в generic аргументах другого если тот конструктор, или равен ему если он переменная:
impl TypeVariable {
fn occurs_in(&self, ty: Arc<Type>,
substitutions: &HashMap<TypeVariable, Arc<Type>>) -> bool {
match ty.as_ref() {
Type::Variable(v @ TypeVariable(i)) => {
if let Some(substitution) = substitutions.get(&v) {
if substitution.as_ref() != &Type::Variable(*v) {
return self.occurs_in(substitution.clone(), substitutions);
}
}
self.0 == *i
}
Type::Constructor(TypeConstructor { generics, .. }) => {
for generic in generics {
if self.occurs_in(generic.clone(), substitutions) {
return true;
}
}
false
}
}
}
}
Также создадим функцию, которая будет рекурсивно проходится, по нашему хранилищу значений переменных типа, чтобы их полностью убрать, то есть например:
?1 = ?2
?2 = ?3
?3 = int
substitute(?1) = substitute(?2) = substitute(?3) = int
impl Type {
fn substitute(&self, substitutions: &HashMap<TypeVariable, Arc<Type>>) -> Arc<Type> {
match self {
Type::Constructor(TypeConstructor { name, generics }) => {
Arc::new(Type::Constructor(TypeConstructor {
name: name.clone(),
generics: generics
.iter()
.map(|t| t.substitute(substitutions))
.collect(),
}))
}
Type::Variable(TypeVariable(i)) => {
if let Some(t) = substitutions.get(&TypeVariable(*i)) {
t.substitute(substitutions)
} else {
Arc::new(self.clone())
}
}
}
}
}
Мы это сделали, мы написали алгоритм унификации! Проверим его на практике! Помните предыдущий пример?
![](https://habrastorage.org/getpro/habr/upload_files/0c4/df6/deb/0c4df6debe1c3128d92284df9650c6f3.png)
Перед тем, как его симулировать, напишем два макроса:
Первый макрос, будет коротко генерировать переменную типа:
macro_rules! tvar {
($i:literal) => {
Arc::new(Type::Variable(TypeVariable($i)))
};
}
Второй макрос, будет коротко генерировать конструктор типа:
macro_rules! tconst {
($name:literal, $($generic:expr),*) => {
Arc::new(Type::Constructor(TypeConstructor {
name: $name.to_owned(),
generics: vec![$($generic),*],
}))
};
($name:literal) => { tconst!($name,) };
}
Теперь просимулируем наш предыдущий пример на нашей реализации алгоритма унификации:
fn main() {
let mut substitutions = HashMap::new();
unify(tvar!(3), tconst!("Array", tvar!(5)), &mut substitutions);
unify(tvar!(4), tconst!("int"), &mut substitutions);
unify(tvar!(4), tvar!(1), &mut substitutions);
unify(tvar!(4), tconst!("int"), &mut substitutions);
unify(tvar!(3), tconst!("Array", tvar!(6)), &mut substitutions);
unify(tvar!(6), tvar!(4), &mut substitutions);
unify(tvar!(3), tvar!(2), &mut substitutions);
for i in 1..=6 {
println!(
"{}: {:?}",
i,
Type::Variable(TypeVariable(i)).substitute(&substitutions)
);
}
}
Получаем вывод:
1: Constructor(TypeConstructor { name: "int", generics: [] })
2: Constructor(TypeConstructor { name: "Array", generics: [Constructor(TypeConstructor { name: "int", generics: [] })] })
3: Constructor(TypeConstructor { name: "Array", generics: [Constructor(TypeConstructor { name: "int", generics: [] })] })
4: Constructor(TypeConstructor { name: "int", generics: [] })
5: Constructor(TypeConstructor { name: "int", generics: [] })
6: Constructor(TypeConstructor { name: "int", generics: [] })
В следующей статье, мы начнем писать свой маленький язык программирования и начнем определять типы простых выражений таких как литералы или массивы!