unbound

The unbound crate handles variable binding for abstract syntax trees. Every typechecker and evaluator for a language with lambdas eventually needs capture-avoiding substitution and alpha equivalence, and getting either wrong produces the most confusing bugs in a compiler. unbound derives both from the shape of your AST, in the spirit of the Haskell library of the same name.

Terms are stored in locally nameless form. Free variables carry a name with a globally unique index. Bound variables are de Bruijn coordinates, installed when a Bind closes over its body and removed again when the binder is opened. A bound variable has no name, so alpha equivalence is structural equality and substitution cannot capture.

Terms

A binder is written Bind<P, T> where P is the pattern and T is the body. The derives generate Alpha and Subst by walking the structure. The variant named Var is the variable case.

#![allow(unused)]
fn main() {
use unbound::prelude::*;
/// A variable by spelling. `Name::global` returns the same name for the same
/// string, so building terms bottom-up resolves scope like a parser would.
pub fn var(x: &str) -> Expr {
    Expr::Var(Name::global(x))
}
/// Abstract `x` in `body`, closing every free occurrence into a de Bruijn
/// index.
pub fn lam(x: &str, body: Expr) -> Expr {
    Expr::Lam(bind(Name::global(x), Box::new(body)))
}
pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
/// Normal-order reduction to beta normal form. `instantiate` substitutes the
/// argument straight into the closed body, so there is nothing to freshen.
pub fn normalize(e: &Expr) -> Expr {
    match e {
        Expr::Var(_) => e.clone(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            Expr::Lam(bind(x, Box::new(normalize(&body))))
        }
        Expr::App(f, a) => match normalize(f) {
            Expr::Lam(b) => normalize(&b.instantiate(a.as_ref())),
            f => app(f, normalize(a)),
        },
    }
}
/// Print a term, renaming a binder only when its spelling would capture a
/// free name the body actually uses.
pub fn pretty(e: &Expr) -> String {
    go(e, &mut NameScope::new(&e.fv()))
}
fn go(e: &Expr, scope: &mut NameScope) -> String {
    match e {
        Expr::Var(x) => scope.get(x).to_owned(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            let s = scope.bind(&x, &body.fv());
            let out = format!("\\{}. {}", s, go(&body, scope));
            scope.pop();
            out
        }
        Expr::App(f, a) => format!("({} {})", go(f, scope), go(a, scope)),
    }
}
#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn alpha_equivalence_ignores_binder_names() {
        assert!(lam("x", var("x")).aeq(&lam("y", var("y"))));
        assert!(!lam("x", var("y")).aeq(&lam("y", var("y"))));
    }

    #[test]
    fn substitution_does_not_capture() {
        let k = lam("x", lam("y", var("x")));
        let e = normalize(&app(k, var("y")));
        assert!(e.aeq(&lam("z", var("y"))));
        assert_eq!(pretty(&e), "\\y1. y");
    }

    #[test]
    fn skk_is_identity() {
        let s = lam(
            "f",
            lam(
                "g",
                lam("x", app(app(var("f"), var("x")), app(var("g"), var("x")))),
            ),
        );
        let k = lam("x", lam("y", var("x")));
        let i = normalize(&app(app(s, k.clone()), k));
        assert!(i.aeq(&lam("a", var("a"))));
    }
}
/// Terms of the untyped lambda calculus. The derives give alpha equivalence
/// and substitution, with `Var` picked out as the variable case by name.
#[derive(Clone, Debug, Alpha, Subst)]
pub enum Expr {
    Var(Name<Expr>),
    Lam(Bind<Name<Expr>, Box<Expr>>),
    App(Box<Expr>, Box<Expr>),
}
}

Name<Expr> carries a phantom type, so a term variable can never be substituted into a type or the other way round. Smart constructors keep the examples readable.

