Luau 中的语义子类型
Luau 是首个将语义子类型化的强大功能交到数百万创作者手中的编程语言。
减少误报
Roblox Studio 中“脚本分析”小工具等工具在报告类型错误时存在的一个问题是误报。这些警告是分析过程中的产物，并不对应运行时可能发生的错误。例如，程序
local x = CFrame.new()
local y
if math.random() < 0.5 then
y = CFrame.new()
else
y = Vector3.new()
end
local z = x * y报告的类型错误在运行时不可能发生，因为CFrame同时支持与Vector3和CFrame的乘法运算。（其类型为((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)。）
对于新用户的入门体验而言，误报尤其糟糕。如果一位对类型感兴趣的开发者开启了类型检查，却立刻面对一堆虚假的红色波浪线，这会强烈促使他立即将其关闭。
类型错误中的不准确性在所难免，因为无法预先判断是否会触发运行时错误。类型系统设计者必须在容忍误报（false positives）或漏报（false negatives）之间做出取舍。在 Luau 中，这由模式决定：strict 模式倾向于产生误报，而 nonstrict 模式则倾向于产生漏报。
尽管不准确性在所难免，但我们仍会尽可能消除它们，因为这些不准确会导致虚假错误，并影响自动补全或 API 文档等基于类型的工具的精确性。
子类型作为误报的来源
Luau（以及 TypeScript 或 Flow 等许多其他类似语言）中假阳性的来源之一是子类型化。每当变量被初始化或赋值时，以及每次调用函数时，都会使用子类型化：类型系统会检查表达式的类型是否是变量类型的子类型。例如，如果我们在上述程序中添加类型
local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then
y = CFrame.new()
else
y = Vector3.new()
end
local z : Vector3 | CFrame = x * y那么类型系统会检查 CFrame 乘法的类型是否是 (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame) 的子类型。
子类型化是一个非常有用的特性，它支持诸如类型联合（T | U）和交集（T & U）等丰富的类型构造。例如，number? 被实现为一个联合类型 (number | nil)，其中包含的值要么是数字，要么是 nil。
遗憾的是，子类型与交集型及并集型的交互可能会产生奇怪的结果。早期 Luau 中有一个简单（但相当人为）的案例：
local x : (number?) & (string?) = nil
local y : nil = nil
y = x -- Type '(number?) & (string?)' could not be converted into 'nil'
x = y此错误由子类型化失败引起，旧的子类型化算法报告称 (number?) & (string?) 不是 nil 的子类型。这是一个误报，因为 number & string 没有成员，因此 (number?) & (string?) 的唯一可能成员是 nil。
这是一个人为构造的示例，但开发者确实因这些问题报告了实际问题，例如 https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5。 目前，这些问题主要影响那些使用复杂类型系统功能的创建者，但随着我们使类型推断变得更加准确，联合类型和交集类型将变得越来越普遍，即使在没有类型注释的代码中也是如此。
在 Luau 中，这一类误报已不再出现，因为我们已从旧的语法子类型化方法转向了一种名为语义子类型化的替代方案。
语法子类型
又名“我们以前的做法”。
语法子类型化是一种基于语法的递归算法。处理交集类型和并集类型时需要处理的有趣情况包括：
- 自反性：
T是T的子类型 - 交集 L：当某些
Tᵢ是U的子类型时，(T₁ & … & Tⱼ)是U的子类型 - 左并集：当所有
Tᵢ都是U的子类型时，(T₁ | … | Tⱼ)是U的子类型 - 交集 R：当
T是所有Uᵢ的子类型时，T是(U₁ & … & Uⱼ)的子类型 - 联合 R：当
T是Uᵢ中的某些集合的子类型时，T即是(U₁ | … | Uⱼ)的子类型。
例如：
- 基于自反性：
nil是nil的子类型 - 因此根据 R 的并集性质：
nil是number?的子类型 - 且：
nil是string?的子类型 - 因此根据交集 R：
nil是(number?) & (string?)的子类型。
太好了！遗憾的是，根据这些规则：
number不是nil的子类型- 因此根据交集 R：
(number?)不是nil的子类型 - 并且：
string不是nil的子类型 - 因此根据并集 L：
(string?)不是nil的子类型 - 因此根据交集 L：
(number?) & (string?)不是nil的子类型。
这是语法子类型化的典型特征：当返回“是”的结果时，它是正确的；但当返回“否”的结果时，它可能是不正确的。该算法是一种保守的近似，由于“否”的结果可能导致类型错误，因此这是产生误报的原因。
语义子类型
又名“我们当前的做法”。
与其将子类型化视为语法导向，我们首先考虑其语义，随后再探讨语义的实现方式。为此，我们采用语义子类型化：
- 类型的语义是一组值。
- 交集类型被视为集合的交集。
- 并集类型被视为集合的并集。
- 子类型化被视为集合的包含关系。
例如：
类型 | 语义 |
|---|---|
| { 1, 2, 3, … } |
| { “foo”, “bar”, … } |
| { nil } |
| { nil, 1, 2, 3, … } |
| { nil, “foo”, “bar”, … } |
| { nil, 1, 2, 3, … } ∩ { nil, “foo”, “bar”, … } = { nil } |
并且由于子类型被解释为集合的包含关系：
子类型 | 超类型 | 因为 |
|---|---|---|
|
| { nil } ⊆ { nil, 1, 2, 3, … } |
|
| { nil } ⊆ { nil, “foo”, “bar”, … } |
|
| { nil } ⊆ { nil } |
|
| { nil } ⊆ { nil } |
因此，根据语义子类型，(number?) & (string?) 等同于 nil，但语法子类型仅支持单向关系。
这听起来很合理，但如果我们想在工具中使用语义子类型，就需要一个算法，而事实证明，检查语义子类型并非易事。
语义子类型化很难
确切地说，是 NP 难问题。
我们可以将图着色问题归约为语义子类型化，方法是将图编码为一个 Luau 类型，使得对类型进行子类型化检查的结果与检查图是否无法着色得到的结果相同
例如，对一个三节点、两颜色的图进行着色，可以使用类型来实现：
type Red = "red"
type Blue = "blue"
type Color = Red | Blue
type Coloring = (Color) -> (Color) -> (Color) -> boolean
type Uncolorable = (Color) -> (Color) -> (Color) -> false此时，图可被编码为一种重载函数类型，其子类型为Uncolorable，超类型为Coloring，该重载函数在约束被违反时返回false。每个重载对应一个约束。例如，一条线段的约束规定相邻节点不能具有相同颜色：
type Line = Coloring
& ((Red) -> (Red) -> (Color) -> false)
& ((Blue) -> (Blue) -> (Color) -> false)
& ((Color) -> (Red) -> (Red) -> false)
& ((Color) -> (Blue) -> (Blue) -> false)三角形的情况类似，但端点也不能具有相同的颜色：
type Triangle = Line
& ((Red) -> (Color) -> (Red) -> false)
& ((Blue) -> (Color) -> (Blue) -> false)现在，Triangle是Uncolorable的子类型，但Line不是，因为线段可以被2种颜色着色。这可以推广到任何具有有限种颜色的有限图，因此子类型检查是NP难的。
我们通过两种方式处理这个问题：
- 缓存类型以减少内存占用，以及
- 若类型缓存过大，则抛出“代码过于复杂”的错误。
希望这种情况在实际中不会经常出现。有充分证据表明，像 Standard ML 这样的类型系统（其类型系统是 EXPTIME-complete 的）在实际应用中不会出现此类问题，但在实践中，你必须费尽周折才能将图灵机磁带编码为类型。
类型规范化
用于判定语义子类型的算法是类型规范化。我们不直接受语法引导，而是先将类型重写为规范化形式，然后在规范化类型上检查子类型关系。
规范化类型是以下类型的并集：
- 一个规范化的空类型（
never或nil） - 一个规范化的数字类型（即
never或number） - 一个规范化的布尔类型（即
never或true或false或boolean） - 一个规范化的函数类型（即
never或函数类型的交集）等
一旦类型被规范化，检查语义子类型关系就变得非常简单。
每个类型都可以被规范化（唉，虽然在泛型类型包方面存在一些技术限制）。关键步骤包括：
- 移除不匹配的原始类型交集，例如将
number & bool替换为never，以及 - 移除函数的联合，例如将 `
((number?) -> number) | ((string?) -> string)` 替换为 `(nil) -> (number | string)`。
例如，对 (number?) & (string?) 进行规范化处理会移除 number & string，最终仅剩 nil。
我们最初尝试实现类型规范化时应用得过于广泛，但这导致了可怕的性能问题（复杂的代码从不到一分钟的类型检查变成了需要运行一整夜）。 原因简单得令人恼火：Luau 的子类型算法中有一项用于处理自反性的优化（T 是 T 的子类型），该优化会执行一次低成本的指针相等性检查。而类型规范化会将指针相等的类型转换为语义等价（但指针不相同）的类型，这会显著降低性能。
鉴于这些性能问题，我们仍将语法子类型化作为子类型化的首选检查方式，仅在语法算法失败时才进行类型规范化。这种做法是可靠的，因为语法子类型化是对语义子类型化的保守近似。
实用语义子类型化
现成的语义子类型检查与 Luau 中实现的略有不同，因为它要求模型是集合论的，这要求函数类型的成员“像函数一样行为”。我们放弃这一要求有两个原因。
首先，我们将函数类型规范化为函数的交集，例如以下这种由函数联合与交集构成的混乱结构：
((number?) -> number?) | (((number) -> number) & ((string?) -> string?))规范化为一个重载函数：
((number) -> number?) & ((nil) -> (number | string)?)集合论语义子类型化不支持这种规范化，而是将函数规范化为析取范式（函数交集的并集）。出于易用性考虑，我们不采用这种做法：重载函数在 Luau 中是惯用语法，但析取范式并非如此，我们不希望向用户展示此类非惯用类型。
我们的规范化依赖于重写掉函数类型的并集：
((A) -> B) | ((C) -> D) → (A & C) -> (B | D)这种规范化在我们的模型中是正确的，但在集合论模型中则不然。
其次，在 Luau 中，若 f 的类型为 (A) -> B 且 x 的类型为 A，则函数调用 f(x) 的类型为 B。 出乎意料的是，在集合论模型中，由于存在无人居住的类型，这一结论并不总是成立。在集合论模型中，如果 x 的类型为 never，则 f(x) 的类型为 never。我们不希望让用户承担函数应用存在特殊边角案例的负担，尤其是因为该边角案例仅可能出现在死代码中。
在集合论模型中，无论 A 和 B 的值为何，(never) -> A 都是 (never) -> B 的子类型。但在 Luau 中并非如此。
基于这两个原因（主要涉及使用便利性而非技术问题），我们放弃了集合论的要求，转而采用务实的语义子类型化。
否定类型
Luau 的类型系统与现成的语义子类型化之间的另一个区别在于，Luau 并不支持所有否定类型。
需要否定类型的一个常见场景是在条件语句的类型检查中：
-- initially x has type T
if type(x) == "string" then
-- in this branch x has type T & string
else
-- in this branch x has type T & ~string
end此处使用了否定类型~string，其值必须是非字符串。
在 Luau 中，我们仅允许对 string、function、Part 等测试类型进行此类类型细化，而不允许对 (A) -> B 等结构类型进行此类操作，从而规避了通用否定类型的常见情况。
原型设计与验证
在设计 Luau 的语义子类型算法期间，方案曾发生过变更（例如，最初我们以为可以使用集合论子类型）。在这个快速变化的阶段，能够快速迭代至关重要，因此我们最初实现了原型，而不是直接跳到正式实现。
验证原型至关重要，因为子类型算法可能存在意想不到的边界情况。出于这个原因，我们选择了 Agda 作为原型设计语言。Agda 不仅支持单元测试，还支持机械化验证，因此我们对设计充满信心。
该原型并未实现 Luau 的全部功能，仅实现了其函数式子集，但这已足以发现一些微妙的功能交互问题——这些问题若在生产环境中出现，很可能演变为难以修复的 bug。
原型设计并非完美无缺，例如我们在生产环境中遇到的主要问题涉及性能和 C++ 标准库，这些是原型设计永远无法检测到的。但除此之外，生产环境的实现过程相当直接（或者说，至少对于 3kLOC 的改动而言已是如此）。
后续步骤
语义子类型化消除了一个误报源，但我们仍需追踪其他问题：
- 重载函数的调用和运算符
- 对复杂类型表达式的属性访问
- 表的只读属性
- 随时间变化的变量（即类型状态）
消除那些多余的红色波浪线的征程仍在继续！
致谢
感谢 Giuseppe Castagna 和 Ben Greenman 对本文草稿提出的宝贵意见。
Alan 负责协调 Luau 类型系统的设计与实现，该系统推动了 Roblox Studio 开发中的许多功能。Jeffrey 博士在编程语言研究领域拥有 30 多年的经验，是众多开源软件项目的活跃成员，并持有英国牛津大学的哲学博士学位。
