PTS是lambda cube的再度延伸
在CoC中
\(\star\)和\(\Box\)被稱為sort
sort是什麼呢？
它是較低層一般型別的型別
舉例來說
\(\forall A. A \to A: \star\)
\(\star \to \star: \Box\)
但假如我們有個從一般kind到一般kind的lambda
它的型別不會是\(\Box\)
而會是\(\Box \to \Box\)

我們再回頭看看CoC的\((form)\)：

\[(form) \quad \dfrac{\Gamma \vdash t_1: s_1 \quad \Gamma, x: t_1 \vdash t_2: s_2}{\Gamma \vdash (x: t_1) \to t_2: s_2}\]

這告訴了我們什麼？
函數型別屬於的sort是由回傳值的型別的sort決定的
這邊牽扯到了3個不同階層的東西
最底層是參數和回傳值
第2層是參數和回傳值的型別
以及整個lambda的型別
最高層是第二層屬於的sort
但為什麼函數型別的型別必定是回傳值的型別的型別決定的呢(好像繞口令)
事實上
這並不是必然的
要是把這樣的限制放寬
我們能得到更多奇妙的lambda系統
還記得稍微限制\((form)\)就可以得到lambda cube中較簡單的系統嗎？
現在我們反過來朝向更複雜的系統邁進
我們定義一個\(\mathcal{R}\)
\(\mathcal{R}\)是一個接收兩個sort
傳回一個sort的函數
除此之外
為了建構每個sort的型別又是什麼
我們還需要另一個函數\(\mathcal{A}\)
A接受一個sort做為參數
回傳它屬於的sort

定義

全部合在一起
PTS不是一個系統
而是一系列的系統
它可以調校的選項有：

\(\mathcal{S}\) 一個包含所有sort的集合
\(\mathcal{A}: \mathcal{S} \to \mathcal{S}\) 一個說明了sort的型別是哪個sort的部分函數
\(\mathcal{R}: \mathcal{S} \times \mathcal{S} \to \mathcal{S}\) 一個由參數和回傳值的型別決定整個函數型別的sort的部分函數

所有的規則如下：

\[\begin{array}{lcl} (var) & \dfrac{\Gamma \vdash t_2: s}{\Gamma, t_1: t_2 \vdash t_1: t_2} & \forall s \in \mathcal{S} \\ (weak) & \dfrac{\Gamma \vdash x_1: t_1 \qquad \Gamma \vdash t_2: s }{\Gamma, x_2: t_2 \vdash x_1: t_1} & \forall s \in \mathcal{S} \\ (appl) & \dfrac{\Gamma \vdash t_1: (x: t_3) \to t_4 \qquad t_2: t_3}{\Gamma \vdash t_1 t_2: t_4[x := t_3]} \\ (abst) & \dfrac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3} & \forall s \in \mathcal{S} \\ (form) & \dfrac{\Gamma \vdash t_1: s_1 \quad \Gamma, x: t_1 \vdash t_2: s_2}{\Gamma \vdash (x: t_1) \to t_2: \mathcal{R}(s_1, s_2)} & \forall s_1, s_2 \in \mathcal{S} \\ (sort) & \emptyset \vdash s: \mathcal{A}(s) & \forall s \in \mathcal{S} \\ (conv) & \dfrac{\Gamma \vdash t: T \qquad \Gamma \vdash U: s }{\Gamma \vdash t_2: U} & \forall s \in \mathcal{S} & \mbox{if } T \equiv U \end{array}\]

注意\(form\)用到了\(\mathcal{R}\)
而\((sort)\)用到了\(\mathcal{A}\)
現在我們來探討一些實際的系統
首先是只有一個sort的系統

1個sort

\[\begin{array}{lcl} \mathcal{S} & = & \{\star\} \\ \mathcal{A} & = & \{(\star, \star)\} \\ \mathcal{R} & = & \{(\star, \star, \star)\} \\ \end{array}\]

這是最簡單的PTS
也是Haskell採取的策略
在這樣的PTS裡
我們可以得到\(\star: \star\)
根據\((form)\)也有\(\star \to \star: \star\)
這樣的系統比CoC簡潔多了不是嗎？
很遺憾的是
這樣的系統不是一致的
也就是說對於任何type
都存在term使得該term的型別是上述type
這麼一來
它就沒有辦法用來證明定理

2個sort

我們已經看過有2個sort的系統了
也就是lambda cube
這裡就不再多談

3個sort

