中研院歷險記

今天第一次乘大眾運輸到中研院，對我是項挑戰 XD。過程運氣其實相當好，只要差一點我就回不了家了 XD。

12:40 吃完老莊，就到捷運科技大樓站幫學生證儲值並退掉舊悠遊卡，約 13:10 抵達昆陽站。雖然在捷運站裡看了一次地圖，一出站就不知身在何方。憑著直覺走到對面看到 212 站牌，很小心地確認這一線有到中研院，而且找了幾個站名，以便上車後可以當向量端點，確認沒坐錯方向。結果 212 竟然衝到離站牌三十公尺遠處 XD。上車後，下一站站名和先前記的站名不合，然後又是兩個「臨時站」，我心中就不安了，畢竟當年我第一次坐台北公車就坐錯方向 XD。不過看周遭景色愈來愈荒涼，又滿符合中研院的印象。最後擠到前面看公車上的路線圖才確定沒坐錯。萬歲！

到了中研院就很順利了，一下車就看到郵局，那是我除了活動中心和資訊所以外唯一去過的地方。抵達資訊所電梯前，往右一看赫然是 scm 老師和老師的妻子，沒注意到我，電梯大概坐到三樓我才被發現 XD。接著辦一些很複雜的人事手續，途中兩次撞見李所長老大（不知為何心裡浮現這個稱號 XD）。14:05 開始 meeting，主要是 scm 老師介紹 yet another dependently-typed language Agda 及一些近程目標。接著是複雜的發薪手續，因為和之前複雜的人事手續有點糾葛，所以還領不到就對了 XD。簽完最後一張很複雜的單子已經五點鐘，我連忙離開，趕搭 17:40 的火車。（對了，scm 老師的 iMac 超大！然後我的正式身分是勞務採辦之類很複雜的稱號，看起來很像工人 XD。）（然後 Agda 用 literate programming tools 如 Nuweb 來寫應該不錯（我會用 Nuweb 試試看），只是 dependency 仍然得自己處理。）（scm 老師要計算 880 * 8 的時候直接打開 hugs（Haskell 的一個 interactive interpreter），全場竊笑 XD。）

最後高潮開始了：四十分鐘內藉大眾運輸從中研院坐上火車！我剛走到中研院大門對面的站牌，往後一看正是 212。17:12 抵達捷運站，17:14 分發車。接著一站坐過一站，我抽樣某回「連續兩次車身速度從零轉正」測量期間時距，差不多是兩分鐘，而昆陽站到台北車站大概是十站。我坐在座位上（從端點開始坐的福利）不斷喃喃自語「衝啊衝啊」，終於在 17:30 抵達台北車站。接著在台北車站內奔走，17:37 我站定在第三月台，五秒後第八號車廂就停在我面前。趕上了！所以現在就在彰化了 XD。

--
看來該玩玩 Agda 了 ─ 在我把 TOY86 linker 寫完之後 XD。