進展

昨天半夜看〈Putting Curry-Howard to Work〉看到一半整個亂掉，決定重頭再慢慢看一次。Second pass 狀況好很多，記住 propositions as types、values as proofs (witnesses)，然後小心釐清誰是 value 誰是 type，就多懂好幾成。不過還僅只於看懂，要講一遍或寫一些 nontrivial programs 還非常吃力 XD。

Extensible kind system 雖然邏輯上是個很自然的延伸，可是寫到 *1 就已經很難理解了 XD。

不過 Omega interpreter 的效能真的很恐怖，我打個 #100 就掛了 XD。

--
最重要的是：我能打出字了 XD。

---

從昨天就想把一般動態的 list [a] 轉成靜態、長度固定的 List a n。這直覺上不可能，但如果能說類似 "exists n. List a n" 的東西，似乎就有機會。剛剛我模仿〈Put Curry-Howard to Work〉section 10 的方法去做：

data List :: *0 ~> Nat ~> *0 where
  Nil :: List a Z
  Cons :: a -> List a n -> List a (S n)

data Covert :: (*0 ~> Nat ~> *0) ~> *0 ~> *0 where
  Hide :: (t a x) -> Covert t a

d2s :: [a] -> Covert List a
d2s [] = Hide Nil
d2s (x : xs) = let (Hide ys) = d2s xs in Hide (Cons x ys)

然後在 Omega interpreter 裡面說

prompt> let (Hide xs) = d2s [1, 2, 3, 4]
xs
prompt> xs
(Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) : List Int _a
prompt> (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))
(Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) : List Int 4t
prompt> Cons 5 xs
(Cons 5 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) : List Int (1+_a)t

顯然那個靜態的長度資訊不可能拿出來，雖然符合直覺可是很可惜 XD。（Epigram 可能就可以了？）文內的例子是 msort :: [Covert Nat'] -> Covert Dss，其中 Dss n 是「最大元素為 n 且遞減的數列」，這裡用 Covert 把 n 藏起來就無關痛癢 ─ 這份資訊只用在 type-checking 時檢驗 msort 的排序性質而已。

---

我實在看不懂 theorem 的寫法。照著〈Omega Users' Guide〉掰一個：

assoc :: Nat' x -> Equal {plus x (S y)} {plus (S x) y}
assoc Z = Eq
assoc (S x) = Eq where theorem indHyp = assoc x 

theorem associativity = assoc 

This works for revcat，可是覺得莫名其妙。

---

喔，是因為已經賦予 assoc 一個 type，所以只寫 Eq 就可以做 inference 嗎？直覺上是可以了，可是內部機制還完全不了解 XD。merge 再加一個 right-identity theorem Nat' x -> Equal {plus x Z} x 也 check 了。

然後若要讓 revcat 在 Epigram 之下 check，這正好是〈Why Dependent Types Matter〉section 4.1 的例子。看起來精神和 Omega 一樣，都是提供一個事實供 typechecker 往下推導。

另外，該節所寫出的兩個 proofs 正好是我寫的 associativity 和 right-identity theorems，讓人懷疑這兩個 theorems 有特殊的地位。我想應該是因為這兩個 theorems 正好對 plus 的第二個參數做 structural induction，然後把 induction 推到第一個參數去，從而迎合 plus 的定義。（想到切牛排要看肌理切 XD。）

---

一個小問題：有沒有辦法設計一個情境，測試 Omega 能否從 {plus (S x) y} 推到 {plus x (S y)}？