在Haskell中,很容易写出algebraic data types (ADTs)具有功能。这允许我们编写依赖 native 函数进行替换的解释器,即 higher-order abstract syntax (HOAS)。 ,众所周知,这是非常有效的。例如,这是一个使用该技术的简单 λ 演算解释器:
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)))
注意如何使用原生函数而不是 de Bruijn 索引。这使得解释器比我们手动替换应用程序要快得多。
我知道 Rust 有闭包和许多 Fn()
类型,但我不确定在这种情况下它们的工作方式是否与 Haskell 闭包完全一样,更不用说如何表达该程序了Rust 的级特性。 是否可以用 Rust 表示 HOAS? Term
数据类型将如何表示?
最佳答案
作为 lambda 演算的粉丝,我决定尝试这个,这确实是可能的,尽管比 Haskell ( playground link) 中的要差一些:
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 建议删除 Rc
下不必要的 Box
在 Lam
中以及如何在更长的 Lam
链中满足借用检查器的要求。
关于haskell - 是否可以在 Rust 中表示高阶抽象语法?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51182640/