講完untyped lambda
接下來就要講typed lambda啦
顧名思義
typed lambda就是有type的lambda
因此必須要被type check
一個合理的type checker不會讓所有程式都type check成功
而是只接受特定的一些「正確的」程式
因此讓程式的錯誤能在編譯時期就被找出來

定義

我們首先從simply typed lambda calculus開始
以下將會取簡稱STLC
STLC的term中
唯一的差別就在於lambda的綁定變數增加了型別標記
原本的lambda

\[\lambda x. t\]

會變成

\[\lambda x: T. t\]

其中的\(T\)是一個type
代表了參數應要有的型態
假如傳入的參數有著其它型態
type check便不會通過

現在問題來了
lambda的型態又是什麼？
一個lambda的資訊主要由兩個部分構成
一個是參數的type
另外一個則是值的type
我們把一個lambda的type寫成\(T \to U\)
其中\(T\)是參數的type
\(U\)則是回傳值的type
一個type為\(T \to U\)的lambda
在接收一個type為\(T\)的參數後
會傳回type為\(U\)的運算式

全部組合起來吧
我們的新系統裡面會有term和type兩個階層
接下來我要分別定義term和type由什麼組成
其中type包含了：

  1. \(Base\)
    這是最基本的type
    它不能被當成一個函數
    假設\(t_1: Base\)(這代表著\(t_1\)的型別是\(Base\))
    則\(t_1 t_2\)絕對無法通過type check

  2. \(T_1 \to T_2\)
    對所有type \(T_1\)和\(T_2\)
    函數型別\(T_1 \to T_2\)是一個type
    也就是說
    我們能夠從\(Base\)開始
    建構一系列更複雜的type
    例如像\(Base \to Base\)、\(Base \to (Base \to Base)\)、\((Base \to Base) \to Base\)……

term則包含了：

  1. 變數

  2. 對所有變數名稱\(x\)
    所有term \(t\)
    和所有type \(T\)
    \(\lambda x: T. t\)是一個term

  3. 對所有運算式\(t_1\)
    和所有運算式\(t_2\)
    \(t_1 t_2\)是一個term

在以上對term和type的定義中
我省略了這句話

除上述之外
沒有任何其它東西是運算式

因為這是顯而易見的
從今以後我都將省略之
並且我要導入一個更簡潔的表示法

\[\begin{array}{rcl} term(t) ::= & \mathbf{var} (x) \\ | & \lambda x: T. t \\ | & t t \\ type(T) ::= & Base \\ | & T \to T \end{array}\]

這樣的表示法相當於上面用文字對term和type的定義
兩相對照之下
應該不難理解它的意思
用Haskell可以寫成這樣：

newtype Symbol = Symbol String
data Term = Var Symbol
          | Lam Symbol Type Term
          | App Term Term
data Type = Base
          | Arrow Type Type

值得一提的是
\(\to\)是右結合的
換句話說
\(T \to U \to V\)代表的是\(T \to (U \to V)\)
為什麼呢？
還記得前面提到的柯里化吧
\(f a b\)中的\(f\)可以被理解成接收兩個參數的函數
假設\(a\)的型別為\(A\)、\(b\)的型別為\(B\)
則\(f\)的型別會是\(A \to (B \to C)\)
在大多的情況中
我們都希望柯里化能運作
因此我們把\(\to\)定義成右結合的

歸約

STLC的歸約和untyped lambda中的歸約差不多
畢竟兩者唯一的差別就只在綁定變數上多了個型別
而目前型別在執行時期是不需要的
不過現在我們大可不必管歸約策略了
為什麼呢？
因為在STLC中
所有term都有NF
並且任何term都能在有限步\(\beta\)-歸約後達到它的NF
所以你大可把所有term歸約成NF
這是型別系統帶來的好處
當然
這代表著我們沒有辦法在STLC裡面跑一個無窮迴圈
例如像是前面提到的\(\Omega\)在STLC中便不存在
也就是說STLC並不是圖靈完全的

為什麼\(\Omega\)不存在？
複習一下
\(\Omega = (\lambda x. x x)(\lambda x. x x)\)
現在假設我們要為它的綁定變數加上型別
變成\(\Omega = (\lambda x: ?. x x)(\lambda x: ?. x x)\)
問號中要填入什麼？
這個問題是無解的

type checking

接下來要講type checking了
先來讓大家嘗鮮一下
以下這堆莫名其妙的符號解釋了STLC的type checking是怎麼進行的

