Elixir 把 set-theoretic 型別變成預設——dynamic()、narrowing 與 verified bug 的編譯期帳本

Elixir 1.20 把醞釀自 2022 的 set-theoretic gradual typing 系統推成語言預設。它不是一個你要 opt-in 的外掛工具，也不是一套要你先補滿 spec 才會動的型別檢查器——它對整個程式做推論與檢查，前提是你一個型別都不必寫。這套系統的野心很明確：在不要求 annotation、不破壞既有程式、且把 false positive 壓到極低的前提下，找出那些「執行到就一定會爆」的型別違規。本文拆解它的構造——型別怎麼用 union／intersection／negation 描述、為什麼 dynamic() 不是傳統 gradual typing 的 any()、narrowing 的推論機制長什麼樣、verified bug 與一般 warning 的判準在哪、為什麼 false-positive 率壓得下來，以及它和 Dialyzer 的 success typing 差在哪。

用 union、intersection、negation 描述型別

set-theoretic typing 的核心很簡單——型別就是值的集合，而集合天生支援三個運算：聯集、交集、補集。把這三個運算當成型別語言的一級公民，整套型別系統就獲得了一種傳統 nominal／structural 型別表達不出來的精確度。

聯集寫成 integer() or binary()，意思是「這個值要嘛是整數，要嘛是 binary」。這不是某個被人為命名的 sum type，而是兩個型別集合的直接 union——任何兩個型別都能即時 or 起來，不需要先宣告一個 wrapper。Elixir 的函式天生會回傳 {:ok, value} 或 :error 這種形狀，union 正好是描述它們的母語。

交集多半隱含在 guard 裡。當你寫 is_list(x) and is_integer(y)，型別系統把它讀成兩條約束的交集——x 落在 list()、y 落在 integer()。intersection 也是描述「同時滿足多個形狀」的工具，例如一個既是 map 又必須含某個 key 的值。

補集（negation）是這套系統最不傳統、也最有威力的一塊。當程式碼裡出現 not is_map_key(x, :foo)，型別系統推得出 x 的型別是 %{..., foo: not_set()}——一張 map，其中 :foo 這個 key 明確「不存在」。negation 讓系統能描述「不是某個東西」，而這正是 case 分支用來剔除可能性的關鍵：走到某個分支，意味著前面的 pattern 都沒中，於是那些型別被 negate 掉了。

把三個運算組合起來，型別就成了一種代數。leading 的 ... 是另一個約定——%{..., a: number()} 表示「一張至少含 a: number() 的 map，其他 key 不限」，相對於封閉的 %{a: number()}（只有這一個 key）。這個開放／封閉的區別在 narrowing 時會反覆出現：每觀察到一次 field access，就往這張 map 上多釘一條約束。

narrowing——型別隨變數被使用而精煉

傳統 gradual typing 的型別在變數宣告當下就定死了；set-theoretic 系統的型別卻是「邊用邊收斂」。這就是 narrowing——一個變數的型別，會隨著你對它做的每一個操作而被精煉。下面這個 playground 把 narrowing 拆成一條操作流水線：你沿著流水線推進，看 data 的推論型別怎麼一步步收緊。

拖曳滑桿沿操作流水線推進 · 5 個步驟逐步收斂型別

操作步數 0 / 4

起點

data :: dynamic()

尚未對 data 做任何觀察，型別維持在最寬的 dynamic()。

把這條流水線寫成真正的 Elixir，就是這樣一段函式：

def add_a_and_b(data) do
  data.a + data.b
end

在這個函式體裡，data 從進來時的 dynamic()，被 .a 與 .b 兩次 field access 加上算術運算，narrow 成 %{..., a: number(), b: number()}。系統沒有要你寫任何 spec——它純粹從「你怎麼用這個變數」反推出它必須是什麼。一旦推到這裡，後面若再出現 data.a + data（把整張 map 拿去和 number 相加），就成了一個無法調和的矛盾：data 同時被要求是 map（因為 .a）又是 number（因為它被當加數）。這個矛盾不是猜測，是 narrowing 累積出來的結論。

