В прошлой статье мы реализовывали алгоритм унификации (unification) на Rust-е. Теперь давайте применим его на реальном примере - простое lambda исчисление.

Синтаксис

Синтаксис выражений у нашего простого lambda calculus-а будет выглядеть так:

<expr> ::= <identifier>
        |  \ <identifier> . <expr>
        | ( <expr> <expr> )

В данном случае \ <identifier> . <expr> это синтаксис для лямбд:

\x.x
 ^ параметр лямбды
   ^ "возвращаемое" значение
\x.\y.x
\x.\y.y
\a.((\x.\y.y) a)

А <expr> <expr>, для применений:

\x.\y.(x y)
       ^ лямбда
         ^ аргумент

Теперь когда с синтаксисом мы ознакомились, мы можем приступить к самому сладкому: реализации!

Токенизация (сканирование, или лексический анализ, или ...)

Первое, что нам нужно сделать с исходником на нашем простеньком языке программирования это превратить его в список токенов, то есть токенизировать:

Токен - здесь можно рассматривать как грамматическую единицу языка: разные виды пунктуации, название (идентификатор), иногда пробелы, ключевые слова и т.д.

Разметим структуру токена в нашем языке:

#[derive(Debug, PartialEq, Eq, Clone, Hash)]
pub enum Token {
    Lambda, // `\`
    OpenParent, // `(`
    CloseParent, // `)`
    Dot, // `.`
    Name(String), // identifier
}

Реализуем токенизацию!

pub fn tokenize(source: &str) -> Vec<Token> {
    let mut chars = source.chars().peekable();
    let mut tokens = Vec::new();

    while let Some(c) = chars.next() {
        match c {
            '(' => tokens.push(Token::OpenParent),
            ')' => tokens.push(Token::CloseParent),
            '\\' => tokens.push(Token::Lambda),
            '.' => tokens.push(Token::Dot),
            _ => {

Здесь мы обрабатываем токены состоящие из единичных символов - пунктуацию. Теперь самое интересное - идентификаторы:

                if c.is_whitespace() {
                    // ignore
                } else if c.is_alphabetic() || c == '_' {
                    ...
                } else {
                    panic!("unexpected character `{}`", c);
                }
            }
        }
    }

    tokens
}

Здесь мы делаем несколько вещей. Во-первых, мы пропускаем пробелы в нашей программе (никакого значения даже с точки зрения синтаксиса они здесь не имеют). Во-вторых, если мы обнаруживаем невалидный символ, мы выводим ошибку (пока-что делаем панику, что позже исправим). В-третьих обрабатываем идентификаторы:

                    let mut name = String::new();

                    name.push(c);

                    while let Some(&c) = chars.peek() {
                        if c.is_alphanumeric() || c == '_' {
                            name.push(c);
                            chars.next();
                        } else {
                            break;
                        }
                    }

                    tokens.push(Token::Name(name));

Пока следующий символ это либо число, либо буква, либо '_', мы продолжаем идти дальше и добавлять символы в нашу строку name, иначе мы прерываем цикл и идем сканировать следующие токены.

Парсер

Теперь же, когда мы имеем список токенов (с которым работать проще, нежели чем с исходным кодом), мы должны провести синтаксический анализ:

Парсер берет список токенов и преобразует его в абстрактное синтаксическое дерево или AST.

Первое, что мы должны сделать - разметить AST для выражений:

#[derive(Debug, PartialEq, Eq, Clone, Hash)]
pub enum Expression {
    Lambda {
        parameter: String,
        value: Box<Self>,
    },
    Apply {
        callee: Box<Self>,
        argument: Box<Self>,
    },
    Variable {
        name: String,
    },
}

Я надеюсь, здесь вопросов не должно быть.

Теперь мы должны создать структуру, которая будет хранить итератор по токенам, для того, чтобы по ним проходиться:

struct ParseState<I>
where
    I: Iterator<Item = Token>,
{
    tokens: Peekable<I>,
}

