Haskell/Denotational semantics

介紹

本章解釋如何將 Haskell 程式的意義形式化，即Denotational Semantics。正式指定程式 square x = x*x 與將每個數字對映到其平方的數學平方函式具有相同的意義，這似乎是在吹毛求疵，但程式 f x = f (x+1) 的意義如何？該程式會永遠迴圈。在接下來的內容中，我們將舉例說明 Scott 和 Strachey 首次採用的方法，併為推理一般函式式程式以及特別是遞迴定義的正確性奠定基礎。當然，我們將集中於那些理解 Haskell 程式所需的主題。

本章的另一個目的是說明嚴格和惰性的概念，這些概念體現了函式是否需要或不需要計算其引數的思想。這是預測 Haskell 程式計算過程的基本要素，因此對程式設計師來說是最重要的。有趣的是，這些概念可以用 Denotational Semantics 本身簡潔地表述，無需引用執行模型。它們將在圖約簡中得到很好的應用，但正是本章將使讀者熟悉 Denotational 定義和相關概念，例如 ⊥（“Bottom”）。只對嚴格性感興趣的讀者可能希望瀏覽Bottom 和偏函式部分，並快速轉到嚴格和非嚴格語義部分。

什麼是Denotational Semantics，它有什麼用？

Haskell 程式的意義是什麼？Denotational Semantics 為這個問題提供了答案。通常，程式語言的 Denotational Semantics 將每個程式對映到一個數學物件（語義），該物件代表了所討論程式的意義。例如，Haskell 程式 10、9+1、2*5 和 sum [1..4] 的數學物件可以用整數10來表示。我們說所有這些程式都表示整數10。這樣的數學物件的集合稱為語義域。

從程式程式碼到語義域的對映通常用程式程式碼周圍的雙方括號（“牛津括號”）來寫下。例如，

$[\![{\texttt {2*5}}]\!]=10.$

語義是可組合的，也就是說，程式 1+9 的意義只取決於其組成部分的意義

$[\![{\texttt {a+b}}]\!]=[\![{\texttt {a}}]\!]+[\![{\texttt {b}}]\!].$

相同的符號用於型別，即

$[\![{\texttt {Integer}}]\!]=\mathbb {Z} .$

但是，為了簡單起見，在後續章節中，我們將隱式地將表示式與其語義物件等同起來，並且僅在需要澄清時使用此符號。

Haskell 等純粹函式式語言的一個關鍵屬性是，像“1+9 代表 10”這樣的直接數學解釋也適用於函式：本質上，型別為 Integer -> Integer 的程式的語義是數學函式 $\mathbb {Z} \to \mathbb {Z}$，它在整數之間進行對映。雖然我們會看到這種表達方式通常需要改進，以包括非終止情況，但對於命令式語言來說情況明顯更糟：具有該型別過程表示的是某種可能會以意外方式改變機器狀態的東西。命令式語言與操作語義緊密相連，後者描述了它們在機器上的執行方式。可以為命令式程式定義一個語義語義，並用它來推理這些程式，但語義通常具有操作性質，有時與函式式語言的語義語義相比必須進行擴充套件。^[2] 相反，純粹函式式語言的含義預設情況下完全獨立於它們的執行方式。Haskell98 標準甚至只指定了 Haskell 的非嚴格語義語義，而沒有規定如何實現它們。

最終，語義語義使我們能夠開發出正式的證明，證明程式確實以數學方式執行了我們想要它們執行的操作。具有諷刺意味的是，為了在日常 Haskell 中證明程式屬性，可以使用等式推理，它將程式轉換為等效程式，而無需過多地檢視我們在本章中關注的底層數學物件。但是，語義語義實際上出現在我們必須對非終止程式進行推理時，例如在無限列表中。

當然，因為它們只說明瞭程式是什麼，所以語義語義無法回答有關程式執行多長時間或消耗多少記憶體的問題；這由求值策略控制，該策略規定計算機如何計算表示式的正規化。另一方面，實現必須尊重語義，在一定程度上，語義決定了如何在機器上求值 Haskell 程式。我們將在嚴格和非嚴格語義中詳細說明這一點。

選擇什麼作為語義域？

現在我們正在尋找合適的數學物件，我們可以將這些物件歸因於每個 Haskell 程式。對於示例10、2*5 和 sum [1..4]，很明顯所有表示式都應該表示整數 10。概括地說，型別為 Integer 的每個值 x 可能表示集合 $\mathbb {Z}$ 中的元素。對於像 f :: Integer -> Integer 這樣的函式，我們可以訴諸於“函式”的數學定義，它是一組 (引數，值) 對，即其圖。

但是，將函式解釋為它們的圖太快了，因為它不適用於遞迴定義。考慮以下定義

shaves :: Integer -> Integer -> Bool
1 `shaves` 1 = True
2 `shaves` 2 = False
0 `shaves` x = not (x `shaves` x)
_ `shaves` _ = False

我們可以將 0、1 和 2 視為長鬍子的男性，問題是誰給誰刮鬍子。人物 1 自己給自己刮鬍子，但 2 由理髮師 0 刮鬍子，因為求值第三個等式得到 0 `shaves` 2 == True。一般來說，第三行說理髮師 0 給所有不給自己刮鬍子的人刮鬍子。

那麼理髮師自己呢，0 `shaves` 0 是真還是假？如果它是真的，那麼第三個等式說它不是真的。如果它不是真的，那麼第三個等式說它是真的。我們感到困惑，我們看到我們無法將 True 或 False 歸因於 0 `shaves` 0；我們用來解釋函式 shaves 的圖必須有一個空位。我們意識到我們的語義物件必須能夠包含偏函式，這些函式對於其引數的某些值是未定義的（..否則引數型別允許）。

