Is it possible to represent Higher-Order Abstract Syntax in Rust?

  • A+

In Haskell, it is very easy to write algebraic data types (ADTs) with functions. This allows us to write interpreters that rely on native functions for substitutions, i.e., a higher-order abstract syntax (HOAS), which is known to be very efficient. For example, this is a simple λ-calculus interpreter using that technique:

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))) 

Notice how native functions were used rather than de Bruijn indices. That makes the interpreter considerably faster than it would be if we substituted applications manually.

I'm aware Rust has closures and many Fn() types, but I'm not sure they work exactly like Haskell closures in this situation, much less how to express that program given the low-level nature of Rust. Is it possible to represent HOAS in Rust? How would the Term datatype be represented?


As a fan of lambda calculus I decided to attempt this and it is indeed possible, though a bit less sightly than in 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) } 

Thanks to BurntSushi5 for the suggestion to use Rc that I always forget exists and to Shepmaster for suggesting to remove the unnecessary Box under Rc in Lam and how to satisfy the borrow checker in longer Lam chains.


:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: