大家好，我是朱子潤，很高興為大家帶來本次有關類型檢查與推導的分享。

本次分享的目標群體是對程序語言理論和類型檢查感興趣的工程師，所以內容以直覺為主，理論為輔。本次分享主要內容分為四個部分：

從日常的編碼場景來說一下類型檢查和類型推導的作用

概念上如何實現一個簡單的類型檢查與推導器（我將用 TC 和 TI 作為類型檢查與推導的簡寫）

學界是如何嚴格定義類型檢查與推導的

探討學界和工業界對其的側重點

# 類型檢查 & 類型推導 #

# 什么是類型檢查？

在介紹類型檢查 (type check) 前，我們先看一個編譯流程圖，如下圖示，輸入的程序會依次進行詞法分析、語法分析、語義分析、中間代碼生成、代碼優化、目標代碼生成。類型檢查其實就被涵蓋在語義分析中（即 semantic analysis）。

圖片來源：https://github.com/Elzawawy/compiler-frontend

如果我們看一個函數式語言的架構圖，比如 Haskell，它可能會明確地標出在解析 parse 與 rename 之后，會有一個類型檢查 type check 的階段，在此之后還有些其他比較復雜的工作比如后端代碼生成。

圖片來源：https://github.com/Elzawawy/compiler-frontend 那么，類型檢查是怎樣的語義分析呢？

顧名思義，類型檢查的主要作用就是 找到程序中的類型錯誤。我們來看兩種簡單而又典型的類型錯誤：不兼容的賦值 incompatible assignment 與 不兼容的函數調用 incompatible function calls。

不兼容的賦值：比如當我們在聲明一個變量后，給其賦一個類型不兼容的值（一個聲明為布爾類型的變量被賦一個整數的值）。

不兼容的函數調用：比如在函數調用時，形參與實參的類型不匹配。

如下是一個 C++ 中比較典型的例子。變量 x 的類型是 Char，給 x 賦值了一個字符串 "abc"，就會出現一個 warning，原因就是賦值時類型不兼容。

下圖 Java 的例子中，我們 switch 了一個布爾值 true，編譯器會報錯：switch 接受一個整數值，不能用布爾值，即類型不兼容。

還有一類情況，如下 Swift 的代碼示例中，我們聲明了兩個類 C 和 D，然后聲明一個變量 x 并用一個三元表達式來初始化，三元表達式的兩個分支分別創建了 C 和 D 的實例。這里編譯器也會報錯，說 C 和 D 類型不匹配，mismatching。這是因為編譯器無法找到 C 和 D 的公共父類型，即編譯器嘗試將 C 和 D 的所有父類找出來，發現它們沒有交集，所以說沒有公共父類型。（不過這樣一類問題其實是通過類型推導發現的。）

而如果 D 繼承 C，那它們的公共父類型就變成 C 了，這個錯誤也就消除了。

前三個例子的對比如下。

# 什么是類型推導？

在第一部分，我們簡單介紹了類型檢查，最后引出了一點兒類型推導 (type inference)：類型推導找類型錯誤的方法是去看程序片段能否有一個類型，這個類型不是事先標注好的。

除此之外，類型推導更大的好處是可以讓程序編碼更加地高效。比如類型推導可以省掉大量無聊的類型注解 type annotations，讓程序員可以聚焦在代碼的業務邏輯上；比如類型推導還可以友好地掩蓋掉像泛型 generics 或者多態 polymorphisms 這樣的類型復雜性。

如下所示的函數調用中，尖括號里很長的部分是一個泛型參數，如果有類型推導的話，那我們可以省略掉這一長串內容，直接寫成 f(m)，程序員無需理解背后的理論，可以輕松地使用多態函數，掩蓋一些復雜度。

f>>(m) ↓ f(m)

分別以 C++，Java，Swift 為例，對比一下在沒有類型推導和有類型推導的情況下，我們寫的代碼。

C++：

Java：

Swift：

借住類型推導，三個例子的對比如下。

接下來，我們看一下如何簡單地實現類型檢查與推導 TC & TI，這部分也是本次分享的干貨。

# 編寫一個類型檢查器 #

# 遞歸下降

類型檢查器 type checker 一般是遞歸下降 (recursive and descent) 的，(個人認為只有骨骼清奇的人才才能寫出自底向上的版本)，我們定義一個函數 Check : (AST, Type) -> Bool。這個函數接受兩個參數，第一個參數是抽象語法樹 AST，即要檢查的語法樹節點，第二個參數是目標類型。函數返回一個布爾值，用于告訴我們檢查的節點是否有給定的目標類型。

