GSS student report, Michaelmas Term 2011

I have mainly been concluding my first year's work since last report: I gave two talks at the DTP workshop in August and WGP (after which I also stayed for ICFP and the Haskell Symposium) in September, both receiving positive feedback; I polished up a dependently typed solution to the Dutch National Flag problem, used that as the motivating example for my transfer dissertation, and passed the transfer viva; a poster was made for the DNF development, which received the best poster award in this year's student conference and will be presented in APLAS in December. For the next stage of my research, I have been making steady progress, albeit slowly at the moment (with no significant output yet). I have set myself some reading tasks (including Jacobs' categorical logic and type theory book and Okasaki's purely functional data structures book as planned in the transfer dissertation), and identified a few concrete examples to play with (including the functional derivation of maximum segment sum and internalist de Bruijn indices used in typed representation of lambda terms), which hopefully can lead to interesting generalisations later. At a higher level, I believe I am having a better idea about how I will formulate the arguments for my thesis, while I estimate that it's possible but not easy to get all the technical results I need in time - hard work is therefore no doubt required!

--
看來 assessors' report (for transfer) 短期內不會出現 — 我真的可以先來寫第一年回顧了！XD

ICFP 2011

一樣搭凌晨五點半的 X70 到 Heathrow，在 BA007 上坐 12 個小時到東京羽田。飛機上幾乎沒睡到（日後幾天時差也調不太動，如 Jeremy 所預測，調完也差不多回去了）。降落時飛機竟然蛇行一陣，不過沒衝出跑道就好了。

到東京的時間是早上五點，出關大約六點，依照計畫直接前往東京電玩展。到機場的單軌電車站後先打開手機，卻悚然發現蓄電量不知為何只剩 3x%，代表我很可能面臨沒有 GPS 可用的窘境，幾張電車地圖也存在手機裡，但事到如今也只能硬著頭皮上了。依照 Wikitravel 等網站的建議先買了一張 Suica（上面圖案是 Q 版的單軌電車人），然後對照幾張地圖比對出我應該搭單軌電車到天王洲島、轉臨海線到新木場、再坐 JR 京葉線到海濱幕張站。在日本轉車是 nontrivial task，因為不同路線可能是不同公司經營，地圖上同一站實際上可能相距好幾百公尺，而且可能還得走到街上。電車很乾淨，那時還早沒什麼人，日文廣播有些許親切感（英文版很可愛），站名也都是漢字。駛過灑滿陽光的東京高樓之間，我還以為我身處第三新東京市 XD。（電車本身自然也完全就是 Eva 的經典場景之一。）

到新木場時，月台上已經有一群群一副宅樣的年輕人站在那兒等車，看來我沒走錯。抵達海濱幕張站時才七點，已經有些人潮，我只要跟著走就行。離會場愈近人愈多，過了當日票銷售據點後人龍出現了，但根據現場的排隊繩佈置來看，高峰期可能還會有四、五倍的人 — 幸好我早到！排隊的感覺有點像回到部隊，所有人擠在一塊跟著前面的人走。入口處有簡單的安檢（比方說不能帶刀劍形狀的東西進去），我完全聽不懂他們說什麼，可是好像也猜得八九不離十，反正看手勢、模仿前面的人就對了。稍後繞著會場外緣真正開始排隊時（剛才只是排安檢），有小販在隊伍外賣飲料，攤子擺在遠處，不會說日文又沒得比手畫腳，該怎麼跟她說我想買什麼呢？！幸好旁邊的人叫了 "ayataka"，看起來是綠茶，我也就跟著說 "ayataka"，獲得無糖綠茶一瓶。排了兩、三個小時，一開始艷陽高照，後來竟然下起暴雨，一陣下完再一陣，第二次還加狂風，讓我不禁回憶起成功嶺上這種天氣得穿異味極重的深藍色雨衣。十點十五分（開場後十五分鐘）終於進入會場，基本上就是廠商架起自己的「攤位」，但大廠商的攤位都相當誇張，是七彩舞台、巨型螢幕、試玩機台的綜合體，走上二樓往下看，只見萬頭攢動，滿滿的人潮真的如潮水一般在攤位間流動交融，中間穿插著 cosplayers 和 showgirls。我很快發現我確實對展出內容沒多大興趣，只想找到免費上網的地方，寄信給 scm 老師看能不能搞定晚餐。scm 老師很快就回信說可以一起吃，看來不用緊張了。這應該會是我唯一一次參觀東京電玩展，所以下午把握機會再進會場看一輪，有看到一些熱血機器人遊戲的廣告片，但沒有變形合體不能算真正熱血啊！

