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)`。）
誤報對於引導新使用者而言尤其不利。若一位對類型感興趣的創作者開啟類型檢查後，立刻面對滿屏的虛假紅色波浪線，便會產生強烈動機立即將其關閉。
型別錯誤中的不準確性是不可避免的，因為無法預先判定是否會觸發執行時錯誤。型別系統設計者必須在「容忍誤報」與「容忍漏報」之間做出取捨。在 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的子類型- 因此根據 L 的並集：
(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 等類型系統的經驗，有充分證據表明此類問題在實際中不會出現，因為 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 中是慣用語法，但 DNF 並非如此，我們不希望向使用者呈現此類非慣用類型。
我們的正規化依賴於重寫掉函數類型的並集：
((A) -> B) | ((C) -> D) → (A & C) -> (B | D)此正規化在我們的模型中是正確的，但在集合論模型中則不然。
其次，在 Luau 中，若函數應用 f(x) 的類型為 B，且 f 的類型為 (A) -> B、x 的類型為 A，則該應用之類型亦為 。 出乎意料的是，在集合論模型中，這並非總是成立，原因在於「無人居住的類型」。在集合論模型中，若 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 的全部功能，僅涵蓋函數式子集，但這已足以發現那些細微的功能交互作用——這些問題若在正式環境中浮現，很可能演變成難以修復的錯誤。
原型開發並非萬無一失，例如我們在生產環境中遭遇的主要問題涉及效能與 C++ 標準函式庫，這些問題絕不可能被原型所偵測到。但除此之外，生產環境的實作過程相當順暢（或者至少以 3,000 行程式碼的變更而言，已屬相當順暢）。
後續步驟
語義子類型化已消除了一種誤報來源，但我們仍有其他問題需要追蹤：
- 重載函式的呼叫與運算子
- 對複雜類型表達式的屬性存取
- 表格的唯讀屬性
- 隨時間變換資料型的變數（又稱資料型態狀態）
消除那些多餘的紅色波浪線的征途仍在繼續！
致謝
感謝 Giuseppe Castagna 和 Ben Greenman 對本文草稿提供的寶貴意見。
Alan 負責統籌 Luau 類型系統的設計與實作，該系統驅動了 Roblox Studio 開發中的許多功能。Jeffrey 博士在程式語言研究領域擁有超過 30 年的經驗，長期活躍於眾多開源軟體專案，並持有英國牛津大學的哲學博士學位。