值得停下來看清楚 narrowing 的單調性——型別只會變窄，不會變寬。每一次對 data 的觀察，都是在它現有的型別上再交集一條新約束：存取 .a 交上 %{..., a: term()}，把 .a 拿去做算術再交上 %{..., a: number()}，多存取一個 .b 又釘上 b: number()。intersection 是這條收斂的底層運算，而 intersection 的結果永遠不會比兩個輸入更寬。這個單調性是整套推論能終止、也能被信任的根本——系統不需要回頭推翻先前的結論，只需要一路把約束疊上去。當這串約束疊到自相矛盾（同一個變數被要求既是 map 又是 number），矛盾就是 narrowing 的自然產物，而不是另外跑一輪分析才湊出來的判斷。

同一個變數在不同 scope 裡可以 narrow 成不同型別，這一點對理解誤報率很關鍵。一個函式參數進來是 dynamic()，在 case 的某一分支被收斂成 binary()，在另一分支被收斂成 nil——這兩個收斂彼此獨立，互不污染。narrowing 是區域性的、跟著控制流走的，系統不會把某一分支裡學到的約束錯誤地套到另一分支。正因如此，它對 Elixir 那種「同一個變數在不同分支代表不同情形」的慣用寫法貼合得很好，而不會因為一個變數在某處被用成 map 就武斷地認定它到處都是 map。

narrowing 不只發生在 field access。guard、pattern match、case 分支都是 narrowing 的來源，這正是 1.20 把型別檢查鋪到語言全部控制流的原因。

guard、pattern matching、case 都被收進推論

1.20 的型別檢查覆蓋了 Elixir 三種最常見的控制流構造，每一種都被當成 narrowing 的訊號源。

guard 是最直接的一種。一道 when is_binary(x) or is_integer(x) 直接把 x 收斂成 binary() or integer()。更精巧的是尺寸類 guard——tuple_size(x) < 3 讓系統記住「x 至多兩個元素」，於是之後若出現 elem(x, 3)，系統知道這個 index 必然越界，直接報違規。map／list 的尺寸檢查也被轉成「是否為空」的分析。

pattern matching 把解構與型別推論綁在一起：

def example({:ok, x} = y) when is_binary(x) or is_integer(x)

這一行同時做了兩件事：pattern {:ok, x} = y 推得 y :: {:ok, binary() or integer()}，而綁在裡頭的 x 被 guard 收斂成 binary() or integer()。tuple 的形狀、元素的型別、外層 binding 的型別，全在一行裡被推完。

case 的威力在於分支之間的型別會互相剔除。看這段幾乎每個 Elixir 程式都會寫的程式：

case System.get_env("SOME_VAR") do
  nil -> :not_found
  value -> {:ok, String.upcase(value)}
end

System.get_env/1 回傳 binary() or nil。第一個分支吃掉 nil，於是走到第二個分支時，value 的型別被 narrow 成「不可能是 nil」——也就是 binary()。系統因此知道 String.upcase(value) 是安全的，不會誤報。這是 negation 在 case 上的具體應用：第二分支的型別是「原型別」減去「前面分支已匹配的型別」。下面這個切換器把這套「分支剔除」攤開來看。

三種構造合起來，narrowing 就不再是 field access 的局部花招，而是貫穿整個函式控制流的推論機制。系統在每個分歧點都重新計算「此處變數還可能是什麼」，並把不可能的情形用 negation 削掉。

dynamic() 為什麼不是 any()

傳統 gradual typing 的逃生艙是 any()——標成 any() 的值，型別檢查器一律放行，不報任何違規。這讓 gradual typing 在實務上常常退化成「動態型別加一層裝飾」：只要某處塞了 any()，矛盾就被它吸收掉。Elixir 的 dynamic() 走的是完全相反的路——它不是「什麼都行」，而是「在 dynamic 範圍內，仍然套用 set-theoretic 的相容性判準」。差別落在兩個性質上：compatibility 與 narrowing。

