Church Numeral

今日 functional programming 談到 untyped lambda calculus，舉了一些例子，其中一個是 Church numeral，即以一組特定的 higher-order functions 表示自然數。我於是趁午休試著用 OCaml 實作，算可以 work：

(* primary definitions *)
let zero = fun f ->fun x -> x
let succ x = fun f -> fun n -> f (x f n)
let plus x y = fun f -> fun n -> x f (y f n)
let mul x y = x (plus y) zero

(* translating functions *)
let cnum2int x = x (fun f -> fun x d -> f (0+x) (d+0) + 1) (fun x d -> 0) 0 0
(* let cnum2int x = x (fun n -> n + 1) 0 *)
let rec iter f n = fun x -> if n = 0 then x else f (iter f (n - 1) x)
let cnum n = iter succ n zero

如果單用 cnum2int (mul (plus (cnum 4) (cnum 5)) (plus (cnum 6) (cnum 7))) 這樣的算式可以 work，但如果先把某個數繫結到 identifier 上而後對它施行某個操作，就會發生（對我而言）複雜的型別錯誤。此類錯誤引我嘗試未註解掉的那個 cnum2int 畸形版本，但問題仍然存在。目前我沒辦法解決，先暫時放著 XD。

下午是 program derivation，穆老師的語速很快，和 cyy 與 Y 老師講課的速度差不多（cyy 平時講話又是另一個等級了 XD），不過整體速度適中。作業看起來很多的樣子 XD。

--
來做做看就知道實際上多不多了 ─ appearances can be deceiving XD。

---

我照 Wikipedia 的方式把乘法的定義改為 let mul x y = fun f -> x (y f) 就好像全部都 work 了，cnum2int 也可以用比較簡單的那個版本。目前尚未去理解為何這樣就 work XD。

---

時間 9:45，program derivation 的作業寫完了，最後一題還滿好玩的 XD。待會再接再厲把 functional programming 的作業也寫一寫 XD。

---

時間 11:17，functional programming 作業也寫完了。前兩題很簡單，第三題我花了很多時間才恍然大悟 type 'a t 的作用和 'a option 很像，之後才慢慢地把 fold/unfold 兜出來。Functional programming 真的很可愛 XD。

---

隨便寫一個 function possum 計算一個 int list 各元素（假設均非負）的和，測試 type nat 的 unfold：

let possum =
  let rec seed l =
    match l with
      [] -> Z
    | 0 :: tl -> seed tl
    | hd :: tl -> S ((hd - 1) :: tl)
  in
    unfold seed

Functional programming 真的很可愛 XD。