用簡單的例子來說明，假設我要檢查這樣一棵語法樹（如下圖所示），看它是不是 Int 類型。這棵樹很簡單，是一個加法，有左右兩個分支，左邊是 1，右邊是 false。按照遞歸下降，我們先遞歸檢查左子樹，往下走一步，看 Lit 節點有沒有 Int 類型，然后再遞歸往下走，看 1 有沒有 Int 類型。

此時，類型檢查返回的結果是 true：即 1 有 Int 類型，那么這個返回結果就可以向上傳遞直至頂層。那么我們對于左子樹的檢查就完成了，它返回 true。

接下來，同樣按照遞歸下降的方式檢查右子樹，直到最后檢查 false 是否是 Int 類型，(鑒于一般語言是不允許的，因此) 結果返回 false。我們將這個返回結果向上傳遞至頂層。

此時左子樹的返回結果 true 與右子樹的返回結果 false 做一個邏輯與的操作，得到最終的檢查結果為 false，即對這棵語法樹的類型檢查會失敗。

# 偽代碼示例

接下來我們用偽代碼來解釋一下如何實現 (這部分代碼會比較像 Haskell)。說明：a <: b 表示 a 是 b 的一個子類型 subtype。

首先，編寫 Check 的類型。Check 有兩個參數：語法樹 ast 和目標類型 ty。我們給 ast 做模式匹配。

?

Check?:?(AST,?Type)?->?Bool
Check?(ast,?ty)?=?case?ast?of?pattern?match

?

加法類型檢查

我們以上一節的加法場景為例，將加法的左右子樹分別綁定到新的變量 l 和 r，分別遞歸檢查左子樹和右子樹，檢查的目標類型仍然是 ty。最后將兩邊子樹的檢查結果用邏輯與 && 連接起來，

?

Check?(ast,?ty)?=
??Add(l,r)?--->?Check(l,?ty)?&&?Check?(r,?ty)

?

字面值類型檢查

在剛才的例子中，我們遇到了字面量，那么我們可以檢查字面量的類型是否是目標類型的子類型，

?

Check?(ast,?ty)?=?case?ast?of?pattern?match
??Lit(n)???--->?typeOf(n)?<:?ty

?

函數定義類型檢查

接下來，我們介紹兩類比較有意思的情況，即函數定義和函數調用的類型檢查。先來看函數定義。如果我們的語法樹是一個函數定義的節點，那么我們可以分別將函數名、函數參數、函數體分別綁定到 f, param, body 上，

?

Check?(ast,?ty)?=
??--?function?definitions
??FunAbs(f,?param,?body)?--->

?

接下來我們來做檢查。因為我們在做函數定義時，形參名 pName 后會跟形參類型 pTy，即 fun(pName : pTy)。因此，我們可以進一步用模式匹配將形參節點解構為聲明處的名字和類型。

這里我們使用 let 來做模式匹配，將 param 解構成 Param(pName, pTy)（即程序片段 fun(pName : pTy) 對應的 AST)，

?

Check?(ast,?ty)?=
??--?function?definitions
??FunAbs(f,?param,?body)?--->
????--?pattern?match?fun(pName?:?pTy)
????let?Param(pName,?pTy)?=?param

?

第二步，我們將輸入的目標類型也通過模式匹配來解構：這個目標類型一定要是一個函數類型才可以，否則報錯 (這里的偽代碼僅做示意，因此省略掉報錯的環節了哈)。那么，函數類型可以解構為參數類型和返回類型。

因此，使用 let 來做模式匹配，將目標類型 ty 中解構出來的參數類型綁定到 parTy，返回類型綁定到 retTy，

?

Check?(ast,?ty)?=
??--?function?definitions
??FunAbs(f,?param,?body)?--->
????--?pattern?match?fun(pName?:?pTy)
????let?Param(pName,?pTy)?=?param
????let?FunTy(parTy,?retTy)?=?ty

?

基于前述步驟解構出來的數據，我們可以用目標類型解構出的返回類型 retTy 來與函數體的類型 body 做檢查，遞歸地檢查函數體是否是 retTy 的子類型。此外，我們還需要檢查函數聲明處的形參類型 pTy，與目標類型解構出來的形參類型 parTy 是否形成了有效的子類型關系 (后面會展開解釋什么是有效的子類型關系)。

?