compatibility 決定何時報違規。把一個 dynamic(integer() or binary()) 餵給一個只接受 map 的函式，any() 會默默放行；dynamic() 則檢查供給型別與接受型別是否 disjoint。只有在兩者「完全不相交」時，才算違規。如果兩者有任何 overlap，系統就假設那次呼叫落在交集裡，放行。這是一條刻意保守的規則——它的目的不是抓出所有可疑之處，而是只在「絕無可能成立」時才喊停。

這條「只在完全 disjoint 時才喊」的規則，避開的正是傳統 gradual typing 最折磨人的那一類 false positive。設想一個函式宣稱接受 integer() or atom()，而你傳進去的值被推成 dynamic(integer() or binary())。這兩個型別有交集——integer() 同時落在供給與接受兩側。一個天真的型別檢查器可能因為 binary() 這一支不被接受就報違規，但這次呼叫在 runtime 完全可能成功（只要實際傳進去的是整數）。dynamic() 的 compatibility 規則因此選擇放行：既然兩集合相交，系統就假設這次呼叫落在交集裡，不喊。它寧可錯過一個「有時會炸」的可疑呼叫，也不願誤殺一個「有時合法」的程式——因為前者頂多漏報，後者卻會教開發者學會無視警告。

把這件事說得更直白：any() 的問題不在於它太寬，而在於它讓矛盾消失。任何牽涉 any() 的操作，型別檢查器都查不出問題，因為 any() 與一切相容。dynamic() 反過來——它一樣寬，但寬不等於沉默。它保留了 set-theoretic 的全部判準，只是把「報違規」的門檻設在 disjoint 這條最保守的線上。於是你得到一個既不會因為塞了逃生艙就整段失明、又不會對相交型別亂喊的中間地帶。這是 1.20 能對海量無註記程式做出「有用但不吵」分析的關鍵設計取捨。

narrowing 則讓 dynamic() 不會永遠停在最寬。前一節那條流水線就是 dynamic 值被 narrow 的過程：即使 data 進來是 dynamic()，一旦你用 .a，它在這個 scope 內就被收斂成含 a 的 map。any() 沒有這個能力——它是一個吸收一切的黑洞，而 dynamic() 是一個會隨上下文收緊的窗。

下面這個切換器把 compatibility 的判準攤開：拖動讓供給型別與接受型別從 disjoint 滑到 overlapping，看系統的判決如何翻轉。

拖曳滑桿讓兩個型別集合分離或重疊 · 看 disjoint 與 overlap 各自的判決

供給／接受重疊度 0%

disjoint —— 違規

供給與接受型別毫無交集，這次呼叫不可能成立，系統報違規。

verified bug 與 warning 的判準

1.20 把它找到的問題分成兩個層級，這個區分是整套系統取信於開發者的關鍵。一般的 warning 是「這裡看起來可疑」；而 verified bug 是「這段程式如果執行到，runtime 保證會失敗」。後者不是推測，是斷言。

判準回到 compatibility：當供給型別與接受型別 disjoint，那次操作在任何 runtime 路徑下都不可能成功——這就是 verified bug。前面 data.a + data 的例子正是如此：data 已被 narrow 成 map，而 + 的另一個運算元要求 number，map 與 number 是 disjoint 的，這行只要被執行就一定炸。系統因此能拍胸脯說這是 bug，而不只是 code smell。

這個兩層分級之所以重要，是因為它直接決定了開發者會不會繼續看警告。一般 warning 帶著「可能」的語氣——它指向一處看起來不對勁、但未必會在每條路徑上失敗的地方，開發者讀的時候得自己判斷值不值得理。verified bug 則沒有這層曖昧——它的契約是「這行只要被執行，runtime 一定爆」。系統敢做這個斷言，是因為它背後站著 disjoint 這個不可動搖的數學事實：兩個毫無交集的型別之間，沒有任何一個值能同時屬於兩者，因此沒有任何 runtime 輸入能讓這次操作成功。warning 是啟發式的觀察，verified bug 是邏輯上的證明，兩者的可信度天差地別。把它們分開，開發者就能對 verified bug 給予近乎無條件的信任，而不必每次都退回去人工複查。

