Moniker

Moniker makes it simple to track variables across nested scopes in programming language implementations.

Instead of implementing name-handling code by hand (which is often tedious and error-prone), Moniker provides a number of types and traits for declaratively describing name binding directly in your language's abstract syntax tree. From this we can derive the corresponding name-handling code automatically!

Motivation

It's interesting to note that the idea of a 'scope' comes up quite often in programming:

| Description | Rust Example | | -------------------- | -------------------------------------------- | | case match arms | match expr { x => /* `x` bound here */ } | | let bindings | let x = ...; /* `x` bound here */ | | recursive functions | fn foo() { /* `foo` bound here */ } | | functions parameters | fn foo(x: T) { /* `x` bound here */ } | | recursive types | enum List { Nil, /* `List` bound here */ | | type parameters | struct Point<T> { /* `T` bound here */ } |

For example, let's take a silly example of a Rust function:

type Count = u32;

fn silly<T>((count, data): (Count, T)) -> T {
    match count {
        0 => data,
        count => silly((count - 1, data)),
    }
}

There's actually lots of name-binding at play here! Let's connect the binders to their corresponding binders:

//            ?
//            |
//            v
type Count = u32;
//     |
//     '----------------------.
//  .-------------------------|------------------.
//  |    .--------------------|----*------.      |
//  |    |                    |    |      |      |
//  |    |                    v    v      v      |
fn silly<T>((count, data): (Count, T)) -> T { // |
//             |      |                          |
//          .--'      |                          |
//          |         *--------------.           |
//          v         |              |           |
    match count { //  |              |           |
//             .------'              |           |
//             |                     |           |
//             v                     |           |
        0 => data, //                |           |
//         .--------------.          |           |
//         |              |          |           |
//         |              v          v           |
        count => silly((count - 1, data)), //    |
//                 ^                             |
//                 |                             |
//                 '-----------------------------'
    }
}

Keeping track of the relationships between these variables can be a pain, and can become especially error-prone when implementing evaluators and type checkers. Moniker aims to support all of these binding structures, with minimal pain!

Example

Here is how we would use Moniker to describe a very small functional language, with variables, anonymous functions, applications, and let bindings:

#[macro_use]
extern crate moniker;

use moniker::{Embed, Binder, Rec, Scope, Var};
use std::rc::Rc;

/// Expressions
///
/// ```text
/// e ::= x               variables
///     | \x => e         anonymous functions
///     | e₁ e₂           function application
/// ````
#[derive(Debug, Clone, BoundTerm)]
//                        ^
//                        |
//              The derived `BoundTerm` implementation
//              does all of the heavy-lifting!
pub enum Expr {
    /// Variables
    Var(Var<String>),
    /// Anonymous functions (ie. lambda expressions)
    Lam(Scope<Binder<String>, RcExpr>),
    /// Function applications
    App(RcExpr, RcExpr),
}

pub type RcExpr = Rc<Expr>;

We can now construct lambda expressions by doing the following:

let f = FreeVar::fresh(Some("f".to_string()));
let x = FreeVar::fresh(Some("x".to_string()));

// \f => \x => f x
Rc::new(Expr::Lam(Scope::new(
    Binder(f.clone()),
    Rc::new(Expr::Lam(Scope::new(
        Binder(x.clone()),
        Rc::new(Expr::App(
            Rc::new(Expr::Var(Var::Free(f.clone()))),
            Rc::new(Expr::Var(Var::Free(x.clone()))),
        )),
    )))
)))

More Complete Examples

More complete examples, including evaluators and type checkers, can be found under the moniker/examples directory.

| Example Name | Description | | --------------------- | --------------------------- | | lc | untyped lambda calculus | | lc_let | untyped lambda calculus with nested let bindings | | lc_letrec | untyped lambda calculus with mutually recursive bindings | | lc_multi | untyped lambda calculus with multi-binders | | stlc | simply typed lambda calculus with literals | | stlc_data | simply typed lambda calculus with records, variants, literals, and pattern matching | | stlc_data_isorec | simply typed lambda calculus with records, variants, literals, pattern matching, and iso-recursive types |

Projects using Moniker

Moniker is currently used in the following Rust projects:

• Pikelet: A dependently typed systems programming language

Overview of traits and data types

We separate data types into terms and patterns:

Terms

Terms are data types that implement the BoundTerm trait.

• Var<N>: A variable that is either free or bound
• Scope<P: BoundPattern<N>, T: BoundTerm<N>>: bind the term T using the pattern P
• Ignore<T>: Ignores T when comparing for alpha equality

Implementations for tuples, strings, numbers, slices, vectors, and smart pointers are also provided for convenience.

Patterns

Patterns are data types that implement the BoundPattern trait.

• Binder<N>: Captures a free variables within a term, but is ignored for alpha equality
• Ignore<T>: Ignores T when comparing for alpha equality
• Embed<T: BoundTerm<N>>: Embed a term T in a pattern
• Nest<P: BoundPattern<N>>: Multiple nested binding patterns
• Rec<P: BoundPattern<N>>: Recursively bind a pattern in itself

Implementations for tuples, strings, numbers, slices, vectors, and smart pointers are also provided for convenience.

Roadmap

Moniker is currently good enough to use for initial language prototypes, but there is more work that we'd like to do to make it a more fully-featured name binding and scope handling toolkit.

• [ ] Initial implementation using a locally nameless representation
  • [x] Implement basic type combinators
    • [x] Embed
    • [x] Ignore
    • [x] Nest
    • [x] Rec
    • [x] Scope
  • [ ] Automatically derive traits
    • [x] BoundTerm
    • [x] BoundPattern
    • [ ] Subst
  • [ ] Allow derives to use identifier types other than String
  • [ ] Implement namespaced variables and binders
  • [ ] Performance optimizations
    • [ ] Cache max-depth of terms
    • [ ] Cache free variables of terms
    • [ ] Perform multiple-opening/closing
    • [ ] Use visitors
• [ ] Explore implementing other name-binding schemes
  • [ ] Named with unique indices
  • [ ] Scope Graphs
  • [ ] ...?

References

Here is a list of interesting references and prior art that was helpful when building Moniker. Note that it isn't necessary to read and understand these to use the library, but they might be useful if you would like to contribute!

Papers

• The Locally Nameless Representation
• Binders Unbound
• An overview of Cαml
• Visitors Unchained
• Engineering Formal Metatheory

Blog Posts

• How I learned to stop worrying and love de Bruijn indices
• Announcing DBLib
• Bound

Other Libraries

The API was main