Реализуем Type inference на Rust — Часть #1: Unification
Если вы пишете свой язык программирования, то вы наверное слышали о type inference. В этом цикле статей, без лишней теории, мы наглядно разберем как это работает и реализуем свой на Rust.
Что такое type inference?
Type inference в контексте компиляторов - это стадия компиляции, в которой компилятор определяет типы для выражений. Type inference в основном присущ функциональным языкам, но и другие группы языков тоже могут его реализовывать.
Разбираем алгоритм
Дисклеймер: Здесь будет минимум теории и некоторые термины и определения могут быть не использованы.
Перед тем как производить анализ типов, нашему компилятору нужно спарсить наш исходник.
Задача же type inference понять какие типы у выражений и name binding-гов в AST или HIR:
В этой статье мы не будем напрямую представлять код в виде абстрактного синтаксического дерева (чтобы было проще понимать примеры), поэтому результат type inference мы будем визуализировать как-то так:
Представим, что у нас есть код на гипотетическом языке программирования, для которого мы хотим реализовать вывод типов:
Так как в сигнатуре функции типы не указаны, нам придется определять их самим. Первое, что нам нужно сделать это создать переменные типов:
Переменная типа — в данном случае обозначает тип, которой мы еще не определили.
Для простоты и наглядности допустим что, сигнатура оператора + это: (int, int) -> int. Тогда, из a + 1 следует, что тип параметра a должен быть int и тип выражения 1 тоже должен быть int. А так как a + 1 равно int и является возвращаемым значением функции inc, то возвращаемое значение функции это int. Таким образом, мы получили информацию об взаимоотношениях между типами или type constraint-ы.
Type constraint - проще говоря, это способ записывать информацию о взаимоотношениях между типами.
Здесь мы используем равенство, но могли и использовать знаки неравенства, для обозначения других взаимоотношений между типами, например для численных типов (что мы в этой статье делать не будем).
Теперь когда мы имеем список этих самых взаимоотношений, мы можем узнать значения переменных типов, это называется - unification (унификация). Суть в том, чтобы из системы уравнений, которая является списком type constraint-ов получить так называемые замены (substitutions) - это как бы решения системы уравнений из type constraint-ов:
Таким образом подставляя значения переменных типов мы получим долгожданный результат!
У читателей мог возникнуть вопрос, что произойдет если у уравнения нет решения? Ответ прост - ошибка mismatched types. Например:
Так как String не может быть равен int, type constraint не соблюден и уравнение не имеет решений. Тогда мы можем увидеть ошибку mismatched types:
Возьмем пример поинтереснее:
Сначала, как в прошлом примере разметим переменные типов для имен и сигнатуры функции:
Теперь посмотрим на место где мы объявляем a - мы создаем пустой массив. Мы можем использовать переменную типа, для того чтобы обозначать тип элементов массива:
Идем дальше:
Предположим, что операторы < и ++ работает только со значениями типа int. Так, что у нас есть 3 новых constraint-а.
Продолжим:
Для дженерика T в метода списка insert нам нужна еще одна переменная типа - ?6.
И самое последнее:
Возвращаемое значение функции это a, значит что ?3 = ?2.
Таким образом получаем систему type constraint-ов:
И снова, с помощью алгоритма унификации, мы можем решить данную систему уравнений и получить:
Подставив эти типы получим результат type inference:
Теперь возможно у читателя появился вопрос, как работает этот загадочный алгоритм унификации который решает систему уравнений из 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-е:
В данном примере 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) = intimpl 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())
}
}
}
}
}Мы это сделали, мы написали алгоритм унификации! Проверим его на практике! Помните предыдущий пример?
Перед тем, как его симулировать, напишем два макроса:
Первый макрос, будет коротко генерировать переменную типа:
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: [] })В следующей статье, мы начнем писать свой маленький язык программирования и начнем определять типы простых выражений таких как литералы или массивы!