眾所周知，這個著名的例子引發了集合論中嚴重的奠基問題。它是一個非預測性定義的例子，一個使用自身的定義，一個邏輯迴圈。不幸的是，對於遞迴定義來說，迴圈不是問題，而是特徵。

底部和偏函式

⊥ 底部

為了定義偏函式，我們引入了一個特殊的值 ⊥，稱為底部，通常用打字機字型寫成 _|_。我們說 ⊥ 是完全“未定義”的值或函式。每個基本資料型別，例如 Integer 或 ()，除了其通常的元素外，還包含一個 ⊥。因此，型別 Integer 的可能值為

$\bot ,0,+1,-1,+2,-2,+3,-3,\dots$

將 ⊥ 新增到值集中也稱為提升。這通常用下標表示，例如在 $\mathbb {Z} _{\bot }$ 中。雖然這是數學集合“提升的整數”的正確表示法，但我們更喜歡談論“型別為 Integer 的值”。我們這樣做是因為 $\mathbb {Z} _{\bot }$ 暗示存在“真實”整數 $\mathbb {Z}$，但在 Haskell 內部，“整數”是 Integer。

作為另一個例子，只有一個元素的型別 () 實際上有兩個居民

$\bot ,()$

目前，我們將堅持使用Integer進行程式設計。任意代數資料型別將在代數資料型別部分進行處理，因為嚴格和非嚴格語言在這些型別如何包含⊥方面存在分歧。

在Haskell中，表示式undefined表示⊥。藉助它，確實可以驗證實際Haskell程式的一些語義屬性。undefined具有多型型別forall a . a，當然可以將其專門化為undefined :: Integer，undefined :: ()，undefined :: Integer -> Integer等等。在Haskell Prelude中，它被定義為

undefined = error "Prelude.undefined"

作為旁註，從Curry-Howard 同構可以得出，任何多型型別forall a . a的值都必須表示⊥。

偏函式和語義近似順序

現在，$\bot$使我們有可能擁有偏函式

$f(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\-2&{\mbox{ if }}n{\mbox{ is }}1\\\bot &{\mbox{ else }}\end{cases}}$

這裡，$f(n)$為$n=0$和$n=1$產生明確定義的值，但對於所有其他$n$產生$\bot$。

型別Integer -> Integer也有其$\bot$，它使用來自Integer的$\bot$以這種方式定義

$\bot (n)=\bot$ 對於所有$n$

其中，左側的$\bot$型別為Integer -> Integer，右側的型別為Integer。

為了形式化，偏函式，比如型別為Integer -> Integer的函式，至少是從提升的整數$\mathbb {Z} _{\bot }=\{\bot ,0,\pm 1,\pm 2,\pm 3,\dots \}$到提升的整數的數學對映。但這還不夠，因為它沒有承認$\bot$的特殊作用。例如，定義

$g(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}\bot \\\bot &{\mbox{ else }}\end{cases}}$

是一個將無限迴圈轉換為終止程式，反之亦然的函式，這解決了停機問題。當$g(1)$ 未定義時，$g(\bot )$ 如何產生一個定義值？直覺是，每個偏函式$g$ 應該對更確定的引數產生更多確定的答案。為了形式化，我們可以說每個具體數字都比$\bot$ **更確定**。

$\bot \sqsubset 1\ ,\ \bot \sqsubset 2\ ,\dots$

這裡，$a\sqsubset b$ 表示$b$ 比$a$ 更確定。類似地，$a\sqsubseteq b$ 將表示$b$ 比$a$ 更確定，或者兩者相等（因此具有相同的確定性）。$\sqsubset$ 也被稱為 **語義近似序**，因為我們可以用更不確定的值來近似確定值，從而將“更確定”解釋為“更好地近似”。當然，$\bot$ 被設計為資料型別的最小元素，我們總是有$\bot \sqsubset x$ 對於所有$x$，除了$x$ 恰好表示$\bot$ 本身的情況。

$\forall x\neq \bot \ \ \ \bot \sqsubset x$

由於沒有一個數字比另一個數字更“定義明確”，因此數學關係 $\sqsubset$ 對任何一對數字都是假的。

$1\sqsubset 1$ 不成立。 無論是 $1\sqsubset 2$ 還是 $2\sqsubset 1$ 都不能成立。

這與普通的順序謂詞 $\leq$ 形成對比，後者可以比較任何兩個數字。記住這一點的一個快速方法是這句話：“$1$ 和 $2$ 在“資訊含量”方面不同，但在“資訊量”方面相等”。這也是我們使用不同符號的原因：$\sqsubseteq$。

無論是 $1\sqsubseteq 2$ 還是 $2\sqsubseteq 1$ 都不能成立， 但 $1\sqsubseteq 1$ 成立。

人們說 $\sqsubseteq$ 指定了一個偏序，並且型別為Integer的值構成一個偏序集（簡稱poset）。偏序的特點是以下三個定律

• 自反性，任何事物都與其自身一樣定義明確：$x\sqsubseteq x$ 對所有 $x$
• 傳遞性：如果 $x\sqsubseteq y$ 並且 $y\sqsubseteq z$，那麼 $x\sqsubseteq z$
• 反對稱性：如果 $x\sqsubseteq y$ 和 $y\sqsubseteq x$ 都成立，那麼 $x$ 和 $y$ 必須相等：$x=y$。

練習
整數集關於 ≤ 序關係是否構成偏序集？

我們可以透過下面的圖來描述 Integer 型別的值上的 ≤ 序關係：

其中每個節點之間的連線表示上面的節點比下面的節點定義更完整。因為只有一個層次（不包括 ⊥），所以我們說 Integer 是一個**扁平域**。這幅圖也解釋了 ⊥ 的名稱：它被稱為**底**，因為它總是位於最底部。