Check?(ast,?ty)?=
??--?function?definitions
??FunAbs(f,?param,?body)?--->
????--?pattern?match?fun(pName?:?pTy)
????let?Param(pName,?pTy)?=?param
????let?FunTy(parTy,?retTy)?=?ty
????parTy?<:?pTy?&&?Check(body,?retTy)?--?allow?subtyping

?

函數調用類型檢查

接下來我們來看函數調用的檢查。我們需要傳入被調用的函數 f 和傳給函數的參數 arg。在此之前該函數已經被定義了，因此可以用 typeOf(f) 獲得定義的函數類型，包括形參類型 parTy 和返回類型 retTy。

?

Check?(ast,?ty)?=?case?ast?of?pattern?match
??--?function?invocations
??FunApp(f,?arg)?--->
????let?FuncTy(parTy,?retTy)?=?typeOf(f)

?

我們要檢查的是函數調用時的實參 arg 是否滿足定義處的形參類型 parTy。以及函數定義處的返回類型 retTy 是否滿足傳入的目標返回類型 ty。

?

Check?(ast,?ty)?=?case?ast?of?pattern?match
??--?function?invocations
??FunApp(f,?arg)?--->
????let?FuncTy(parTy,?retTy)?=?typeOf(f)
????Check(arg,?parTy)?&&?retTy?<:?ty

?

以上就是幾個簡單常見的類型檢查例子，偽代碼示意如下。要進一步說明的是，“是否滿足子類型關系”在函數相關的類型檢查中是比較特殊的。在檢查返回類型時，我們需要判斷是否滿足協變 co-variance，即 retTy <: ty；而在檢查入參類型時，需要判斷是否滿足逆變 contra-variance，即 parTy <: pTy。

?

Check?:?(AST,?Type)?->?Bool
Check?(ast,?ty)?=?case?ast?of?pattern?match
??Add(l,r)?--->?Check(l,?ty)?&&?Check?(r,?ty)
??Lit(n)???--->?typeOf(n)?<:?ty

??--?function?definitions
??FunAbs(f,?param,?body)?--->
????--?pattern?match?fun(pName?:?pTy)
????let?Param(pName,?pTy)?=?param
????let?FunTy(parTy,?retTy)?=?ty
????parTy?<:?pTy?&&?Check(body,?retTy)?--?allow?subtyping

??--?function?invocations
??FunApp(f,?arg)?--->
????let?FuncTy(parTy,?retTy)?=?typeOf(f)
????Check(arg,?parTy)?&&?retTy?<:?ty

?

類型檢查的環境

為了簡化偽代碼，我們有幾處做了忽略。事實上，Check 函數還有一個額外的參數 —— 環境，用于存放變量名/函數名到其類型的映射，即 Check : (Env, AST, Type) -> Bool。因此，一般情況下，我們會先做全局掃描，抓到所有的函數名和其對應類型并創建 Env，這樣便能應付（互）遞歸的函數定義了。在檢查的過程中，我們也會 (根據局部變量的生命周期) 動態地往 Env 中加入、刪除局部變量。

# 泛型函數類型檢查

接下來，我們來看一下如何做泛型 generics (或多態 polymorphic) 函數的類型檢查。

我們以 Kotlin 的語法為例，如下所示。定義一個函數 f，該函數有兩個泛型類型參數 X 和 Y；給定一個如下的函數調用 (因為是檢查模式，所以這里是用 f<> 的形式調用的)，應該如何檢查函數調用是否合法呢？

?

//?define
fun?f(a?:?X,?b?:?Y)?{?}

//?use
f(true,?0)

?

如下所示，先建立一個類型上的映射 (或者叫代換 substitution) m，具體來說，我們需要根據位置關系，將 X 映射到 Bool 類型，Y 映射到 Int 類型；第二步，我們需要找到函數 f 的定義，并且將類型中所有的 X 和 Y 用映射 m 代換掉，這樣一來，我們就成功地將泛型函數類型檢查替換為非泛型函數的類型檢查了。

?

//?Step?1:?建立映射
m?=?[X?-->?Bool,?Y?-->?Int]

//?Step?2:?用?m?代換泛型版本?f?的類型，得到
f?:?(a?:?Bool,?b?:?Int)?{?}

//?Step?3:?對代換后的函數進行類型檢查
......

?

進一步地，現在很多語言支持在泛型上定義上界 upper bounds。對帶泛型上界的函數類型檢查其理念其實也很簡單。

?

//?define
fun?f(a?:?X,?b?:?Y)?where?X?<:?Y?{?}

//?use
f(true,?0)

?

和前面一樣，我們先建立類型映射 m 并且做代換。需要注意的是，我們需要優先檢查代換后的上界是否還是正確的。（例子中的上界是 where Bool <: Int。）

