在之前STLC的教學中
我們的世界被分成了兩個階層：term和type
接下來
我們會希望這兩者的差別變得更模糊
為什麼要這麼做？
因為lambda calculus可以被當作是程式語言的核心
在寫程式的時候
建立抽象是必要的過程
有了高層次的抽象
能讓不同的東西被視為一樣的
減少重複的冗餘程式碼
因此程式語言上也應該提供更高的抽象能力以幫助使用者

在STLC中
固然型別的介紹提供了更強的安全性
它卻同時限制了程式抽象的能力
原因是我們的世界被分成了2個階層term和type
為了提供更強的抽象
我們應該試圖把這兩者視為一樣的
在lambda的世界裡要怎麼建立抽象呢？
答案就是……lambda XD

我就直接說明白接下來要做什麼好了
在STLC中
我們有著接收一個term
傳回另一個term的函數
同理
type階層也應該要有函數
也就是接收一個type
傳回另外一個type的函數
除此之外
term和type之間還應該要有更強的互動
所以type到term和term到type的的函數也應該被導入

導入了以上所有新的lambda之後
我們會得到一個比STLC還強大很多的系統
但那樣的系統因為和STLC的差距太大
過高的抽象可能讓讀者無法吸收
因此我按照慣例
先導入type到term的函數
STLC加上type到term的函數的系統被叫做system F
首先我先比較舉一些比較直覺的例子
之後再有系統性地敘述

還記得前面提到過的\(\mathbf{I}\)嗎？
也就是\(\lambda x. x\)
要怎麼在STLC內寫出這個函數呢？
我們沒辦法寫\(\lambda x: T. x\)
因為\(T\)根本不是一個真正的 type
而比較像是一個系統外的變數
這樣的變數被叫做元變數
type的元變數內可以填入真正的type
例如像\(Base\), \(Base \to Base\), \(Base \to Base \to Base\), \((Base \to Base) \to Base\)……
所以我們可以有\(\lambda x: Base. x\), \(\lambda x: Base \to Base. x\), \(\lambda x: Base \to Base \to Base. x\)
但系統內卻不存在一個通用的\(\mathbf{I}\)
可以套用在任何型別的參數上頭

怎麼辦呢……
很簡單
只要擴張我們的系統(STLC)
讓原本的元變數變成系統內的變數就好啦
這也就是system F的用意

在system F中
我要導入從type到term的term
這麼一來
可以把\(\mathbf{I} \: A\)當成一個\(A\)型別上頭的\(\mathbf{I}\)
\(\mathbf{I} \: B\)當成\(B\)型別上的\(\mathbf{I}\)
現在我要介紹system F裡面\(\mathbf{I}\)的定義了
(記得嗎
\(\mathbf{I}\)只不過是一個真正的term的簡稱罷了)

\[\mathbf{I} \stackrel{def}{\equiv} \Lambda A. \lambda x: A. x\]

這邊出現了新的符號：\(\Lambda\)
\(\Lambda\)是希臘文中\(\lambda\)的大寫
\(\mathbf{I}\)可以被解釋成一個函數
接收所有型別\(A\)
傳回一個接收type為\(A\)的參數的的函數的函數
同理
\(\Lambda A B. \lambda x: A. \lambda y: B. x\)可以被當成是system F中的\(K\)
事實上
Haskell的Prelude裡面也有\(\mathbf{I}\)和\(\mathbf{K}\)
只不過它們分別被叫做id和const
另外也能在system F中定義自然數

定義

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

和STLC比
system F中的結構多了很多
現在我來一一解釋新添加的部分

1. \(\Lambda X. t\)
   這是從type到term的函數
   也可以理解成適用於所有type \(X\)的term \(t\)
   上面應該提得夠多囉

2. \(t T\)
   小寫\(t\)是term的元變數
   大寫\(T\)則是type的元變數
   既然有了type到term的函數\(\forall\)
   當然也要有調用這類函數的方法
   我們依照之前STLC的慣例
   直接把函數和參數並列寫在一起代表函數調用
   當然我們也會有這類函數的柯里化