#![allow(unused)]
fn main() {
use unbound::prelude::*;
/// Terms of the untyped lambda calculus. The derives give alpha equivalence
/// and substitution, with `Var` picked out as the variable case by name.
#[derive(Clone, Debug, Alpha, Subst)]
pub enum Expr {
    Var(Name<Expr>),
    Lam(Bind<Name<Expr>, Box<Expr>>),
    App(Box<Expr>, Box<Expr>),
}
/// Abstract `x` in `body`, closing every free occurrence into a de Bruijn
/// index.
pub fn lam(x: &str, body: Expr) -> Expr {
    Expr::Lam(bind(Name::global(x), Box::new(body)))
}
pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
/// Normal-order reduction to beta normal form. `instantiate` substitutes the
/// argument straight into the closed body, so there is nothing to freshen.
pub fn normalize(e: &Expr) -> Expr {
    match e {
        Expr::Var(_) => e.clone(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            Expr::Lam(bind(x, Box::new(normalize(&body))))
        }
        Expr::App(f, a) => match normalize(f) {
            Expr::Lam(b) => normalize(&b.instantiate(a.as_ref())),
            f => app(f, normalize(a)),
        },
    }
}
/// Print a term, renaming a binder only when its spelling would capture a
/// free name the body actually uses.
pub fn pretty(e: &Expr) -> String {
    go(e, &mut NameScope::new(&e.fv()))
}
fn go(e: &Expr, scope: &mut NameScope) -> String {
    match e {
        Expr::Var(x) => scope.get(x).to_owned(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            let s = scope.bind(&x, &body.fv());
            let out = format!("\\{}. {}", s, go(&body, scope));
            scope.pop();
            out
        }
        Expr::App(f, a) => format!("({} {})", go(f, scope), go(a, scope)),
    }
}
#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn alpha_equivalence_ignores_binder_names() {
        assert!(lam("x", var("x")).aeq(&lam("y", var("y"))));
        assert!(!lam("x", var("y")).aeq(&lam("y", var("y"))));
    }

    #[test]
    fn substitution_does_not_capture() {
        let k = lam("x", lam("y", var("x")));
        let e = normalize(&app(k, var("y")));
        assert!(e.aeq(&lam("z", var("y"))));
        assert_eq!(pretty(&e), "\\y1. y");
    }

    #[test]
    fn skk_is_identity() {
        let s = lam(
            "f",
            lam(
                "g",
                lam("x", app(app(var("f"), var("x")), app(var("g"), var("x")))),
            ),
        );
        let k = lam("x", lam("y", var("x")));
        let i = normalize(&app(app(s, k.clone()), k));
        assert!(i.aeq(&lam("a", var("a"))));
    }
}
/// A variable by spelling. `Name::global` returns the same name for the same
/// string, so building terms bottom-up resolves scope like a parser would.
pub fn var(x: &str) -> Expr {
    Expr::Var(Name::global(x))
}
}

#![allow(unused)]
fn main() {
use unbound::prelude::*;
/// Terms of the untyped lambda calculus. The derives give alpha equivalence
/// and substitution, with `Var` picked out as the variable case by name.
#[derive(Clone, Debug, Alpha, Subst)]
pub enum Expr {
    Var(Name<Expr>),
    Lam(Bind<Name<Expr>, Box<Expr>>),
    App(Box<Expr>, Box<Expr>),
}
/// A variable by spelling. `Name::global` returns the same name for the same
/// string, so building terms bottom-up resolves scope like a parser would.
pub fn var(x: &str) -> Expr {
    Expr::Var(Name::global(x))
}
pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
/// Normal-order reduction to beta normal form. `instantiate` substitutes the
/// argument straight into the closed body, so there is nothing to freshen.
pub fn normalize(e: &Expr) -> Expr {
    match e {
        Expr::Var(_) => e.clone(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            Expr::Lam(bind(x, Box::new(normalize(&body))))
        }
        Expr::App(f, a) => match normalize(f) {
            Expr::Lam(b) => normalize(&b.instantiate(a.as_ref())),
            f => app(f, normalize(a)),
        },
    }
}
/// Print a term, renaming a binder only when its spelling would capture a
/// free name the body actually uses.
pub fn pretty(e: &Expr) -> String {
    go(e, &mut NameScope::new(&e.fv()))
}
fn go(e: &Expr, scope: &mut NameScope) -> String {
    match e {
        Expr::Var(x) => scope.get(x).to_owned(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            let s = scope.bind(&x, &body.fv());
            let out = format!("\\{}. {}", s, go(&body, scope));
            scope.pop();
            out
        }
        Expr::App(f, a) => format!("({} {})", go(f, scope), go(a, scope)),
    }
}
#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn alpha_equivalence_ignores_binder_names() {
        assert!(lam("x", var("x")).aeq(&lam("y", var("y"))));
        assert!(!lam("x", var("y")).aeq(&lam("y", var("y"))));
    }

    #[test]
    fn substitution_does_not_capture() {
        let k = lam("x", lam("y", var("x")));
        let e = normalize(&app(k, var("y")));
        assert!(e.aeq(&lam("z", var("y"))));
        assert_eq!(pretty(&e), "\\y1. y");
    }

    #[test]
    fn skk_is_identity() {
        let s = lam(
            "f",
            lam(
                "g",
                lam("x", app(app(var("f"), var("x")), app(var("g"), var("x")))),
            ),
        );
        let k = lam("x", lam("y", var("x")));
        let i = normalize(&app(app(s, k.clone()), k));
        assert!(i.aeq(&lam("a", var("a"))));
    }
}
/// Abstract `x` in `body`, closing every free occurrence into a de Bruijn
/// index.
pub fn lam(x: &str, body: Expr) -> Expr {
    Expr::Lam(bind(Name::global(x), Box::new(body)))
}
}

