В прошлой статье мы реализовывали алгоритм унификации (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, интересных фишках и много другого!
AnthonyMikh
У меня вопрос по коду. Насколько я могу видеть, вы полагаетесь на то, что имена переменных уникальны и не учитываете, что имена аргументов вложенных лямбд могут затенять имена аргументов обрамляющих функций.
И этой действительно проблема. Скажем, если в окружение добавить факт, что имя
"y"
имеет тип"int"
, то для такого выражения:ваш алгоритм корректно выводит тип выражения, как
int
, но для чуть более сложноговыводит неправильный
Variable(TypeVariable(1))
.abs0luty Автор
Да, вы правы! Я указал, что подход работы с окружением еще очень простой. Здесь для простоты сделано пока так. Я просто пранировал сделать это в следующей статье.