函數式程式設計:型別與語意 Types and Semantics

完整中文教學筆記 — Week 7

課程來源:5CCS2PLD — Programming Language Design Paradigms,King's College London
講者:Dr. Odinaldo Rodrigues / Prof. Maribel Fernández
對應講義:Week7_TYPES_AND_SEMANTICS.pdf(共 84 頁,4 小節:7.1–7.4)

本份教材以「先理解、再形式化、再實作」的順序,把講義中的所有定義、規則、範例、練習以中文重新整理,並補上必要的脈絡與證明細節。

本講總覽:從型別到語意,我們到底在學什麼?
Part 7.1 — 型別系統導論 (Introduction to Types) - 1.1 什麼是型別 (Typing)? - 1.2 靜態型別 vs 動態型別 - 1.3 Haskell 的型別概觀 - 1.4 多型 (Polymorphism) - 1.5 重載 (Overloading) 與型別類別 (Type Classes) - 1.6 型別推論 (Type Inference)
Part 7.2 — Lists 與使用者定義型別 - 2.1 Linked Lists 的型別與構造子 - 2.2 Pattern Matching 與 List 函數 - 2.3 使用者定義型別 (data declarations) - 2.4 結構歸納法 (Structural Induction)
Part 7.3 — 函數式語意導論:SFUN 語言 - 3.1 為什麼需要形式語意? - 3.2 SFUN 的語法 (Syntax) - 3.3 SFUN 程式 (Programs) - 3.4 Call-by-value 大步操作語意 - 3.5 推導樹範例與練習 - 3.6 標準形唯一性 (Determinism / Unicity of Normal Forms)
Part 7.4 — Call-by-name、型別與 Typing - 4.1 Call-by-value 的問題 - 4.2 Call-by-name 求值 - 4.3 SFUN 的型別 (Types) - 4.4 Typing 規則:良型項 (Well-typed Terms) - 4.5 Typing 一個 SFUN 程式 - 4.6 用歸納法證明 SFUN 程式的性質
全部練習題與詳解
重點摘要與考試提示
參考資料

0. 本講總覽:從型別到語意,我們到底在學什麼?

這個 Week 7 是整門課從 語法 (syntax) 過渡到 語意 (semantics) 的關鍵章節,主軸有兩個:

型別系統 (Type System):在 執行之前,我們如何用一套規則檢查「這個程式表達式是否合法」?以 Haskell 風格的多型型別系統為主要範例。
操作語意 (Operational Semantics):在 執行時,程式要怎麼「一步步」算出最終值?以一個迷你的函數式語言 SFUN 作為形式化對象,給出 call-by-value 與 call-by-name 兩種大步語意 (big-step)。

章節	主題	對應的形式工具	對應的 Haskell 概念
7.1	型別、多型、型別推論	型別變數、最一般型別、unification	`(.) :: (b->c)->(a->b)->(a->c)` 等
7.2	Lists、使用者定義型別、結構歸納法	歸納定義的資料型別	`data Tree a = Leaf a \| Branch ...`
7.3	操作語意基礎、SFUN、CBV	大步推導規則	函數呼叫的求值順序
7.4	Call-by-name、Typing 規則	環境、判斷式 Γ ⊢ε t : τ	Haskell lazy evaluation 的原型

學習提示:7.1 與 7.2 比較像「使用者觀點」,著重看你會不會在 Haskell 寫程式;7.3 與 7.4 比較像「設計者觀點」,要求你能像編譯器那樣形式化地推導。期末/考試容易考的就是 CBV / CBN 的推導樹 與 typing derivation tree。

Part 7.1 — 型別系統導論 (Introduction to Types)

1.1 什麼是型別 (Typing)?

核心定義:型別 (type) 把所有合法的「值 (values)」分類成一個個集合,每個型別會綁定一組可在其上施行的運算 (operations)。

例如:

Int 是整數的型別,可以做 + - * /,但不能對它呼叫 not。
Bool 是真假值的型別,可以做 && || not,但不能對它做 +。

為什麼需要型別?

抓錯誤:像 1 + True 這種表達式雖然語法上看起來像合法字串,但語意上完全不合理。型別系統可以在 程式執行前 把這種錯誤攔下來。
型別 = 一種輕量的規格 (specification):當你看到 length :: [a] -> Int,不用看實作就大概知道它做什麼。
編譯器最佳化:有了型別資訊,編譯器可以選用更有效率的機器表示。

型別可以怎麼來?

顯式 (explicit):程式設計師自己標註 — 像 C++ 中的 void wait(string message) { ... }。
隱式 (implicit / inferred):由型別系統自動推論 — 像 Haskell 通常不需要寫型別標註,GHC 會自動推出。

// 講義中的 C++ 範例:型別「string」是顯式給定的
void wait (string message) {
    cout << message << endl;
    cout << "Press ENTER to continue..." << flush;
    cin.ignore (100, '\n');
}

1.2 靜態型別 vs 動態型別

「檢查型別是否被正確使用」這件事,可以發生在兩個不同的時機:

種類	何時檢查	代表語言
靜態型別 (static typing)	編譯時	C, C++, Java, Haskell
動態型別 (dynamic typing)	執行時	Python, JavaScript, PHP

靜態型別的特性

規則:每個合法的表達式都「必須」有一個型別。沒辦法被指派型別的表達式會被編譯器拒絕,完全不會被執行。

優點:

早期偵測錯誤:許多 bug 在編譯期就被擋下,不必等到執行才炸。
規格作用:型別本身就是一種輕量的形式化規格。

重要提醒:通過型別檢查 並不保證 程式行為正確!它只保證「執行時不會發生型別錯誤」(沒有 type error at runtime)。例如 head [] 在 Haskell 仍會在執行期 crash,但那是因為 head 對空 list 沒有定義,不是型別錯誤。

1.3 Haskell 的型別概觀

Haskell 預設提供以下型別,並允許使用者自訂新型別:

基本資料型別 (Basic data types)

Bool:布林值
Char:字元
Int:固定寬度整數 (通常 64-bit)
Integer:任意精度整數 (大整數)
Float、Double:浮點數

構造型別 (Constructed types)

元組 (tuples):(Int, Bool) 表「整數與布林的對」
List:[Integer] 表「任意精度整數的 list」
String:其實就是 [Char],字元的 list

函數型別 (Function types)

