Haskell/Denotational 語義

介紹

本章解釋瞭如何將 Haskell 程式的含義形式化，即Denotational 語義。從形式上指定程式 square x = x*x 與將每個數字對映到其平方的數學平方函式相同，這似乎是吹毛求疵，但像 f x = f (x+1) 這樣無限迴圈的程式的含義呢？在以下內容中，我們將舉例說明 Scott 和 Strachey 最初提出的方法，並獲得一個基礎，可以用來推理功能程式的正確性，尤其是遞迴定義的正確性。當然，我們將專注於理解 Haskell 程式所需的那些主題。^[1]

本章的另一個目的是說明嚴格和惰性的概念，這些概念反映了函式是否需要或不需要計算其引數。這是預測 Haskell 程式評估過程的基本要素，因此對程式設計師至關重要。有趣的是，這些概念可以用 Denotational 語義單獨簡潔地表達，不需要參考執行模型。它們將在 圖約簡 中得到很好的利用，但本章將使讀者熟悉 Denotational 定義和涉及的概念，如 ⊥（“底部”）。只對嚴格性感興趣的讀者可能希望瀏覽 底部和偏函式 部分，並快速前往 嚴格和非嚴格語義 部分。

什麼是 Denotational 語義，它有什麼用？

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

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

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

denotations 是組合的，即程式 1+9 的含義只取決於其組成部分的含義

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

同樣的符號也用於型別，即

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

為了簡化，在後續章節中我們將默默地將表示式與其語義物件識別起來，並且只在需要澄清時使用這種符號。

Haskell 等純粹函式式語言的關鍵特性之一是，像“1+9 表示 10”這樣的直接數學解釋也適用於函式：本質上，型別為 Integer -> Integer 的程式的語義是一個數學函式$\mathbb {Z} \to \mathbb {Z}$，在整數之間。雖然我們將看到這個表示式通常需要細化，以包括非終止，但對於命令式語言來說情況明顯更糟：具有該型別的過程表示會以可能意想不到的方式改變機器狀態的東西。命令式語言與操作語義緊密相連，操作語義描述了它們在機器上的執行方式。可以為命令式程式定義一個語義解釋，並使用它來推理這些程式，但語義通常具有操作性質，有時必須擴充套件與函式式語言的語義解釋相比。 相反，純粹函式式語言的含義預設情況下完全獨立於它們的執行方式。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，而右手邊的$\bot$ 的型別是 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$。

練習
整數在順序 $\leq$ 方面是否形成偏序集？

我們可以透過以下圖形描述型別 Integer 的值上的順序 $\sqsubseteq$

其中，兩個節點之間的每條連線都指定了上方的節點比下方的節點更精確。因為只有一個層次（不包括 $\bot$），因此可以說 Integer 是一個扁平域。此圖還解釋了 $\bot$ 的名稱：它被稱為底部，因為它的位置始終在最底部。

單調性

我們對偏函式的直覺現在可以表述為：每個偏函式 $f$ 都是偏序集之間的單調對映。更精確的自變數將產生更精確的值

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

特別是，一個具有 $h(\bot )=1$ 的單調函式 $h$ 是常數：對於所有 $n$，$h(n)=1$。請注意，這裡至關重要的是 $1\sqsubseteq 2$ 等關係不成立。

翻譯成 Haskell，單調性意味著我們不能使用 $\bot$ 作為條件，即我們不能對 $\bot$ 或其等效項 undefined 進行模式匹配。否則，上述示例 $g$ 可以用 Haskell 程式表示。正如我們將在後面看到，$\bot$ 還表示非終止程式，因此無法在 Haskell 中觀察到 $\bot$ 與停機問題有關。

當然，更精確的概念可以透過說一個函式在所有可能的自變數上都比另一個函式更精確，從而擴充套件到偏函式。

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

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

遞迴定義作為不動點迭代

階乘函式的近似值

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

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

雖然我們看到直接將這個遞迴函式解釋為集合描述可能會導致問題，但我們直覺地知道，為了計算對於每個給定的 $n$ 的 $f(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 是否真的對所有引數都是未定義的。

收斂

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

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

如果對於語義近似順序情況也是如此，我們可以明確地確定近似階乘函式的單調函式序列確實有一個極限。對於我們的指稱語義，我們將只遇到具有最小元素 $\bot$ 的 dcpo，它們被稱為 **完備偏序集** (**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 也應該不會停止。^[3] 它表明，人們可以自由選擇這種或另一種函數語言程式設計語言的設計。人們稱語言為嚴格或非嚴格，具體取決於函式預設情況下是嚴格還是非嚴格。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 也是如此。顯然，cond 如果 x 和 y 都是 ⊥，則肯定為 ⊥，但如果它們中至少有一個是定義的，則不一定為 ⊥。這種行為稱為聯合嚴格性。

顯然，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 時會評估兩個分支，這使得它幾乎沒有用。這讓我們瞭解了非嚴格性比嚴格性為程式碼重用提供更多靈活性的普遍觀察結果。有關此主題的更多資訊，請參閱惰性 ^[4] 一章。

代數資料型別

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

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

建構函式

讓我們以示例型別為例

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

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

請記住，⊥ 作為最小元素新增到值 True 和 False 的集合中，我們說該型別是提升 ^[5] 的。其偏序圖只包含一個級別的域稱為扁平域。我們已經知道 $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 中是嚴格的。請注意，雖然萬用字元是 non-strictness 的一個普遍標誌，但這取決於它們相對於建構函式模式匹配的位置。

練習
對邏輯 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 語言定義 中，詳細介紹了 模式匹配的語義，現在你應該能夠理解它。所以繼續看看吧！ 考慮一個帶有兩個 Boolean 引數的函式 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 表示什麼？ 在前面的練習中，有時可以將 filter 替換為 takeWhile。為什麼只有有時可以，如果這樣做會發生什麼？

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

Haskell 特性：嚴格性註釋和新型別

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 ⊥ 的匹配不會失敗。

Newtype 也可用於定義遞迴型別。例如，列表型別 [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 實際上在二階多型 λ 演算中構造了 U 的等價物。在那裡，所有項都具有正規化，即當我們不包含原始遞迴運算子 fix :: (a -> a) -> a 時，只存在總函式。因此，實際上不需要偏函式和 ⊥，但樸素的集合論語義失敗了。我們只能推測這與並非所有數學函式都是可計算的這一事實有關。特別是，可計算函式的集合 Nat -> Bool 的基數不應該大於 Nat。

外部連結

關於語義學的線上書籍

• Schmidt, David A. (1986). 語義學。一種語言開發方法. Allyn 和 Bacon。