Name::global returns the same name for every call with the same spelling. Building a term bottom-up with global names gives every occurrence its nearest enclosing binder, which is exactly lexical scope. A parser can use this directly and skip a separate renaming pass.

Alpha Equivalence

\x. x and \y. y are both stored as \. #0, so aeq is a lockstep walk with no renaming context.

assert!(lam("x", var("x")).aeq(&lam("y", var("y"))));
assert!(!lam("x", var("y")).aeq(&lam("y", var("y"))));

Normalization

unbind opens a binder with fresh names. instantiate skips the round trip and substitutes a value straight into the closed body, which is exactly beta reduction.

#![allow(unused)]
fn main() {
use unbound::prelude::*;
/// Terms of the untyped lambda calculus. The derives give alpha equivalence
/// and substitution, with `Var` picked out as the variable case by name.
#[derive(Clone, Debug, Alpha, Subst)]
pub enum Expr {
    Var(Name<Expr>),
    Lam(Bind<Name<Expr>, Box<Expr>>),
    App(Box<Expr>, Box<Expr>),
}
/// A variable by spelling. `Name::global` returns the same name for the same
/// string, so building terms bottom-up resolves scope like a parser would.
pub fn var(x: &str) -> Expr {
    Expr::Var(Name::global(x))
}
/// Abstract `x` in `body`, closing every free occurrence into a de Bruijn
/// index.
pub fn lam(x: &str, body: Expr) -> Expr {
    Expr::Lam(bind(Name::global(x), Box::new(body)))
}
pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
/// Print a term, renaming a binder only when its spelling would capture a
/// free name the body actually uses.
pub fn pretty(e: &Expr) -> String {
    go(e, &mut NameScope::new(&e.fv()))
}
fn go(e: &Expr, scope: &mut NameScope) -> String {
    match e {
        Expr::Var(x) => scope.get(x).to_owned(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            let s = scope.bind(&x, &body.fv());
            let out = format!("\\{}. {}", s, go(&body, scope));
            scope.pop();
            out
        }
        Expr::App(f, a) => format!("({} {})", go(f, scope), go(a, scope)),
    }
}
#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn alpha_equivalence_ignores_binder_names() {
        assert!(lam("x", var("x")).aeq(&lam("y", var("y"))));
        assert!(!lam("x", var("y")).aeq(&lam("y", var("y"))));
    }

    #[test]
    fn substitution_does_not_capture() {
        let k = lam("x", lam("y", var("x")));
        let e = normalize(&app(k, var("y")));
        assert!(e.aeq(&lam("z", var("y"))));
        assert_eq!(pretty(&e), "\\y1. y");
    }

    #[test]
    fn skk_is_identity() {
        let s = lam(
            "f",
            lam(
                "g",
                lam("x", app(app(var("f"), var("x")), app(var("g"), var("x")))),
            ),
        );
        let k = lam("x", lam("y", var("x")));
        let i = normalize(&app(app(s, k.clone()), k));
        assert!(i.aeq(&lam("a", var("a"))));
    }
}
/// Normal-order reduction to beta normal form. `instantiate` substitutes the
/// argument straight into the closed body, so there is nothing to freshen.
pub fn normalize(e: &Expr) -> Expr {
    match e {
        Expr::Var(_) => e.clone(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            Expr::Lam(bind(x, Box::new(normalize(&body))))
        }
        Expr::App(f, a) => match normalize(f) {
            Expr::Lam(b) => normalize(&b.instantiate(a.as_ref())),
            f => app(f, normalize(a)),
        },
    }
}
}