Char -> Bool          -- 從字元到布林的函數
(Int -> Int) -> Int   -- 接收「Int 函數」並回傳 Int

⚠ 關鍵語法規則:箭號型別構造子 -> 是 右結合 (right-associative) 的!也就是

Int -> Int -> Int 等同於 Int -> (Int -> Int),而非 (Int -> Int) -> Int。

這正是 currying (柯里化) 的形式表現:一個「兩個 Int 給出一個 Int」的函數,實際上是「拿一個 Int,回傳一個 Int → Int 的函數」。

1.4 多型 (Polymorphism)

單型 (monomorphic) 系統:每個表達式最多只有一個型別。
多型 (polymorphic) 系統:有些表達式可以有多個型別。

1.4.1 經典範例:函數合成

(.) :: (b -> c) -> (a -> b) -> (a -> c)

這裡 a, b, c 都是 型別變數 (type variables),代表「任意型別」。(.) 的意思是:「給我兩個函數 g :: b -> c 與 f :: a -> b,我幫你算出合成 g . f :: a -> c。」

1.4.2 多型型別的形式化文法

講義給出的型別文法:

V ::= a | b | c | …                            (型別變數)
C ::= Int | Bool | Char | (->) | [] | () | …    (型別構造子)
T ::= V | C(T₁, T₂, …, Tₙ)                      (型別)

也就是說,一個型別就是「型別變數」或「以型別構造子作用在其他型別上」。C 可以是:

原子 (atomic):Int、Bool、Char 等(0 個參數)
帶參數:->(2 個參數,寫成 T₁ -> T₂)、[](1 個參數,寫成 [T])、(,)(寫成 (T₁, T₂))

多型型別的語意:一個多型型別代表「它所有 實例 (instance) 的集合」。把型別變數代換 (substitution) 成具體型別,就得到一個實例。

例如 (.) :: (b -> c) -> (a -> b) -> (a -> c) 的一個實例是 (Int -> Int) -> (Int -> Int) -> (Int -> Int)(把 a, b, c 全代成 Int)。

1.4.3 與 C++ template 的比較

C++ 也有型別變數的概念,只是寫成 template<typename A, typename B>:

template<typename A, typename B>
pair<B,A> flip_pair(const pair<A,B> &p) {
    return pair<B,A>(p.second, p.first);
}

觀念差異:

C++ template 是 編譯時程式碼產生 (code generation):每出現一個新的型別組合,編譯器就生成一份特化版本。

Haskell 的多型是 參數化的 (parametric):同一份函數定義可以對所有型別共用,因為函數行為與型別無關。

1.4.4 多型實例化 (Instantiation) 的範例

考慮兩個函數:

square :: Integer -> Integer
sqrt   :: Integer -> Float

合成 quad = square . square:

(.) 在這裡被實例化為:
(.) :: (Integer -> Integer)        -- b -> c, 把 b=c=Integer
    -> (Integer -> Integer)        -- a -> b, 把 a=Integer
    -> (Integer -> Integer)
所以 quad :: Integer -> Integer

合成 sqrt . square:

(.) 在這裡被實例化為:
(.) :: (Integer -> Float)          -- b -> c, b=Integer, c=Float
    -> (Integer -> Integer)        -- a -> b, a=Integer
    -> (Integer -> Float)
所以 sqrt . square :: Integer -> Float

觀念:同一個 (.) 函數,在不同的使用脈絡會被「實例化」成不同的具體型別。

1.4.5 另一個多型範例:`error`

error :: String -> a

error 拿一個字串,然後…回傳「任何型別」。為什麼?因為它根本不會回傳任何東西!它的作用是 中止執行 並印出訊息。所以無論在哪個位置用它,型別都「自動配合」。

fact :: Integer -> Integer
fact n
  | n > 0  = n * fact (n - 1)
  | n == 0 = 1
  | n < 0  = error "negative argument"   -- 這裡 error 被當成 String -> Integer

1.5 重載 (Overloading) 與型別類別 (Type Classes)

1.5.1 什麼是重載?

重載 (overloading),又稱 特設多型 (ad-hoc polymorphism):同一個函數名/運算子,因應不同型別有不同的「實作」。

例如 + 在不同型別下是不同的機器運算:

整數加法:整數電路
浮點加法:浮點電路
字串連接:在某些語言裡也用 +

1.5.2 為什麼純多型不夠用?

對 + 你可能會想寫:

(+) :: a -> a -> a

但這「太一般」了!它會允許 'a' + 'b'(把字元相加),這是不合理的。

1.5.3 三種解法

講義列出三種常見對策:

(1) 不同型別用不同名字

OCaml:整數用 +、浮點用 +.、字串用 ^。
Haskell:整數除法用 div,實數除法用 /。

缺點:符號暴增,程式不直觀。

(2) 型別交集 (intersection types)

(+) :: (Integer -> Integer -> Integer)
     ∧ (Float   -> Float   -> Float)

意思是 + 同時具備兩種型別。但這種「交集型別」會讓型別系統變得非常複雜。

(3) 型別類別 (Type Classes) — Haskell 的選擇 ✅

(+) :: Num a => a -> a -> a

讀作:「對於任何 a,只要 a 是 Num 類別的成員,+ 就有型別 a -> a -> a。」

Num a => 部分稱為 型別約束 (type class constraint)。
Num 是一個 型別類別,集合了所有「可以做加減乘除」的型別。Int、Integer、Float、Double 都是 Num 的實例 (instance)。
Char 不是 Num 的實例,所以 'a' + 'b' 會被型別系統擋下。

記憶法:=> 左邊是「條件 (constraints)」,右邊是「型別 (type)」。Haskell 的多型是「參數多型 + 約束 (constrained polymorphism)」的混合體,理論上稱為 bounded parametric polymorphism。

1.6 型別推論 (Type Inference)

核心想法:程式設計師不必自己標註型別;編譯器會根據表達式的構造,推出 最一般 (most general) 的型別。如果推不出來,就拒絕該程式。

1.6.1 推論的工作機制

表達式的型別由其 組成元件 (components) 決定。
元件如何被組合在一起,決定了型別變數必須滿足的 約束 (constraints)。
用 單元化 (unification) 演算法解這些約束:解得出 → 推論成功;解不出 → 表達式無法被型別化 (untypeable)。

1.6.2 推論範例 1:`square` 的初步推論

考慮:

square x = x * x

步驟:

square 是個函數,所以最一般的型別 初始假設 為 a -> b(一個輸入型別 a,一個輸出型別 b)。
由定義 square x = x * x:x :: a 而 x * x :: b。
已知 (*) :: Int -> Int -> Int(假設這是唯一的 *)。
所以 x :: Int 且 x * x :: Int。
因此 a = Int、b = Int。

結論:square :: Int -> Int。

1.6.3 推論範例 2:更一般的 `square`

如果我們把 (*) 看成「對所有 Num c 都可用」:

(*) :: Num c => c -> c -> c

那麼上面的推論變成:

x :: a,且 x :: Num c => c,所以 a = c(在 Num 約束下)。
x * x :: Num c => c,所以 b = c(同樣在 Num 約束下)。

結論:square :: Num c => c -> c。

觀念:型別變數的「最一般化 (generalisation)」是 Hindley-Milner 型別系統的核心步驟。Haskell 的編譯器會盡量保留越多型別變數,讓程式越通用越好。

1.6.4 推論範例 3:推論失敗的例子

假設 square :: Int -> Int,我們嘗試推論:

square square 3

注意:函數應用是 左結合 (left-associative),所以這個式子讀作 (square square) 3。

推論:

square 期望輸入型別 Int。
但這裡傳給它的卻是另一個 square :: Int -> Int。
產生約束 Int = (Int -> Int),這個約束 無法被解 (因為 Int 不是函數型別)。

結論:表達式無法被型別化 (untypeable),編譯器報錯。

練習提醒:期末考非常常考「給定型別,問下列表達式可不可以被型別化」。重點是

應用左結合

一旦約束矛盾就拒絕

Part 7.2 — Lists 與使用者定義型別

2.1 Linked Lists 的型別與構造子

在大多數函數式語言中,linked list (鏈結串列) 是最重要的內建型別之一。Haskell 提供四個基本操作:

函數	型別	意義
`[]`	`[a]`	空 list
`(:)`	`a -> [a] -> [a]`	在 list 前面加一個元素(讀作 "cons")
`head`	`[a] -> a`	取非空 list 的第一個元素
`tail`	`[a] -> [a]`	取非空 list 的剩餘部分

這四個合稱「list 的構造子與選擇子」。值得注意的是,所有 list 其實都是用 (:) 與 [] 一個個拼出來的:

1 : 2 : 3 : []      -- 完整的構造形式
[1, 2, 3]           -- Haskell 的語法糖,等價於上式

範例

[]                                  :: [a]
(1 : 2 : [])                        :: [Int]    -- 也可寫 [1,2]
['c', 'a', 't']                     :: [Char]   -- 等同於 "cat"
[3.0, 3.1, 3.14, 3.141, 3.1415]     :: [Double]
[[True, False], [True]]             :: [[Bool]]

重要事實:Haskell 的字串其實就是 [Char]!所以

haskell "cat" == ['c','a','t'] -- True "cat" == 'c' : ['a','t'] -- True

2.2 Pattern Matching 與 List 函數

規則:對於任何「歸納定義」的型別(例如 list、自然數、樹),最自然的寫函數方式就是 pattern matching:對每一個構造子各寫一條方程式。

範例:list 的長度 `size`

size :: [a] -> Int
size []        = 0
size (x : xs)  = 1 + size xs

第一行對應 [] 構造子:空 list 的長度是 0。
第二行對應 (:) 構造子:x 是 head、xs 是 tail,長度等於「1 + tail 的長度」。

求值範例:

size [1, 6, 1, 8, 0]
→ 1 + size [6, 1, 8, 0]
→ 1 + (1 + size [1, 8, 0])
→ 1 + (1 + (1 + size [8, 0]))
→ 1 + (1 + (1 + (1 + size [0])))
→ 1 + (1 + (1 + (1 + (1 + size []))))
→ 1 + (1 + (1 + (1 + (1 + 0))))
→ 5

練習 1:`elem'` — 檢查元素是否在 list 中

題目:寫一個函數 elem' x l,檢查 x 是否出現在 list l 中。型別是什麼?

解答:

elem' :: Eq a => a -> [a] -> Bool
elem' _ []       = False
elem' x (y : ys) = (x == y) || elem' x ys

空 list:x 一定不在 → False。
非空 list:看看 x 是不是 head;否則遞迴往下找。
因為要用 (==),所以型別需要 Eq a 約束。

練習 2:`take'` — 取前 `n` 個元素

題目:寫 take' n l,回傳 list l 的前 n 個元素。

講義範例解答:

take' :: Int -> [a] -> [a]
take' 0 _        = []
take' _ []       = []
take' n (x : xs) = x : take' (n - 1) xs

第 1 行:不管 list,只要 n = 0,回傳空 list。
第 2 行:不管 n,只要 list 是空的,回傳空 list。
第 3 行:把 head 留下,然後遞迴處理 tail,要的個數變成 n - 1。

小細節:第 1、2 行的順序很重要 — Haskell 從上往下匹配,所以 take' 0 [] 會匹配第一條(回傳 []),這是正確行為。

2.3 使用者定義型別 (data declarations)

語法:data 型別名 [型別參數] = 構造子1 args | 構造子2 args | …

每個構造子是一個「資料構造子 (data constructor)」,用來建造該型別的值。

範例 1:自然數 (Natural numbers)

data Nat = Zero | Succ Nat

Nat 是新型別。
Zero 與 Succ 是它的兩個資料構造子:
Zero :: Nat
Succ :: Nat -> Nat

由此可以建造各種值:

Zero                    :: Nat   -- 對應數字 0
Succ Zero               :: Nat   -- 對應數字 1
Succ (Succ Zero)        :: Nat   -- 對應數字 2
Succ (Succ (Succ Zero)) :: Nat   -- 對應數字 3

這就是 Peano 自然數。

範例 2:多型遞迴型別 — `Seq a`

data Seq a = Empty | Cons a (Seq a)

Seq 是 型別構造子 (type constructor):它本身不是型別,而是「拿一個型別 a 給出一個型別 Seq a」。
Empty 與 Cons 是資料構造子:
Empty :: Seq a
Cons :: a -> Seq a -> Seq a

觀念:這其實就是內建 list 的雛型!Empty 對應 []、Cons 對應 (:)。

可建造的值:

Empty                              :: Seq a
Cons (Succ Zero) Empty             :: Seq Nat       -- 含一個 Nat
Cons True (Cons False Empty)       :: Seq Bool      -- 含兩個 Bool

