Pointed? Lifted!
目錄
相信讀者在閱讀 Haskell 相關文件的時候，偶而會碰到兩個形容詞：「pointed」和「lifted」。他們通常是用來描述資料結構或是型別，例如說 pointed datatype 或 lifted type 等等。在某些情境下這兩個東西會指涉到同一個概念上，但是這不是一定的。所以，究竟這兩者之間的差異何在？就讓我們從「我們寫出來的程式究竟代表什麼」這個故事開始吧！
所謂「一支程式究竟代表什麼」有好幾種不同的理解方式與詮釋方法。例如說「這個程式所有可能計算出來的結果」、「這個程式如何計算出一組結果」或「這個程式滿足哪些條件/特性」等等。
我們這邊要講的是第一種，也就是說，我們用「一支程式所有可能計算出來的結果」來代表這程式的意義。或是，直覺地來說，就是一支程式(或一段程式碼)所可能包含的所有資訊量。這種對於程式意義的解讀方式稱之為「指稱語意」 denotational semantics。例如說，正整數加法 (+) :: Nat → Nat → Nat 可能回傳出任一正整數，所以我們就用「所有正整數」來表示 (+) 的意義。而 even :: Nat → Bool 只可能回傳 True 或是 False 這兩個數值的其中一種，所以我們用 Bool 來表示 even 這支程式的意義。這種「一段程式所有可能回傳的結果」被稱之為該程式的 semantics domain，或直接簡稱為 domain。所以我們可以(粗略地)說，Nat 是 (+) 的 domain 而 Bool 是 even 的 domain。
有了 domain 這個觀念，我們就可以進一步來討論一支程式的意義，或是比較好幾支不同程式之間的差異。不過，一旦我們真的要拿 domain 來討論程式的意義，我們就不能簡單地用「 domain 就是一群某程式可以算出來的數值」這樣模糊的概念。對於 domain，我們需要更加精確的定義！
Sets as Domains
首先，最直觀地，因為是「一群數值」，所以理所當然地我們可以先試著用 set 去當做 domain 的 formal definition。舉例來說，我們可以說：上面的程式 even 的 set-theoretical domain 就是
\[\{True, False\}\]
嗯～ 這樣的 domain 看起來豪棒棒！不過，很可惜地，set 雖然可以表示「一群數值」，但是只有這樣的表示力其實還不夠我們用來討論程式。如果我們想單純用一個 set 來表示一個程式的意義，那麼，recursive function 就變成一個有點讓人尷尬的狀況了。因為我們可以寫出像是：
這樣的 function，但是他們的 domain 顯然不會是一個簡單的 set 就可以表示的(因為他們根本不會停下來！)。除此之外，還有另一種尷尬的情況是：我們不是永遠都是在處理 total function。而對 partial function 而言，是有可能給在碰到某些 input 時會沒法計算 (因為 undefined 嘛)。
關於這個問題其實還有其他更多東西可以探討，但是這可能超過了這篇文章的主軸。我們這邊需要知道的就只是 set 不夠用來描述程式這件事情就好。如果對於完整的原因有興趣可以參考Domain Theory - G. Hutton裡面的第一篇講義。
Pointed Sets as Domains
好，現在我們已經知道 set 不夠用了。那麼，set 欠缺了什麼？從上面的例子中我們知道說，我們欠缺了描述「程式不會停」(或者說「程式算不出東西」)這種情況的方法。所以，好像擴充 set 讓他可以多一個「東西」去專門表示這種情況似乎會是個不錯的主意。所以，這裡我們引入 pointed set 這個數學結構！
給定一個 set \(\mathcal{A}\)， 一個 pointed set 是指 \(\mathcal{A}\) 本身以及某個 \(\mathcal{A}\) 之中的特定元素 \(x\) (\(x \in \mathcal{A}\))。
這個 \(x\) 被稱為 base point，而這個 pointed set 則被表示為 \((\mathcal{A}, x)\)。
Pointed set 說穿了沒什麼了不起，就是一個 set 和該 set 裡面某個被特別指定的 element 而已。不過，就因為它具有這樣的一個 explicit membership，剛好就可以讓我們利用來偷偷多塞一個用來表示「算不出來」的 element 到某個集合上面。例如說，我們可以在 \[\{True, False\}\] 上多塞一個 element，而使其成為 \[\{True, False, \mathtt{Bt}\}\] 其中 \(\mathtt{Bt}\) 就是那個我們企圖用來表示「算不出來/算不完」的東西。然後，我們就可以說 even 的 domain 現在是 pointed set \[(\{True, False, \mathtt{Bt}\}, \mathtt{Bt})\] 而且顯然這個結構會比 \(\{True, False\}\) 這個單純的 set 更厲害！因為我們現在可以描述「算不完」或是「undefined」。
Posets as Domains
不過，仔細想想，光是有 base point 似乎還是不夠。比如說，我們知道 \(True \land True = True\) ，但是我們似乎沒有那麼肯定 \(True \land \mathtt{Bt}\) 會是什麼。從這裡我們可以觀察到說，\(\mathtt{Bt}\) 和 \(True\)(或 \(False\))之間似乎存在著某種本質上的差異。
某個程度我們可以把這個差異理解成「資訊量」的不同。尤其是當我們把 \(\mathtt{Bt}\) 理解成 undefined。一個直覺上的理解是，\(True\) 不管是表示「真」還是「正確」或是「非零整數」，它總歸來說是表示了某種資訊，但是反過來說，\(\mathtt{Bt}\) 本身表示的就是「得不到任何資訊」。
要注意的是，這裡所謂的資訊量和資訊內容的數值無關。舉例來說，整數 1 和 10 顯然數值上是 10 比較大，但是兩者個資訊的資訊含量是一樣的，都是「一個整數」而已。反過來說，(1, 1) 和 1 相比之下，顯然就是前者資訊量比較多。
請注意！上面例子裡的 1 和 10 這些的數值都是自然數，而且是指 primitive datatype 而不是 algebraic datatype。 如果這裡的自然數是 algebraic datatype 像 data Nat = Z | S Nat 這種，那這種 Nat 的資訊量的大小就是那個數值的大小。
為了體現這樣的資訊量差異，我們這邊引入了 information ordering 和 poset。一個 information ordering 是一個 partial ordering relation，並且會用符號 \(\sqsubseteq\) 表示。
對一個 set，\(\mathcal{A}\)，和一個定義在 \(\mathcal{A}\) 上面的 partial ordering relation，\(\sqsubseteq_{\mathcal{A}}\)，
我們可以做出一個數學結構：poset，表示成 \((\mathcal{A}, \sqsubseteq_{\mathcal{A}})\)。而且 \(\sqsubseteq_{\mathcal{A}}\) 要滿足：
reflexive 、 transitive 和 anti-symmetric。
另外，對一個 poset \((\mathcal{A}, \sqsubseteq_{\mathcal{A}})\) 來說，如果其中存在一個 \(b \in \mathcal{A}\) 使得 \(\forall x \in \mathcal{A}\) ， \(b \sqsubseteq_{\mathcal{A}} x\) 都成立，
則 \(b\) 被稱為 least element，並且標記為 ⊥。
現在，既然我們這邊討論的 \(\sqsubseteq_{\mathcal{A}}\) 代表的是資訊量的大小，所以顯然這個 ⊥ 就表示了「這個結構中資訊含量最小者」。
「資訊含量最小」不見得就是「沒有資訊」。慣例上，通常我們是直接使用 ⊥ 來表示「沒有資訊」，也就是前文內的 \(\mathtt{Bt}\) 這個角色。但是這不是必然的。因此在討論和使用 ⊥ 的時候要特別注意前後文和當時討論的情境。一個簡單例子是，(⊥,⊥) 會可以是某個 domain 的 least element，但是他本身其實並不是完全沒有資訊量。因為，雖然說 pair 裡面沒有資訊，但是我們知道這是一個 pair！
結合前面的 pointed set 和 information ordering，我們現在改用 pointed poset 來當做是 domain 的 formal definition！而這樣的 domain 比之前面的 set 或是 pointed set 而言，它可以更精確的描述一段程式可能回傳的結果(包含回傳不了任何結果)。
Pointed Domain and Lifting
雖說 pointed poset 很好，但是現實上我們程式語言裡面是存在著很多沒有 least element 的 datatype 的。例如說 Int, Double, Char 或 Bool 等等的 primitive type 都沒有內建 least element。這種沒有內建 least element 的 domain 有時候會被稱為 primitive domain。而有 least element 的則被稱為 pointed domain。
既然有兩種不同的 domain，理所當然我們就會想要找出辦法來將其中一個轉換成另一個。而 lifting 就是將 primitive domain 給轉換成 pointed domain 的 operation！也就是說，「lifting a domain」就是指在該 domain 上面放上 (introduce) 一個新的 ⊥，而且這個 ⊥ 真的就是表示「沒有資訊」。這裡需要特別注意的是，lifting 這個 operation 其實是產生一個新的 domain (因為是新的 set 和新的 partial ordering relation)，稱為 lifted domain。
事實上 lifting 是 constructions on domain 中的其中一個。一般常見的 constructions on domain 包含： product domain 、 co-product domain 、 lifting domain 和 function domain。任何複雜的 domain 都是由 primitive domain 配合上這個 constructions on domain 建構而成的。更多細節請參考文末的參考資料中關於 domain theory 的部份。
現在，終於要進入這篇文章的重點了！pointed domain 和 lifted domain 的主要差別是：
- pointed domain 只要求有一個可以當做 least element 的東西存在就好。既然只是 least element，所以它不必然要表示「沒有資訊」。
- lifted domain 必須要求那個 ⊥ 必須要是新加上的，而且必然要表示「沒有資訊」。
例如說，假設我們將 Unit 表示成 ()--⊥，接者我們用一個 wrapper 去將 Unit 包裝起來：data CU = C ()。那這個 CU 本身是 pointed，因為它可以表示成 (C ())--(C ⊥)，而其中 (C ⊥) 就是 least element。但是 CU 不是 lifted，因為顯然 (C ⊥) 不是表示「沒有資訊」。而如果我們 lifting CU，則會得到一組 (C ())--(C ⊥)--⊥ ，而這個就會是 lifted！
用 ⊥ 和 (C ⊥) 來當做一個 domain 的 least element 在惰性運算時是會有不同運算結果的。假設我們有 yo x y = y 這樣的一個 function， 那麼 yo ⊥ 1 和 yo (C ⊥) 1 會有完全不同的結果。 後者會可以回傳出 1，但是前者就爆炸了。
顯然，lifted domain 一定會是 pointed。但是反過來不成立！例如說 product of two pointed domains 還會是 pointed (least element 會是 (⊥,⊥))，可是不會是 lifted。其實這也不會很讓我們意外，因為除了 lifting 以外，其實沒有別的 constructions on CPOs 可以產生出新的 ⊥，所以生出 lifted domain 唯一個方法就只能是透過 lifting。
Conclusion
如果我們把 constructing a constructure 給想像成是一種 function 的話，那麼顯然 domain 也會適用在描述資料結構上！因此我們可以簡單總結如下。
Pointed type 的概念源自於 pointed set 和 poset，它強調的重點是「存在一個可以作為 least element 的東西」。對那個 element 本身沒有什麼額外的要求。
Lifted type 則是源自於 constructions on domain，它強調的重點在於「插入一個新的 ⊥ 來當做新的(且沒有任何資訊意義的) least element」。而因為那個 ⊥ 是新插入的，所以它會是外顯 (explicit) 的，也就是說它不能被包在某個資料結構中。
