Реализуем 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:

Пример ошибки компилятора Rust-а - rustc

Возьмем пример поинтереснее:

Сначала, как в прошлом примере разметим переменные типов для имен и сигнатуры функции:

Теперь посмотрим на место где мы объявляем 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-е:

Ошибка ко��пилятора Rust-а - rustc — Ошибка компилятора Rust-а - rustc

В данном примере 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())
                }
            }
        }
    }
}

Мы это сделали, мы написали алгоритм унификации! Проверим его на практике! Помните предыдущий пример?

Перед тем, как его симулировать, напишем два макроса:

Первый макрос, будет коротко генерировать переменную типа:

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: [] })

В следующей статье, мы начнем писать свой маленький язык программирования и начнем определять типы простых выражений таких как литералы или массивы!

Реализуем Type inference на Rust — Часть #1: Unification

Что такое type inference?

Разбираем алгоритм

Unification algorithm (Алгоритм унификации)

Публикации

Ближайшие события