在資料構造子上做 Pattern Matching

isempty :: Seq a -> Bool
isempty Empty      = True
isempty (Cons _ _) = False

重點區別:

型別構造子 (type constructor):出現在「型別層級」,例如 []、Seq、Maybe、Tree。

資料構造子 (data constructor):出現在「值層級」,例如 []、(:)、Empty、Cons、Just、Nothing。

注意 [] 在兩個層級都會出現:它既是空 list 的資料構造子,也是 list 的型別構造子!

練習:二元樹 (Binary Tree)

題目:

定義 Tree a 表示「資料只存在葉子」的二元樹。用 Leaf 和 Branch 兩個構造子。

構造一棵樹:左子樹是 Leaf 1,右子樹是 Branch (Leaf 2) (Leaf 3)。

寫 height t,葉子高度為 1。

height 的型別?

解答:

-- (1) 型別定義
data Tree a = Leaf a | Branch (Tree a) (Tree a)

-- (2) 範例樹
exampleTree :: Tree Int
exampleTree = Branch (Leaf 1) (Branch (Leaf 2) (Leaf 3))

-- (3) 計算高度
height :: Tree a -> Int
height (Leaf _)     = 1
height (Branch l r) = 1 + max (height l) (height r)
  where
    max x y = if x > y then x else y

驗算:

height exampleTree
= height (Branch (Leaf 1) (Branch (Leaf 2) (Leaf 3)))
= 1 + max (height (Leaf 1)) (height (Branch (Leaf 2) (Leaf 3)))
= 1 + max 1 (1 + max (height (Leaf 2)) (height (Leaf 3)))
= 1 + max 1 (1 + max 1 1)
= 1 + max 1 (1 + 1)
= 1 + max 1 2
= 1 + 2
= 3   ✓

(4) height :: Tree a -> Int — 不需要約束,因為我們不需要比較 a 的內容,只需走訪結構。

2.4 結構歸納法 (Structural Induction)

核心觀念:對於遞迴定義的型別,我們可以用 結構歸納法 (structural induction) 來證明性質 P 對所有元素成立。歸納的步驟「跟著型別的構造子走」。

對 `Nat` 的結構歸納法

要證明性質 P 對所有 Nat 成立,需:

基底 (base case):證明 P(Zero)。
歸納步驟 (inductive step):假設 P(n) 成立(歸納假設 IH),證明 P(Succ n)。

這就是熟悉的 數學歸納法:

( P(0) ∧ ∀n. ( P(n) ⇒ P(n+1) ) )   ⟺   ∀n. P(n)

範例:`Zero` 是加法的中性元素

定義加法:

add :: Nat -> Nat -> Nat
add Zero     y = y
add (Succ x) y = Succ (add x y)

目標:對所有 n :: Nat,證明 add n Zero = n(也就是 Zero 在右邊也是中性元素)。

證明:用對 n 的結構歸納法。

Base case (n = Zero):

add Zero Zero = Zero         (依 add 第一條方程式)

✓ 成立。

Inductive step:假設 add n Zero = n(歸納假設 IH),證 add (Succ n) Zero = Succ n。

add (Succ n) Zero
= Succ (add n Zero)         (依 add 第二條方程式)
= Succ n                    (依 IH)

✓ 成立。

由結構歸納法,add n Zero = n 對所有 n :: Nat 成立。 ∎

練習:證明 `sumNat n = n(n+1)/2`

題目:給定

haskell sumNat x | x == 0 = 0 | x > 0 = x + sumNat (x - 1) | otherwise = error "Negative argument!"

證明:對所有自然數 n,sumNat n = n(n+1)/2。

證明(數學歸納法,沿著 n 的非負整數結構):

Base case (n = 0):

sumNat 0 = 0      (由定義第一條,因為 0 == 0)
0(0+1)/2 = 0      ✓

Inductive Hypothesis (IH):假設對某 n ≥ 0,sumNat n = n(n+1)/2。

Inductive step:證 sumNat (n+1) = (n+1)(n+2)/2。

由於 n + 1 > 0,符合第二條 guard:

sumNat (n+1)
= (n+1) + sumNat ((n+1) - 1)
= (n+1) + sumNat n
= (n+1) + n(n+1)/2          (用 IH)
= (n+1) * (1 + n/2)
= (n+1) * (2 + n) / 2
= (n+1)(n+2)/2              ✓

由歸納法,結論對所有自然數成立。 ∎

學習要點:結構歸納法是函數式程式設計者「驗證程式正確性」的主要武器。它把對程式的推理變成數學上的證明。

Part 7.3 — 函數式語意導論:SFUN 語言

3.1 為什麼需要形式語意?

到目前為止我們已經知道:

型別系統可以攔下「明顯不合理」的表達式。
pattern matching 與遞迴定義可以寫出函數。

但仍有一個關鍵問題沒解決:

「給定一個表達式,它應該如何被求值 (evaluate)?最終會得到什麼值?」

這就是 語意 (semantics) 要回答的問題。為此,我們需要一個形式化的描述工具 — transition system(轉換系統),透過 structural operational semantics (SOS) 把「表達式如何一步步算出值」精確地寫下來。

我們不在大語言上做這件事(那會太複雜),而是用一個迷你的、純函數式的語言:SFUN。

與 Week 5–6 的 SIMP 對比:SIMP 是命令式的,有 store 和 mutation;SFUN 是純函數式的,只有表達式、函數呼叫、整數與布林值。對 SFUN 而言,「執行」就是「求值表達式」。

3.2 SFUN 的語法 (Syntax)

設:

V:變數集合 {x, y, z, ...}。
F:函數名集合 {f₁, f₂, ...},每個函數 fᵢ 有固定的 arity (引數個數),記為 ⟨fᵢ⟩。

運算子分類:

op  ::= + | - | * | /             (算術運算子)
bop ::= > | < | = | ≤ | ≥          (比較運算子)

項 (terms) 的文法:

t ::= n                            (整數常量, n ∈ ℤ)
    | b                            (布林常量, b ∈ {True, False})
    | x                            (變數)
    | t₁ op t₂                     (算術運算)
    | t₁ bop t₂                    (比較運算)
    | ¬t₁                          (邏輯非)
    | t₁ ∧ t₂                      (邏輯且)
    | if t₀ then t₁ else t₂        (條件式)
    | f(t₁, …, t⟨f⟩)               (函數應用)