\[\begin{array}{lcl} (var) & \Gamma \vdash x: T & \mbox{if } x: T \in \Gamma \\ (appl) & \dfrac{\Gamma \vdash t_1: T \to U \qquad \Gamma \vdash t_2: T}{\Gamma \vdash t_1 t_2: U} \\ (abst) & \dfrac{\Gamma, x: T \vdash t: U }{\Gamma \vdash (\lambda x: T. t): T \to U} \end{array}\]

接下來我會用直覺解釋要怎麼進行type check
然後再引導讀者理解上面這些符號代表的意義

概述

首先我先來定義何謂term的內外層
以untyped lambda來說
\((\lambda x. x x)\)在\((\lambda x. x x)(\lambda x. x x)\)的內層
而\(x x\)又在\((\lambda x. x x)\)的更內層
注意綁定變數\(x\)不在\((\lambda x. x x)\)的內層
那只是一個變數而已
不是一個term

還記得目前有哪些term吧
變數、lambda、函數調用
當我們在term的最外層時
可能遇到的肯定是這三者的其中一個
現在我打算對這三個可能性逐個擊破
首先先講遇到函數調用時怎麼辦
當遇到函數調用時
有兩個內層的term
左邊那個必須是函數
右邊則是丟給左邊那個函數的參數
而且右邊那個term的型別必須要和左邊函數綁定變數後面標示的型別互相吻合
我們只要分別對左右邊進行type check
再確定左邊是不是個函數
而且它標示的型別和右邊term相吻合就好

如果遇到了一個lambda \(\lambda x: T. t\)
則我們要把\(x\)的型別是\(T\)這個事實記錄下來
然後在這個事實的大前提下
檢查\(t\)的型別是什麼
就把\(t\)的型別叫做\(U\)好了
那麼整個lambda的型別就是\(T \to U\)
因為有可能\(x \in FV(t)\)
所以\(x\)的型別資訊在檢查\(t\)的型別時是必要的

用更精確的詞來說
當遇到一個lambda \(\lambda x: T. t\)時
我們把\(x\)的型別是\(T\)這樣的資訊存放在語境中
然後用這樣的語境檢查\(t\)的型別
如果在lambda的內層遇到另一個lambda要怎麼辦？
只要把它的綁定變數也加入語境就好了
然後用這個更改過的語境檢查更內層term的type

最後
如果遇到變數怎麼辦？
要是單獨一個\(x\)在檢查型別時肯定是會失敗的
我們根本沒辦法決定\(x\)的型別啊！
但\(\lambda x: Base. x\)卻應該被成功編譯
為什麼呢？
因為在檢查內層的\(x\)時
我們的語境已經含有了\(x: Base\)的資料
現在能用這樣的資料檢查內層\(x\)的型態
換句話說
遇到變數時
我們只要在語境中進行搜索就好了

回到那堆符號上

符號

\[(var) \quad \Gamma \vdash x: T \quad \mbox{if } x: T \in \Gamma\]

我們把\(\Gamma \vdash x: T\)叫做一個裁決
裁決什麼？
裁決了\(x\)的type是\(T\)
由什麼裁決？
由語境\(\Gamma\)
\(\Gamma\)代表著語境
要如何進行這個裁決呢？
看看後面的\(\mbox{if } x: T \in \Gamma\)
這告訴我們如果在語境\(\Gamma\)中找到了\(x\)的type是\(T\)
我們便能進行裁決
\(\in\)讀成屬於
整個組合起來是這樣：
如果\(x: T\)在語境\(\Gamma\)中
則由\(\Gamma\)可以裁決\(x\)的型別是\(T\)

不難對吧？
而且還很像是廢話

\[(appl) \quad \dfrac{\Gamma \vdash t_1: T \to U \qquad \Gamma \vdash t_2: T}{\Gamma \vdash t_1 t_2: U}\]

你應該立刻會注意到那條橫線
橫線上頭的裁決被稱為前提
下面則是結論
要是前提都成立的話
結論便也成立
前提有兩個
第一個是\(\Gamma \vdash t_1: T \to U\)
這是一個\(\Gamma\)對\(t_1: T \to U\)的裁決
第二個是\(\Gamma \vdash t_2: T\)
這是一個\(\Gamma\)對\(t_2: T\)的裁決
結論是\(\Gamma \vdash t_1 t_2: U\)
這是一個\(\Gamma\)對\(t_1 t_2: U\)的裁決
全部組合起來
如果在\(\Gamma\)裁決\(t_1: T \to U\)和\(t_2: T\)的前提下
\(\Gamma\)對\(t_1 t_2: U\)的裁決成立
以目前來說也能反過來讀
要檢查\(t_1 t_2\)的型別
只要檢查\(\Gamma\)能否裁決\(t_1: T \to U\)和\(t_2: T\)就好
然後回傳結果\(U\)
這也就是我們type check函數調用的方法
接下來要講如何type check lambda

