2009/02/19

戰意

Haskell-cafe 一個討論串突然拐到 dependent types 來,有人寫了一小段 Coq 證明 length (map f (xs ++ ys)) = length xs + length ys,駁斥「dependently-typed languages 裡的證明都極為冗長、寫起來很煩」的說法。看到 Coq 不知所云的證明(XD)頓時不知從哪裡湧出一股戰意:Agda 的證明漂亮得多呀!Agda 有直覺的 proof terms 和美麗的 mixfix unicode operators,造就了人人稱讚的 equational reasoning combinators,Coq 怎麼比呀!

很快就意識到這種情緒實在太不邏輯了,顯然是因為 Coq 的 pi-calculus code 裡面用上千行 tactics 堆起來的證明不用 coqide 看就看不懂的緣故 XD。

--
顯然今天沒辦法實現新策略 XD。

Labels:

<< 回到主頁