?

//?Step?1:?建立映射
m?=?[X?-->?Bool,?Y?-->?Int]

//?Step?2:?做代換
f?:?(a?:?Bool,?b?:?Int)?where?Bool?<:?Int?{?}

//?Step?3:?優先驗證?`where?Bool?<:?Int`?是否滿足子類型關系

// Step 4:?若驗證成功，則對代換后的函數進行類型檢查；
//?????????若驗證失敗，則可以提前終止類型檢查
......

?

以上是一些簡單的示例，我在參考部分補充了復雜的例子，感興趣的同學可以進一步閱讀。

# 編寫一個類型推導器 #

現在我們來看一下如何實現一個類型推導器。

類型推導 type inference 在文獻里常被叫做 類型重構造 type reconstruction。相比類型檢查而言，類型推導一般會更困難 (當然，這個困難在本次分享中不會體現得很明顯)。

類型推導一個很關鍵問題就是，什么類型可以被推導出來。一般來說，我們會有局部 local推導和全局 all/global 推導兩種情況。

局部一般使用 局部類型推導 local type inference (或者 雙向類型檢查 bidirectional type checking) 的推導方法，通常來講，它只推導局部的變量定義、初始化、表達式、泛型函數調用等的類型，分界明顯。

全局，會掃描代碼里所有的定義和表達式，根據它們的聲明和使用收集約束，最后，使用合一的方法 purely unification-based approaches 把類型解出來。(熟悉的朋友應該了解 Hindley-Milner [1] 的類型推導算法 Algorithm W [2][3]，該算法在實踐中被證明是很有效的，已成功應用于很多的大型項目中。)

# 局部 —— 雙向類型檢查

我們先從局部的部分開始，即使用雙向類型檢查。

一般來講，程序可以被切割成 非泛型的部分 和 泛型的部分。對于非泛型部分 (后面會有具體的例子解釋說明)，我們會將定義處的類型信息傳遞到使用處，或者將使用處的類型信息傳遞到定義處，從而完成一個簡單的類型推導；對于泛型部分，我們會選用合一的方法來做推導（這是比較困難的部分?）。

以變量聲明為例，若開發者標注了變量的類型，我們便可以將該類型用作目標類型，來檢查初始化表達式 expr 的類型；我們也允許開發者在定義變量的時候不指定類型，那么此時，我們需要先找到初始化表達式 expr 的類型，再將該類型當做變量的類型。這兩種情況下類型的傳播方向是雙向的，即雙向類型檢查。

下圖是函數返回類型的雙向類型檢查例子。如果開發者顯式標注了函數的返回類型，那么我們可以用該類型去檢查函數體中每一個 return 表達式的類型，類型傳播如下圖左邊所示；當然，我們也允許開發者省略掉函數返回類型的標注，此時我們需要找出函數體中所有可能的 return 表達式的類型，將這些類型的公共父類型作為該函數的返回類型。省略返回類型一般在 lambda 表達式里比較有用。

如下是函數調用的例子。若在函數定義時，開發者聲明了形參的類型，那在函數調用處，我們可以省略標注實參的類型，直接用形參的類型作為目標類型來檢查實參類型即可。

類型推導在高階函數的場景中是有好處的。如下所示例子中，函數調用的實參是一個 lambda 表達式，我們可以省略標注 lambda 表達式中形參 x 的類型，用函數定義處的形參類型 ParTy 作為 x 的類型即可；也可以使用定義處的返回類型 RetTy 來檢查 lambda 體的類型。

以上就是四個簡單的例子，用來說明如何使用雙向類型檢查的框架去做局部的類型推導，其實質就是將類型信息從已知的部分傳遞到未知的部分。

#?偽代碼示例

接下來，我們來看如何實現一個類型推導器（雙向類型檢查器）。

首先，定義一個?Infer?函數，接受環境?Env?和要推導類型的節點?AST?為參數，返回該節點的類型。如下，

?

--?recall?that?`Check:(AST,?Type)?->?Bool`
Infer?:?(Env,?AST)?->?Type

?

字面值類型推導

和類型檢查類似，我們需要對正在被類型推導的樹做模式匹配。字面值的類型推導比較簡單，它是一種原子節點，這種情況下，我們可以直接用?typeOf()?獲取字面值的類型。

?

Infer?(env,?Lit(n))?=?typeOf(n)?--?pattern?match

?

加法類型推導