兩點鐘離開電玩展，坐 JR 京葉線到東京站接地鐵系統，四點入住 Hotel Villa Fontaine 神保町分店（所以確實有點距離）。房間比較小一點，但整潔程度令人讚嘆，特別浴室裡一切能發亮的東西都擦得閃亮亮全無水漬，讓我不太敢用。浴室裡另一個特點自然是日本特產免治馬桶，第一次試用稍微有點不習慣，但清潔效果極佳，剎時有搬一個回英國的衝動 XD。六點和 scm 老師和 WGP 另一個 co-chair Jaakko Järvi 一起去吃生魚片蓋飯，這是我第一次吃真的生魚片（在中辦的時候愛家炒麵有一次附素生魚片）和哇沙米，還滿不錯的 — 那時其實沒有很餓，但竟然還滿輕鬆地整碗吃完了。晚餐後又練習一下隔天的 talk，情況還不錯，剩下能準備的大概就只有睡飽一點了。

可惜晚上沒有真的睡好，所以隔天 WGP 即將開始時我已經有點想睡，只能希望待會腎上腺素多分泌一點。Jaakko 負責開場，scm 老師主持第一個 session，我是第二個講者（第一個是 Andres Löh）。Jaakko 才剛開始，房間內卻突然迴盪著來源不明的開場詞，原來是隔壁 ML workshop 的聲音也接到我們這裡了。狀況稍後排除，Andres 很快就講完（Q&A 的時候還幫我宣傳了一下）輪到我，講起來還算順，雖然有時候切換投影片不很順 — R800 好幾次按下去沒反應，一些連接詞／句也沒處理好。講了大約五分鐘，我想看一下剩餘時間，卻發現我忘了啟動 R800 的計時器，這下只好靠 scm 老師計時啦（我這時還是啟動計時，結果稍後 Venanzio Capretta 擔任我的討論人時，我放在桌上的 R800 振動起來嚇了他一跳）。講到高潮 ornament fusion 時，我按下按鈕把 sorted lists 和 vectors 融合成 sorted vectors 然後略為停頓，就在此時，隔壁 ML workshop 的人正好拍起手來，時間捉得剛剛好！（WGP 一些人也很捧場地笑了幾聲 XD。）單為這個點我就很想重看錄影 XD。我講完後 Venanzio Capretta 接手討論，問的第一個問題就是重點（用我的 framework 到底省了什麼力氣？），我猶豫一下之後決定召喚 DTP 的 backup slides 回應。第二個問題也很棒（如果有個 function 把 sorted list 轉成 search tree，用我的 framework 也可以把它升級成比較精確的版本嗎？），但也很容易回應。再來 Tim Sheard（此人稍後猛力攻擊一個 Utrecht 的 PhD student，說他一開始要解的問題根本不對，不過旁邊其他人幫那個學生圍剿他）想看 ornaments 實際上長什麼樣子，我也有 backup slides（本來有放在「正講」裡面，後來覺得很難講，改成 backup slides，雖然事後覺得其實還是應該放在正講裡面比較完整）。之後好幾個人都跟我說喜歡我的 talk，Oxford 方面 Dan 說他覺得我的 talk 是當天最好的，Jeremy 說他被我說服投影片用 transitions 是有意義的。所以算是（初步）成功了吧！我個人是覺得離完美還有不小的距離，就等錄影上網再研究修正嘍。午餐遇到 Oleg 和久仰大名的單中杰老師，晚上和他們一起去吃印度菜（單老師妙語如珠，果然名不虛傳）。

隔天 ICFP 正式登場。主辦人胡振江老師開場時超興奮，一直講 "ICFP two-thousand-one"，我和 Oleg 一直笑 XD。稍後另一個 general co-chair（還是 local arrangement chair？我忘了）好心提醒大家日本地震頻繁，遇到不要驚慌，還有輻射量已經回到正常水準，不放心的話樓下有測量儀器。Invited talk 結束後就輪到 Jeremy 上場了。Jeremy 果然很會講，投影片也很優雅（最後還放了一張 Captain Kirk！）。讓我印象深刻的一個地方是 Jeremy 在講一條 monadic law，他說他不詳細講，但還是加了一小句關於發射飛彈的比喻，只那幾個字就讓我剎那間猜到那條 law 的意思，用字之精準有力令人瞠乎其後。三天下來不少 talks 都很有意思，講者功力也都有一定水準，雖然也有幾場讓人覺得是 trivial work 或是根本聽不懂在講什麼。Agda 出現在 ICFP 令人感到親切（內容是關於模擬 type classes 用的 instance arguments），幾場關於 modular composition 的 talks（包括 WGP 最後一場）讓我考慮 ornament framework 有沒有可能涵蓋這些例子，experience reports 有人用 Haskell 研究上古生物和音樂和聲，相當有趣。到第三天，會場隱隱瀰漫著一股不安氣氛 — 有颱風要來了！我下午精神不濟想溜走，但走到門口一看，外頭已經狂風暴雨，根本走不了。東京的公共運輸系統幾乎停擺，local arrangement chair 上台宣佈各線電車行駛狀況，只聽到暫停暫停暫停，大家只能留在會場等颱風過去。scm 老師說 Graham Hutton 把外頭情況錄下來想告訴家人沒什麼事，結果畫面裡樹枝亂舞，驚悚得很。會場外還吹倒了一棵不小的樹。事後得知這個洛克颱風是個超級強颱，略過台灣直撲日本，卻剛好被我撞上了。