3. 要講type的部分了
   首先注意到\(Base\)不見了
   取而代之的是type變數
   這邊的變數是真正的變數而不只是元變數
   事實上
   在上面我們已經多次使用到了type變數
   也就是\(\mathbf{I}\)和\(\mathbf{K}\)中的\(A\)和\(B\)
   既然要有type到term的函數
   就一定要有type的變數
   好能在內層的term使用它
   事實上
   \(\Lambda\)後面緊接著的變數被稱為\(\Lambda\)的綁定變數
   再來
   解釋\(Base\)不見了的原因
   因為已經有了type上的變數
   \(Base\)再也沒有存在的必要了
   因為\(Base\)本來就不是一個很特別的type
   我們無法建構type為\(Base\)的term
   \(Base\)只是被用作建構更複雜的type的基礎
   而現在它的目的已經被type變數取代了
   我們能用任意的type變數建構更複雜的type

4. \(\forall X. T\)
   \(\forall\)讀成for all
   翻譯成中文就是對於所有
   既然STLC的term都有type
   system F的\(\Lambda X. t\)也應該有type
   而\(\Lambda\)的type便是\(\forall\)
   更詳細地說
   \(\forall\)內層的\(T\)記錄了\(\Lambda\)內層\(t\)的型別
   而term的綁定變數\(X\)直接被記錄在type的綁定變數上頭(一樣叫\(X\))

歸約

和STLC差不多
system F只是多了\(\Lambda\)而已
\(\Lambda\)和\(\lambda\)差不多
只不過差在調用\(\lambda\)時要對內層term的自由變數進行取代
而調用\(\Lambda\)時需要對內層type自由變數進行取代

因為在STLC中
所有term都有NF
並且任何term都能在有限步\(\beta\)-歸約後達到它的NF

在system F中
同樣的性質也成立
這邊我要告訴大家這樣性質的形容詞
要是在一個系統裡面
所有term都有NF
這樣的系統被稱為弱規範化的
如果任何term都能在有限步\(\beta\)-歸約後達到它的NF
則系統被稱為強規範化的
顯然強規範化意味著弱規範化
但反之則否

type checking

在前面的STLC中
我們有3條規則
或者被稱為推導規則(derivation rule)
一個規則包含了它的前提和結論
前提可以是多個判決
而結論是另一個判決
在system F中
規則變成了6條
以下將會介紹這6條規則

啊 對了
先解釋一下判決在STLC和system F的不同之處
在STLC裡面
所有的 type在空語境下都是合法的
但現在我們有了type變數
我們要更限制怎樣的type才是合法的
更精確的說
我要定義空語境下只有沒有自由變數的type才是合法的
也就是說
\(\forall A. A \to A\)是合法的
(這是上面提到的\(\mathbf{I}\)的type)
\(A \to A\)卻不是
因為在後者中\(A\)是自由變數
現在
為了聲明一個type是合法的
我們還要把判決的定義延伸
原先
判決包含了一個語境及它右方變數的型別
現在我們要添加另一種可能性
它判決的是一個type是合法的
寫作\(\Gamma \vdash T: \star\)
你可以想成是type也有型別
而它們的型別被叫作\(\star\)
所以所有合法的type都有型別\(\star\)
這麼一來就解釋得通了
所以\(\emptyset \vdash \forall A. A \to A: \star\)
這次真的要開始講規則了

\[\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}\]

到這裡都和STLC完全一樣

\[(form) \quad \Gamma \vdash T: \star \: \mbox{if } T是type, T的所有自由變數在\Gamma中\]

所以由\((form)\)這條規則
\(\emptyset \vdash \forall A. A \to A\)是對的
因為\(\forall A. A \to A\)沒有自由變數
如果有自由變數的話
則語境內應該也要有這個變數
舉例來說
\(A: \star \vdash A \to A\)

\[(appl_2) \quad \dfrac{\Gamma \vdash t: \forall X. T \qquad \Gamma \vdash U: \star}{\Gamma \vdash t U: T[X:=U]}\]

對照著\((appl)\)和\((appl_2)\)看
這兩條規則很像
只不過一個是用在\(\lambda\)上
另一個是用在\(\Lambda\)上而已
我們也因此要在type checking時進行取代的動作
既然有\((appl_2)\)
那一定也有\((abst_2)\)：

\[(abst_2) \quad \dfrac{\Gamma, X: \star \vdash t: T }{\Gamma \vdash (\Lambda X. t): \forall X. T}\]

這應該不難懂
由下往上讀
把約束變數丟進語境裡面檢查內層的型別

system F就這樣囉