impl<I> ParseState<I>
where
    I: Iterator<Item = Token>,
{
    fn new(tokens: I) -> Self {
        Self {
            tokens: tokens.peekable(),
        }
    }

Теперь можно приступить к самому интересному! Начнем с выражений завернутых в скобки:

    fn parse_parenthesized_expression(&mut self) -> Expression {
        let inner_expression = self.parse_expression();

        if !matches!(self.tokens.next(), Some(Token::CloseParent)) {
            panic!("expected `)`");
        }

        inner_expression
    }

Здесь мы не проверяем на открывающую скобку, потому-что предполагается, что при вызове функции она уже обработана.

Теперь обработка лямбд:

    fn parse_lambda(&mut self) -> Expression {
        let parameter = match self.tokens.next() {
            Some(Token::Name(name)) => name,
            _ => panic!("expected identifier"),
        };

        if !matches!(self.tokens.next(), Some(Token::Dot)) {
            panic!("expected `.`");
        }

        let value = self.parse_primary_expression();

        Expression::Lambda {
            parameter,
            value: Box::new(value),
        }
    }

Здесь тоже предполагается, что \ уже обработан.

В данном случае мы можем заметить метод parse_primary_expression. Это по сути парсинг всех выражений кроме применений (<expr> <expr>), потому-что например здесь:

\x.x a

Мы парсим не x a цельно, а берем толькоx. И поэтому получаем совершенно другой порядок действий, так как \x.x и a это два раздельных выражения.

Реализуем этот самый метод!

    fn parse_primary_expression(&mut self) -> Expression {
        match self.tokens.next() {
            Some(Token::Lambda) => self.parse_lambda(),
            Some(Token::OpenParent) => self.parse_parenthesized_expression(),
            Some(Token::Name(name)) => Expression::Variable { name },
            _ => panic!("expected expression"),
        }
    }

Здесь мы вызываем все функции, которые мы написали до этого и еще обрабатываем простые переменные.

Теперь же нам нужно обрабатывать применения (<expr> <expr>):

    fn parse_expression(&mut self) -> Expression {
        let mut left = self.parse_primary_expression();

        while !matches!(
              self.tokens.peek(), 
              Some(Token::CloseParent) | None) {
            let argument = self.parse_primary_expression();

            left = Expression::Apply {
                callee: Box::new(left),
                argument: Box::new(argument),
            };
        }

        left
    }
}

Здесь мы продолжаем анализировать выражения пока не встретим закрывающую скобку или пока не уткнемся в конец входных данных:

          while !matches!(
              self.tokens.peek(), 
              Some(Token::CloseParent) | None) { ... }

Ну и самое логичное, мы анализируем аргумент при применении и сохраняем это все в AST:

            let argument = self.parse_primary_expression();

            left = Expression::Apply {
                callee: Box::new(left),
                argument: Box::new(argument),
            };

Таким образом мы реализовали простой парсер за ~130 строк кода для lambda исчисления. А теперь то чего мы так долго ждали:

Type inference

Помните в прошлой статье, я говорил про type constraint-ы? Так-вот пока для простоты у нас будет только 1 вид constraint-ов - равенство:

#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
enum Constraint {
    Eq { left: Arc<Type>, right: Arc<Type> },
}

То есть как раньше пояснялось, constraint требует, чтобы тип были равны. Соответственно unification будет как раньше принимать левый и правый тип и давать нам новые замены (substitutions).

Теперь, так как мы уже начинаем работать со scope-ами, нам нужно где-то хранить информацию о типах. Мы пока-что сделаем это самым очевидным способом:

#[derive(Debug, Clone, PartialEq, Eq, Default)]
struct Environment {
    variables: HashMap<String, Arc<Type>>,
}

impl Environment {
    fn new() -> Self {
        Self::default()
    }
}

Теперь создадим контекст для нашего type inference-а:

#[derive(Debug, PartialEq, Eq)]
struct InferenceContext<'env> {
    constraints: Vec<Constraint>,
    environment: &'env mut Environment,
    last_type_variable_index: usize,
}

impl<'env> InferenceContext<'env> {
    fn new(environment: &'env mut Environment) -> Self {
        Self {
            constraints: Vec::new(),
            environment,
            last_type_variable_index: 0,
        }
    }

Как видим, здесь есть интересное поле - last_type_variable_index. Нужно оно для генерации новых уникальных переменных типа. Помните?

Напишем функции, которые будут генерировать новые переменные типов и сами типы заполнители:

    fn fresh_type_variable(&mut self) -> TypeVariable {
        self.last_type_variable_index += 1;
        TypeVariable(self.last_type_variable_index)
    }

    fn type_placeholder(&mut self) -> Arc<Type> {
        Arc::new(Type::Variable(self.fresh_type_variable()))
    }

А теперь делаем завершающие штрихи. Напишем функцию, которую назовем infer_type. Она будет возвращать тип данного выражения:

    fn infer_type(&mut self, expression: &Expression) -> Arc<Type> {
        match expression {
            Expression::Variable { name } => self
                .environment
                .variables
                .get(name)
                .unwrap_or_else(|| panic!("unbound variable: {}", name))
                .clone(),

Первое, что мы должны обработать это самый простой случай. Если выражение - переменная, берем информацию о типе из scope-а.

            Expression::Lambda {
                parameter,
                value,
            } => {
                let parameter_type = self.type_placeholder();

                self.environment
                    .variables
                    .insert(parameter.clone(), parameter_type.clone());

                let value_type = self.infer_type(value);

                Arc::new(Type::Constructor(TypeConstructor {
                    name: "Function".to_owned(),
                    generics: vec![parameter_type, value_type],
                }))
            }

С лямбдами все поинтереснее. Во-первых, мы не знаем тип параметра лямбды. Единственное, что мы можем узнать это ее возвращаемое значение, что мы и делаем:

                let value_type = self.infer_type(value);

Соответственно, для типа параметра, мы пока оставим переменную типа (которую после можно будет убрать с помощью замен) и конечно же добавляем в текущий scope, чтобы можно было использовать параметр, при анализации возвращаемого значения:

                let parameter_type = self.type_placeholder();

                self.environment
                    .variables
                    .insert(parameter.clone(), parameter_type.clone());

Заметим, что мы возвращаем type constructor, с названием Function:

                Arc::new(Type::Constructor(TypeConstructor {
                    name: "Function".to_owned(),
                    generics: vec![parameter_type, value_type],
                }))

В данном случае, первый generic аргумент это тип параметра лямбды, а второй это тип возвращаемого значения.

Теперь приступим к анализации применений:

            Expression::Apply { callee, argument } => {
                let callee_type = self.infer_type(callee);
                let argument_type = self.infer_type(argument);

                let return_type = self.type_placeholder();

                self.constraints.push(Constraint::Eq {
                    left: callee_type.clone(),
                    right: Arc::new(Type::Constructor(TypeConstructor {
                        name: "Function".to_owned(),
                        generics: vec![argument_type.clone(), return_type.clone()],
                    })),
                });

                return_type
            }
        }
    }

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

                self.constraints.push(Constraint::Eq {
                    left: callee_type.clone(),
                    right: Arc::new(Type::Constructor(TypeConstructor {
                        name: "Function".to_owned(),
                        generics: vec![argument_type.clone(), return_type.clone()],
                    })),
                });

А исходя из информации, что Function<A, ?t> = Function<A, B> мы и так узнаем тип возвращаемого значения (?t = B), а еще и во-вторых проверим типы на type mismatch.

Поздравляю, мы почти закончили!

Теперь, нам нужна функция, которая будет проходиться по type constraint-ам и применять нашу написанную в прошлой статье функцию unify, чтобы получать замены для типовых переменных:

    fn solve(self) -> HashMap<TypeVariable, Arc<Type>> {
        let mut substitutions = HashMap::new();

        for constraint in self.constraints {
            match constraint {
                Constraint::Eq { left, right } => {
                    unify(left, right, &mut substitutions);
                }
            }
        }

        substitutions
    }
}

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

fn main() {
    let mut environment = Environment::new();

    environment.variables.insert(
        "add".to_owned(),
        tconst!(
            "Function",
            tconst!("int"),
            tconst!("Function", tconst!("int"), tconst!("int"))
        ),
    );

    let expression = ParseState::new(tokenize("\\a.(add a a)").into_iter()).parse_expression();

    let mut context = InferenceContext::new(&mut environment);
    let ty = context.infer_type(&expression);
    let substitutions = context.solve();

    println!("{:?}", ty.substitute(&substitutions));
}

Как видим алгоритм понял, что тип выражения \a.(add a a) если add это Function<int, Function<int, int>> это Function<int, int>, что звучит логично:

Constructor(TypeConstructor { name: "Function", generics: [Constructor(TypeConstructor { name: "int", generics: [] }), Constructor(TypeConstructor { name: "int", generics: [] })] })

Github

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

Окончание

Спасибо большое за внимание! Я следующих статьях, мы будем говорить о более продвинутых способах реализации type inference, интересных фишках и много другого!

Комментарии (2)


  1. AnthonyMikh
    08.08.2023 09:14
    +3

    У меня вопрос по коду. Насколько я могу видеть, вы полагаетесь на то, что имена переменных уникальны и не учитываете, что имена аргументов вложенных лямбд могут затенять имена аргументов обрамляющих функций.


    И этой действительно проблема. Скажем, если в окружение добавить факт, что имя "y" имеет тип "int", то для такого выражения:


    (\x.x)(y)

    ваш алгоритм корректно выводит тип выражения, как int, но для чуть более сложного


    (\y.y)(y)

    выводит неправильный Variable(TypeVariable(1)).


    1. abs0luty Автор
      08.08.2023 09:14
      +1

      Да, вы правы! Я указал, что подход работы с окружением еще очень простой. Здесь для простоты сделано пока так. Я просто пранировал сделать это в следующей статье.