還是按照剛才的加法例子，我們輸入加法的語法樹，如下。分別遞歸地推導左右子樹的類型，如果推導出的左右子樹類型相等，那么返回該類型作為加法的類型；否則，返回一個錯誤類型?ErrTy。

?

Infer?(env,?Add(1,?r))?=
??let?tyL?=?Infer(env,?1)
??let?tyR?=?Infer(env,?r)
??in??if?(tyL?==?tyR)?then?tyL?else?ErrTy

?

函數調用類型推導

我們再看一個函數調用的例子。給函數?Infer?輸入參數?env?和函數調用節點?FunApp(f, x)?(f?是被調用的函數，x?是?f?的入參)。

?

Infer?(env,?FunApp(f,?x))

?

首先在環境?env?中找到?f?在定義處的類型，將查找到的函數類型使用模式匹配解構到形參類型?parTy?和返回類型?retTy。

?

Infer?(env,?FunApp(f,?x))?=
??let?FunTy(parTy,?retTy)?=?LookUp(env,?f)

?

然后我們就到了類型檢查的階段。我們需要檢查，函數的實參?x?是否可以有形參類型?parTy，或者說實參類型與形參類型是否匹配。如果匹配，則我們可以將查找到的函數返回類型?retTy?當做實際函數調用表達式的返回類型；否則，返回錯誤類型?ErrTy。

?

Infer?(env,?FunApp(f,?x))?=
??let?FunTy(parTy,?retTy)?=?LookUp(env,?f)
??in??if?(Check(env,?x,?parTy))?then?retTy?else?ErrTy

?

函數定義類型推導

再來看函數定義的例子。我們將函數定義的名字綁定到變量?f，函數形參綁定到?par，函數體綁定到?body，函數定義的返回類型綁定到?retTy，如下。

?

Infer?(env,?FunAbs(f,?par,?body),?retTy)

?

將形參解構為形參名?x?與形參類型?tyX。

?

Infer?(env,?FunAbs(f,?par,?body),?retTy)?=
??let?(x,?tyX)?=?par

?

在檢查函數體類型之前，我們需要先做一步擴展環境的動作，將變量?x?有類型?tyX?這個事實加到環境中 (這是因為，函數體?body?里會有對變量?x?的引用)。

?

Infer?(env,?FunAbs(f,?par,?body),?retTy)?=
??let?(x,?tyX)?=?par
??--?the?new?env?has?mapping?x?:?tyX
??let?env'?=?extendEnv(env,?x,?tyX)

?

如果我們想支持遞歸 (即在函數體內引用函數?f?自己)，那么我們也需要將函數?f?本身的定義類型?FunTy(tyX, retTy)?加到環境中，如下。

?

