Можно ли представить абстрактный синтаксис более высокого порядка в ржавчине?
В Haskell очень легко писать алгебраические типы данных (ADT) с функциями. Это позволяет нам писать интерпретаторы, которые полагаются на нативные функции для подстановок, т. Е. Абстрактный синтаксис более высокого порядка (HOAS), который, как известно, очень эффективен. Например, это простой переводчик -calculus, используя этот метод:
data Term
= Hol Term
| Var Int
| Lam (Term -> Term)
| App Term Term
pretty :: Term -> String
pretty = go 0 where
go lvl term = case term of
Hol hol -> go lvl hol
Var idx -> "x" ++ show idx
Lam bod -> "λx" ++ show lvl ++ ". " ++ go (lvl+1) (bod (Hol (Var lvl)))
App fun arg -> "(" ++ go lvl fun ++ " " ++ go lvl arg ++ ")"
reduce :: Term -> Term
reduce (Hol hol) = hol
reduce (Var idx) = Var idx
reduce (Lam bod) = Lam (\v -> reduce (bod v))
reduce (App fun arg) = case reduce fun of
Hol fhol -> App (Hol fhol) (reduce arg)
Var fidx -> App (Var fidx) (reduce arg)
Lam fbod -> fbod (reduce arg)
App ffun farg -> App (App ffun farg) (reduce arg)
main :: IO ()
main
= putStrLn . pretty . reduce
$ App
(Lam$ \x -> App x x)
(Lam$ \s -> Lam$ \z -> App s (App s (App s z)))
Обратите внимание, как используются собственные функции, а не индексы Bruijn. Это делает переводчика значительно быстрее, чем это было бы, если бы мы заменяли приложения вручную.
Я знаю, что у Rust есть замыкания и много типов Fn()
, но я не уверен, что они работают точно так же, как закрытие Haskell в этой ситуации, тем более, как выразить эту программу, учитывая низкий уровень Rust. Возможно ли представлять HOAS в Rust? Как будет отображаться тип данных Term
?
Ответы
Ответ 1
Будучи поклонником лямбда-исчисления, я решил попробовать это, и это действительно возможно, хотя и немного менее заметным, чем в Haskell (ссылка на игровые площадки):
use std::rc::Rc;
use Term::*;
#[derive(Clone)]
enum Term {
Hol(Box<Term>),
Var(usize),
Lam(Rc<dyn Fn(Term) -> Term>),
App(Box<Term>, Box<Term>),
}
impl Term {
fn app(t1: Term, t2: Term) -> Self {
App(Box::new(t1), Box::new(t2))
}
fn lam<F: Fn(Term) -> Term + 'static>(f: F) -> Self {
Lam(Rc::new(f))
}
fn hol(t: Term) -> Self {
Hol(Box::new(t))
}
}
fn pretty(term: Term) -> String {
fn go(lvl: usize, term: Term) -> String {
match term {
Hol(hol) => go(lvl, *hol),
Var(idx) => format!("x{}", idx),
Lam(bod) => format!("λx{}. {}", lvl, go(lvl + 1, bod(Term::hol(Var(lvl))))),
App(fun, arg) => format!("({} {})", go(lvl, *fun), go(lvl, *arg)),
}
}
go(0, term)
}
fn reduce(term: Term) -> Term {
match term {
Hol(hol) => *hol,
Var(idx) => Var(idx),
Lam(bod) => Term::lam(move |v| reduce(bod(v))),
App(fun, arg) => match reduce(*fun) {
Hol(fhol) => Term::app(Hol(fhol), reduce(*arg)),
Var(fidx) => Term::app(Var(fidx), reduce(*arg)),
Lam(fbod) => fbod(reduce(*arg)),
App(ffun, farg) => Term::app(Term::app(*ffun, *farg), reduce(*arg)),
},
}
}
fn main() {
// (λx. x x) (λs. λz. s (s (s z)))
let term1 = Term::app(
Term::lam(|x| Term::app(x.clone(), x.clone())),
Term::lam(|s| Term::lam(move |z|
Term::app(
s.clone(),
Term::app(
s.clone(),
Term::app(
s.clone(),
z.clone()
))))));
// λb. λt. λf. b t f
let term2 = Term::lam(|b| Term::lam(move |t|
Term::lam({
let b = b.clone(); // necessary to satisfy the borrow checker
move |f| Term::app(Term::app(b.clone(), t.clone()), f)
})
));
println!("{}", pretty(reduce(term1))); // λx0. λx1. (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))))))))
println!("{}", pretty(reduce(term2))); // λx0. λx1. λx2. ((x0 x1) x2)
}
Спасибо BurntSushi5 за предложение использовать Rc
, которого я всегда забываю, и Shepmaster за то, что вы предлагаете удалить ненужный Box
под Rc
в Lam
и как удовлетворить проверку займа в более длинных цепочках Lam
.
Ответ 2
В принятом решении используется Rc
для создания клонированного выделенного кучи.
С технической точки зрения, это не обязательно, так как нет необходимости в подсчете времени выполнения. Все, что нам нужно, это закрытие как объект-признак, а также клонирование.
Однако Rust 1.29.2 не позволяет нам иметь такие вещи, как dyn Clone + FnOnce(Term) → Term
, это ограничение может быть смягчено в будущем. Ограничение имеет два фактора: Clone
не является безопасным для объекта (который вряд ли будет ослаблен), и если мы объединим две черты вместе, один из них должен быть автоматическим признаком (это может быть ослаблено ИМХО).
Ожидая улучшения языка, мы можем представить новую черту, чтобы обойти это:
// Combination of FnOnce(Term) -> Term and Clone
trait TermLam {
// The FnOnce part, declared like an Fn, because we need object safety
fn app(&self, t: Term) -> Term;
// The Clone part, but we have to return sized objects
// (not Self either because of object safety), so it is in a box
fn clone_box(&self) -> Box<dyn TermLam>;
}
// Blanket implementation for appropriate types
impl<F> TermLam for F
where
F: 'static/*' highlighting fix */ + Clone + FnOnce(Term) -> Term
{
// Note: when you have a Clone + FnOnce, you effectively have an Fn
fn app(&self, t: Term) -> Term {
(self.clone())(t)
}
fn clone_box(&self) -> Box<dyn TermLam> {
Box::new(self.clone())
}
}
// We can now clone the box
impl Clone for Box<dyn TermLam> {
fn clone(&self) -> Self {
self.clone_box()
}
}
Затем мы можем удалить необходимость использования Rc
.
#[derive(Clone)]
enum Term {
Hol(Box<Term>),
Var(usize),
Lam(Box<dyn TermLam>),
App(Box<Term>, Box<Term>),
}
impl Term {
fn app(t1: Term, t2: Term) -> Self {
App(Box::new(t1), Box::new(t2))
}
fn lam<F>(f: F) -> Self
where
F: 'static/*' highlighting fix */ + Clone + FnOnce(Term) -> Term
{
Lam(Box::new(f))
}
fn hol(t: Term) -> Self {
Hol(Box::new(t))
}
}
fn pretty(term: Term) -> String {
fn go(lvl: usize, term: Term) -> String {
match term {
Hol(hol) => go(lvl, *hol),
Var(idx) => format!("x{}", idx),
Lam(bod) => format!("λx{}. {}", lvl, go(lvl + 1, bod.app(Term::hol(Var(lvl))))),
App(fun, arg) => format!("({} {})", go(lvl, *fun), go(lvl, *arg)),
}
}
go(0, term)
}
fn reduce(term: Term) -> Term {
match term {
Hol(hol) => *hol,
Var(idx) => Var(idx),
Lam(bod) => Term::lam(move |v| reduce(bod.app(v))),
App(fun, arg) => match reduce(*fun) {
Hol(fhol) => Term::app(Hol(fhol), reduce(*arg)),
Var(fidx) => Term::app(Var(fidx), reduce(*arg)),
Lam(fbod) => fbod.app(reduce(*arg)),
App(ffun, farg) => Term::app(Term::app(*ffun, *farg), reduce(*arg)),
},
}
}
fn main() {
// (λx. x x) (λs. λz. s (s (s z)))
let term1 = Term::app(
Term::lam(|x| Term::app(x.clone(), x.clone())),
Term::lam(|s| {
Term::lam(move |z| {
Term::app(
s.clone(),
Term::app(s.clone(), Term::app(s.clone(), z.clone())),
)
})
}),
);
// λb. λt. λf. b t f
let term2 = Term::lam(|b| {
Term::lam(move |t| {
Term::lam({
//let b = b.clone(); No longer necessary for Rust 1.29.2
move |f| Term::app(Term::app(b.clone(), t.clone()), f)
})
})
});
println!("{}", pretty(reduce(term1))); // λx0. λx1. (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))))))))
println!("{}", pretty(reduce(term2))); // λx0. λx1. λx2. ((x0 x1) x2)
}
Детская площадка
Это был оригинальный способ, которым попытался другой ответ, который автор не смог решить.