接下來是3個sort的系統
一般我們會把\(\Box\)的型別叫做\(\triangle\)
來介紹一下system U-：

\[\begin{array}{lcl} \mathcal{S} & = & \{\star, \Box, \triangle\} \\ \mathcal{A} & = & \{(\star, \Box), (\Box, \triangle)\} \\ \mathcal{R} & = & \{(\star, \star, \star), (\Box, \Box, \Box), (\Box, \star, \star), (\triangle, \Box, \Box)\} \\ \end{array}\]

很可惜的是
這個系統也是不一致的
為什麼它是不一致的呢？
這和它是自我指涉的有關
現在我來解釋這邊說的自我指涉是什麼

來說一點歷史
大約在19世紀末時
為了建立一個所有數學理論的基礎
數學家們發明了集合論
一開始的集合論被稱作樸素集合論
後來樸素集合論演化成了公理化集合論
公理化集合論比樸素集合論更為嚴謹
而且修正了原本理論中自我指涉的部分
因此不會遇到著名的羅素悖論
羅素悖論有個比較通俗的版本
被稱為理髮師悖論
這個悖論是這麼說的

小城裡的理髮師放出豪言
他要為城裡所有不為自己刮鬍子的人刮鬍子，而且只為那些不為自己刮鬍子的人刮鬍子。
但問題是：理髮師該給自己刮鬍子嗎？
如果他給自己刮鬍子，那麼按照他的豪言「只為那些不為自己刮鬍子的人刮鬍子」他不應該為自己刮鬍子；
但如果他不給自己刮鬍子，同樣按照他的豪言「為城裡所有不為自己刮鬍子的人刮鬍子」他又應該為自己刮鬍子。

我們無法判斷這位理髮師幫不幫自己刮鬍子
問題出在自我指涉上
因為他在刮鬍子的條件中
又以刮鬍子為條件
樸素集合論也遇到了類似的問題
造成某些命題無法被判斷為真或假

回到lambda calculus上
我們又在哪部分自我指涉了呢？
試想\((x: \star) \to x \to x\)這個型別
它的\(x\)也可以代入\((x: \star) \to x \to x\)
變成\(((x: \star) \to x \to x) \to ((x: \star) \to x \to x)\)
這不就是自我指涉嗎？
從一個更高的觀點看
這和\(\mathcal{R}(\Box, \star) = \star\)有關
如果函數的參數的型態的型態是\(\Box\)
且回傳值的型態的型態是\(\star\)
那麼整個函數的型態會是\(\star\)
因為\(\star: \Box\)
函數的參數型態可以是\(\star\)
因此你可以把整個函數的型態丟進去

所以CoC是自我指涉的……
幸好
自我指涉不一定會帶來問題
因此CoC是一致的
事實上
但system U-就沒那麼幸運了
\((\triangle, \Box, \Box)\)造成了它的不一致

3個sort的PTS差不多就到這邊
最後提一下
system U-加上\(\mathcal{R}(\triangle, \star) = \star\)的系統被叫做system U
當然system U也是不一致的
你可能想問的是
為什麼不設定\(\mathcal{R}(\triangle, \Box) = \triangle\)就好了呢？
這樣不就不會有自我指涉的問題了嗎？
其實這就是我們將要做的事情
更進一步的是
我將導入有無限個sort的PTS

無限個sort

\[\begin{array}{lcl} \mathcal{S} & = & Prop, Type_n & \forall n \in \mathbb{N}^+ \\ \mathcal{A}(Prop) & = & Type_1 \\ \mathcal{A}(Type_n) & = & Type_{n+1} & \forall n \in \mathbb{N}^+ \\ \mathcal{R}(Prop, Prop) & = & Prop \\ \mathcal{R}(Type_n, Prop) & = & Prop & \forall n \in \mathbb{N}^+ \\ \mathcal{R}(Prop, Type_n) & = & Type_n & \forall n \in \mathbb{N}^+ \\ \mathcal{R}(Type_m, Type_n) & = & Type_{max(m, n)} & \forall m, n \in \mathbb{N}^+ \\ \end{array}\]

以上這樣的PTS是CIC(Calculus of Indective Constructions)的核心
CIC過去是Coq的基礎
用文字說明一下吧
這個系統內有無限個sort
其中\(Prop: Type_1\), \(Type_1: Type_2\), \(Type_2: Type_3\), \(Type_3: Type_4\)…
\(Prop\)相當於原本的\(\star\)
\(Type_1\)是\(\Box\)
\(Type_2\)是\(\triangle\)
現在除了安全的\(Prop\)之外
並不會有自我指涉的問題了
因為\(\mathcal{R}(Type_2, Type_1) = Type_2\)
對於更高階層的sort來說道理也差不多

