雲深不知處

今天早上的 type system 前段很輕鬆，我的主要工作只需把 formal detail 和既有的 OO 概念連結起來就可以了。到後面 recursive record types 進來，就又得用力追，最後一段跟本來就不熟的 Java 5 generics 印證，一邊努力回憶一邊聽講一邊連結，有點辛苦 XD。不過真正的魔王是下午的特別演講 ─ 傳說中的 Gödel 不完備定理。董世平老師講得很清晰精彩，可惜我還是捉不牢要義，頂多只能 follow。台下老師們常適時提出問題或 comments，常常引出一番深度討論（e.g. a qualitative description of why Goodstein's theorem cannot be proved in Peano arithmetic），此時我就像鄉巴佬進城，雖然不懂但聽個大概，讚嘆一下而已 XD。

陳恭老師今天講到 "contravariant return type is dangerous" 時，完全把 Animal 和 Mammal 之間的 subtyping 關係搞混，之後又說「鳥類是哺乳類」，最後乾脆自爆高一時唯一睡過的課就是生物課 XD。今晚來對付 type system，然後週末要複習統整一下。

--
愉快的週末 XD。