false-positive 率壓得低，根源也在這裡。系統只在能拿出 disjoint 證明時才升級成 verified bug，其餘一切疑點要嘛降級成普通 warning，要嘛乾脆沉默。這條紀律的代價是會漏掉一些「多數路徑會炸、但理論上存在一條僥倖成功路徑」的情形——這些被刻意放過了。但這正是設計者願意付的代價：一個會誤殺合法程式的工具，用不了幾次就會被整個團隊在 CI 裡靜音；而一個只在百分之百確定時才開口、開口就準的工具，才會被人真正信任並據以行動。誤報率不是一個被動的統計結果，而是被 disjoint 這條判準主動鎖住的設計指標。

同一套 disjoint 分析還順手抓出 dead code。當 case 的某個分支，其 pattern 的型別與「走到此處時主題還可能的型別」完全 disjoint，那個分支永遠不會被選中——它是死的。narrowing 跨分支累積出的剩餘型別，讓系統能標出既有 codebase 裡的冗餘分支與不可達程式。verified bug 與 dead code 共用同一個引擎：前者是「該成立卻不可能成立」，後者是「該被選中卻不可能被選中」。

把 disjoint 當判準的代價是保守——系統只在「百分之百會失敗」時才升級成 verified bug，其餘一律降級或沉默。官方的說法是，1.20 能在既有程式裡有效率地找出 verified bug，不增加開發者負擔，且 false positive 率極低。下面這個 slider 把 success typing 與 set-theoretic 對同一段程式的反應並排——左邊是 Dialyzer 的 success typing，右邊是 1.20。

拖曳中線比較兩套系統對同一段程式的報告

Dialyzer · success typing

data.a + data

傾向沉默。success typing 的設計哲學是「只報絕對成立的失敗」，且需要靠 inference 與 spec；對未標註程式的覆蓋與精度，常常不足以斷言這一行必敗。

Elixir 1.20 · set-theoretic

data.a + data

verified bug。data 已 narrow 成 map，與 number 的接受型別 disjoint——這行執行到必失敗。零註記、編譯期、極低誤報。

這個對照值得展開，因為 Elixir 社群對「BEAM 上的型別分析」並不陌生——Dialyzer 的 success typing 早已是 Erlang／Elixir 世界的既有方案。理解 1.20 的價值，最快的路徑是看它和 success typing 在哲學與機制上的異同。

相同之處在於「保守」這個取向。success typing 的核心信條是寧可漏報、絕不誤殺——它只在能證明某個呼叫必定失敗時才警告。set-theoretic 的 compatibility 規則骨子裡是同一種克制：只有 disjoint 才報違規。兩者都把「不誤殺合法程式」放在「抓出所有 bug」之上，因為一旦誤報多了，開發者就會整體忽略警告，工具的價值歸零。

差異在於表達力與覆蓋。success typing 在 BEAM 層做 over-approximation，對未標 spec 的程式，其推論精度與對 Elixir 語言構造（pattern、guard、protocol）的貼合度有限。set-theoretic 系統把 union／intersection／negation 設成一級運算，narrowing 機制讓它能在零註記下沿控制流逐步收斂型別，於是對 case 分支剔除、guard 收斂、field access 這類 Elixir 慣用法的推論精度高得多。更關鍵的是定位：1.20 不是一個要你另外跑的工具，而是語言預設的一部分——每次編譯都在做。

1.20 的另一張底牌是基準成績。它在 If T: Benchmark for Type Narrowing 的 13 個類別裡通過了 12 個——這是一套專門量測 type narrowing 能力的基準。下表把覆蓋面攤開。

點欄位標題排序 · narrowing 來源 × 機制 × 狀態

