本文为原文前 6,000 字符的节选翻译，完整内容请查看原文。

Compile-Time Dependent Types

Compile-time dependent types seem destined to become a part of systems programming. C++ has templates and constexpr, Rust has const generics, Zig has comptime, and even C has _Generic. However, these features are often highly restricted, lack a proper type system, or both. I am developing Syl, a language that aims to encode compile-time computation within a modal type system. Syl is primarily inspired by András Kovács’ work on two-level type theory, as well as plans for OxCaml. The Syl compiler is available on GitHub.

编译期依赖类型似乎注定要进入系统编程领域。C++ 有模板和 constexpr，Rust 有 const 泛型，Zig 有 comptime，甚至 C 语言也有 _Generic。然而，这些特性往往受到高度限制，缺乏完善的类型系统，或者两者兼而有之。我正在开发 Syl，这是一种旨在将编译期计算编码到模态类型系统中的语言。Syl 主要受到 András Kovács 关于两级类型理论的工作以及 OxCaml 计划的启发。Syl 编译器可以在 GitHub 上找到。

Modes

In Syl, all values possess both a mode and a type. Modes describe properties of values that are independent of their types. For example, OxCaml uses modes to indicate whether a value is uniquely owned, writable, or sendable to another thread. Syl features two mode axes: staticity and erasure. On the staticity axis, a value can be static or dynamic. On the erasure axis, it can be erased or unerased. A static value is knowable at compile time, while a dynamic value may not be. An unerased value is knowable at runtime, while an erased value may not be.

模式

在 Syl 中，所有值都拥有一个模式和一个类型。模式描述了独立于类型的值的属性。例如，OxCaml 使用模式来指示一个值是否被唯一拥有、是否可写，或者是否可以发送到另一个线程。Syl 有两个模式轴：静态性和擦除性。在静态性轴上，值可以是静态的或动态的。在擦除性轴上，值可以是已擦除的或未擦除的。静态值在编译期是可知的，而动态值则不一定。未擦除的值在运行期是可知的，而已擦除的值则不一定。

For instance, literals are static and unerased, as they are clearly knowable at both compile time and runtime. You can verify this with a mode annotation: let x = 0 @ static unerased;;. Each mode axis has a sub-moding relation. If you have a static value, it is safe to forget that it is knowable at compile time and treat it as dynamic. Similarly, an unerased value can be treated as erased. Mode annotations can “weaken” a mode, but not “strengthen” it.

例如，字面量是静态且未擦除的，因为它们在编译期和运行期显然都是可知的。你可以通过模式注解来验证这一点：let x = 0 @ static unerased;;。每个模式轴都有一个子模式关系。如果你有一个静态值，将其视为动态值是安全的，因为这相当于忘记了它在编译期是可知的。同样，未擦除的值也可以被视为已擦除的。模式注解可以“削弱”模式，但不能“加强”它。

Dependent Types

On their own, static and erased modes allow us to explicitly request specialization-based optimizations, but they do not provide dependent types. Functions of static arguments do. For example, let f = fn (erased x : bool) -> if erased x then 0 else true;; allows us to return an integer if x is true and a boolean otherwise. Thus, f has a dependent function type, which encodes how the result type depends on the value of the input.

依赖类型

静态和已擦除模式本身允许我们显式请求基于特化的优化，但它们并不提供依赖类型。静态参数函数则可以。例如，let f = fn (erased x : bool) -> if erased x then 0 else true;; 允许我们在 x 为真时返回整数，否则返回布尔值。因此，f 具有依赖函数类型，它编码了结果类型如何依赖于输入值。

Proofs

Syl supports general recursion in compile-time computations and provides type : type. Allowing either of these features implies that constructing an expression of type t does not prove the proposition corresponding to t. For example, we can implement a function that ostensibly returns a value of any type: let magic = fn (erased t : type) -> fun loop (_ : unit) : t = loop () in loop () ;;. Despite having the type erased type as t -> t, this function never actually produces a value—it is an infinite loop.

证明

Syl 在编译期计算中支持通用递归，并提供了 type : type。允许其中任何一个特性都意味着构造一个类型为 t 的表达式并不能证明与 t 对应的命题。例如，我们可以实现一个表面上返回任何类型值的函数：let magic = fn (erased t : type) -> fun loop (_ : unit) : t = loop () in loop () ;;。尽管其类型为 erased type as t -> t，但该函数实际上从不产生值——它是一个无限循环。