重點:

沒有 store、沒有 mutation、沒有 sequence — 這是純函數式!

沒有 lambda — SFUN 是 first-order 函數式語言,函數只能透過 程式中的方程式 來定義,不能在表達式裡臨時定義匿名函數。

if-then-else 是 表達式 (expression),不是 statement — 它必須有值,所以 else 永遠不能省略。

變數與封閉項

用 vars(t) 表示項 t 中出現的所有變數。

範例:

vars(x) = {x}
vars(f(y, z)) = {y, z}
vars(3 + (x * 2)) = {x}

封閉項 (closed term):vars(t) = ∅,也就是 不含任何自由變數 的項。例如 3 + 4 * 2 是封閉的;x + 1 不是。

只有封閉項才能被「求值」— 因為含自由變數的項根本不知道變數的值是什麼。

3.3 SFUN 程式 (Programs)

定義:SFUN 的一個 程式 (program) 是一組 遞迴方程式 (recursive equations):

f₁(x₁, …, x⟨f₁⟩) = d₁ ⋮ fₖ(x₁, …, x⟨fₖ⟩) = dₖ

條件:

每個 dᵢ 是 SFUN 的項。

vars(dᵢ) ⊆ {x₁, …, x⟨fᵢ⟩}(dᵢ 中出現的變數都必須是 fᵢ 的形式參數)。

每個函數名 fᵢ 只能有一條方程式定義。

方程式可以遞迴 — dᵢ 中可以呼叫 f₁, …, fₖ(包括 fᵢ 本身)。

範例程式

max(x, y)              = if x ≥ y then x else y
fact(x)                = if x ≤ 0 then 1 else x * fact(x - 1)

square(x)              = x * x
quadratic(x, a, b, c)  = a * square(x) + b * x + c

mod(x, y)              = if x - y < 0 then x else mod(x - y, y)
even(x)                = mod(x, 2) = 0
collatz(x)             = if x = 1 then 1 else
                         if even(x) then x/2 else 3*x + 1

觀念:SFUN 程式就像一本「定義的辭典」 — 給定一個表達式時,當需要展開 fᵢ 的時候,我們去辭典查 fᵢ 的方程式。

3.4 Call-by-value 大步操作語意

大步語意 (big-step semantics):用單一個推導關係 t ⇓_P v,表示「在程式 P 的脈絡下,項 t 求值得到值 v」。

與「小步語意」(每次只走一步)相對 — 大步直接從表達式 一步到位 跳到最終值。

值 (values):整數 n 或布林 b。

求值規則(call-by-value)

下面是講義給出的 9 條規則(用 ASCII 推導格式)。下標 P 表示「在程式 P 的脈絡下」。

推導樹閱讀法:橫線 ───── 上方是 前提 (premises),下方是 結論 (conclusion),線右邊括號內是 規則名,線右後方的方括號是 側條件 (side condition)。

1. 整數常量 (axiom n)

─────────  (n)
n ⇓_P n

「整數常量已經是值,直接求出自己。」

2. 布林常量 (axiom b)

─────────  (b)
b ⇓_P b

3. 算術運算 (op)

t₁ ⇓_P n₁     t₂ ⇓_P n₂
─────────────────────────  (op)   [若 n₁ op n₂ = n]
      t₁ op t₂ ⇓_P n

「先把兩邊算成整數,再用內建的算術運算算出結果。」

4. 比較運算 (bop)

t₁ ⇓_P n₁     t₂ ⇓_P n₂
─────────────────────────  (bop)  [若 n₁ bop n₂ = b]
      t₁ bop t₂ ⇓_P b

5. 邏輯且 (and)

t₁ ⇓_P b₁     t₂ ⇓_P b₂
─────────────────────────  (and)  [若 b₁ ∧ b₂ = b]
       t₁ ∧ t₂ ⇓_P b

6. 邏輯非 (not)

   t ⇓_P b₁
──────────────  (not)             [若 b = ¬b₁]
  ¬t ⇓_P b

7. 條件式 — true 分支 (ift)

t₀ ⇓_P True     t₁ ⇓_P v₁
─────────────────────────────────  (ift)
if t₀ then t₁ else t₂ ⇓_P v₁

8. 條件式 — false 分支 (iff)

t₀ ⇓_P False    t₂ ⇓_P v₂
─────────────────────────────────  (iff)
if t₀ then t₁ else t₂ ⇓_P v₂

注意:7、8 兩條共同保證了 if 是 short-circuit 的:只有 被選中的那個 分支會被求值。另一個分支即使求值後會 crash 或不停止,也完全不會執行。

9. 函數呼叫 — call-by-value (fnval) ★

t₁ ⇓_P v₁   …   t_⟨fᵢ⟩ ⇓_P v_⟨fᵢ⟩    dᵢ{x₁↦v₁, …, x_⟨fᵢ⟩↦v_⟨fᵢ⟩} ⇓_P v
─────────────────────────────────────────────────────────────────────  (fnval)
                  fᵢ(t₁, …, t_⟨fᵢ⟩) ⇓_P v

(其中程式 P 中有方程式 fᵢ(x₁, …, x⟨fᵢ⟩) = dᵢ。)

語言上的閱讀:呼叫一個函數時:

先把所有引數 tⱼ 都各自求值成值 vⱼ(這就是「先算引數」的 call-by-value)。

再把方程式右側 dᵢ 中的形式參數 xⱼ 代換成對應的值 vⱼ。

最後求值代換後的右側,得到最終答案 v。

記號:d{x₁ ↦ v₁, …, xₙ ↦ vₙ} 表示「在 d 中把所有 xⱼ 同時代換成 vⱼ」。

3.5 推導樹範例與練習

範例 1:`fortytwo(0)` 在 CBV 下的求值

程式:

infinity = infinity + 1
fortytwo(x) = 42
square(x) = x * x

要證:fortytwo(0) ⇓_P 42。

推導樹:

                          ────(n)              ────(n)
                          0 ⇓_P 0              42 ⇓_P 42
                          ──────────────────────────────────(fnval) [因為 42{x ↦ 0} = 42]
                                  fortytwo(0) ⇓_P 42

讀法:fortytwo(0) 用 (fnval) 規則,前提是 (a) 引數 0 ⇓ 0(用 (n) 公理),(b) 42{x↦0} = 42 ⇓ 42(用 (n) 公理)。

範例 2:`fortytwo(infinity)` 在 CBV 下不終止

