大起大落

早上看了一點 Richard Bird 的 Zippy Tabulations of Recursive Functions 和 Jeremy Gibbons 的 Unfolding Abstract Datatypes。原來寒假去英國的時候 Richard Bird 講的 "F-structure of L-structures all of the same shape" 就是在講這一篇啊 XD。中午和來台大考試的國中導師吃飯。下午寫了一小段 Agda，突然覺得很沒意義：現在會做的事情好像就真的只是一股腦兒地把東西放到 types 裡面。接著就亂產出一些沒意義的 code 把時間消磨掉…

--
這種時候還是先看別人的論文吧 XD。