第二天晚上有不少節目，另起一段。Phil Wadler 頒獎給 ICFP'01 影響最深的論文（沒記錯的話應該是 Recursive Structures for Standard ML），我和 scm 老師完全猜錯；再來頒發程式語言軟體成就獎，由 Simon Peyton Jones & Simon Marlow 拿下，理由自然是 GHC。稍後 Simon Peyton Jones 在大會聚餐上發表感言，敘述 GHC 二十餘年來的歷史，包括他兒女覺得他比較愛 GHC 沒那麼愛他們、一開始效率怎麼打也打不過 Lennart Augustsson、GHC 曾經有過最有意思的 bug 是把有 type error 的檔案直接刪掉、以及一些經典笑話例如在 GHCi 打 fix error 之類的。在我們前往聚餐場地前，還有今年 ICFP programming contest 的報告和頒獎：這次題目是某種紙牌對戰遊戲，因為地震後有限電措施，沒辦法在東京的 clusters 上對戰，所以要找（印象中像是在）關西和北海道一帶大學的 clusters 幫忙。冠軍由牛津博士生（都是 Luke Ong 的學生）組成的隊伍拿下（YA!!），使用語言是 F#。前往聚餐地點一路上我死巴著 Jeremy，果然坐到舞台旁的搖滾桌（Phil Wadler 的 "application, abstraction, and variable" toast 和 Simon Peyton Jones 講 GHC 歷史我都得以近距離目睹），和 Graham Hutton、Tim Sheard、Andy Gill 同桌，稍後 Jeremy 又把 scm 老師的前老闆武市正人老師拉過來坐我旁邊。武市正人老師極其親切，說起英文來慢慢的、沒有難懂的日本口音，一直記得要跟我聊天。到後來，他突然說想問我一個可能很難回答的問題：你們這一代對日本的觀感如何？呃，其實一點都不難啊，我就說我們這一代都是看日本動漫長大，受日本文化影響滿多，對日本很有好感，像我到東京還覺得街景很熟悉親切。他提到他經歷二戰，我就說那對我們已經是上一代的事情了，他才一副放心的樣子。（我倒是不太敢問他問這個問題的動機。）席間不免要有日本傳統文化表演，幾位藝妓先在台上跳三支舞然後下場陪酒。那些舞相當 subtle，我看到最後一支舞才勉強看出（或以為看出）一些端倪。回旅館的路上和 Jeremy 聊女僕與獸耳（他無法體會獸耳的意義，覺得日本人很會做可愛的東西但有點過頭了 XD）。

因為機票價錢的關係，我在 Haskell Symposium 之後多留一天整體會比較便宜。Oleg 邀我去當天晚上的 delimited continuations tutorial，早上我就自己出去逛，目標是淺草寺和秋葉原，不過我一下就覺得無趣，草草離開：淺草寺不大，而且因為經過轟炸重建，建築看起來嶄新得不太自然，前面的購物街我不太逛（只買了人形燒來吃），宗教活動我也沒打算碰。下一站秋葉原也差不多，模型店逛過去清一色是不認識的東西。兩個小時以內（含通車時間）就覺得此行目的已經達成。看來以後如果自己一個人出門逛可以不用排太多時間 — 我自己對逛街提不起興趣，但和朋友一起逛又是另一回事了。

回程電車又是一番折騰。我從神保町站出發，但走進錯誤的入口，不能搭半藏門線，只好改沿新宿線坐一站、換千代田線坐一站接回半藏門線、再坐一站依原計劃轉銀座線、最後在上野站搭上京成線往成田機場的特急電車，總共搭了五條線，每轉一次都得走一段。即使是星期六，電車上還是有不少學生通勤（甚至 WGP 那個星期天路上也有學生）。Hm, 日本升學壓力也是很大啊。成功抵達成田機場之後就沒什麼了，已經自己旅行好幾次，機場一切流程都很熟悉。沒意外的話，以後還有數不清的獨自長途旅行吧。

--
我也是很會拖稿⋯

New house and the Knight K10

Harry took the wand. He felt a sudden warmth in his fingers. He raised the wand above his head, brought it swishing down through the dusty air and a stream of red and gold sparks shot from the end like a firework, throwing dancing spots of light on to the walls. — Harry Potter and the Sorcerer's Stone

With the help of Duen-Wei, a friend of Shin whom I met during our trip to Oxford in 2008, I moved from Merton Street to a house on Marlborough Road, sharing it with Pan, Eric, and Nien-Ti Tsou who is now writing his DPhil dissertation and will stay for 6 months with his girlfriend. The first 4 characters of the old and new postcodes agree, so the newly rented house is not far away from the city centre. If I go to the city centre via Abingdon Road, I would first walk along a path besides the River Thames, which has a beautiful scene. The area is very quiet, but soon there will be something more in the air, because I've just rented a Knight K10 upright piano and expect to play it frequently — that's the point of getting a piano in where one lives!