The classic capture hazard is (\x. \y. x) y. Naive substitution produces \y. y, the identity. Here the inner y is a de Bruijn index and the free y is a name, so they cannot collide and the result is the constant function returning the free y.

Printing

Opening a binder yields a fresh index but may reuse a spelling, so printing names naively can show \y. y for a term whose body is the free y. NameScope tracks the spelling of every name in scope and renames a binder only when it would capture a name the body actually uses.

#![allow(unused)]
fn main() {
use unbound::prelude::*;
/// Terms of the untyped lambda calculus. The derives give alpha equivalence
/// and substitution, with `Var` picked out as the variable case by name.
#[derive(Clone, Debug, Alpha, Subst)]
pub enum Expr {
    Var(Name<Expr>),
    Lam(Bind<Name<Expr>, Box<Expr>>),
    App(Box<Expr>, Box<Expr>),
}
/// A variable by spelling. `Name::global` returns the same name for the same
/// string, so building terms bottom-up resolves scope like a parser would.
pub fn var(x: &str) -> Expr {
    Expr::Var(Name::global(x))
}
/// Abstract `x` in `body`, closing every free occurrence into a de Bruijn
/// index.
pub fn lam(x: &str, body: Expr) -> Expr {
    Expr::Lam(bind(Name::global(x), Box::new(body)))
}
pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
/// Normal-order reduction to beta normal form. `instantiate` substitutes the
/// argument straight into the closed body, so there is nothing to freshen.
pub fn normalize(e: &Expr) -> Expr {
    match e {
        Expr::Var(_) => e.clone(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            Expr::Lam(bind(x, Box::new(normalize(&body))))
        }
        Expr::App(f, a) => match normalize(f) {
            Expr::Lam(b) => normalize(&b.instantiate(a.as_ref())),
            f => app(f, normalize(a)),
        },
    }
}
/// Print a term, renaming a binder only when its spelling would capture a
/// free name the body actually uses.
pub fn pretty(e: &Expr) -> String {
    go(e, &mut NameScope::new(&e.fv()))
}
#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn alpha_equivalence_ignores_binder_names() {
        assert!(lam("x", var("x")).aeq(&lam("y", var("y"))));
        assert!(!lam("x", var("y")).aeq(&lam("y", var("y"))));
    }

    #[test]
    fn substitution_does_not_capture() {
        let k = lam("x", lam("y", var("x")));
        let e = normalize(&app(k, var("y")));
        assert!(e.aeq(&lam("z", var("y"))));
        assert_eq!(pretty(&e), "\\y1. y");
    }

    #[test]
    fn skk_is_identity() {
        let s = lam(
            "f",
            lam(
                "g",
                lam("x", app(app(var("f"), var("x")), app(var("g"), var("x")))),
            ),
        );
        let k = lam("x", lam("y", var("x")));
        let i = normalize(&app(app(s, k.clone()), k));
        assert!(i.aeq(&lam("a", var("a"))));
    }
}
fn go(e: &Expr, scope: &mut NameScope) -> String {
    match e {
        Expr::Var(x) => scope.get(x).to_owned(),
        Expr::Lam(b) => {
            let (x, body) = b.unbind_ref();
            let s = scope.bind(&x, &body.fv());
            let out = format!("\\{}. {}", s, go(&body, scope));
            scope.pop();
            out
        }
        Expr::App(f, a) => format!("({} {})", go(f, scope), go(a, scope)),
    }
}
}

The capture example above prints as \y1. y, which reads back as the same term.

Best Practices

Reach into a binder through unbind or unbind_ref, never body. The body is stored closed and its bound variables are raw de Bruijn coordinates.

Prefer instantiate for beta reduction and type application. It avoids generating fresh names that are immediately substituted away.

Use Vec<Name<T>> as the pattern for binders that introduce several names at once, such as forall a b. t, and (Name<T>, Ann) for annotated binders. An annotation sits outside the scope of its own binder.

Use #[subst(Ty)] on a term type to derive substitution of types into terms, which is what type application in System F needs. Use #[subst(_)] for types with no variables of their own.

Freshness comes from a global counter, so unbind is safe anywhere. Reach for FreshM only when you want readable fresh spellings like x1 in output.