亂導

在英國問 scm 老師 inductive/coinductive datatypes 的 Church encoding（scm 老師寫過一篇〈Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus〉介紹）。這很自然讓我想起莊老師在 FLOLAC '07 上的 Functional Programming，投影片曾經提到一句 "What is a tree, anyway? A tree of type α tree is a value that can be folded." 這句一副就是在講 Church encoding 的樣子 XD。之後我覺得兩種編碼的關係密切，就隨便亂導一下：

完全是矇著眼睛操作語法就是了 XD。

--
真正的情況到底是什麼呢？