單調性

我們對偏函式的直覺現在可以表述如下：每個偏函式 f 都是偏序集之間的**單調**對映。定義更完整的引數將產生定義更完整的值

$x\sqsubseteq y\Rightarrow f(x)\sqsubseteq f(y)$

特別是，一個單調函式 h 滿足 h(⊥) = 1，它是一個常數函式：對於所有 n，都有 h(n) = 1。請注意，這裡至關重要的是 1 ≤ 2 等等不成立。

翻譯成 Haskell，單調性意味著我們不能使用 ⊥ 作為條件，即我們不能對 ⊥ 或其等價物 undefined 進行模式匹配。否則，上面提到的 g 的例子就可以用 Haskell 程式來表達。正如我們將在後面看到的那樣，⊥ 也表示非終止程式，因此在 Haskell 中無法觀察到 ⊥ 與停機問題有關。

當然，"定義更完整"的概念可以透過以下方式擴充套件到偏函式：如果一個函式在每個可能的引數上都比另一個函式定義更完整，那麼它就比另一個函式定義更完整

$f\sqsubseteq g{\mbox{ if }}\forall x.f(x)\sqsubseteq g(x)$

因此，偏函式也構成一個偏序集，其中未定義函式 ⊥(x) = ⊥ 是最小元素。

遞迴定義作為不動點迭代

階乘函式的近似值

現在我們有了描述偏函式的方法，可以對遞迴定義進行解釋。讓我們以階乘函式 $f(n)=n!$ 為例，其遞迴定義為

$f(n)={\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f(n-1)$

雖然我們看到將這個遞迴函式直接解釋為集合描述可能會導致問題，但我們直觀地知道，為了計算 $f(n)$ 對於給定的每一個 $n$，我們必須迭代右手邊。這個迭代可以形式化如下：我們計算一個函式序列 $f_{k}$，每個函式都由右手邊應用於前面的函式組成，即

$f_{k+1}(n)={\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f_{k}(n-1)$

我們從未定義函式 $f_{0}(n)=\bot$ 開始，得到的偏函式序列如下

$f_{1}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\\bot &{\mbox{ else }}\end{cases}}\ ,\ f_{2}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\1&{\mbox{ if }}n{\mbox{ is }}1\\\bot &{\mbox{ else }}\end{cases}}\ ,\ f_{3}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\1&{\mbox{ if }}n{\mbox{ is }}1\\2&{\mbox{ if }}n{\mbox{ is }}2\\\bot &{\mbox{ else }}\end{cases}}$

等等。顯然，

$\bot =f_{0}\sqsubseteq f_{1}\sqsubseteq f_{2}\sqsubseteq \dots$

我們期望這個序列收斂於階乘函式。

迭代遵循著著名的不動點迭代方案

$x_{0},g(x_{0}),g(g(x_{0})),g(g(g(x_{0}))),\dots$

在本例中，$x_{0}$ 是一個函式，而 $g$ 是一個 泛函，它將函式對映到另一個函式。我們有

$x_{0}=\bot$ 以及

$g(x)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n*x(n-1)\,$

如果我們從 $x_{0}=\bot$ 開始，迭代將產生越來越接近階乘函式的定義

$\bot \sqsubseteq g(\bot )\sqsubseteq g(g(\bot ))\sqsubseteq g(g(g(\bot )))\sqsubseteq \dots$