考慮 fortytwo(infinity)。要套用 (fnval),我們必須先求 infinity ⇓ ?。但:

infinity = infinity + 1

要算 infinity ⇓ ?,要先用 (fnval),而 (fnval) 要先算 infinity + 1 ⇓ ?,而這又要先算 infinity ⇓ ?…無窮遞迴下去,推導樹永遠建不完。

結論:在 CBV 下,fortytwo(infinity) 沒有值(求值不終止),即使 fortytwo 完全用不到引數。這是 CBV 的「缺點」。

範例 3:`square(2 + 1)` 在 CBV 下的求值

                                                       ──(n)   ──(n)
                                                       3 ⇓ 3   3 ⇓ 3
   ──(n)  ──(n)                                        ─────────────(op)
   2 ⇓ 2  1 ⇓ 1                                        (x*x){x↦3} = 3*3 ⇓ 9
   ─────────────(op)                                   ─────────────────────(fnval)
   2 + 1 ⇓ 3                                                       
   ──────────────────────────────────────────────────────────────────────────(fnval)
                              square(2 + 1) ⇓_P 9

關鍵:2 + 1 在 CBV 下先被求成 3,所以後面的 x * x 在代換時只需算 3 * 3,不會重複算 (2+1) * (2+1)。

練習:`max(3, square(2))` 在 CBV 下的推導

解答(CBV):

                                               ──(n)  ──(n)
                                               2 ⇓ 2  2 ⇓ 2
                                               ─────────────(op)
                                               (x*x){x↦2} ⇓ 4
                                               ──────────────(fnval)
                                ──(n)          square(2) ⇓ 4
                                3 ⇓ 3                 ─────────  
                                ──────────────────────────────(bop)
                                3 ≥ 4 ⇓ False
                                ──────────────────────────────────────(iff)
   ──(n)  ──(n)                 if x ≥ y then x else y {x↦3, y↦4} ⇓ 4
   3 ⇓ 3  4 ⇓ 4                  
   ───────────────────────────────────────────────────────────────────(fnval)
                              max(3, square(2)) ⇓_P 4

重要觀察:在 max 開始展開之前,兩個引數都已經被先算成了值 — 第一個 3 ⇓ 3(本身就是值),第二個 square(2) ⇓ 4(整個函數呼叫先求完)。這正是 CBV 的精神。

3.6 標準形唯一性 (Determinism / Unicity of Normal Forms)

定理 (Determinism):對任意封閉項 t,若 t ⇓_P v₁ 且 t ⇓_P v₂,則 v₁ = v₂。

也就是說:同一個項在同一支程式下,如果有值,值就是唯一的。CBV 求值是「決定性 (deterministic)」的。

證明大綱(rule induction)

觀念:這要靠 推導規則的歸納法 (rule induction):對推導 t ⇓ v 的「規則應用」做歸納。

對任意項 t,觀察:對於 t 而言,只有一條規則可以應用(因為規則是按照 t 的最外層結構分案的)。

Base cases (公理):

t = n(整數):只能用 (n) 公理,結果只能是 n。
t = b(布林):只能用 (b) 公理,結果只能是 b。

(沒有變數的 base case,因為 t 是封閉項。)

Inductive cases (規則):

例如 t = fᵢ(t₁, …, t⟨fᵢ⟩),只能用 (fnval)。要建立 fᵢ(t₁, …) ⇓ v,前提是:

t₁ ⇓ v₁, …, t⟨fᵢ⟩ ⇓ v⟨fᵢ⟩
dᵢ{x₁ ↦ v₁, …} ⇓ v

依 歸納假設 (子項目都比 t 結構小):每個 tⱼ 的值唯一,v₁, …, v⟨fᵢ⟩ 因此唯一,從而代換後的右側也唯一,最終 v 也唯一。

其他規則((op)、(bop)、(and)、(not)、(ift)、(iff))的論證完全類似:都是「子項的值唯一 ⟹ 整個項的值唯一」。 ∎

重要意涵:雖然數學上的「函數」總是決定性的,但形式系統 並不自動 是決定性的!例如有些 lambda calculus 變體允許自由地選擇要先 reduce 哪個子項,結果可能不同(雖然 confluence 定理保證最終值一樣)。SFUN + CBV 直接從規則層級就保證了單一性。

Part 7.4 — Call-by-name、型別與 Typing

4.1 Call-by-value 的問題

回顧 CBV 的函數呼叫規則:

t₁ ⇓_P v₁   …   t_⟨f⟩ ⇓_P v_⟨f⟩    dᵢ{xⱼ↦vⱼ} ⇓_P v
───────────────────────────────────────────────────  (fnval)
                fᵢ(t₁, …) ⇓_P v

CBV 強制要求 所有引數都先被求成值。這在以下情況會出問題:

問題 1:不必要的不終止

infinity = infinity + 1
fortytwo(x) = 42

fortytwo(infinity) 在 CBV 下永遠 不終止,因為要先算 infinity。但語意上 — fortytwo 根本不用到 x!如果策略夠「懶」,應該可以直接回傳 42。

問題 2:可能浪費計算

fortytwo(2³⁵⁴²) — 計算 2^3542 是個天文數字,但 fortytwo 用不到它,白算。

解法:改用 call-by-name 求值策略。

4.2 Call-by-name 求值

核心改變:不要先求引數,直接把 引數的表達式本身 代換進函數體!

只需把 (fnval) 換成下列 (fnname) 規則:

9'. 函數呼叫 — call-by-name (fnname) ★

dᵢ{x₁↦t₁, …, x_⟨fᵢ⟩↦t_⟨fᵢ⟩} ⇓_P v
─────────────────────────────────  (fnname)
   fᵢ(t₁, …, t_⟨fᵢ⟩) ⇓_P v

注意:沒有要求 tⱼ ⇓ vⱼ!直接把 tⱼ(項本身) 代換到 dᵢ 中。

直觀:CBN 是「按需求值 (on-demand)」 — 只有當函數體 真的用到 該引數時,才會去算它。如果沒用到,就根本不算。

CBN 仍然 deterministic

定理:CBN 系統依然滿足 t ⇓_P v₁ ∧ t ⇓_P v₂ ⟹ v₁ = v₂。

證明同樣是 rule induction,跟 CBV 的證明結構一樣。