Infer?(env,?FunAbs(f,?par,?body),?retTy)?=
??let?(x,?tyX)?=?par
??--?the?new?env?has?mapping?x?:?tyX
??let?env'??=?extendEnv(env,?x,?tyX)
??--?support?recursion
??let?env''?=?extendEnv(env',?f,?FunTy(tyX,?retTy))

?

接下來，我們就可以直接檢查函數體有沒有返回類型?retTy?了。如果有，則返回?FunTy(tyX, retTy)?作為函數定義的類型，否則返回錯誤類型?ErrTy。

?

Infer?(env,?FunAbs(f,?par,?body),?retTy)?=
??let?(x,?tyX)?=?par
??--?the?new?env?has?mapping?x?:?tyX
??let?env'??=?extendEnv(env,?x,?tyX)
??--?support?recursion
??let?env''?=?extendEnv(env',?f,?FunTy(tyX,?retTy))
??--?use?the?new?env?to?check
??in??if?(Check(env'',?body,?retTy))
????then?FunTy(tyX,?retTy)
????else?ErrTy

?

環境擴展的作用是為了讓我們可以在函數體?body?內查到?x?和?f?的類型。當然，更好的做法是，如前文所說，先做一次全局掃描，將所有函數的定義全部添加到環境?env?中，這樣就可以處理互遞歸函數的情況了。

#?泛型函數類型推導

接下來我們一起看一下，對于一般初學者來講比較難的部分，即泛型函數中泛型形參的類型推導 (本次分享我們只提供一個大的框架，有興趣的小伙伴可以查閱文末的參考文獻)。

依舊以 Kotlin 語法為例講解一下如何做泛型函數的類型求解。定義一個?snd()?函數，有兩個泛型形參類型?X?和?Y，接受兩個參數?x?和?y，并返回第二個參數的類型?Y。調用函數?snd(1, true)，并將結果返回給聲明為?Bool?類型的變量?res。那么，我們應該怎樣去解泛型函數參數的類型呢？

?

//?define
fun??snd(x?:?X,?y?:?Y)?:?Y

//?use
val?res?:?Bool?=?snd(1,?true)

?

我們先收集實參 args 的類型，1 : Int, true : Bool，以及函數定義處形參 params 的類型，即?x : X, y : Y。

這里有一個規則 (或者事實)，要求實參類型必須是形參類型的子類型，即?args <: params。據此我們可以得到這樣兩條規則，

Int <: X

Bool <: Y

鑒于我們的環境表示函數的返回類型必須是?Bool，我們又會有一個規則需要遵循，要求函數聲明處的返回類型，必須是我們環境/上下文中要求的類型的子類型，即?return <: context-type，因此我們可以得到，

Y <: Bool

根據前述步驟，我們將已獲得的子類型關系按照變量整理收集，可以得到如下兩條關系。我們可以看到，變量 ?X?只有下界?Int，而變量?Y?有上下界，都是?Bool。

Int <: X

Bool <: Y <: Bool

據此，我們得到了可能的解，即?X?只要是?Int?的父類型即可，而?Y?只能是?Bool。

Int <: X

Y = Bool

最后，結合考慮子類型關系、協變、逆變等因素，盡可能地找到一個最優解，如下。

X = Int

Y = Bool

#?如何實現合一

前面介紹的方法就是合一 (即 unifications)，接下來我們簡單介紹一下如何實現。

第一步，定義合一函數?unify，輸入兩個類型，輸出一組約束。

?

unify?:?(Type,?Type)?->?Constraints

?

對輸入的類型參數做模式匹配，假設第一個參數輸入的是類型變元 (例如前面例子中的?)，那么我們需要生成一條約束，表示該類型變元應該小于等于上界類型?sup。

?

--?a?singleton?set
unify(TyVar(tv),?sup)?=?{?tv?<:?sup?}

?

假設我們給第二個參數輸入類型變元，那么對應地，我們可以生成如下這樣的約束，表示該類型變元有下界?sub。

?

unify(sub,?TyVar(tv))?=?{?sub?<:?tv?}

?

還有一些其他的類型，比較有趣的是如下示例的函數類型。我們需要分別對兩個函數的參數類型和返回類型遞歸地生成約束，再取并集，得到最終的約束。這里需要注意的是，入參的部分是逆變的，返回類型部分是協變的。

?

unify(FunTy(S1,?S2),?FunTy(U1,?U2))?=
??unify(U1,?S1)?`union`?unify(S2,?U2)

?

其它情況下，我們只需要檢查左邊的類型?sub?是否是右邊類型?sup?的子類型。

?

unify(sub,?sup)?=?checkSubTy(sub,?sup)

?

現實中的語言會很復雜，這邊就不展開介紹了。

# 局部 vs 全局

上一小節，我們簡單介紹了如何對程序中非泛型部分和泛型部分做類型推導。那么，局部和全局的方法應該如何選用呢？

對比來看，局部的類型推導使用合一的方法來尋找泛型（多態）函數調用的類型變元的代換 (需要單獨處理每個函數調用)；全局的類型推導算法 (比如 Hindley-Milner-liked/Algorithm W) 使用合一的算法來推導所有表達式、定義的類型 (先將新的類型變元賦給表達式，然后再找到它們的代換)。

除了一些基于技術難度的考量外，局部和全局的選擇也是一種設計理念上的哲學，比如，認為類型是文檔的一部分 (為了代碼的可讀性，一些語言可能會傾向于不允許省略類型標注，比如函數定義部分的形參類型和返回類型)；認為使用處不應該影響定義處等等。基于這些設計理念的考慮，一些語言，特別是工業語言，也可能會選擇一種相對局部的類型推導技術。

#?如何嚴格地定義類型檢查和類型推導 #

接下來，我們來看一下，應該如何嚴格地定義類型檢查和推導，以及它們要滿足的一些規則有哪些。

# 嚴格的類型檢查

要嚴格地定義類型檢查，我們需要做這些事情，

語法定義

首先，語法上需要定義程序里哪些是項 terms，哪些是項運行后的結果 values，哪些是類型 types。

項 Terms：即我們常說的表達式和語句。

值 Values：不可化簡（規約）的項，包括字面量，函數和 lambda 等。

類型 Types：項的抽象。一個正確的 term 永遠會有一個類型，我們用??表示二者的二元關系。

我們使用擴展的 BNF 來定義語法。

我們說，一個項 term 可以是一個整數，布爾值，加法，變量，可以是函數定義 (，lambda abstraction，定義一個函數，其形參是?，函數體是?)，可以是函數調用?，還可以是序列?。基于這樣的描述，我們就可以規定出如下的簡單語法。?(注意：此處的語法定義中，"+" ";" 等這種符號是字面量，而??相當于是占位符，可以展開為定義中的任一種。請讀者區分。)

?

t ::= 0 | 1 | 2...    ; integers
    | true | false    ; booleans
    | t "+" t         ; additions
    | x, y...         ; variables
    | λx "." t        ; abstraction
    | t "(" t ")"     ; application
    | t ";" t         ; sequence
    | ...

?

值 values 的語法定義如下。值是不可被化簡（規約）的部分，比如整數?0、1、2、3?等，但?1+2?不是值，因為它可以被化簡（規約）為?3。

?

v ::= 0 | 1 | 2...    ; integers
    | true | false    ; booleans
    | λx.t            ; application
    |...

?

我們還需要定義類型 types，語法規則如下。類型可以是類型變元，可以是多態類型，可以是函數類型，可以是布爾類型、整數類型等，如果我們還需要處理子類型關系的話，大概率系統里還需要一個頂類型和底類型 (頂類型 top type，即所有類型的公共父類；底類型 bottom type，即所有類型的公共子類)。

?

T ::= X               ; type variables
    | ?X <: T.T       ; polymorphic types
    | T → T           ; function types
    | Bool            ; booleans
    | Int             ; integers
    | ?               ; the Top type
    | ⊥               ; the Bottom type
    | Unit            ; the Unit type
    | ...

?

類型規則

在有了語法之后，我們需要定義一組?類型關系 type relations?。

類型關系用??描述，此處??是 term 和 type 之間的二元關系。

如果類型關系沒有橫線，則表示該描述恒成立，如下圖所示。?表示??永遠是??類型，?表示??永遠有??類型。

若類型關系如下所示，則表示橫線上面??是橫線下??的前提 (此處??表示環境，?表示在環境??下??成立），即如果我們的環境??中存放了變量??到類型??的映射關系，那么我們就知道在環境??下??一定有類型?。

下面是函數定義的類型規則。它告訴我們如果在環境??加上??有類型??的前提下，函數體??有??類型，則我們可以說，在環境??下，lambda 表達式??有??的類型。

上述類型規則，還可以用前面介紹過的雙向類型檢查框架拆分為檢查規則??和推導規則?。

對比來看，檢查的規則多出了目標類型這一輸入：lambda 表達式的目標類型為?，我們檢查其是否成立；而在推導的規則中，“目標類型”是缺失的。不難看出，只有檢查的規則 (abs check2) 允許 lambda 表達式省略其形參 x 的類型。通常來說，我們應優先使用檢查規則 (如果可用)，因為它通常速度更快且可以在更多的場景工作。

子類型關系

在定義了類型關系之后，我們還需要定義子類型關系 (其實 abs check1 已經使用了子類型關系)。子類型關系是兩個類型上的二元關系，即?。

以下是一些恒成立的子類型關系規則，比如一個類型永遠是它自身類型的子類型 (自反性)，一些語言會有底類型??(Bottom、Nothing 等) ，它是所有類型的子類型，一些語言中還有頂類型??(Top、Any 等)，它是所有類型的父類型。

以下是在一些條件下會成立的子類型關系 (?表示類型上的環境，會包含一些類型上下界等相關的信息)。

如下是大多數類型系統都具有的性質：子類型的傳遞性 transitivity。若存在??是??的子類型，且??是??的子類型，則我們可以得到，?是??的子類型。

如下是函數類型的子類型關系，在此（又）要注意協變和逆變。當我們要證明??時，對于函數參數類型我們要用逆變關系，即?；對于函數的返回類型我們要用協變關系，即?。

# 類型系統的證明規則

當我們定義了前述的語法和類型規則后，接下來我們就需要去證明我們的類型系統需要滿足什么規則。

一般來講，需要滿足兩條規則，可靠性 soundness?和?完備性 completeness。

可靠性 Soundness

可靠性指的是，類型正確的表達式在運行的時候是不會出錯的 (well-typed terms do not go wrong)。即，如果一個表達式通過了類型檢查，或者說它可以被賦予一個類型的話，那它運行的時候一定不會出錯。

那么，要如何保證這點呢？這里又可以細分為兩個子規則，一個叫 progress，一個叫 preservation。Progress?指，一個 term 或是一個 value，或可以被進一步計算（而最終得到 value），比如??可以被計算到?。Preservation?指，term 在經過計算后仍然擁有一個合法的類型。下面這個例子就驗證了上述兩條規則。

完備性 Completeness

對于類型檢查器來說，完備性即?每一個正確的表達式都可以通過檢查；對于類型推導器來說，完備性指?要為每一個正確的表達式分配一個類型。不過在實際中，我們不一定能完全做到后者。那怎么辦呢？很簡單，我們只需要將類型標注出來，然后“退回到”類型檢查即可。畢竟檢查一般來說會比推導兼容更多的場景。

# 舉個例子

下面我們用一些反例來說明為什么前述兩條規則是重要的。

如果我們的程序不滿足可靠性，那么很可能的是，程序可以編譯通過，但運行行為是未定義的 undefined。

而如果我們的類型檢查器是很不完備的，那么可能一些明顯正確的代碼，比如?1 + 2 : Int，也無法編譯。如果類型推導器是十分不完備的，那么編譯器很有可能會很煩人，要求我們在每個很明顯的地方顯式指定類型，比如我們不能寫?var a = true，而需要明確寫出?bool a = true。

我們來看一個真實的例子。以 C++ 為例，程序中定義了公共父類?class C，C?有兩個子類?D?和?E。我們聲明一個類型為?C?的變量?c，并且用一個簡單的二元表達式來初始化它。C++ 的編譯器會在這里報錯：它說它無法找到?D?和?E?的公共父類?——?即便這里只能是 C。

?

class?C?{?};
class?D?:?public?C?{?};
class?E?:?public?C?{?};

C?c?=?true???D()?:?E();
//?error:?incompatible?operand
//?types?('D'?and?'E')

?

我們嘗試將上面的代碼改成推導模式，讓編譯器推導?c?的類型，程序仍然無法通過編譯。

?

auto?c?=?true???D()?:?E();
//?error:?imcompatible?operand
//?types?('D'?and?'E')

?

我們只能將某個分支的類型 (比如?D) 強轉到父類型?C，來達到目的。

?

auto?c?=?true???(C)D()?:?E();
//?this?works

?

當然，這只是 C++ 編譯器的行為。但如果我們用 Kotlin 或者 Swift 來寫上面的代碼，都是可以編譯通過的。

# 學界 vs 工業界 #

最后，我們簡單討論一下，學界和工業界關心什么？

# 學界 Academic

學界最關心的就是前面介紹的兩條定律 可靠性 soundness 和 完備性 completeness，這是第一要位；學界通常是在保證類型系統、類型檢查和推導在滿足這兩條定律的情況下，再向語言中增加新的特性，并且保證擴展后的類型檢查和推導器仍然滿足這兩條定律，同時提供 (經過編譯器驗證的) 證明。

學界還十分關注抽象的核心語言 core languages (核心語言中語言的特性越少越好)。學界希望能找到一組最簡單的特性，能夠通過組合來表達更多的特性。因為這樣一來，需要做的證明是最少的。

此外，相比性能，學界更關注語言的表達能力。

當然，學界對現代的語言特性也很感興趣，比如 effect handlers，gradual typing，refinement types，dependent types，linear types，session types 等。

學界語言還擁抱百花齊放的編程范式，比如 OO，FP，logic，relational，probabilistic，concurrent (parallel)...

# 工業界 Industrial

于工業界來說，人們對語言最首要的需求就是語言要有很多方便易用的語法、特性，從而語言的使用者能用更短的代碼去解決實際問題。比起證明，人們往往使用測試用例來提高軟件質量。

工業界對語言的表達能力和性能都很關注，也會在一些場景中，為了性能引入一些讓用戶比較頭疼的語言特性。

工業語言對前沿語言特性的引入一般持保守態度。它們更傾向于引入一些偏向實際且已經較為成熟穩定的語言特性 (大概會和學界有十年到二十年的差距)。比如 C++ 這樣的工業語言還會關注零代價抽象，后向兼容等。

就編程范式而言，一般來說，工業界語言還是以面向對象 OO 為主，相比學界來說就沒有那么百花齊放。

# 總結 #

總結一下，本次分享簡單地介紹了一下類型檢查和推導做了什么，然后介紹了如何實現一個類型檢查和推導器，并且介紹了如何嚴格地定義其要滿足的定律，以及定律的重要性；在最后，就學界語言和工業界語言做了一個簡單的對比。

如果大家對類型檢查和推導相關的內容感興趣，還可以就以下的參考文獻進行擴展閱讀。

　　審核編輯：湯梓紅