\[(abst) \quad \dfrac{\Gamma, x: T \vdash t: U }{\Gamma \vdash (\lambda x: T. t): T \to U}\]

這邊出現了新的符號：逗號
只要解釋這個逗號的意義
整個應該就能被讀懂了
\(\Gamma, x: T\)代表的是在\(\Gamma\)上加上\(x: T\)的新語境
一整個讀起來會是這樣
若\(\Gamma\)加上\(x: T\)的新語境能裁決\(t: U\)
\(\Gamma\)便能裁決\(x: T. t\)的型別是\(T \to U\)
type check時只要反過來讀就好

實例

來舉個實際例子好了
我們試著找找看\((\lambda x: Base \to Base. x)(\lambda y: Base. y)\)的型別
首先看看最外層的term
它是一個函數調用
因此我們應該要先試圖檢查左右兩邊的型別
然後根據這樣的資料檢查一整個term的型別
用符號表示是這樣：

\[(appl) \quad \dfrac{\Gamma \vdash (\lambda x: Base \to Base. x): ?_1 \qquad \Gamma \vdash (\lambda y: Base. y): ?_2}{\Gamma \vdash (\lambda x: Base \to Base. x)(\lambda y: Base. y): ?_3}\]

只要解決了\(?_1\)和\(?_2\)
你就知道\(?_3\)要填入什麼
先解決\(?_1\)
注意到了這個term是個lambda
因此我們要在這裡套用\((abst)\)

\[(abst) \quad \dfrac{\Gamma, x: Base \to Base \vdash x: ?_4 }{\Gamma \vdash (\lambda x: Base \to Base. x): ?_1}\]

現在我們想知道\(?_4\)是什麼
我們已經遇到了一個變數
因此接下來應該要用\((var)\)求得\(?_4\)
在這邊
我們根本不需要\(\Gamma\)
因為\(\vdash\)左邊的語境中已經有\(x\)的型別資訊了
而這代表著\(\Gamma\)可以是個空語境
寫作\(\emptyset\)
我來提出一個解釋語境究竟是什麼的想法
語境是自由變數的型別資料
為什麼檢查lambda的型別時要把約束變數的資料加入到語境裡面呢？
因為原本在\(\lambda x. t\)中不自由的\(x\)變數
到了\(t\)裡面變成自由的了！
因此檢查\(t\)的型別時要在語境中加入\(x\)的資料
回到原本的主題上
\(\Gamma\)可以是個空語境代表著什麼？
這代表著我們不需要任何其它自由變數的資料就能進行判決
由這個判決
可以得到\(x: Base \to Base\)
也就是說\(?_4 = Base \to Base\)
回到\((abst)\)上
要來解\(?_1\)
我們可以把\(?_4 = Base \to Base\)填入了：

\[(abst) \quad \dfrac{\emptyset, x: Base \to Base \vdash x: Base \to Base }{\Gamma \vdash (\lambda x: Base \to Base. x): ?_1}\]

根據\((abst)\)
我們可以得到\(?_1 = (Base \to Base) \to (Base \to Base)\)
用和上述類似的方法
我們得到\(?_2 = Base \to Base\)
因此上面提到過的\((appl)\)變成這樣：

\[(appl) \quad \dfrac{\emptyset \vdash (\lambda x: Base \to Base. x): (Base \to Base) \to (Base \to Base) \qquad \emptyset \vdash (\lambda y: Base. y): Base \to Base}{\Gamma \vdash (\lambda x: Base \to Base. x)(\lambda y: Base. y): ?_3}\]

得到結論
\(\emptyset \vdash (\lambda x: Base \to Base. x)(\lambda y: Base. y): Base \to Base\)
也就是說我們不需要其他自由變數的資料
就能得到\((\lambda x: Base \to Base. x)(\lambda y: Base. y)\)的型別是\(Base \to Base\)

補充

啊對了
差點忘記說一件事情
你可能會想問
假設有個函數\(\lambda x: Base. x\)
要怎麼丟一個\(Base\)型態的參數給它呢？
我根本就沒提到怎麼建構type為\(Base\)的term啊
答案是……沒有辦法XD
至少在我介紹的這個最簡化的系統裡面沒辦法
但就算沒辦法建構型別為\(Base\)的term
這個系統還是有某些用處的
這個系統內存在type為\(Base \to Base\)
或者\((Base \to Base) \to (Base \to Base)\)的term
即使沒有\(Base\)型態的term
我們還是能由系統內的term進行一些有意義的運算