narrowing 來源	收斂機制	範例構造	狀態
field access	open map 釘約束	data.a	covered
type guard	union 收斂	is_binary(x) or is_integer(x)	covered
size guard	越界／空性分析	tuple_size(x) < 3	covered
key guard	negation 補集	not is_map_key(x, :foo)	covered
pattern match	解構 + binding 推論	{:ok, x} = y	covered
case 分支	分支剔除 negation	nil -> ...; value -> ...	covered
dead code	disjoint 分支偵測	不可達 clause	covered
recursive type	遞迴展開	巢狀自指型別	roadmap
parametric type	型別參數化	泛型容器	roadmap

第一個里程碑，以及 roadmap 上還沒到的站

1.20 完成的是「第一個開發里程碑」——對每一個 Elixir 程式做型別推論與 gradual 型別檢查，全程不引入任何型別註記。這個里程碑的具體產出是：自動偵測 dead code、找出 verified bug、極低的 false positive、以及把型別檢查鋪到 guard／pattern matching／case 與大量標準函式庫。但「語言預設」不等於「功能完整」——roadmap 上還有幾站沒到，而它們正是擋在「真正的型別簽章」前面的技術障礙。

1.20 完成的里程碑與 roadmap 上未到的站

• 全程式型別推論done · 1.20

  零註記對每個 Elixir 程式做推論與 gradual 檢查。

• narrowing 與 verified bugdone · 1.20

  沿控制流收斂型別，找出保證 runtime 失敗的違規。

• dead code 偵測done · 1.20

  用 disjoint 分析標出不可達分支與冗餘 clause。

• recursive typesroadmap

  尚待解決能否「有效率地」實作遞迴型別。

• parametric typesroadmap

  能否高效實作參數化型別仍在研究中。

• map 列舉roadmap

  把 map 當 enumerable 高效走訪 key-value，解法仍在研究。

全程式型別推論 · done

1.20 對每個 Elixir 程式做型別推論與 gradual 型別檢查，不需任何型別註記。這是「第一個開發里程碑」的核心承諾——把分析做成語言預設，而非 opt-in 工具。

narrowing 與 verified bug · done

型別沿 field access、guard、pattern、case 逐步收斂；當供需型別 disjoint，升級成 verified bug——保證 runtime 失敗的違規。極低的 false positive 率是設計目標。

dead code 偵測 · done

與 verified bug 共用 disjoint 引擎：當某 clause 的型別與「走到此處的剩餘型別」完全 disjoint，那條 clause 永不被選中，被標為不可達。

recursive types · roadmap

能否「有效率地」實作遞迴型別仍待研究。沒有它，自指型別（如樹、鏈表）無法被完整描述，這是型別簽章前的障礙之一。

parametric types · roadmap

參數化（泛型）型別的高效實作同樣未定。它關乎容器型別能否帶著元素型別資訊流動。

map 列舉 · roadmap

把 map 當 enumerable 高效走訪 key-value 的方案仍在研究。這三項都解決後，typed struct 定義與最終的型別簽章才會被引入。

把這幾站連起來看，1.20 的定位就清楚了：它先把「無註記也能推論與檢查」這件最難的事做穩——拿到 narrowing、verified bug、dead code 與極低誤報——再回頭處理 recursive、parametric 這些表達力上的缺口。順序是刻意的：先讓系統對既有的、沒人寫過型別的海量 Elixir 程式有用，再談錦上添花的 annotation。

對下週就要寫 Elixir 的人來說，最實際的影響是：升上 1.20 之後，編譯器會開始對你那些 {:ok, _} 與 case 慣用法做真正的型別推論，並在它「百分之百確定會炸」時告訴你——而且它幾乎不會在不確定時亂喊。這意味著既有 codebase 升級時，你看到的不會是滿屏雜訊，而是一張精挑過的 verified bug 與 dead code 清單。

What this enables：set-theoretic 型別讓 Elixir 在不要求一行 annotation 的前提下，把「這段程式執行到一定會失敗」從工程師的直覺變成編譯器的斷言——union／intersection／negation 是語法，narrowing 是引擎，而 disjoint 是它敢於開口的底線。