範例 1:`fortytwo(infinity)` 在 CBN 下

                                  ──(n)
                                  42 ⇓ 42
                                  ──────────────────────(fnname) [因為 42{x↦infinity} = 42]
                                  fortytwo(infinity) ⇓_P 42

✓ 直接得 42,完全不去算 infinity!

範例 2:`square(2 + 1)` 在 CBN 下

不像 CBV 先把 2+1 算成 3,CBN 會直接把 (2+1) 代換到 x*x,得到 (2+1) * (2+1),然後 2+1 在這裡 被算了兩次:

                ──(n) ──(n)                       ──(n) ──(n)
                2 ⇓ 2 1 ⇓ 1                       2 ⇓ 2 1 ⇓ 1
                ──────────(op)                    ──────────(op)
                2+1 ⇓ 3                           2+1 ⇓ 3
                ──────────────────────────────────────────────(op)
                (x*x){x↦2+1} = (2+1)*(2+1) ⇓ 9
                ──────────────────────────────────────────────(fnname)
                                square(2 + 1) ⇓_P 9

觀察:CBN 在純 (没有 side-effect) 語言裡結果跟 CBV 相同,但「中間過程」可能重複求值同一個子表達式。

真實世界的 Haskell 用的是 call-by-need(也叫 lazy evaluation):是 CBN 的「優化版」 — 第一次求值後把結果快取起來,之後直接拿快取,所以不會重算。

練習:`max(3, square(2))` 在 CBN 下的推導

解答(CBN):

                                                         ──(n) ──(n)
                                                         2 ⇓ 2 2 ⇓ 2
                                                         ──────────────(op)
                                                         (x*x){x↦2} ⇓ 4
                                                         ───────────────(fnname)
                                                         square(2) ⇓ 4
                            ──(n)                        ──────────────
                            3 ⇓ 3                        
                            ───────────────────────────────────────(bop)
                            3 ≥ square(2) ⇓ False     [因為 3 ≥ 4 = False]
                                                                                  ──(n)──(n)
                                                                                  2 ⇓ 22 ⇓ 2
                                                                                  ──────────(op)
                                                                                  (x*x){x↦2}⇓4
                                                                                  ────────────(fnname)
                                                                                  square(2) ⇓ 4
                            ─────────────────────────────────────────────────────(iff)
                            (if x≥y then x else y){x↦3, y↦square(2)} ⇓ 4
                            ─────────────────────────────────────────────────────(fnname)
                                          max(3, square(2)) ⇓_P 4

觀察:跟 CBV 比,你會看到 square(2) 出現了兩次 — 一次在比較 3 ≥ square(2),一次在 then 分支(其實是 else 分支對應的 y 被選中時)被代換進來再次求值。CBV 只算一次。

4.3 SFUN 的型別 (Types)

到目前為止,我們的語意只在「良型項 (well-typed terms)」上運作,但 SFUN 的語法允許像 1 + True 這種 語法合法但語意不通 的項。要排除它們,我們需要 SFUN 的 型別系統。

型別文法

σ ::= int | bool                       (基底型別)
τ ::= (σ₁, …, σₙ) → σ                  (函數型別)

當 n = 0(無引數的「函數」 = 常數)時,τ 直接寫成 σ。

例如:

int — 整數

bool — 布林

(int, int) → int — 拿兩個整數、回傳一個整數的函數

(int) → bool — 拿一個整數、回傳布林

觀察:SFUN 的函數型別 固定 arity — 沒有 currying!(int, int) → int 不等於 int → int → int。SFUN 是 first-order:函數本身不能被當作值傳遞。

4.4 Typing 規則:良型項 (Well-typed Terms)

判斷 (judgement):Γ ⊢ε t : τ

讀作「在變數環境 Γ 與函數環境 ε 下,項 t 有型別 τ」。

兩個環境的角色:

Γ:變數環境 — 從變數 x 對應到基底型別 σ。是 finite partial function。
ε:函數環境 — 從函數名 f 對應到該函數的型別 (σ₁, …, σ⟨f⟩) → σ。
如果 ⟨f⟩ = 0,ε(f) = σ。
如果 ⟨f⟩ = n ≥ 1,ε(f) = (σ₁, …, σₙ) → σ。

定義:Γ ⊢ε t : τ 由下列公理與規則歸納定義。

Typing 規則一覽表

公理:布林與整數常量

─────────────────              ─────────────────
Γ ⊢ε b : bool                  Γ ⊢ε n : int

變數 (variable)

─────────────  [若 Γ(x) = σ]
Γ ⊢ε x : σ

「變數的型別由變數環境查表決定。」

算術運算

Γ ⊢ε t₁ : int     Γ ⊢ε t₂ : int
─────────────────────────────────  (op-ty)
     Γ ⊢ε t₁ op t₂ : int

比較運算

Γ ⊢ε t₁ : int     Γ ⊢ε t₂ : int
──────────────────────────────────  (bop-ty)
     Γ ⊢ε t₁ bop t₂ : bool

邏輯非

   Γ ⊢ε t : bool
──────────────────  (not-ty)
   Γ ⊢ε ¬t : bool

邏輯且

Γ ⊢ε t₁ : bool     Γ ⊢ε t₂ : bool
──────────────────────────────────  (and-ty)
       Γ ⊢ε t₁ ∧ t₂ : bool

條件式 (if)

Γ ⊢ε t₀ : bool   Γ ⊢ε t₁ : τ   Γ ⊢ε t₂ : τ
──────────────────────────────────────────────  (if-ty)
   Γ ⊢ε if t₀ then t₁ else t₂ : τ

重點:then 與 else 兩個分支必須有同樣的型別 τ!整個 if 表達式的型別也是 τ。

函數應用

Γ ⊢ε t₁ : σ₁   …   Γ ⊢ε t_⟨f⟩ : σ_⟨f⟩
──────────────────────────────────────────  (app-ty)  [若 ε(f) = (σ₁,…,σ_⟨f⟩)→σ]
        Γ ⊢ε f(t₁, …, t_⟨f⟩) : σ

重點:每個引數的型別必須 對得上 函數簽章。回傳型別由函數簽章決定。

特例:當 ⟨f⟩ = 0 時,規則退化為公理:Γ ⊢ε f() : σ(不需要前提)。

Typing Derivation 範例

例子:給定 Γ(x) = int 且 ε(fact) = (int) → int,求 if x ≤ 0 then 1 else x * fact(x - 1) 的 typing 推導。