(證明序列遞增：第一個不等式 $\bot \sqsubseteq g(\bot )$ 來自於 $\bot$ 比任何其他東西都少定義。第二個不等式來自第一個不等式，透過將 $g$ 應用於兩邊並注意到 $g$ 是單調的。第三個來自第二個，以同樣的方式，等等。）

用 Haskell 表達這種迭代方案非常具有說明性。由於泛函只是普通的更高階函式，所以我們有

g :: (Integer -> Integer) -> (Integer -> Integer)
g x = \n -> if n == 0 then 1 else n * x (n-1)

x0 :: Integer -> Integer
x0 = undefined

(f0:f1:f2:f3:f4:fs) = iterate g x0

現在我們可以對函式 f0,f1,... 進行示例引數評估，並檢視它們是否產生 undefined。

 > f3 0
 1
 > f3 1
 1
 > f3 2
 2
 > f3 5
 *** Exception: Prelude.undefined
 > map f3 [0..]
 [1,1,2,*** Exception: Prelude.undefined
 > map f4 [0..]
 [1,1,2,6,*** Exception: Prelude.undefined
 > map f1 [0..]
 [1,*** Exception: Prelude.undefined

當然，我們不能用它來檢查 f4 是否真的對所有引數都是 undefined。

收斂

對於數學家來說，這個問題是這個逼近序列是否收斂仍然需要解答。為此，我們說一個偏序集是一個 有向完全偏序集 (dcpo) 當且僅當每個單調序列 $x_{0}\sqsubseteq x_{1}\sqsubseteq \dots$ （也稱為 鏈）都有一個最小上界（上確界）

$\sup _{\sqsubseteq }\{x_{0}\sqsubseteq x_{1}\sqsubseteq \dots \}=x$.

如果是這樣的話，對於語義逼近順序，我們可以清楚地確定，逼近階乘函式的單調函式序列確實有一個極限。對於我們的語義解釋，我們將只遇到具有最小元素 $\bot$ 的 dcpos，它們被稱為 完全偏序集 (cpo)。

Integers 明顯構成一個 (d)cpo，因為由兩個以上元素組成的單調序列必須是以下形式

$\bot \sqsubseteq \dots \sqsubseteq \ \bot \sqsubseteq n\sqsubseteq n\sqsubseteq \dots \sqsubseteq n$

其中 $n$ 是一個普通數字。因此，$n$ 已經是最小上界。

對於函式 Integer -> Integer，這個論據不成立，因為單調序列可能具有無限長度。但由於 Integer 是一個 (d)cpo，我們知道對於每個點 $n$，存在一個最小上界

$\sup _{\sqsubseteq }\{\bot =f_{0}(n)\sqsubseteq f_{1}(n)\sqsubseteq f_{2}(n)\sqsubseteq \dots \}=:f(n)$.

由於語義近似順序是逐點定義的，函式 $f$ 是我們尋找的最小上界。

這些是我們將階乘函式的非謂詞定義轉化為一個定義明確的構造的目標的最後幾步。當然，還需要證明 $f(n)$ 實際上對於每個 $n$ 都能產生一個定義的值，但這並不難，而且比一個完全形式錯誤的定義更合理。

底部包含非終止

嘗試將我們新獲得的對遞迴定義的洞察應用於一個不終止的例子，這是很有啟發性的。

$f(n)=f(n+1)$

近似序列如下

$f_{0}=\bot ,f_{1}=\bot ,\dots$

並且只包含 $\bot$。顯然，得到的極限是 $\bot$。從操作的角度來看，執行此程式的機器將無限迴圈。因此，我們看到 $\bot$ 也可能表示一個 **非終止** 函式或值。因此，鑑於停機問題，在 Haskell 中對 $\bot$ 進行模式匹配是不可能的。

最小不動點的解釋

早些時候，我們將近似序列稱為眾所周知的“不動點迭代”方案的一個例子。當然，階乘函式的定義$f$也可以被認為是泛函$g$的不動點規範。

$f=g(f)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f(n-1)$

然而，可能存在多個不動點。例如，存在多個$f$滿足規範

$f=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}f(n+1)$,

當然，當執行這樣的程式時，機器將在$f(1)$或$f(2)$上無限迴圈，因此不會產生關於$f(1)$值的有價值資訊。這對應於選擇最不確定的不動點作為語義物件$f$，這實際上是一個規範選擇。因此，我們說

$f=g(f)$,

定義了$g$的最小不動點$f$。顯然，最小是相對於我們的語義近似順序$\sqsubseteq$。

如果我們新增一個條件，即$g$必須是連續的（有時也稱為“鏈連續”），那麼我們就可以保證最小不動點的存在。這意味著$g$尊重單調序列的上確界

$\sup _{\sqsubseteq }\{g(x_{0})\sqsubseteq g(x_{1})\sqsubseteq \dots \}=g\left(\sup _{\sqsubseteq }\{x_{0}\sqsubseteq x_{1}\sqsubseteq \dots \}\right)$

然後我們可以爭論，用

$f=\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}$

我們有

${\begin{array}{lcl}g(f)&=&g\left(\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\right)\\&=&\sup _{\sqsubseteq }\{g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\\&=&\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\\&=&f\end{array}}$

並且迭代極限確實是 $g$ 的一個不動點。你可能也想要說服自己，不動點迭代產生的不動點是 *最小的* 不動點。

練習
證明由以 $x_{0}=\bot$ 為起點的不動點迭代獲得的不動點也是最小的不動點，即它小於任何其他不動點。(提示：$\bot$ 是我們 cpo 的最小元素，而 $g$ 是單調的)

順便說一句，我們怎麼知道我們寫下的每個 Haskell 函式確實是連續的？就像單調性一樣，這必須由程式語言強制執行。誠然，這些屬性可以在一定程度上隨意地強制執行或破壞，所以這個問題感覺有點空洞。但直觀地說，單調性透過不允許對 $\bot$ 進行模式匹配來保證。對於連續性，我們注意到對於任意型別 a，每個簡單函式 a -> Integer 自動是連續的，因為 Integer 的單調序列是有限長度的。任何型別 a 的無限鏈都對映到 Integer 的有限鏈，對上確界的尊重成為單調性的結果。因此，Integer -> Integer 特殊情況的所有函式都必須是連續的。對於像 $g$::(Integer -> Integer) -> (Integer -> Integer) 這樣的泛函，連續性則是由於柯里化而實現的，因為該型別與 ::((Integer -> Integer), Integer) -> Integer 同構，我們可以取 a=((Integer -> Integer), Integer)。

在 Haskell 中，階乘函式的固定解釋可以編碼為

factorial = fix g

藉助於不動點組合子

fix :: (a -> a) -> a.

我們可以透過以下方式定義它

fix f = let x = f x in x

這讓我們有點困惑，因為當展開 $factorial$ 時，結果與我們在 Haskell 中第一次定義階乘函式的方式沒有什麼不同。但當然，這整個部分所討論的構造在執行真正的 Haskell 程式時根本不存在。它只是一種將 Haskell 程式的數學解釋放在牢固基礎上的方法。然而，我們可以藉助於 undefined 在 Haskell 本身中探索這些語義，這非常棒。

嚴格語義和非嚴格語義

在詳細闡述了 Haskell 程式的語義解釋之後，我們將放棄用於語義物件的數學函式符號 $f(n)$，而採用現在等效的 Haskell 符號 f n。

嚴格函式

一個只有一個引數的函式 f 被稱為 **嚴格** 函式，當且僅當

f ⊥ = ⊥.

以下是一些嚴格函式的例子

id     x = x
succ   x = x + 1
power2 0 = 1
power2 n = 2 * power2 (n-1)

它們沒有什麼出奇之處。但為什麼它們是嚴格的呢？證明這些函式確實是嚴格的很有啟發性。對於 id，這來自定義。對於 succ，我們必須思考 ⊥ + 1 是 ⊥ 還是不是。如果不是，那麼例如我們應該有 ⊥ + 1 = 2 或者更一般地 ⊥ + 1 = k，其中 k 是某個具體數字。我們記得每個函式都是 *單調* 的，所以例如我們應該有

2 = ⊥ + 1 ⊑ 4 + 1 = 5

因為 ⊥ ⊑ 4。但 2 ⊑ 5、2 = 5 或者 2 ⊒ 5 都不成立，所以 k 不能是 2。一般來說，我們得到矛盾

k = ⊥ + 1 ⊑ k + 1 = k + 1.

因此，唯一可能的選擇是

succ ⊥ = ⊥ + 1 = ⊥

所以 succ 是嚴格的。

練習
證明 power2 是嚴格的。雖然可以基於“顯而易見”的事實，即 power2 n 等於 $2^{n}$，但最好使用不動點迭代法來證明。

非嚴格和嚴格語言

尋找非嚴格函式時，發現只有一種型別為 Integer -> Integer 的非嚴格函式原型。

one x = 1

它的變體是 const k x = k，對於每個具體數字 k。為什麼這些是唯一可能的？記住，one n 的定義不能少於 one ⊥。由於 Integer 是一個扁平域，兩者必須相等。

為什麼 one 是非嚴格的？為了證明它是，我們使用一個 Haskell 直譯器並嘗試

> one (undefined :: Integer)
1

它不是 ⊥。這是合理的，因為 one 完全忽略了它的引數。在操作意義上將 ⊥ 解釋為“非終止”，可以說 one 的非嚴格性意味著它不會強制評估它的引數，因此在評估引數 ⊥ 時避免了無限迴圈。但也可以說，每個函式都必須在計算結果之前評估它的引數，這意味著 one ⊥ 也應該等於 ⊥。也就是說，如果計算引數的程式沒有停止，one 也應該不會停止。 ^{這表明，可以自由選擇函數語言程式設計語言的這種設計或另一種設計。如果函式預設情況下是嚴格的或非嚴格的，則稱該語言是嚴格的或非嚴格的。Haskell 選擇的是非嚴格語言。相反，函式式語言 ML 和 Lisp 選擇了嚴格語義。}

具有多個引數的函式

嚴格性的概念擴充套件到具有多個變數的函式。例如，如果一個函式 f 具有兩個引數，當且僅當

f x ⊥ = ⊥

對於所有 x 成立時，該函式在第二個引數上是嚴格的。但對於多個引數，嚴格性取決於其他引數給定值的混合形式更為常見。一個例子是條件表示式

cond b x y = if b then x else y

我們可以看到，它在 y 上是嚴格的，取決於測試 b 是 True 還是 False

cond True  x ⊥ = x
cond False x ⊥ = ⊥

同樣，對於 x 也是如此。顯然，如果 x 和 y 都是 ⊥，那麼 cond 肯定等於 ⊥，但當它們中至少有一個是定義的時，它不一定等於 ⊥。這種行為稱為聯合嚴格性。

顯然，cond 的行為類似於 if-then-else 語句，在該語句中，不評估 then 和 else 分支至關重要。

if null xs then 'a' else head xs
if n == 0  then  1  else 5 / n

在這裡，當條件滿足時，else 部分等於 ⊥。因此，在非嚴格語言中，我們有可能將 if-then-else 等原始控制語句封裝到 cond 這樣的函式中。這樣，我們可以定義自己的控制運算子。在嚴格語言中，這是不可能的，因為在呼叫 cond 時，兩個分支都會被評估，這使得它相當無用。這讓我們瞥見了這樣一個普遍觀察結果：與嚴格性相比，非嚴格性為程式碼重用提供了更大的靈活性。有關此主題的更多資訊，請參見章節 惰性。

代數資料型別

在處理 Integer 之間的偏函式的動機案例後，我們現在想將語義學範圍擴充套件到 Haskell 中的任意代數資料型別。

關於命名法的一句話：特定型別的語義物件集合通常稱為域。這個術語更像是一個通用名稱，而不是一個特定的定義，我們決定我們的域是 cpos（完全偏序集），即值集合以及滿足某些條件的更定義關係，以允許不動點迭代。通常，人們會向 cpos 新增額外的條件，以確保我們的域的值可以在計算機上以某種有限的方式表示，從而避免考慮不可數無限集的扭曲方式。但由於我們不打算證明一般的域理論定理，因此這些條件只是透過構造而偶然成立。

建構函式

讓我們以示例型別為例

data Bool    = True | False
data Maybe a = Just a | Nothing

這裡，True、False 和 Nothing 是零元建構函式，而 Just 是一個一元建構函式。Bool 的成員形成以下域

記住，⊥ 作為最小元素被新增到 True 和 False 的值集中，我們說該型別是提升的。 ^{偏序圖只有一個層次的域稱為扁平域。我們已經知道 $Integer$ 也是一個扁平域，只是 ⊥ 上方層次的元素數量是無限的。}

Maybe Bool 可能有哪些成員？它們是

⊥, Nothing, Just ⊥, Just True, Just False

因此，一般規則是將所有可能的值插入一元（二元、三元……）建構函式中，就像往常一樣，但不要忘記 ⊥。關於偏序，我們記得建構函式應該像其他任何函式一樣單調。因此，偏序如下所示

但有一點值得思考：為什麼 Just ⊥ = ⊥ 不成立？我的意思是，“Just 未定義”和“未定義”一樣未定義！答案是，這取決於語言是嚴格的還是非嚴格的。在嚴格語言中，所有建構函式預設情況下都是嚴格的，即 Just ⊥ = ⊥，並且該圖將簡化為

因此，嚴格語言的所有域都是扁平的。

但在像 Haskell 這樣的非嚴格語言中，建構函式預設情況下是非嚴格的，Just ⊥ 是一個與 ⊥ 不同的新元素，因為我們可以編寫一個對它們做出不同反應的函式

f (Just _) = 4
f Nothing  = 7

由於 f 忽略了 Just 建構函式的內容，f (Just ⊥) 為 4，但 f ⊥ 為 ⊥（直觀地說，如果將 ⊥ 傳遞給 f，則無法確定是使用 Just 分支還是 Nothing 分支，因此將返回 ⊥）。

這產生了非扁平域，如前圖所示。這些有什麼用？在圖約簡的上下文中，我們也可以將 ⊥ 視為一個未評估的表示式。因此，值 x = Just ⊥ 可能會告訴我們，一個計算（例如查詢）成功了，並且不是 Nothing，但實際值尚未評估。如果我們只關心 x 是否成功，這實際上可以節省我們不必要的計算工作，以確定 x 是 Just True 還是 Just False，就像在扁平域中那樣。非扁平域的全部影響將在章節 惰性 中探討，但其中一個突出的例子是在遞迴資料型別和無限列表部分處理的無限列表。

模式匹配

在嚴格函式部分，我們透過檢查不同輸入上的結果並堅持單調性，證明了一些函式是嚴格的。但是，從代數資料型別的角度來看，在現實生活中的 Haskell 中，只有一個嚴格性的來源：模式匹配，即 case 表示式。一般規則是，對 data 型別建構函式進行模式匹配將強制函式變得嚴格，即，將 ⊥ 與建構函式進行匹配始終會導致 ⊥。為了說明，考慮

const1 _ = 1

const1' True  = 1
const1' False = 1

第一個函式 const1 是非嚴格的，而 const1' 是嚴格的，因為它會確定引數是 True 還是 False，儘管它的結果不依賴於此。函式引數中的模式匹配等效於 case 表示式

const1' x = case x of
   True  -> 1
   False -> 1

同樣，它們對 x 強加了嚴格性：如果 case 表示式的引數表示 ⊥，那麼整個 case 也將表示 ⊥。然而，case 表示式的引數可能更復雜，例如

foo k table = case lookup ("Foo." ++ k) table of
  Nothing -> ...
  Just x  -> ...

並且很難追蹤這對 foo 的嚴格性意味著什麼。

在等式風格中，多個模式匹配的例子是邏輯 or

or True _ = True
or _ True = True
or _ _    = False

請注意，方程是從上到下匹配的。or 的第一個方程將第一個引數與 True 進行匹配，因此 or 在第一個引數上是嚴格的。同一個方程還告訴我們 or True x 在 x 上是非嚴格的。如果第一個引數是 False，那麼第二個引數將與 True 進行匹配，並且 or False x 在 x 上是嚴格的。請注意，雖然萬用字元通常是非嚴格性的標誌，但這取決於它們相對於建構函式模式匹配的位置。

練習
對邏輯 and 進行類似的討論 如果我們知道另一個引數，邏輯“異或”（xor）是否可以在一個引數上是非嚴格的？

還有另一種形式的模式匹配，即不可否認模式，用波浪號 ~ 表示。它們的使用示例如下

f ~(Just x) = 1
f Nothing   = 2

不可否認模式總是會成功（因此得名），導致 f ⊥ = 1。但當將 f 的定義改為

f ~(Just x) = x + 1
f Nothing   = 2      -- this line may as well be left away

我們有

f ⊥       = ⊥ + 1 = ⊥
f (Just 1) = 1 + 1 = 2

如果引數與模式匹配，x 將被繫結到相應的值。否則，任何類似 x 的變數都將被繫結到 ⊥。

預設情況下，let 和 where 繫結也是非嚴格的

foo key map = let Just x = lookup key map in ...

等效於

foo key map = case (lookup key map) of ~(Just x) -> ...

練習
Haskell 語言定義詳細介紹了模式匹配的語義，你現在應該能夠理解它了。所以繼續看看吧！ 考慮一個有兩個 Bool 型別的引數的函式 or，它具有以下性質: or ⊥ ⊥ = ⊥ or True ⊥ = True or ⊥ True = True or False y = y or x False = x 這個函式是聯合嚴格性的另一個例子，但它更尖銳: 只有當兩個引數都為 ⊥ 時，結果才為 ⊥ (至少當我們限制引數為 True 和 ⊥ 時)。這樣的函式可以在 Haskell 中實現嗎？

遞迴資料型別和無限列表

遞迴資料結構的情況與基本情況並沒有太大區別。考慮一個單元值的列表

data List = [] | () : List

雖然這看起來像一個簡單的型別，但實際上，你可以用$\bot$ 填入各種位置，因此對應的圖很複雜。這個圖的底部顯示在下面。省略號表示圖在這個方向上繼續。一個元素後面的紅色橢圓表示這是一個鏈的末端；該元素處於正規化。

等等。但現在，也有無限長的鏈，比如

⊥ $\sqsubseteq$ ():⊥ $\sqsubseteq$ ():():⊥ $\sqsubseteq$ ...

這給我們帶來了一些麻煩，正如我們在收斂部分指出的那樣，每個單調序列都必須有一個最小上界。只有當我們允許使用無限列表時，這才是可能的。無限列表 (有時也稱為流) 被證明非常有用，它們的多方面用例在延遲計算章節中得到了詳細介紹。在這裡，我們將展示它們的語義應該是什麼以及如何對它們進行推理。請注意，雖然下面的討論僅限於列表，但它很容易推廣到任意遞迴資料結構，例如樹。

在下面，我們將切換回標準的列表型別

data [a] = [] | a : [a]

以縮小與 Haskell 中使用無限列表的實際程式設計之間的語法差距。

練習
繪製與 [Bool] 對應的非扁平域。 對於 [Integer]，圖形如何改變？

用無限列表計算最好用例子來說明。為此，我們需要一個無限列表

ones :: [Integer]
ones = 1 : ones

當將不動點迭代應用於這個遞迴定義時，我們看到 ones 應該是

⊥ $\sqsubseteq$ 1:⊥ $\sqsubseteq$ 1:1:⊥ $\sqsubseteq$ 1:1:1:⊥ $\sqsubseteq$...,

這是一個由 1 組成的無限列表。讓我們嘗試理解 take 2 ones 應該是什麼。根據 take 的定義

take 0 _      = []
take n (x:xs) = x : take (n-1) xs
take n []     = []

我們可以將 take 應用於 ones 的近似序列的元素

take 2 ⊥       ==>  ⊥
take 2 (1:⊥)   ==>  1 : take 1 ⊥      ==>  1 : ⊥
take 2 (1:1:⊥) ==>  1 : take 1 (1:⊥)  ==>  1 : 1 : take 0 ⊥
               ==>  1 : 1 : []

我們看到 take 2 (1:1:1:⊥) 等等必須與 take 2 (1:1:⊥) = 1:1:[] 相同，因為 1:1:[] 是完全定義的。在輸入列表序列和結果輸出列表序列上都取上界，我們可以得出結論

take 2 ones = 1:1:[]

因此，取 ones 的前兩個元素的行為完全符合預期。

從這個例子推廣，我們看到關於無限列表的推理涉及考慮近似序列並傳遞到上界，即真正的無限列表。不過，我們還沒有給它一個堅實的基礎。解決方案是將無限列表與整個鏈本身等同起來，並將其正式地作為新元素新增到我們的域中：無限列表就是其近似序列。當然，任何無限列表，比如 ones，都可以簡明地描述為

ones = 1 : 1 : 1 : 1 : ...

這僅僅意味著

ones = (⊥ $\sqsubseteq$ 1:⊥ $\sqsubseteq$ 1:1:⊥ $\sqsubseteq$ ...)

練習
當然，除了 ones 之外，還有更多有趣的無限列表。你能在 Haskell 中寫出遞迴定義嗎？ 自然數 nats = 1:2:3:4:... 迴圈 cycle123 = 1:2:3: 1:2:3 : ... 看看 Prelude 函式 repeat 和 iterate，並嘗試藉助它們來解決前面的練習。 使用文字中的示例來找到表示式 drop 3 nats 表示的值。 假設在嚴格環境中工作，即 [Integer] 的域是扁平的。域是什麼樣的？無限列表呢？ones 表示什麼值？

那麼計算機如何用無限列表進行計算呢？畢竟這需要無限的時間？好吧，這是真的。但訣竅在於，如果計算機只考慮無限列表的有限部分，它可能在有限的時間內完成。所以，無限列表應該被認為是潛在的無限列表。一般來說，中間結果的形式是無限列表，而最終值是有限的。語義解釋的優點之一是可以將中間無限資料結構視為真正無限的，以便在推理程式正確性時可以這樣做。

練習
為了演示無限列表作為中間結果的用法，請證明 take 3 (map (+1) nats) = take 3 (tail nats) 首先計算與 map (+1) nats 相對應的無限序列。 當然，我們應該舉一個最終結果確實需要無限時間的例子。那麼 filter (< 5) nats 表示什麼？ 有時，可以在前面的練習中用 takeWhile 代替 filter。為什麼只有有時，以及如果這樣做會發生什麼？

最後要注意的是，遞迴域的構造可以透過類似於函式遞迴定義的不動點迭代來完成。然而，必須明確解決無限鏈的問題。有關形式構造，請參見外部連結中的文獻。

Haskell 特性：嚴格性註釋和 Newtypes

Haskell 提供了一種方法來更改資料型別建構函式的預設非嚴格行為，即透過嚴格性註釋。在像

data Maybe' a = Just' !a | Nothing'

這樣的資料宣告中，建構函式引數前面的感嘆號 ! 指定它應該對這個引數嚴格。因此，在我們的例子中，我們有 Just' ⊥ = ⊥。更多資訊可以在嚴格性章節中找到。

在某些情況下，人們想要重新命名資料型別，例如

data Couldbe a = Couldbe (Maybe a)

但是，Couldbe a 包含 ⊥ 和 Couldbe ⊥ 兩個元素。藉助 newtype 定義

newtype Couldbe a = Couldbe (Maybe a)

我們可以安排 Couldbe a 在語義上等同於 Maybe a，但在型別檢查時不同。特別是，建構函式 Couldbe 是嚴格的。然而，這個定義與

data Couldbe' a = Couldbe' !(Maybe a)

略有不同。為了解釋其中的區別，請考慮函式

f  (Couldbe  m) = 42
f' (Couldbe' m) = 42

這裡，f' ⊥ 將導致對建構函式 Couldbe' 的模式匹配失敗，導致 f' ⊥ = ⊥。但對於 newtype，對 Couldbe 的匹配永遠不會失敗，我們會得到 f ⊥ = 42。從某種意義上說，這種差異可以表述為

• 對於嚴格情況，Couldbe' ⊥ 是 ⊥ 的同義詞
• 對於 newtype，⊥ 是 Couldbe ⊥ 的同義詞

並約定對 ⊥ 的模式匹配會失敗，而對 Constructor ⊥ 的匹配不會失敗。

Newtypes 也可用於定義遞迴型別。一個例子是列表型別 [a] 的備用定義

 newtype List a = In (Maybe (a, List a))

同樣，重點是建構函式 In 不會引入額外的提升，帶有 ⊥。

以下是一些更多示例，用於區分 newtype 與非嚴格和嚴格的 data 宣告 (在互動式提示符中)

 Prelude> data D = D Int
 Prelude> data SD = SD !Int
 Prelude> newtype NT = NT Int
 Prelude> (\(D _) -> 42) (D undefined)
 42
 Prelude> (\(SD _) -> 42) (SD undefined)
 *** Exception: Prelude.undefined
 [...]
 Prelude> (\(NT _) -> 42) (NT undefined)
 42
 Prelude> (\(D _) -> 42) undefined
 *** Exception: Prelude.undefined
 [...]
 Prelude> (\(SD _) -> 42) undefined
 *** Exception: Prelude.undefined
 [...]
 Prelude> (\(NT _) -> 42) undefined
 42

其他選定主題

抽象解釋和嚴格性分析

由於惰性求值意味著恆定的計算開銷，Haskell 編譯器可能希望發現根本不需要固有非嚴格性的位置，這使其能夠在這些特定位置刪除開銷。為此，編譯器執行 **嚴格性分析**，就像我們在某些函式中證明為嚴格一樣，參見部分 嚴格函式。當然，嚴格性細節取決於引數的精確值，例如我們示例中的 cond，不在討論範圍之內（這通常是不可判定的）。但編譯器可能會嘗試查詢近似的嚴格性資訊，這在許多常見情況下都有效，例如 power2。

現在，**抽象解釋** 是一個強大的思想，用於推理嚴格性：...

有關嚴格性分析的更多資訊，請參閱 Haskell wiki 上關於嚴格性分析的研究論文。

冪集解釋

到目前為止，我們已經透過指定其屬性抽象地介紹了 ⊥ 和語義近似順序 $\sqsubseteq$。然而，無論是 ⊥ 還是任何資料型別的成員，例如 Just ⊥，都可以解釋為普通集合。這被稱為 **冪集構造**。

注意：我不確定這是否真的正確。知道的人請更正。

我對更正的可能更正如下，您對底部的表示不是冪集，它只是一個集合，這導致了我的更正。閱讀更多之後，我不得不撤回更正，但我懷疑在第一個示例中 undefined = { {}, {()} }，我不確定它在 Haskell 表示法中是否有任何意義，所以我想稱之為 ⊥ 應該是正確的。 原始更正：這是不正確的，考慮 ()，它會導致 undefined = ()，這在 Haskell 中是不正確的。 {()} \ \ ⊥ = {()} 此外 {Just True} {Just False} \ / \ / {Nothing} {Just True, Just False} \ / \ / ⊥ = {Nothing, Just True, Just False} 排除 Just ⊥ 但也許如果我們能說 data powerset Writer a b = Writer a b 並得到 ∀x y.Writer x y / \ / \ ∀x.Writer x ⊥ ∀y.Writer ⊥ y \ / \ / Writer ⊥ ⊥ 其中 undefined = Writer ⊥ ⊥ 是最不確定的成員。

這個想法是將 ⊥ 視為 *所有可能值的集合*，並且計算透過選擇子集來檢索更多資訊。從某種意義上說，值的指代從所有值的集合開始，這些集合將透過計算進行縮減，直到只剩下一個包含單個元素的集合。

舉個例子，考慮 Bool，其中域看起來像

{True}  {False}
   \      /
    \    /
   ⊥ = {True, False}

值 True 和 False 被編碼為單例集合 {True} 和 {False}，而 ⊥ 是所有可能值的集合。

另一個例子是 Maybe Bool

 {Just True}   {Just False}
         \     /
          \   /
{Nothing} {Just True, Just False}
     \      /
      \    /
 ⊥ = {Nothing, Just True, Just False}

我們看到語義近似順序等效於集合包含，但引數已切換

$x\sqsubseteq y\iff x\supseteq y$

這種方法可以用於為 Haskell 中的異常提供語義 。

樸素集合不適合遞迴資料型別

在部分 選擇什麼作為語義域？ 中，我們認為將簡單集合作為型別的指代對於偏函式來說效果不佳。在遞迴資料型別的背景下，情況變得更糟，正如 John C. Reynolds 在其論文 *多型性不是集合論的* 中所表明的那樣。

Reynolds 實際上考慮了遞迴型別

newtype U = In ((U -> Bool) -> Bool)

將 Bool 解釋為集合 {True,False}，並將函式型別 A -> B 解釋為從 A 到 B 的函式集合，型別 U 不能表示集合。這是因為 (A -> Bool) 是 A 的子集集合（冪集），由於類似於 Cantor 的論證的對角論證，即存在比自然數更多的實數，它總是比 A 具有更大的基數。因此，(U -> Bool) -> Bool 具有比 U 更大的基數，並且它沒有辦法與 U 同構。因此，集合 U 不應該存在，這是一個矛盾。

在我們的偏函式世界中，這個論證失敗了。在這裡，U 的一個元素由從域序列中提取的一系列近似值給出

⊥, (⊥ -> Bool) -> Bool, (((⊥ -> Bool) -> Bool) -> Bool) -> Bool 等等

其中 ⊥ 表示具有單個成員 ⊥ 的域。雖然本文作者坦率地說不知道這樣的東西應該意味著什麼，但建構函式為 U 給出了一個完全定義良好的物件。我們看到型別 (U -> Bool) -> Bool 僅僅包含移位的近似序列，這意味著它與 U 同構。

最後一點，Reynolds 實際上在二階多型 lambda 演算中構造了 U 的等效項。在那裡，恰好所有項都具有正規化，即當我們不包含原始遞迴運算子 fix :: (a -> a) -> a 時，只存在總函式。因此，對於偏函式和 ⊥，沒有真正的需要，然而，樸素的集合論語義失敗了。我們只能推測這與並非所有數學函式都是可計算的事實有關。特別是，可計算函式的集合 Nat -> Bool 不應該具有比 Nat 更大的基數。

外部連結

關於語義學的線上書籍

• Schmidt, David A. (1986). 語義學。語言開發的方法論. Allyn and Bacon.