Moniker

Moniker使跟踪编程语言实现中嵌套作用域内的变量变得简单。

而不是手动实现名称处理代码（这通常很繁琐且容易出错），Moniker提供了一些类型和特质，用于在语言的抽象语法树中声明性描述名称绑定。从这个角度来看，我们可以自动推导出相应的名称处理代码！

动机

值得注意的是，"作用域"这一概念在编程中经常出现

例如，让我们来看一个Rust函数的愚蠢示例

type Count = u32;

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

这里实际上有很多名称绑定！让我们将这些绑定者与其对应的绑定者联系起来

//            ?
//            |
//            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)), //    |
//                 ^                             |
//                 |                             |
//                 '-----------------------------'
    }
}

跟踪这些变量之间的关系可能会很痛苦，在实现评估器和类型检查器时尤其如此。Moniker旨在以最小痛苦的方式支持所有这些绑定结构！

示例

以下是使用Moniker描述一个非常小的函数式语言的示例，包括变量、匿名函数、应用和let绑定

#[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>;

我们现在可以通过以下方式构建lambda表达式

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

更完整的示例

更完整的示例，包括评估器和类型检查器，可以在 moniker/examples 目录下找到。

使用Moniker的项目

Moniker目前正在以下Rust项目中使用

• Pikelet: 一种依赖类型系统编程语言

特性和数据类型概述

我们将数据类型分为项和模式

项

项是实现了BoundTerm特质的枚举。

• Var<N>: 一个自由或绑定的变量
• Scope<P: BoundPattern<N>, T: BoundTerm<N>>: 使用模式 P 绑定项 T
• Ignore<T>: 在比较α等价时忽略 T

还提供了元组、字符串、数字、切片、向量和指针的实现，以方便使用。

模式

模式是实现了 BoundPattern 特质的枚举。

• Binder<N>: 在项内捕获自由变量，但在α等价比较时被忽略
• Ignore<T>: 在比较α等价时忽略 T
• Embed<T: BoundTerm<N>>: 将项 T 嵌入模式中
• Nest<P: BoundPattern<N>>: 多重嵌套绑定模式
• Rec<P: BoundPattern<N>>: 递归绑定模式自身

还提供了元组、字符串、数字、切片、向量和指针的实现，以方便使用。

路线图

Moniker目前足够用于初始语言原型，但我们希望做更多工作，使其成为一个更完整的名称绑定和作用域处理工具包。

• 使用局部无名称表示的初始实现
  • 实现基本类型组合
    • 嵌入
    • 忽略
    • 嵌套
    • 递归
    • 作用域
  • 自动推导特质
    • BoundTerm
    • BoundPattern
    • Subst
  • 允许使用除了 String 之外的标识符类型进行派生
  • 实现命名空间变量和绑定器
  • 性能优化
    • 缓存项的最大深度
    • 缓存项的自由变量
    • 执行多次打开/关闭操作
    • 使用访问者
• 探索实现其他名称绑定方案
  • 使用唯一索引命名
  • 作用域图
  • ...?

参考

以下是构建Moniker时有所帮助的一些有趣参考文献和先验知识。请注意，阅读和理解这些内容并非使用库的必要条件，但如果你希望贡献，它们可能有用！

论文

• 本地无名表示法
• 解除绑定
• Cαml概述
• 解除约束的访问者
• 形式元理论工程

博客文章

• 如何停止担忧并爱上de Bruijn索引
• 宣布DBLib
• 绑定

其他库

API主要受Haskell的Unbound和Unbound-Generics库的启发，有一些不同之处。我们做的最主要的变化是将Unbound的单个Alpha类型类替换为两个独立的特质（BoundTerm和BoundPattern）。我们发现这更好地捕捉了库的语义，并且大大减少了意外误用的可能性。

存在许多不同的语言的自绑定库

• Unbound：使用一组表达性类型组合子指定您的数据类型的绑定结构，然后由Unbound处理其余部分！自动推导alpha等价性、自由变量计算、避免捕获的替换等。
• Unbound-Generics：Unbound的独立重新实现，但使用GHC.Generics而不是Replib。
• Cαml：将所谓的“绑定规范”转换为OCaml编译单元的工具。
• alphaLib：一个OCaml库，帮助处理抽象语法树中的绑定结构。
• abbot：为SML生成抽象绑定树
• rabbot：将SML的Abbot移植到Rust
• DBLib：在Coq中处理de Bruijn索引的设施
• Bound：Haskell的DeBruijn索引
• Metalib：宾夕法尼亚本地无名字元理论库
• LibLN：具有有限量化局部无名字符串表示法

贡献

我们非常希望鼓励新贡献者帮助我们！请到我们的Gitter频道聊天 - 如果你对该项目有任何问题，或者只是想打个招呼！

致谢

这项工作部分得益于YesLogic的慷慨支持。