Syl：编译期依赖类型的新探索
Compile-Time Dependent Types
C++、Rust 和 Zig 等语言虽已具备部分编译期计算能力，但往往受限或缺乏完善的类型系统。我正在开发 Syl 语言，旨在通过模态类型系统（Modal Type System）将编译期计算编码得更自然。Syl 引入了 static 和 erased 两种模式轴，区分值在编译期和运行期的可见性。这使得函数能根据 static 参数进行特化，实现依赖类型，同时保持运行期简单类型。Syl 允许编译期计算包含通用递归，因此类型检查不可判定，无需全性检查器，更适合实际编程而非定理证明。通过 Typed Interpreter 和长度索引向量等示例，展示了 Syl 如何在编译期完成复杂逻辑推导，生成高效且类型安全的运行期代码。
Syl 在编译期是依赖类型的，而在运行期则是简单类型的。
HN 评论区
17- nextaccountic
> 编译期依赖类型
> 编译期依赖类型进入系统编程领域似乎是不可避免的。
C++ 拥有模板和 constexpr，Rust 拥有 const generics，Zig 拥有 comptime，甚至连 C 语言也有 _Generic。然而，这些特性往往受到严格限制，缺乏完善的类型系统，或者两者兼有。
不过……这些语言特性并不是依赖类型的例子。
> 也就是说，Syl 在编译期是依赖类型的，而在运行时则是简单类型的。
> 这是 Staged Compilation with Two-Level Type Theory（https://andraskovacs.github.io/pdfs/2ltt.pdf）的核心思想，尽管它没有被表述为模态类型系统。
但依赖类型（以及静态类型总体而言）在运行时根本不存在！
不过我猜你的意思是，Syl 实现了依赖类型且没有额外开销，比如不需要字典传递（dictionary passing）。也就是说你可以实现完全的型擦除（type erasure）。这个理解准确吗？（我会去读那篇论文）
- carterschonwald
太酷了！我有个长期搁置的项目，在设计理念和影响范围上与它有所重叠，但走向了非常不同的方向。
- superxpro12
我想知道 LTO 在优化这类东西方面表现如何，与手动完成所有编译期解析多态函数和对象的工作相比。