Eric came back late (as usual) on Friday evening and we gathered in the living room. Pan played his guitar, and while we were on the topic of music, he suggested that I get a piano in the living room. That suggestion was dreamy! I immediately checked the website of Roberts Pianos (which is a very informative website, by the way) and found that I can in fact rent a piano for a decent price. The first piano I was interested in was a Steinway grand, but later I noticed that unfortunately it has been rented (and it would be hard to move it through the door of the living room anyway). After browsing the website over the night, I had a reasonably good idea about the pianos in stock, and the rest of the job was to actually touch the pianos.

Pan accompanied me to the workshop of Roberts Pianos the next day in the afternoon and Eric joined us a bit later, straight from his lab. There were lots of grand and upright pianos to play with, each having a different tone and quality. I played the Steinway and indeed it was amazing. There was a Chappell baby grand which I liked but was reserved. Other grands either sounded too old or were simply too expensive. Therefore I went on to try the uprights. There were quite a few Yamahas, but they sounded ordinary to me — perhaps I am too familiar with Yamaha pianos. Then we walked into a small room crowded with uprights, and there was a Knight K10 in the corner. Well, it was just like when Harry met his wand. I loved the tone and I could easily make it sing. It responded very well to my fingers. I would say that the decision was made at the very moment, but still I tried some more pianos to make sure the decision was right. Soon it became clear that it was the Knight that will enter our house, and the problem reduced to: Should I rent it or buy it and then sell it?

We asked the gentleman who welcomed us when we arrived. He said there was a special rental scheme (due to lack of storage space) so I can rent it at £28 per month for the first 10 months, and then at the usual rate, which is 3% of the price per month. Later we discovered that, strictly speaking, the special rental scheme does not apply to this Knight, because it was for pianos under £2,700, whereas the Knight was priced at £2,950. The gentleman phoned the boss explaining the situation that he had told us that we could get the piano under the special rental scheme, and the boss agreed! So I rented the Knight for 2 years for slightly more than half of the price, which sounds reasonable. It will arrive at some time in the next two weeks.

Now that I get a piano at home to practise regularly, I think it is much more plausible to hold a few home recitals during the next 2 years. Just thinking about the possibility of doing this makes me excited!

--
Living in the house is going to be a really great pleasure because of this, and I really have to thank Pan and Eric for their support!

GSS student report, Trinity Term 2011

After successfully resolving my medical problem in Taiwan, I returned to Oxford around mid-April with an early draft of a paper which has been completed at the beginning of May and submitted to the Workshop on Generic Programming recently. Also, the abstract of the paper was submitted to the informal Dependently Typed Programming workshop to report the work to a more specialised audience and get feedback from them. I have also finished the essay which was intended to be submitted to Jeremy at the end of April but was delayed due to the medical problem. Admittedly, I lost some time and there was "damage," but now it seems that the loss was not as substantial as I had estimated, and there is a good chance that I can transfer to DPhil status as normally scheduled. Next I intend to carry on with the research work based on the result of the paper. Specifically, I will experiment with the programming technique proposed in the paper by implementing more interesting data structures, and study fibred categories so the technique can be given a hopefully cleaner and semantic account.

--
Uneventful. XD

Wordle for OAOAOO

Closed-beta version of the OAOAOO paper (formally Realisability for modularising inductive families) released!

寫作

最近時間都花在原名為 "Ornamental-algebraic ornaments, algebraic ornament-ornaments" 的 paper 上 — Jeremy 說還是不要用這個模仿 Conor 的標題，因為破他還沒發表的梗不好意思 XD。上次兩個版本的 AoPA papers 光只是在旁邊看 scm 老師寫就已經覺得艱辛，這次自己上陣就更不用說了。有了程式實作但解決的問題到底確切是什麼、故事情節應該怎麼編排才能讓讀者容易融入、概念該用什麼例子輔助講解、該寫怎樣的句子才解釋得清楚、各種子句該怎麼排讀起來才順、動詞搭配的介系詞到底是哪個、哪些詞要加 's' 哪些不要加，從大到小每個環節都得仔細推敲實驗，遠看近觀判斷效果如何，要塗改到滿意可得花不少時間。Jeremy 已經先還給我一份紅筆加註的草稿，不少意見都讓我有回到高中英文課的錯覺，比方說 "relationship" 前面要加 "the" 啦、"structurally similar" 這種「什麼 -ly 怎樣」的兩個字中間不要加 hyphen 啦、be 動詞單複數用錯啦 XD，另外也指出一些情節上需要加強的地方。可能因為還只是草稿的關係，感覺上 Jeremy 的火力離全開還有一段距離，而且 Jeremy 信裡說「我得說我真的認真讀之後發現其實寫得還不錯」，讓我拾回一點信心 XD。我也得說，觀摩 AoPA paper 的寫作實在惠我良多，讓我對寫 paper 的難度有點心理準備，不然這次我可能會嚇得手足無措吧 XD。

照目前趨勢看來，寫作會佔我日後工作很大一部份。說實在有點怕，因為花在琢磨字句篇章的時間心力之多，往往和最後完成的文章長度不成正比。不過和周遭的人對照也沒什麼好說的 — 科技業加班到三更半夜已成常態，連公務員都要隨叩隨到（雖然社會行政不太意外啦⋯ XD），自己的工作如果太過輕鬆也說不過去呀。更何況若能以寫作為業（能吧？），就算是走在自己設定的路上 —「尋求抽象型式的規則」、「層層深究事物的道理脈絡」並加以解釋記錄，應當好好享受才是。特別在 DPhil 這段時間沒什麼其他雜務纏身，更該把握嘍。

而且還不只是論文寫作而已！我的終極關懷是證成，而證成有很多型式與對象，論文寫作只是其中一種。比方說，教職必定是極有意思的挑戰（尤其我口才不便給⋯），還有我想終有一天我會嘗試科普寫作吧，原因⋯待續 XD。

--
會試著讓這個 blog 的發文頻率回升一點 XD。

GSS student report, Hilary Term 2011

Since Christmas I have had a peptic ulcer which, though cannot be described as severe, has been serious enough to cause substantial interference with my work. This term I had expected to finish a long essay for my reading course and produce at least some small results on datatype ornaments in dependently-typed programming, but the plans were not successfully carried out, frequently disrupted by abdominal pain over the past two months. I have decided to go back to Taiwan for about a month to try to get rid of this medical problem completely and intend to catch up with the expected progress as soon as I am back in a good enough condition.

--
A somewhat discouraging report...

GSS student report, Michaelmas Term 2010

This term I focused mainly on coursework but also started my survey on Type Theory and Intuitionism in general. First I list below some brief remarks about the three courses I take this term.

1. Lambda Calculus & Types: Since lambda-calculus is so fundamental to functional programming, I have heard of its various properties like Church-Rosser, strong normalisation of simply-typed lambda-calculus (and System F), but have never actually looked into their proofs. This course offered me a good opportunity to organise these topics and fill in the missing details.
2. Categories, Proofs & Processes: Category theory is also a frequently used tool whose essence I had never grasped except for the simplest ideas. Surprisingly, during this course I started to gain some intuition about universality and adjunctions, now being able to regard them as beautiful rather than incomprehensible. I will need to think more about these concepts, though, to understand them better and be able to use them reasonably intuitively.
3. Program Analysis: The keyword that attracted me was Galois connections, which is a specialised but highly useful form of adjunctions. Also I thought the mixture of theory and practice offered by this course may help me gain some concrete feelings about the application side which I am less familiar with. I find the course amusing but feel a bit awkward doing the practicals. It seems I am now more comfortable with writing proofs rather than hacking computer systems!

For the survey on Type Theory, I have basically finished reading [NPS90] on Martin-Löf's Type Theory and a few relevant papers like [ML87]. Perhaps as a bit of excursion, I have also skimmed through [Hey71] and [Dum77] on intuitionistic mathematics, whose details I am not in a hurry to go into. I am now in the middle of [Luo94] on the Extended Calculus of Constructions, which is based on Martin-Löf's Type Theory but proposes major modifications to it and adopts a different approach to presentation, and I find the book rather dry and considerably harder to comprehend. To make the survey more goal-oriented, I have started to think about how I might write the essay on Type Theory and dependently-typed programming which I am going to submit to Jeremy next term and work on a very early draft from time to time, hoping that could somehow guide my direction of surveying. What makes me slightly worried now is, though confident that I should be able to give a logically smooth summary, it seems more difficult to dig out all relevant previous works and include them in my writing. Hopefully it will look less difficult after I chase more references.

Finally, a comment on my work pattern. I did not do much planning this term, and, sadly, I do not think I have attained reasonable productivity, so a free style does not work very well for me. (Coursework may have taken a lot of my time, but I still think I could have been more productive.) Therefore, I intend to try to follow a timetable and work in a regular manner after this term ends. (It doesn't seem necessary to do the planning right now as the homework and coming exams will occupy most of my time.) Also I will try to set short-term goals for myself. Hopefully this strategy would enable me to complete the survey more quickly and spend more time thinking about some smaller research problems I have in hand.

* References

[Dum77] M. Dummett. Elements of Intuitionism. Clarendon Press, 1977.
[Hey71] A. Heyting. Intuitionism: An Introduction. Amsterdam: North-Holland Publishing, third revised version, 1971.
[Luo94] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Clarendon Press, 1994.
[ML87] P. Martin-Löf. Truth of a proposition, evidence of a judgement, validity of a proof. Synthese, 73(3):407-420, December 1987.
[NPS90] B. Nordström, K. Peterson, and J. M. Smith. Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press, 1990.

--
譯成中文版我可能會被罵浪費時間⋯？XD

入學典禮 (Matriculation)

其實我到剛剛還是一頭霧水：我真的正式入學了嗎？今天天氣是完美的晴天，但氣溫是我到牛津以來最低的一次，幸好 "subfusc"（定義：黑西裝 + 白襯衫 + 黑襪黑鞋 + 白領結）和學袍（gown，一件披在身上後面長兩條尾巴的無袖黑色背心，正常研究生的學袍長度及膝）穿起來還算暖和。我們先在學院集合，簽名領一張編有自己名字的 3 of 9 條碼（我唯一認得的條碼型式 — 意思不是我讀得出來 XD），照個人照（側身四十五度、雙手捧著不能戴上的方帽（要畢業才能戴））和團體照（Radcliffe quadrangle（學院比較新那一半的四方形草地）架起高高的站台讓所有人分層站好，照完後將條碼依序回收，以便辨識團體照裡的每個人），然後進隔壁間 Examination Schools 的 North School 開始入學典禮。幾個學院（沒有全部）的人填滿房間後，校長（Vice-Chancellor）走進來和台下的一個代表用拉丁文對話幾句（但我看不到他們因為我站在後面），然後用英文發表歡迎詞並解釋入學典禮的意義，就結束了。但我那時候不知道已經結束，跟著想必是 St Catherine's College 的學生走回他們的學院，一心以為是前往下一個目的地。我跟著前人愈走愈偏僻心生狐疑，到了 St Catherine's 的現代建築看到人停下來聚成一團團聊天拍照，只能推斷我跟錯了。這下糟糕，剛剛走了那麼一大段路我幾乎沒在看，想回 Univ 都不知道走不走得回去。沒想到隨便憑印象走一下還真的走回我認識的 Broad Street，拿在手上備用的手機 Google Maps 沒派上什麼用場。Univ 裡也是一團團的人來來去去，毫無還有下一攤的感覺，我只好再次推斷我應該已經完成入學儀式了，回房間上網一查也好像沒錯。好像挺天兵的 XD。

I had been rather confused until just a moment ago: Have I matriculated? Today is perfectly sunny but also the coldest day since I arrived at Oxford. Fortunately I felt warm enough in subfusc and gown. We first assembled in the College, signed our names and got a 3 of 9 bar code (which is the only format of bar codes I can recognise - I'm not saying I can actually read the codes XD), took personal photos and group photos (after the group photos were taken the bar codes were collected in order so each person in the photos can be identified), and then went next door into the North School in the Examination Schools for Matriculation. Students from several (but not all) colleges fill in the room, the Vice-Chancellor walked in, exchanged a few Latin sentences with a representative (I could not see them, though, since I was standing at the back), and delivered an English speech welcoming all of us to the University and explaining the meaning of Matriculation. Then the ceremony was over, which I did not realise at the time. I followed other students who must be in St Catherine's to their college, thinking that I was heading for the next destination. I was forced to deduce I got lost after we reached St Catherine's and the students ahead stopped and formed groups chatting and taking photos. "This is bad," I told myself, because I did not pay attention to the route we took. Hoping to get back to Univ, I walked and turned with my vague memory, and miraculously I ended up on Broad Street, which I am familiar with. I had launched Google Maps on my phone but it was not necessary. People in Univ were also in groups and the atmosphere was relaxed, not showing the sign that there was a next event, so I was again forced to deduce that I have matriculated. And it did seem so after I made a check on the Internet back in my room. Rather stupid, I think I was today XD.

--
我還是覺得像是一齣真實上演的古裝劇 XD。

發票

University College (Univ) 寫信來問我學費發票寄到哪，我填 Graduate Admissions & Funding (GAF) Office 的地址。然後我看 Univ 之前寄來的 MPLS Scholarship 通知信，裡面說 Univ 出的部份 GAF Office 會直接寄學費發票給 Univ。欸，所以 Univ 和 GAF Office 之間就發票寄來寄去的？

--
幸好教育部沒來參一腳 XD。

再一次錄取

99 年教育部留學獎學金今日放榜，電資學群錄取的 25 人當中 22 人留美、2 人留英、1 人留日。對我而言，獲錄取代表更多的溝通要進行… 幸好我現在比較沒那麼怕這種事了 XD。

--
仍然是八點前就公佈。教育部的承辦人真的很認真！（或其實是定時自動貼上的？XD）

Aggressive

今早初次搭高鐵北上，參加教育部留學獎學金面試。出發前就為服裝猶豫一陣，最後還是覺得襯衫加牛仔褲比較自然，結果報到的會議室內清一色是正式西裝，牛仔褲應該只有一件 XD。不過面試時坐在圓桌後面，下半身穿什麼都不重要 XD。

面試提早開始，中間的主席扮演和藹長者，左手邊的老師積極進攻，右手邊的老師則一聲不響，只在主席問到為何留英時問到 scm 老師是哪畢業的。全場中文進行，我覺得我的攻擊性好強，語氣聽起來好尖銳，不自覺就和左手邊的黑臉老師對抗起來。其中一個有趣的問題是「你做過證明嗎？」我愣了一下，不管上數學課、做 derivations、還是寫 Agda，不是都在做證明嗎？一番來回之後才搞清楚是原創的證明，那 partial greedy theorem 應該勉強算吧，雖然手寫版證明的規模其實和習題差不多。又問到為什麼我的圖論成績特別差（69 分），我本來開始進行一連串的背景補充，但他們看起來其實沒很大興趣，打斷我請我一言以蔽之，那我就說「有點隔閡」好啦。事後檢討，我覺得面試或多或少有點攻防的意味，把語氣調成 aggressive 提升氣勢不見得是壞事，但似乎也不是非常好就是了。

尾聲，黑臉老師問道有沒有和我列的三所學校的老師連絡過，這次很快就告訴我為什麼問這問題，因為要是換學校的話研究計畫也很可能跟著換。這顯然是個好機會，我就告訴他們研究計畫是 Jeremy 和我一起寫的，已經拿到 admission from Oxford 加全額獎學金，站在我自己立場的話應該就不來了，但那邊還是希望我能繼續找 external funding。雖然簡章規定拿了全額就不能申領，但學校那邊可以調整額度，詳細程序反正是申領時候的事情，就先面試再說了。至此面試結束，黑臉老師說我是個「好 case」，會比別人更快進入狀況，恭喜，請加油，送客。

剛剛看到消息，似乎很多人放棄面試。面試完之後我還是無法決定（要是我是評審的話）該不該給自己這份獎學金，但好像就是因為無法決定，今天才先暫且來參加面試嘛。等結果出來再說…

--
月底要寫作文。等主管收發的王姐五月初回來，應該就可以讀著 categories 待退了吧 XD。

甲類面試清單公告

教育部 99 年留學獎學金甲類面試清單（及乙類錄取榜單）剛剛公告（一上班就貼出來耶，真敬業 XD），我的收理單號也毫無意外地出現在清單內（研究計畫內容是 Jeremy 擬的嘛）。我已經猶豫一陣子到底要怎麼處理留學獎學金申請。站在教育部的立場，把獎學金發給已經拿到（真）全額獎學金的學生顯然沒什麼效益。（補個「真」字是因為很多人聽到全額獎學金的直覺反應是「那生活費勒？」但誠如 XOO 所說，沒包生活費就不算全額了 XD。）但換個角度，這算是 Jeremy 和我一塊找錢的一部分努力（研究計畫內容是 Jeremy 擬的嘛），而 Jeremy 表示過他希望我還是能繼續追這筆錢（畢竟是 external funding）。現在暫時陷入兩難情勢，我決定還是保持 lazy evaluation 的策略，等真正結果出爐再說 XD。

這一週我都在看 Sharon Curtis 和 scm 老師剛投出去的 ICFP '10 paper〈Functional Pearl: Maximally Dense Segments〉─ ICFP + pearl 耶！希望會上 XD。可惜本週雜事略多，時間切割得很零碎，到現在還沒真正把它看完。下週起我又要充當半個收發，為期一月，留學獎學金面試（24-26 April）之前又想多看一點 adjunctions 充場面。時間難橋啊！距離退伍的時間也愈來愈短嘍…

--
面試地點竟然在中央聯合辦公大樓南棟（上次出差地點）。欸，要穿制服去面試嗎？XD

Fourth offer

昨天家裡收到第三封紙本的 offer letter，是 Clarendon Scholarship 的 funding offer。緊接著今天凌晨就收到第四封 offer letter (by email)，是 Clarendon Scholarship 的更新版，因為 University College 也把它（今年唯一）的 MPLS Scholarship 頒給我了！（讓我開始懷疑我大概是 MPLS division 今年唯一一個進 Univ 的海外人…）這個獎學金是和 Clarendon Fund 合辦的，所以我拿到的總數不變，但頭銜變得更長（Clarendon Scholarship - University College MPLS Scholarship）XD。牛津的學院制讓整個申請過程變得有點複雜，大學、學系、學院各有不同權責，雖然劃分得還算清楚，但有時候會覺得不是很方便，例如大學已經給了全額的 Clarendon Scholarship 但學院還叫我填 financial guarantee form。現在獎學金改由大學和學院個別出錢，倘若 EPSRC grant 和留學獎學金又通過，我的 funding sources 就變成四個，情況會非常複雜吧 XD。

--
"Somehow" 走得有點太順…

University College

第三封 offer letter 原來已經等在家裡，來自 University College。學院的信味道就是不一樣，全部資料看下來，重點差不多就是 financial guarantee。看起來我必須附上獎學金錄取信的正本，但申請簽證好像也要用到，那不就代表我至少需要兩份？唔，反正整個 financial arrangement 也還沒完成，等一陣子再說吧 XD。

--
Comlab 的 offer letter 紙本是被吃掉了？

Transformed, but not yet so naturally

最近再次進攻 natural transformations 和 representations，已經不知道是第幾次嘍。每次讀都有新一層的體悟，或是該說隔閡變得更少了，像現在看到 "natural in X" 至少會有個圖像，不會那麼茫茫然。對於 natural transformations 我已經有 morphisms of functors 的直覺，但說它是 "natural" 就還不太了解 ─ 為什麼這樣的定義就隱寓那一系列的 mappings 是依循同一種方式定義呢？還是先把這問題擱著，今天對付一個特別難纏的 parameter theorem（如果一個 parameterised functor 對每個 parameter value 都有一個 representation，使得 representing object/natural bijection 也是 parameterised，那麼這個 parameterised representation 對於 parameter 也是 natural），準備轉進 adjoint functors 嘍。現在是跟著 Mac Lane & Birkhoff 的 undergraduate algebra 倒數第二章走，走過了再重新挑戰 Mac Lane！

已經收到兩封 email offer letters，一封來自 comlab，另一封今天剛收到，是 Clarendon Scholarship 的正式 offer letter。我先前寄的成績單老早就到英國了，果真是飛快：

Parcel number: EC331371631GB（JK 注：郵包號有變喔，從 TW 變成 GB！）
Status: Delivered
Signed for by: HAMBRIDGE P

Parcel tracks

Date	Time	Location	Tracking Event
04-03-2010	10:10	Oxford Depot	Parcel delivered
04-03-2010	05:49	Oxford Depot	Out for delivery
04-03-2010	05:46	Oxford Depot	Arrived at delivery depot
04-03-2010	01:31	National Hub	Scanned at Hub
03-03-2010	17:07	International Hub	En route to delivery depot
03-03-2010	17:07	International Hub	Arrived in destination country
02-03-2010	03:44	Delivery Agent - TAIPEI - PTT	Left origin country

但 offer letter 紙本都還沒收到。我的 application 現在不知道落在哪家 college，來來往往大概還要再收個兩三封 offer letters 吧 XD。

Offer 永遠不嫌多，scm 老師在我破百當天來信邀我繼續玩一陣子 pi-calculus with dependent types，說他有新的想法。Sounds interesting! 而且我老早就在盤算退伍後回台北窩一下中研院的可能性，參加 FLOLAC '10、申請簽證、聽音樂會什麼的都方便很多。本來打算靠近一點再說，至少也等 scm 老師回國之後，結果被 scm 老師搶先一步，可以說整個被 scm 老師看透了呀！XD 不過這代表我得找短期租屋，租三個月應該勉強可以？

依三人成虎定理，我每次參加 FLOLAC 都會多一個讀牛津的人！XD

--
還積欠好多事情沒寫…

BR067

五天前收到 pdf 版的 offer letter，裡面要我滿足的學術條件是把大學和 IELTS 成績單正本寄過去，昨天就用郵局的國際快捷寄出三張 A4 紙，一張 100 塊 XD。剛剛查進度（EE011705712TW），這三張成績單就要坐今天的 BR067 長榮班機先到英國去啦（9:10AM 出發，經曼谷至 Heathrow，歷時 18 小時）。

--
應該不會少一張吧 XD。

---

突然發現破百了…

--
好快…

DPhil at Oxford University Computing Laboratory, Fully Funded!!

在床上讀《飛狐外傳》到最終一回突然打住，想英國現在正是下午，不如起來收個信。結果真的有信，還來兩封，而且一封掉在 Jeremy Gibbons 的專屬信匣內！

時候終於到了。

我一直不太敢面對我只申請一家的事實，特別是看到身邊眾人動輒投四、五家，並經歷整個申請過程的諸般波折之後，其實暗暗有做心理準備，可能得回中研院待一年。如果真的失敗了，下次自然不能這麼托大，連美國的學校都得納入考量。

幸好看來是沒第二次了。

忐忑打開標題為 "Application to Oxford" 的信，火速一看 ─

Dear Mr. Ko,

I am pleased...

是 "I am pleased" 不是 "We regret"！第一步總算是到位了（因為學費生活費還沒著落呢）。緊接著看完：

Dear Mr. Ko,

I am pleased to inform you that we are able to offer you a place to study for the D.Phil in Computer Science at Oxford University Computing Laboratory under the supervision of Jeremy Gibbons.

We are also able to offer you Clarendon funding which will pay your fees at the overseas rate together with a stipend of approximately £13290 per annum for three years.

Will you please confirm that you will be accepting this funded place by Wednesday 24th February at the latest and I will then prepare the official paperwork.

Many thanks and I look forward to hearing from you.

Julie

--
Julie Sheppard
Graduate Studies Administrator
Oxford University Computing Laboratory
Wolfson Building
Parks Road
Oxford
OX1 3QD

Phone: 01865 273817
Email: julie.sheppard@comlab.ox.ac.uk

Goodness, Clarendon fund! 傳說中去年錄取率只有 7% 的獎學金，還是全額！這下全解決啦，未來三年挑戰由此開始。

--
其他經費來源可能再橋一橋，反正可以確定所有花費都被罩住了，只剩下我的投入啦。