逐步建立推導樹(由下往上、由外往內):

要型別化整個 if,需要:

Γ ⊢ε x ≤ 0 : bool
Γ ⊢ε 1 : int
Γ ⊢ε x * fact(x - 1) : int

並且整個 if 的型別等於兩個分支的共同型別 int。

子推導 1:x ≤ 0 : bool

   ────[Γ(x)=int]    ────(int axiom)
   Γ ⊢ x : int       Γ ⊢ 0 : int
   ──────────────────────────────(bop)
              Γ ⊢ x ≤ 0 : bool

子推導 2:1 : int(直接公理)

子推導 3:x * fact(x - 1) : int

                                ────[Γ(x)=int]    ────(int axiom)
                                Γ ⊢ x : int       Γ ⊢ 1 : int
                                ──────────────────────────────(op)
                                          Γ ⊢ x - 1 : int
                                ────────────────────────────────[ε(fact) = (int)→int]
   ────[Γ(x)=int]                          Γ ⊢ fact(x - 1) : int
   Γ ⊢ x : int                             
   ──────────────────────────────────────────────────────────────(op)
                  Γ ⊢ x * fact(x - 1) : int

最終樹:

   {子推導 1}        {子推導 2}        {子推導 3}
   ────────────────────────────────────────────(if)
   Γ ⊢ if x ≤ 0 then 1 else x * fact(x - 1) : int

練習:`max(3, square(2))` 的 typing 推導

題目:給定 ε(max) = (int, int) → int、ε(square) = (int) → int,給 max(3, square(2)) 的 typing 推導。

解答:

                          ────(int axiom)
                          Γ ⊢ 2 : int
                          ─────────────────────────[ε(square) = (int)→int]
   ────(int axiom)        Γ ⊢ square(2) : int
   Γ ⊢ 3 : int                  
   ────────────────────────────────────────────────[ε(max) = (int,int)→int]
                  Γ ⊢ max(3, square(2)) : int

(注意這裡 Γ 可以是空環境,因為沒有自由變數。)

4.5 Typing 一個 SFUN 程式

定義:給定 SFUN 程式

f₁(x₁, …, x⟨f₁⟩) = t₁ ⋮ fₖ(x₁, …, x⟨fₖ⟩) = tₖ

與函數環境 ε,程式 P 是 typeable 的若對每條方程式 fᵢ(x₁, …, x⟨fᵢ⟩) = tᵢ,都存在某個變數環境 Γᵢ 與型別 τᵢ,使:

Γᵢ ⊢ε fᵢ(x₁, …, x⟨fᵢ⟩) : τᵢ(左側 typeable)

Γᵢ ⊢ε tᵢ : τᵢ(右側 typeable,且型別等於左側)

直觀:每條方程式的「左 = 右」必須有相同型別,而且這個型別跟 ε(fᵢ) 一致。

範例:檢查程式 `P` 是 typeable

程式:

infinity     = infinity + 1
fortytwo(x)  = 42
square(x)    = x * x

設:

ε(infinity) = int
ε(fortytwo) = (int) → int
ε(square) = (int) → int

檢查:

infinity = infinity + 1 - 左:Γ ⊢ε infinity : int(因為 ε(infinity) = int)。 - 右:infinity + 1 : int,因為 infinity : int 且 1 : int。✓
fortytwo(x) = 42 - 變數環境取 Γ(x) = int。 - 左:Γ ⊢ε fortytwo(x) : int(x : int ✓ ⟹ fortytwo(x) : int)。 - 右:42 : int。✓
square(x) = x * x - 變數環境取 Γ(x) = int。 - 左:Γ ⊢ε square(x) : int(x : int ⟹ square(x) : int)。 - 右:x * x : int,因為 x : int 兩次。✓

✅ P 是一個 typeable program。

4.6 用歸納法證明 SFUN 程式的性質

SFUN 因為是純函數式的,所以「對自然數 n 證明性質 P(n)」變成可以直接用 SFUN 程式來陳述的數學定理。

範例:證明 `fact(n) = n!`

fact 的定義:

fact(x) = if x ≤ 0 then 1 else x * fact(x - 1)

目標:對所有自然數 n,證明 fact(n) = n!。

證明(對 n 做歸納):

Base case (n = 0):

要證 fact(0) = 0! = 1。

由定義:0 ≤ 0 為 True,套用 then 分支,fact(0) = 1。 ✓

Inductive Hypothesis (IH):假設對某 n,fact(n) = n!。

Inductive step:證 fact(n + 1) = (n + 1)!。

由於 n ≥ 0,(n + 1) ≤ 0 為 False,套用 else 分支:

fact(n + 1)
= (n + 1) * fact((n + 1) - 1)       (依 fact 定義)
= (n + 1) * fact(n)                  (算術簡化)
= (n + 1) * n!                       (依 IH)
= (n + 1)!                           (階乘的定義)

✓ 由歸納法,結論對所有自然數 n 成立。 ∎

觀念總結:SFUN 的形式化讓我們可以把「程式 = 數學物件」這件事完全嚴謹化。型別保證程式不會在執行時亂掉,操作語意定義它的行為,結構歸納法讓我們證明它的正確性。

5. 全部練習題與詳解

以下匯整講義中所有練習題並補上完整解答。

練習 5.1:`elem'`

寫一個函數 elem' x l,檢查 x 是否出現在 list l 中。

elem' :: Eq a => a -> [a] -> Bool
elem' _ []       = False
elem' x (y : ys) = x == y || elem' x ys

型別 Eq a => a -> [a] -> Bool(因為要用 (==))。

練習 5.2:`take'`

寫 take' n l,回傳 list 的前 n 個元素。

take' :: Int -> [a] -> [a]
take' 0 _        = []
take' _ []       = []
take' n (x : xs) = x : take' (n - 1) xs

練習 5.3:`Tree a` 與 `height`

data Tree a = Leaf a | Branch (Tree a) (Tree a)

t :: Tree Int
t = Branch (Leaf 1) (Branch (Leaf 2) (Leaf 3))

height :: Tree a -> Int
height (Leaf _)     = 1
height (Branch l r) = 1 + max (height l) (height r)
  where max x y = if x > y then x else y

驗算:height t = 3。

練習 5.4:用歸納法證 `add n Zero = n`(對 `Nat`)

見 § 2.4 完整證明。

練習 5.5:用歸納法證 `sumNat n = n(n+1)/2`