Cartesian Closed Categories 與簡單型別論 (一)

介紹

範疇論對理論電腦科學影響重大，其中一個應用提供各種型別理論（複數以上 type theories）的模型語意。為了解釋這兩者之間的關係，我們以 simply-typed lambda calculus $\lambda_\to$（或簡稱 simple type theory、STT）為例，討論其範疇上的詮釋。在 STT 中只討論最基本的函數型別（function type）以及變數型別，具體來看是非常簡單的函數式語言，型別系統只負責處理 function application 是否合適。

這題材預計分做兩篇，首先解釋 Cartesian closed category （簡稱 CCC）跟 simply typed lambda calculus 的定義跟基本性質，接著談論如何聯繫 CCC 與 simply typed lambda calculus 兩者。

背景知識

一個範疇 $\mathscr{C}$ 是 Cartesian closed 若

1. 所有有限的 product 都存在以及
2. 對任意的物件 $y, z \in \mathscr{C}$ 都有 exponential object $z^y$。

更明確地說，第一個條件相當於 $\mathscr{C}$ 有 terminal object $1$ 以及對任意物件 $x, y$ 其 binary product $x \times y$ 都存在。第二個條件的 exponential object 定義為一個 object $z^y$ 以及一個「取值」態射 $\epsilon\colon z^y \times y \to z$ 滿足

對任意的物件 $x \in \mathscr{C}$ 以及任意的態射 $g\colon x \times y \to z$ 存在一個唯一的態射 $\lambda g \colon x \to z^y$ 使得 $g = \epsilon \circ (\lambda g \times \mathit{id}_y)$

基本的範例有集合範疇 $\mathbf{Set}$：在此範疇下，只包含一個元素的集合 $\{*\}$ 為 terminal object，對任意集合 $X, Y$ 都可以組成其卡式積 $X \times Y = \{\, (x, y) \mid x \in X, y \in Y\,\}$ 為此範疇的 binary product。而對 exponential object 則為所有從 $Y$ 到 $Z$ 構成的函數集合 $Y \to Z = \{\, f \colon Y \to Z \,\}$ 以及取值函數 $\mathrm{eval}\colon Z^Y \times Y \to Z$ 定義為 $\mathrm{eval}(f, y) = f(y)$。

我們可以再整理一下 exponential object 的定義：任意 exponential object $z^y$ 都存在若對所有的 $y$ 都具有以下對 $x$ 以及 $z$ 自然的一一對應
\begin{align*}
\hom(x, z^y) & \cong \hom(x \times y, z) \\
\lambda g\colon x \to z^y & \mapsto g = \epsilon \circ (\lambda g \times \mathit{id}_y) = \epsilon \circ (\lambda g \times y)
\end{align*}
（an isomorphism natural in $x$ and $z$），也就是說將 $(-)\times y$ 看成一個函子的話，具有一個 right adjoint $(-)^y$。

另外一個例子是給定一個 Boolean algebra $A$，用 $A$ 上的 poset 結構當作一個範疇，也會得到一個 Cartesian closed category，留給讀者分辨對應的 product 跟 exponential object 是什麼。

基本性質

在 $\mathbf{Set}$ 上的 $Z^Y$ 恰好是函數空間，也就是 $\mathbf{Set}(Y, Z)$。一般來說，exponential object $z^y$ 可以看作是將 $\hom(y, z)$ 內化成範疇內的物件，考慮以上 adjunction 的刻畫，因為 $y \cong 1 \times y$，我們可以推出：

\[ \hom(y, z) \cong \hom(1 \times y, z) \cong \hom(1, z^y) \]

對於所有態射 $f\colon y \to z$ 都可以對應到態射 $\lambda f\colon 1 \to z^y$。

這個態射 $\lambda f \colon 1\to z^y$ 代表什麼意思呢？從 $\mathbf{Set}$ 來看，任意 $x\colon 1 \to X$ 的函數，唯一決定 $X$ 上的一點 $x(*) \in X$。我們可以將 $1 \to X$ 當作是 $X$ 上的一個點。還可以從 exponential object 的「取值」態設來驗證這個想法：

引理：在 CCC 中，任意態設 $f\colon x \to y$ 以及任一點 $a\colon 1 \to x$，我們有 \[1 \xrightarrow{\langle \lambda f, a \rangle} y^x \times x \xrightarrow{\epsilon} y = 1 \xrightarrow{a} x \xrightarrow{f}y\] 

證明：給定任意 $f\colon x \to y$，考慮 $f' = f\circ \pi \colon 1 \times x \to x \to y$ 我們有\[\xymatrix{1\times x\ar[d]_{\lambda f' \times x}\ar[rd]^{f'}\\ y^x \times x\ar[r]_{\epsilon} & y}\] 也就是 $f' = \epsilon \circ (\lambda f' \times \mathit{id}_x)$。從此不難推出 $fa = \epsilon \circ \langle \lambda f, a \rangle$。

除此之外，exponential object 跟 products 有著常見的指數運算，例如

1. $(x^y)^z \cong x^{y \times z}$：從 adjunction 可輕易推得
2. $x¹\cong x$（同上）
3. $1^x \cong 1$ 從 $1$ 是 terminal 跟 adjunction 推得
4. $(x \times y)^z \cong x^z \times y^z$ 因為 $(-)^y$ 是 right adjoint。

 Cartesian closed 函子

我們對於保持 CCC 結構的函子特別有興趣，相當於代數上 homomorphism 保持代數結構操作的觀念：給定兩個 Cartesian closed 範疇 $\mathscr{C}, \mathscr{D}$，我們稱函子 $F\colon\mathscr{C}\to\mathscr{D}$ 為 Cartesian closed 的若 $F$ 保持 finite products 以及 exponential objects。具體來說，這代表

1. $F(1_\mathscr{C}) \cong 1_\mathscr{D}$
2. $F(x \times y) \cong Fx \times Fy$ 
3. $F(z^y) \cong F(z)^{F(y)}$ 

要特別注意的是，這邊的 $\cong$ 不單指同構而是將諸如投影態射 $\pi_x \colon x \times y \to x$ 同樣對應到 $Fx \times Fy \xrightarrow{F\pi} Fx$ 投影態射。

舉例來說，給定兩個 Boolean algebra $A, B$，所有從 $A$ 到 $B$ 的 Boolean algebra homomorphism $f$ 都可以視作 Cartesian closed 函子，因為任意的 Boolean algebra homomorphism 都滿足 $f(\top_A) = \top_B$、$f(a \wedge_A b) = fa \wedge_B fb$ 且 $f(a \to_A b) = fa \to_B fb$。

下一篇將介紹 simply-typed lambda calculus $\lambda_\to$ 並且討論如何將 $\lambda_\to$ 當作 Cartesian closed 範疇。