1,941 每月下载量
在 2 crates 中使用

MIT 许可证

6.5MB
209K SLoC

Lambda Mountain

λ☶ (发音为Lambda Mountain) 是一个编译器后端，提供了一个相对干净的 System F<: with Specialization 实现。整个编译器只有5000行代码，因此这可以是一个需要JIT或AOT编译代码生成的项目的良好起点。

LM提供了您想要的抽象级别，从您想要的级别向下。每个LM程序指定要创建的确切二进制对象，因此编译器没有解释的空间。平台特定的定义和功能由库提供。因此，编译器没有关于如何处理平台架构的硬编码逻辑。

LM通过语言前端与语言后端之间的N x M问题进行了解决。LM项目可能需要与定义前端或后端的大代码库进行接口，但核心LM演算可以保持小巧。

汇编器将数据块组合在一起。汇编器不一定理解它们所做的事情的意义，它们只是做。

片段是字符串到S-表达式的键值映射。这种数据结构比典型的汇编器允许更详细的代码操作。

如果我们有多个重载的函数，那么专门化允许我们为任何特定应用程序选择最佳匹配。

f := λ(: x X). x;
f := λ(: y Y). y;

f (: x X)

在这个例子中，函数应用与期望Y类型参数的应用不匹配，因此只有一个可能的候选函数。

type X implies Y;

f := λ(: x X). x;
f := λ(: y Y). y;

f (: x X)

现在两个候选函数都“匹配”，然而X比Y类型窄。所有X都是Y，但不是所有Y都是X。在这种情况下，我们说X比Y是一个“更好的匹配”。

f := λ(: x X). form 1;
f := λ(: x X). form 2;

f (: x X)

在这个例子中，两个候选函数都“匹配”且等效。在这种情况下，我们应用度量来确定最佳匹配。度量是应用于项/类型对的顺序，以确定在非语义情况下哪个是“更好的匹配”。度量在存在不同性能特征的代码表示的等效形式存在多个等效类时非常有用。等效类是另一个高级概念，不需要名义上等效。

专业化使我们能够在通用功能语言级别表达高级思想，并且能够透明地将代码编译成机器码。编译器中没有隐藏的层级。程序员可以检查和验证每个单个转换直到单独的指令。

只要所有重载的函数都提供了显式类型，类型系统就是强归一化和可判定的。

突出特性包括

lambda_mountain