或者
要不乾脆讓所有sort都非自我指涉的？

\[\begin{array}{lcl} \mathcal{S} & = & Type_n & \forall n \in \mathbb{N} \\ \mathcal{A}(Type_n) & = & Type_{n+1} & \forall n \in \mathbb{N} \\ \mathcal{R}(Type_m, Type_n) & = & Type_{max(m, n)} & \forall m, n \in \mathbb{N} \\ \end{array}\]

這樣的系統是MLTT(Martin-Löf type theory)的核心
MLTT是Agda的基礎
\(Type_n\)在Agda中被稱為\(Set_n\)
現在我們沒有Prop了
系統裡不再有任何自我指涉的問題
那……
可不可以同時有自我指涉版本和非自我指涉版本的\(\star\)呢？

\[\begin{array}{lcl} \mathcal{S} & = & Prop, Type_n & \forall n \in \mathbb{N} \\ \mathcal{A}(Prop) & = & Type_1 \\ \mathcal{A}(Type_n) & = & Type_{n+1} & \forall n \in \mathbb{N} \\ \mathcal{R}(Prop, Prop) & = & Prop \\ \mathcal{R}(Type_n, Prop) & = & Prop & \forall n \in \mathbb{N} \\ \mathcal{R}(Prop, Type_n) & = & Type_n & \forall n \in \mathbb{N} \\ \mathcal{R}(Type_m, Type_n) & = & Type_{max(m, n)} & \forall m, n \in \mathbb{N} \\ \end{array}\]

這是pCIC(predicative Calculus of Inductive Constructions)的基礎
被用在新版本的Coq上
其中上面的\(Type_0\)在Coq中被稱為\(Set\)

PTS的部分大概就是這樣了

更高的抽象

我們現在有了無限個sort
在這些sort上頭
我們還能玩一些把戲以得到更高的抽象
接下來要講3個延伸的方向

universe polymorphism

這是Agda的做法
在上面的\(Type_n\)裡面
\(n\)事實上是個元變數
也就是說
它不是系統裡面一個普通的數
而是系統外的概念
還記得在談system F的時候
我把原本type的元變數納入系統中的事情嗎？
現在我要做的事情類似：
我要把\(Type_n\)中的\(n\)納入系統裡
在Agda中
\(n\)的型別被稱為\(Level\)
首先
\(0\)是一個\(Level\)：

\[\texttt{zero}: Level\]

有兩個\(Level\)相關的內建函數
第一個函數接收一個\(Level\)
傳回它的下一個數：

\[\texttt{suc}: Level \to Level\]

另一個函數取得兩個\(Level\)中較大的一個：

\[\texttt{max}: Level \to Level \to Level\]

\(Type\)現在變成了一個函數
它的型別有點詭異
不過姑且接受它吧：

\[Type: (l: Level) \to Type (suc (suc \: l)) \\ Type \stackrel{def}{\equiv} \lambda l: Level. Type_l\]

如此一來
我們就能抽象於\(Level\)上
寫出依賴於\(Level\)的函數：

\[(l: Level) \to ...\]

坦白說
我對這樣的系統有點意見
除了在理論上基礎薄弱之外
現實寫程式上會變成當需要用到\(Type\)的時候
常常手癢忍不住對\(Level\)進行抽象
儘管絕大多數你只會使用到\(Type_0\)而已
難道不能由電腦自己判斷\(Level\)嗎？
事實上是可以的
而接下來我要說的方法就是由電腦自動判斷\(Level\)

typical ambiguity

這其實沒啥好說的
簡單來說就是不用寫出\(Type_n\)的下標\(n\)
只要寫\(Type\)就好
然後電腦自動判斷你用\(Type\)的方式是一致的
Idris有實作這個
除此之外
Idris還實作了cumulative universes
以下介紹那東西又是啥鬼

cumulative universes

這個功能讓各sort之間有子型別的關係
只要一個型別是\(Type_k\)的成員
那它就是\(Type_{k + n}\)的成員
其中\(n\)是一個自然數
以符號表示是這樣：

\[\dfrac{\Gamma \vdash t: Type_m}{\Gamma \vdash t: Type_{\texttt{suc} \: m}}\]