2011/09/26

[facebook digest] ICFP

  1. Call for posters in APLAS'11 announced! ↦ cfpt [The Ninth Asian Symposium on Programming Languages and Systems, APLAS 2011]    [2011-08-31 16:07:35 +0100]  [ 2 人說讚！]
    • T*************** ⇒ Please submit one and attend APLAS + CPP 2011!    [2011-09-01 02:54:40 +0100]
    • L************** ⇒ Considering submitting a poster on coequational presentation if I can work it out on time...    [2011-09-02 00:43:24 +0100]
  2. Wha-ha, now I cannot call the WGP slides an adaptation of the DTP version — they are basically a new set of slides...    [2011-09-01 14:38:02 +0100]
  3. 觸鍵要多下點功夫了⋯    [2011-09-01 19:06:05 +0100]  [ 1 人說讚！]
  4. 「你必須愛上一塊石頭，」斯文嚴肅地說。「你看過成打的石頭，你說，啊！不對我的胃口。然後你看到那一塊，細緻又優雅的一塊，你就愛上它了。就和女人一樣。但接踵而至的婚姻卻很可怕。你拚命抵抗，但石頭堅硬無比。你好絕望，然後，剎那之間，彷彿蠟一般，石頭在你手裡融化了，於是你塑出一個形象。」    [2011-09-01 20:06:14 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ Gerald Durrell. Chapter 11, Birds, Beasts, and Relatives. 唐嘉慧譯。    [2011-09-01 20:06:53 +0100]
    • 洪** ⇒ 挖...難得你寫了中文,不過我還是看不懂    [2011-09-02 05:56:46 +0100]
    • Josh Ko ⇒ 練琴和這個有類似的感覺。    [2011-09-02 08:30:01 +0100]
    • 洪** ⇒ 都是我不懂的感覺拉!阿你啥米時候回台灣阿?    [2011-09-02 12:06:54 +0100]
    • Josh Ko ⇒ 可能十二月吧。    [2011-09-02 16:44:04 +0100]
  5. I guess I'll just stick to a slower Ocean..    [2011-09-02 16:36:39 +0100]
  6. Pressing the "Intensify" button (à la iPhoto) for my music.    [2011-09-02 20:02:03 +0100]
  7. Ocean 這樣練下來，手應該是有比較強壯啦，可是愈彈愈快，每次彈完還是很痠⋯    [2011-09-03 18:11:50 +0100]  [ 1 人說讚！]
  8. Zimerman 那個線條之流暢靈動⋯ 真是無話可說。    [2011-09-03 21:58:15 +0100]
  9. Skipping algebraic ornamentation for the WGP talk.    [2011-09-05 09:41:06 +0100]  [ 1 人說讚！]
    • L************** ⇒ I'd like to see your slides...    [2011-09-05 10:07:11 +0100]
    • Josh Ko ⇒ Not finished yet. XD    [2011-09-05 13:15:52 +0100]
  10. The PhD movie will be screened at Exam Schools in November, organised by the MPLS division! ↦ http://www.jorgecham.com/screenings/screening_info.php?p=oxford    [2011-09-05 18:42:09 +0100]
  11. (Finally) reusing the slides for function upgrade and ornament fusion.    [2011-09-05 20:37:36 +0100]
  12. 東京電玩展 17, 18 號開放參觀 — 17 號剛好是我到日本的第一天！可是我現在對電玩沒什麼興趣了⋯    [2011-09-05 21:36:35 +0100]  [ 4 人說讚！]
  13. An excerpt of a comment: "Many talks by PhD students are just horrible. Especially the Asian students that lack sufficient English skills to give a talk. I've attended lots of these that are nothing but painful to sit through." Hm, so allow me to plan and practise a lot in advance.. ↦ Are You Talking to Me?    [2011-09-06 08:39:21 +0100]  [ 1 人說讚！]
    • 黃** ⇒ 題外話：我一直覺得Vardi留那個鬍子感覺非常權威，不過據說他是一個非常nice的人.    [2011-09-06 15:33:36 +0100]
    • Josh Ko ⇒ 我和他在 IIS 的電梯裡聊過兩句，他知道牛津有條 Logic Lane..    [2011-09-06 17:44:29 +0100]
  14. I think I have the slides for WGP. Without mentioning (ornamental-) algebraic ornamentation, the slides look simpler — even weaker. But I believe the central idea — exploiting the connection between internalism and externalism to structure internalist libraries modularly — is successfully highlighted.    [2011-09-06 14:55:01 +0100]
    • Josh Ko ⇒ I should perhaps put some backup slides explaining algebraic ornamentation after the "Thanks!" slide.    [2011-09-06 15:04:15 +0100]
  15. Op 62 No 2 好像快熟了。    [2011-09-06 19:13:41 +0100]
  16. Transfer application submitted!    [2011-09-07 11:04:52 +0100]  [ 4 人說讚！]
  17. And I'll submit a poster on the Dutch National Flag problem to APLAS'11!    [2011-09-07 11:52:25 +0100]  [ 1 人說讚！]
  18. 我彈的時候聽到的東西和錄音聽到的東西愈來愈接近了，很好。    [2011-09-07 18:27:25 +0100]  [ 4 人說讚！]
  19. "If programming language design is to become a science, we need more experiments like this one."

    I have doubts, though. We should take empiricists seriously, but I am not sure this kind of experience is really relevant. ↦ Wadler's Blog: An experiment about static and dynamic type systems    [2011-09-07 19:27:52 +0100]
  20. I am wondering whether I can redo the derivation of the linear time solution to the maximum segment sum problem with ornamentation?    [2011-09-07 21:24:16 +0100]
    • Josh Ko ⇒ I would guess that it's possible using only algebraic ornamentation, given the fact that only fold fusion is used in the derivation.    [2011-09-07 21:27:12 +0100]
    • Josh Ko ⇒ Maybe all it takes is take the slides from the Program Derivation course in FLOLAC'07 and rewrite them with inductive families.    [2011-09-07 21:31:23 +0100]
  21. Another Dijkstra's argument for pure symbolic reasoning. ↦ SpringerLink - Abstract    [2011-09-07 23:00:17 +0100]
    • Josh Ko ⇒ I hope the argument does not eventually lead to the conclusion that "we should delegate the job to automatic theorem provers since they can manipulate and produce symbols better than we can." To me that's a contradiction: The symbolic derivations (even short ones) they produce do not necessarily constitute a justification for us — they can well be incomprehensible. For the symbols to convince us that a theorem is correct, an interpretation is unavoidable.    [2011-09-07 23:01:15 +0100]
  22. 秋葉原是不可不逛的，應該就排在 23 號，可能再搭配一兩個看風景的地方。東京電玩展⋯欸⋯看一下門票和時間好了，不然 17 號 4:55AM 就到羽田機場也不知道要幹嘛。    [2011-09-08 14:52:26 +0100]  [ 4 人說讚！]
    • 翁** ⇒ 你要去日本丸喔!!!    [2011-09-08 14:54:01 +0100]
    • Josh Ko ⇒ 要去開會！XD    [2011-09-08 14:54:14 +0100]
    • Josh Ko ⇒ 有推薦東京景點嗎？    [2011-09-08 14:54:29 +0100]
    • 翁** ⇒ 看你要去多久阿~建議去背包客棧查看看    [2011-09-08 14:55:01 +0100]
    • E********* ⇒ 秋葉原不錯! 會有很多女僕在路上發傳單 XD    [2011-09-08 14:55:31 +0100]
    • Josh Ko ⇒ Wikitravel 說秋葉原毫無疑問是御宅族的集中地，看日本動畫看這麼久不去一下說不過去呀 XD。（雖然熱血勇者系的可能很冷門了⋯）    [2011-09-08 14:58:00 +0100]
    • C********* ⇒ 淺草寺傍晚去,仲見世通的街燈打亮時會更熱鬧有趣    [2011-09-08 16:27:41 +0100]
    • C************ ⇒ 女僕咖啡廳不得不逛阿，那是經典景點!!XD    [2011-09-08 17:46:15 +0100]
    • Josh Ko ⇒ @ 嚴老師：謝謝！應該會排到行程裡面！
      @ 舉哥：連我們 group 的英國人都知道有 "maid café"，還說日本男性心理真是奇妙，喜歡這種東西（不過他們很想去見識一下 XD）。    [2011-09-08 18:12:01 +0100]
    • 柯** ⇒ 幾月幾號要去？去幾天？    [2011-09-09 04:00:46 +0100]
    • Josh Ko ⇒ 九月 16–24.    [2011-09-09 08:06:59 +0100]
    • 柯** ⇒ 日本的玉子燒以前我煎給你吃時你都很喜歡，這次去東京你可以外帶玉子燒到宿舍，我想你會印象深刻的，給你一個網址，自己可以google一下除了這個網址的"大定"這家外，是否還有別家有名、更好吃~http://blog.yam.com/venuslin0113/article/12079017    [2011-09-09 11:17:45 +0100]
    • 柯** ⇒ 忍不住再po一個網址給你： http://blog.xuite.net/maomi/Food01/9235005    [2011-09-09 11:20:22 +0100]
    • 柯** ⇒ 最後一個網址啦~~萬用型的喔！ http://taicphoto.myweb.hinet.net/    [2011-09-09 11:23:00 +0100]
  23. 目前的 Op 62 No 2.
    http://sites.google.com/site/joshkos/Op62No2_20110908.mp3    [2011-09-08 18:19:03 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ Hm, 還有不少地方可以再精雕細琢一番。    [2011-09-08 18:45:16 +0100]
  24. Op 55 No 1 愈彈愈爛⋯不過這種情況也不是第一次了。    [2011-09-08 19:04:05 +0100]
    • J********** ⇒ 是那部鋼琴來亂的啦~~    [2011-09-08 19:44:37 +0100]
    • Josh Ko ⇒ 鋼琴已經特別挑過，不能怪它了 XD。    [2011-09-08 19:50:43 +0100]
    • J********** ⇒ 我不管><    [2011-09-08 19:51:35 +0100]
  25. 細讀一次 Op 62 No 2 的譜。啊，想把那堆極其隱晦的細節（subtlety）都彈出來不知道要練多久⋯    [2011-09-08 20:14:27 +0100]
    • Josh Ko ⇒ “You have no subtlety, Potter,” said Snape, his dark eyes glittering. “You do not understand fine distinctions. It is one of the shortcomings that makes you such a lamentable potion-maker.”    [2011-09-08 20:19:47 +0100]
  26. They LIKED my talk..!!! ↦ /home/laney/.irssi/irclogs/Freenode/2011/#agda/August.log    [2011-09-08 21:36:07 +0100]  [ 3 人說讚！]
    • Josh Ko ⇒ ‎[wires_] augur, Saizan on DTP 2011 two days ago there was a nice talk explaining ornaments
      [augur] oh?
      [Saizan] yeah, i wanted to go :\
      [augur] whats DTP
      [wires_] http://www.cs.ru.nl/dtp11/program.html
      [wires_] see the talk by Josh Ko
      [Saizan] were the talks filmed?
      [augur] oh that explains why conor was tweeting about nijmegen
      [wires_] sadly, not filmed
      [wires_] i brought a camera but forgot to use it
      [wires_] did record a little bit of conors talk, which was very entertaining as usual
      [kosmikus] :)
      [wires_] hehe
      [wires_] Josh explained it really nicely, so it's a bummer that it wasn't recorded
      [wires_] But his slides are very nice too
      [kosmikus] Josh's talk was great
      [wires_] agreed, many talks were great
      [kosmikus] yes, but this was one I didn't know what to expect of (hadn't looked at the paper before, didn't know the speaker)
      [kosmikus] so it was unexpectedly great    [2011-09-08 21:39 +0100]
    • E********* ⇒ Good job!!! :D    [2011-09-08 21:41 +0100]
    • Josh Ko ⇒ When I saw the comments my eyes were momentarily filled with tears of joy.. XD    [2011-09-08 21:44:59 +0100]
    • J************* ⇒ Well done!    [2011-09-09 16:34:14 +0100]
  27. Assessors confirmed: Ralf and Tom Melham!    [2011-09-09 09:14:54 +0100]  [ 1 人說讚！]
    • J********** ⇒ 電死他們!!    [2011-09-09 11:46:47 +0100]
    • Josh Ko ⇒ 是被電死吧⋯    [2011-09-09 11:56:25 +0100]
    • J********** ⇒ 我是說, 他們 mentally 電你, 你就 physically 電回去 (日本那邊應該買得到電擊棒吧?!)    [2011-09-09 11:58:11 +0100]
    • Josh Ko ⇒ 說不定帶不上飛機⋯    [2011-09-09 14:07:18 +0100]
    • J********** ⇒ 買樂高的    [2011-09-09 14:14:42 +0100]
  28. Looks like a strong argument. (However, I wouldn't say tau/pi is right/wrong, only convenient/redundant.) ↦ No, really, pi is wrong: The Tau Manifesto    [2011-09-10 07:16:19 +0100]
    • L********* ⇒ Just want to replace symbol Pi with Tau??    [2011-09-10 07:48:07 +0100]
    • Josh Ko ⇒ No, tau = 2pi.    [2011-09-10 08:03:44 +0100]
    • L********* ⇒ Haha, I took just five seconds to read it.    [2011-09-10 08:12:38 +0100]
  29. Exercise 2.4.15 from Barendregt: Suppose a symbol of the lambda-calculus alphabet is always 0.5cm wide. Write down a lambda-term with length less than 20cm having a nf with length at least 10^10^10 lightyear. The speed of light is c = 3.10^10 cm/sec.    [2011-09-10 08:05:41 +0100]
  30. Regarding tau vs. pi: Is there any empirical experiment that can provide sound support for any of the sides? (This is related to Wadler's comment on "programming language design as a science".)    [2011-09-10 08:29:56 +0100]
    • Josh Ko ⇒ This one, perhaps..
      http://tauday.com/a-tau-testimonial    [2011-09-10 08:31:18 +0100]
    • Josh Ko ⇒ The problem with this "experiment" is that the factor of using tau instead of pi is not isolated - it could be the whole restatement that makes the difference, for instance.    [2011-09-10 09:59:39 +0100]
    • Josh Ko ⇒ And I cannot imagine that the experimental result can be reproduced precisely..    [2011-09-10 10:01:00 +0100]
  31. I am really a slow writer..    [2011-09-11 09:52:45 +0100]  [ 1 人說讚！]
    • 翁** ⇒ 慢工出細活?    [2011-09-11 11:29:15 +0100]
    • Josh Ko ⇒ 希望是有那個細度啦⋯    [2011-09-11 12:17:49 +0100]
  32. "It's tough to design new programming languages and tougher to get them established. The payoff, though, can take several forms: higher programmer productivity, software that runs more efficiently, hardware features that can be tapped."

    Hm, only efficiency concerns, no mention of correctness.. ↦ Google to debut Dart, a new language for the Web    [2011-09-12 09:20:41 +0100]
    • P************* ⇒ no idea how their Go is going....    [2011-09-12 09:29:20 +0100]
  33. 6 days to WGP - already looking forward to meeting Shin again (who together with Jeremy will presumably introduce a lot of famous people to me)! But before that I really need to get my talk ready..    [2011-09-12 21:52:19 +0100]
    • Josh Ko ⇒ Shin (presumably) is going to present his first ICFP paper, and I my first first-author paper, so the event is a milestone for both of us!    [2011-09-12 21:56:15 +0100]
    • Josh Ko ⇒ And I'm curious what Jeremy's talk will be like — I've never heard him give a talk before. (AoP meetings are informal..) Particularly, I'd love to know how he will interpret my DTP slides, but since I won't go to that workshop, I can only hope to see him present his axiomatic monadic reasoning paper in ICFP.    [2011-09-12 22:03:29 +0100]
    • Josh Ko ⇒ Personally I feel that the WGP slides are less interesting than the DTP version, but anyway..    [2011-09-12 22:19:59 +0100]
  34. "Hang out with your supervisor... for the purpose of meeting people, not comfort. (But don’t be a nuisance.)" ↦ http://www.cs.ox.ac.uk/teaching/dphil/talk.pdf    [2011-09-12 22:26:14 +0100]
    • Josh Ko ⇒ I think Comlab does an adequate job in getting students ready for the academia. Andrew's talk on presentation skills was very helpful, and the information in this set of slides by Tom Melham is very useful, too.    [2011-09-12 22:29:15 +0100]
  35. Hm, I think there's a Galois connection between the Desc universe and the Orn universe..    [2011-09-13 07:44:49 +0100]
    • Josh Ko ⇒ It is likely that Conor has already noticed that: He used the floor function symbol for the translation of ornaments to descriptions.    [2011-09-13 07:55:34 +0100]
  36. Inverse Function Theorem.. ah, painful memories... ↦ The inverse function theorem for everywhere differentiable maps    [2011-09-13 08:12:42 +0100]  [ 1 人說讚！]
  37. Still, only Op 62 No 2 can be described as adequate. I am still struggling to reach an acceptable speed for the ocean etude (and it seems that the struggle is going to last for quite a long time). Even Op 9 No 2 is substandard. I think now is indeed a good time to leave the piano for a while, exercising my musical imagination instead.    [2011-09-14 20:28:20 +0100]
  38. 東京電車有辦法弄得這麼複雜確實不簡單⋯    [2011-09-15 09:04:13 +0100]  [ 2 人說讚！]
    • P************* ⇒ 倫敦地鐵可以弄的這麼髒 車上沒有空調 空氣超差 收費居然還這麼高 也是非常不簡單    [2011-09-15 11:10:57 +0100]
  39. 目前唯一結論：到羽田先買張 Suica 再說⋯    [2011-09-15 09:36:10 +0100]  [ 1 人說讚！]
    • C************ ⇒ 可以買passmo卡    [2011-09-15 10:43:42 +0100]
    • Josh Ko ⇒ 我查到的資料是說在東京裡兩張卡沒差別。所以⋯都可以？    [2011-09-15 10:52:44 +0100]
    • L************** ⇒ Suica!! 會印吉祥物上去嗎？    [2011-09-15 11:04:29 +0100]
    • Josh Ko ⇒ 好像會？
      http://en.wikipedia.org/wiki/File:Suica.jpg    [2011-09-15 11:07:18 +0100]
    • L************** ⇒ 可不可以收購你用剩的 Suica? XD    [2011-09-15 11:13:18 +0100]
    • Josh Ko ⇒ 回來再看看吧 XD。    [2011-09-15 11:19:24 +0100]
    • C************ ⇒ http://kunghc.pixnet.net/blog/post/27313597-%E7%BE%BD%E7%94%B0%E6%A9%9F%E5%A0%B4%E9%80%B2%E6%9D%B1%E4%BA%AC%EF%BC%8C%E4%B8%8D%E5%8F%AF%E4%B8%8D%E7%9F%A5%E7%9A%84%E5%84%AA%E6%83%A0%E4%BA%A4%E9%80%9A%E7%A5%A8%E5%88%B8%E6%95%B4    [2011-09-15 14:43:08 +0100]
    • C************ ⇒ 前些日子去東京也是買PASMO，原因是因為有外國人優惠套票，簡單來說就是羽田到品川是400円，但PASMO+來回套票600円(總之是省200円....XD)    [2011-09-15 14:46:09 +0100]
    • Josh Ko ⇒ 了解。不過我是羽田進成田出，用不到來回票⋯ 還是謝啦！    [2011-09-15 14:56:45 +0100]
  40. 我對山手線的唯一印象是「扒手」：怪醫黑傑克有一集是山手線的扒手慣犯扒到黑道被切斷手指，長期追捕他的警官找黑傑克去把手指完美地接回去，讓他可以繼續偷，警官才可以繼續追捕他 (?!)。    [2011-09-15 09:42:13 +0100]  [ 2 人說讚！]
    • 楊** ⇒ 這啥鬼道理...    [2011-09-15 12:53:17 +0100]
    • L********* ⇒ 警察永遠抓不完小偷的道理 XD    [2011-09-15 14:58:30 +0100]
    • C************ ⇒ 好閒的警察~沒事找事做XD    [2011-09-15 16:05:22 +0100]
  41. 這時候就有點後悔沒好好研究一下勇者特急裡的多款列車，去就不能享受指認拍照的樂趣了。    [2011-09-15 09:45:54 +0100]
  42. 從東京電玩展的海濱幕張站到神保町站好像要轉不少次。啊，不管啦，到時候按圖索驥了。    [2011-09-15 09:55:16 +0100]  [ 2 人說讚！]
  43. Now on board the X70 (again), leaving for the legendary ICFP.    [2011-09-16 05:34:06 +0100]
  44. 這班早上五點到羽田的班機根本是為了要排東京電玩展的隊而設計得這麼早的嘛！經歷約三小時日曬雨淋風吹，十點十五分成功進入會場，現在是用免費提供的無線網路。    [2011-09-17 03:04:29 +0100]  [ 4 人說讚！]
  45. 來到日本頓時覺得自己英文真好！XD    [2011-09-17 03:08:21 +0100]  [ 4 人說讚！]
    • 陳** ⇒ WOW, 去參加研討會嗎XD    [2011-09-17 03:17:37 +0100]
    • Josh Ko ⇒ Yes. 海關官員的日本腔之重，我很驚訝我竟然不用請他們複述 XD。    [2011-09-17 03:20:53 +0100]
  46. In English: I am now at the Tokyo Game Show! (But I am really more attracted to the free wifi rather than the show itself.. XD)    [2011-09-17 03:32:19 +0100]
  47. 早上六點多接到 JR 京葉線新木場站的時候，突然宅氣沖天，已經有小撮人群聚集要往海濱幕張站了。到站後只要跟著人群走就行，才七點會場已經排成一大條長龍，但看現場佈置還離高峰遠得很⋯    [2011-09-17 03:44:39 +0100]  [ 4 人說讚！]
    • Josh Ko ⇒ 補充：入場時間是十點。    [2011-09-17 03:45:44 +0100]
    • Josh Ko ⇒ 主辦單位嚴禁過夜排隊，不然我想我就可以直接放棄了⋯    [2011-09-17 03:46:35 +0100]
  48. 看到海龜按讚才想到：有個小小的攤位是 SIGGRAPH Asia 2011 的樣子，但是剛進場的時候看沒擺什麼東西。    [2011-09-17 03:58:04 +0100]
    • C*********** ⇒ SIGGRAPH 2011 的時候也是這樣. 擺個桌子讓人拿傳單而已.    [2011-09-17 04:15:54 +0100]
  49. Hm, 聽到工作人員大喊一連串聽不懂的日語還是有點心慌。    [2011-09-17 04:09:08 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ 那些喊話幾乎都是「那賽」結尾，這是某種敬語吧？    [2011-09-17 04:09:55 +0100]
    • 楊** ⇒ 類似語尾助詞吧    [2011-09-17 04:41:17 +0100]
    • 洪** ⇒ 那你就大喊中文讓他也聽不懂：）    [2011-09-17 06:58:19 +0100]
  50. 想睡但是才中午，待會回飯店也應該再練習一下明天的 talk。不知道為何，一直練不到有一定程度的把握。    [2011-09-17 04:14:16 +0100]  [ 1 人說讚！]
    • C*********** ⇒ 這是時差吧    [2011-09-17 04:14:59 +0100]
    • Josh Ko ⇒ Yes, I think so..    [2011-09-17 04:49:37 +0100]
  51. Now I am thinking about just practising my talk right here, right now.. Hm, so the show indeed does not attract me. Perhaps I'll just go in once more, walk around for a while, and then get out and stay in the free WiFi area..    [2011-09-17 04:56:07 +0100]
  52. Arrived at the hotel, 1 hour than I expected.    [2011-09-17 08:12:58 +0100]
    • Josh Ko ⇒ 1 hour "later"    [2011-09-17 11:42:47 +0100]
  53. 連 ptt/ptt2 愈快代表離家愈近。    [2011-09-17 08:14:08 +0100]  [ 4 人說讚！]
    • L********* ⇒ 所以你家住在台大？ XDD    [2011-09-17 08:16:42 +0100]
    • Josh Ko ⇒ 台灣各都市的連線速度應該感覺不出差別吧 XD。    [2011-09-17 08:18:20 +0100]
    • L********* ⇒ 哈哈，那是理論上；實際上市區和「電信」市郊還是有差的，用3G上網更慢 XD    [2011-09-17 08:30:50 +0100]
  54. 總覺得投影片到後段有亂流出現 — 可能是因為直接從 DTP 版借過來的關係⋯    [2011-09-17 13:20:05 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ 晚上這一次有比較順，看來睡飽是最重要的。    [2011-09-17 13:25:57 +0100]
    • Josh Ko ⇒ 倒數十二個小時的時候還加了一句，希望不會出差錯。    [2011-09-17 13:40:10 +0100]
  55. It's really great to be able to give my talk in the first session on the first day, so I can fully enjoy the rest of ICFP! BTW, the hotel is wonderfully tidy, fully living up to the hype about Japanese hotels. In particular, the toilet is equipped with an advanced cleaning device and can be heated, and the entire bathroom is so shinily clean that I hesitated to use it!    [2011-09-17 22:30:09 +0100]  [ 2 人說讚！]
  56. 如果從日本搬一個免治馬桶座回去會不會太熱血了？XD    [2011-09-17 22:36:23 +0100]  [ 4 人說讚！]
    • P************* ⇒ 英國的廁所有插座可以插嗎    [2011-09-17 23:02:03 +0100]
    • Josh Ko ⇒ 不知道 XD。    [2011-09-17 23:31:03 +0100]
  57. 早餐吃得下，希望是好徵兆。待會再練一遍。    [2011-09-17 23:32:04 +0100]  [ 4 人說讚！]
    • 賴** ⇒ 鋼琴?    [2011-09-17 23:36:38 +0100]
    • Josh Ko ⇒ 報告我的論文！    [2011-09-17 23:39:45 +0100]
    • 賴** ⇒ 加油^^    [2011-09-17 23:40:00 +0100]
    • Josh Ko ⇒ 這場應該會錄影；我準備穿邪惡娃娃頭的黑 T-shirt，錄起來效果應該會不錯。    [2011-09-17 23:41:08 +0100]
    • 陳** ⇒ 到時伸影片連結? XD    [2011-09-18 03:00:03 +0100]
  58. Given my talk. The ML guys next doors clapped just after I showed the animation of ornament fusion, at the right time.    [2011-09-18 06:02:42 +0100]  [ 1 人說讚！]
  59. The talk itself went ok, though not close to perfect. During the discussion time I just couldn't form complete sentences, even though I knew what I intended to say. Perhaps it was due to jet lag.. Anyway, I will try to courageously watch the recording afterwards.    [2011-09-18 06:06:09 +0100]
  60. Met Oleg and finally the lengendary Ken (who looks much younger than I had expected) during lunch.    [2011-09-18 06:07:22 +0100]
  61. Of course we'd love to have some kinds of derivations for internalist programs, but we are really in short of fine examples of internalist programs, so there are not many things to derive!    [2011-09-18 14:47:28 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ My hope is, of course, that I can add a "yet" at the end of the comment. It's certainly one direction I am very interested in, namely rewriting more sophisticated algorithms in the internalist style.    [2011-09-18 19:05:18 +0100]
  62. Oleg & Ken invited me to the tutorial session of their continuation workshop on Friday evening. It will be a gentle introduction to (delimited) continuations, which I think is a very nice opportunity to learn about the topic (which I don't understand, sadly).    [2011-09-18 19:13:49 +0100]
    • Josh Ko ⇒ Just sent a registration email.    [2011-09-18 19:34:14 +0100]
  63. Failed spectacularly to sleep again after I woke up at 3am, about three and a half hours ago.    [2011-09-18 22:35:47 +0100]
  64. I am thinking about whether it is possible for the ornament framework to subsume "datatype à la carte". For now it seems I need new constructs like "strong deletion" and "ornament co-fusion". (Hm, this is easily confused with "confusion"?)    [2011-09-19 12:21:41 +0100]
    • Josh Ko ⇒ It looks like that these new constructs are dual to what we've got right now (field insertion/refinement and ornament fusion); if we form any categorical characterisation of ornaments, it must be able to give a satisfactorily clear explanation about this duality (in particular).    [2011-09-19 12:27:47 +0100]
    • Josh Ko ⇒ Second thought: "Co-fusion" is indeed confusing - I haven't figured out even whether there is such a construction.    [2011-09-19 12:37:37 +0100]
    • Josh Ko ⇒ And there is always the danger of making the ornament language unnecessarily complicated.    [2011-09-19 12:41:23 +0100]
    • J************* ⇒ The opposite of "fusion" is "fission", isn't it?    [2011-09-19 15:07:20 +0100]
    • Josh Ko ⇒ I was thinking not about tearing datatypes apart but another way of fusing datatypes. It is not clear to me now whether this idea makes sense, though.    [2011-09-19 18:15:05 +0100]
  65. Finally had an acceptably good sleep.    [2011-09-19 22:38:42 +0100]  [ 1 人說讚！]
    • J************* ⇒ Just in time to head home :-).    [2011-09-20 07:02:33 +0100]
  66. I see! I think this is something I wish to see in an internalist solution to MSS: a precise description of how the final program computes the optimal solution. ↦ Trek through Pure Reason: Maximum Segment Sum 的成長故事    [2011-09-20 00:17:33 +0100]
    • Josh Ko ⇒ And it might be like translating the functional derivation to a "datatype" derivation.    [2011-09-20 00:19:06 +0100]
    • Josh Ko ⇒ It is possible that this would degenerate to using some trivial internalist type, however. Of course, I hope it's not the case..    [2011-09-20 20:36:03 +0100]
  67. 定風波．蘇軾

    （王定國歌兒柔奴，姓宇文氏，眉目娟麗，善應對。家住京師。定國南遷歸，余問柔：「廣南風土，應是不好？」柔對曰：「此心安處，便是吾鄉。」因為綴詞云。）

    常羨人間琢玉郎，天應乞與點酥娘。自作清歌傳皓齒。風起。雪飛炎海變清涼。　　萬里歸來年愈少。微笑。笑時猶帶嶺梅香。試問嶺南應不好。卻道。此心安處是吾鄉。    [2011-09-20 23:42:35 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ 想回牛津的家，有感。    [2011-09-20 23:46:12 +0100]
  68. Yesterday Patrik, the co-author on AoPA I had never met in person, told me that he was impressed that I gave the talk very clearly, despite that I am Asian. Hm, so perhaps my English is not as bad as I imagined. Anyway, I'll be able to see for myself what the talk was like when the video goes online.    [2011-09-21 00:11:49 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ And Andres Löh came forward to me after the talk to say that he enjoyed both of my talks. That was really encouraging!    [2011-09-21 00:19:32 +0100]
  69. Now that the WGP talk was delivered, my job on the OAOAOO paper can be considered finished, and it is time that I do some interesting new work — which is hard. But well, no one says it's easy..    [2011-09-21 00:22:49 +0100]
    • W********* ⇒ 雖然知道OAO是縮寫 但你不覺得很像表情符號嗎XD 還可以切成好幾個位置來看    [2011-09-21 02:48:01 +0100]
    • Josh Ko ⇒ 反正只是 internal code name XD.    [2011-09-21 03:08:32 +0100]
  70. Presumably this is the final version of the webpage for OAOAOO.
    http://www.cs.ox.ac.uk/people/hsiang-shang.ko/OAOAOO/ ↦ Department of Computer Science, University of Oxford: Publication - Modularising inductive families    [2011-09-21 00:27:28 +0100]
    • Josh Ko ⇒ Actually no: I will put a link to the video recording after it's online.    [2011-09-23 19:51:12 +0100]
  71. But, naturally, it's still difficult to chat with Oleg, who simply knows so much. I don't think this situation will improve in the near future..    [2011-09-21 00:31:09 +0100]
    • W************ ⇒ It's time to improve the situation. I believe you can do it better.    [2011-09-21 00:52:35 +0100]
  72. Bump into a Japanese typhoon.. (Its direction is different from those of Taiwan!)    [2011-09-21 00:54:08 +0100]
  73. 被困在 ICFP 會場了… 日本颱風也挺強的嘛！    [2011-09-21 09:08:33 +0100]
    • L********* ⇒ 是那個傳說不會侵台的ROKE嗎？沒想到剛好讓你在日本碰上 XD    [2011-09-21 13:30:57 +0100]
    • Josh Ko ⇒ 正是。會場外面一棵樹還被吹倒在路上。    [2011-09-21 13:32:00 +0100]
    • L********* ⇒ 有沒有離家很近的感覺 XDDDD    [2011-09-21 13:35:48 +0100]
    • Josh Ko ⇒ 剛剛還來個小地震，應該不是錯覺吧⋯    [2011-09-21 14:32:47 +0100]
  74. Held in Asia for the first time, beginning with an earthquake and making it all the way to a typhoon, this year's ICFP will truly be legendary.    [2011-09-21 11:47:24 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ I am lucky enough to be able to stay in a hotel nearby. Lots of people are still taking shelter at the venue, as the public transport system almost shuts down.    [2011-09-21 11:56:06 +0100]
    • L******* ⇒ Take good care!    [2011-09-21 12:38:46 +0100]
    • Josh Ko ⇒ I heard that the typhoon has left Tokyo. It's all calm now.    [2011-09-21 13:12:42 +0100]
  75. Earthquake.. long time no see.    [2011-09-21 14:32:18 +0100]  [ 1 人說讚！]
    • L********* ⇒ 所以英國除了暴風雪或暴雨之外好像沒什麼其他天災！？    [2011-09-21 14:48:53 +0100]
    • Josh Ko ⇒ 是啊，滿平靜的 XD。    [2011-09-21 14:51:12 +0100]
  76. Brightly sunny again today! Hope it's the same tomorrow.    [2011-09-22 00:51:12 +0100]  [ 1 人說讚！]
  77. To avoid binding oneself with a particular pair of a basic universe and a corresponding universe, there seems to be two approaches, one extensional and another intensional:    [2011-09-22 02:46:52 +0100]
    • Josh Ko ⇒ The extensional approach is an axiomatic one, listing the essential properties for two datatypes to be ornamentally related;    [2011-09-22 02:51:32 +0100]
    • Josh Ko ⇒ the intensional approach pushes datatype-generic programming to an extreme (perhaps inspired by The Art of Gentle Levitation), using a sufficiently powerful (adjoint) pair of basic and ornament universes to describe generically how an ornament universe can be derived from a basic universe.    [2011-09-22 02:58:06 +0100]
    • Josh Ko ⇒ I'd love to explore both approaches (and relate them!), but it's not obvious to me how either of them can be done yet.    [2011-09-22 03:01:49 +0100]
  78. 美國腔很刺耳…    [2011-09-22 06:19:39 +0100]  [ 2 人說讚！]
    • N*********** ⇒ 深有同感！！    [2011-09-22 11:55:49 +0100]
    • 柯** ⇒ 你感染了英國病    [2011-09-22 13:10:13 +0100]
  79. 明天早上淺草寺，下午秋葉原好了，買模型比較方便 XD。（晚上有 continuation workshop 附設的 tutorial.）    [2011-09-22 11:19:42 +0100]  [ 2 人說讚！]
    • 陳** ⇒ 學長準備好銀彈了嗎XD    [2011-09-22 11:27:37 +0100]
  80. I didn't take any photo in this trip, which I now slightly regret. Nevertheless, I intend to write a long blog post on this trip, as I used to do, and a retrospect of the past year, as I usually do. (I plan to write both of them in Chinese and then translate them into English.) Hopefully after I finish this task I will have overcome the jet lag and can resume my research work (instead of presentations, which I like but should not spend too much time on) - I've now got some potentially interesting (but still vague) ideas to try!    [2011-09-22 17:12:33 +0100]  [ 2 人說讚！]
    • 翁** ⇒ j應該要拍照的~    [2011-09-22 17:25:33 +0100]
    • Josh Ko ⇒ 第一天到東京就要一個人坐單軌電車、地鐵、火車到語言幾乎不通的東京電玩展，飛機上又沒怎麼睡到，又累又緊張的情況下就沒想要拍照，接下來乾脆也比照辦理 XD。    [2011-09-22 17:32:23 +0100]
    • 翁** ⇒ 喔~太可惜了!!!!去那邊就是要拍拍拍~~~    [2011-09-22 17:34:09 +0100]
    • 柯** ⇒ 沒圖沒真相丫……    [2011-09-23 04:12:50 +0100]
  81. Just received a notification about the departmental student conference this year. If I participate, I can simply give my WGP talk again, but I don't feel like talking about it once more - in fact I am getting tired of it (and the fact that it's the only thing I can talk about) and think I should really move on to something new. So I intend to skip the conference (unless someone can convince me not to do so).    [2011-09-22 17:24:20 +0100]
    • J************* ⇒ How about a talk on what you intend to do next? Perhaps thinking about the talk will help in planning.    [2011-09-23 01:15:08 +0100]
    • Josh Ko ⇒ I didn't know that's a plausible topic for the student conference! Well, still, I prefer giving a talk on something more substantial.. (Writing a proposal for transfer is quite enough guesswork, I think..)    [2011-09-23 05:27:19 +0100]
  82. 結果淺草寺 + 秋葉原只逛了兩個多小時！淺草寺不大就算了，秋葉原的東西我都滿陌生，機器人只認得 Eva 和 Wing Zero。這樣自然沒什麼看頭，中午就回旅館了。    [2011-09-23 05:14:56 +0100]
    • Josh Ko ⇒ 喔，是有看到 GaoGaiGar 和 Great Ganbarugar 啦，可是都小小隻的，一點都不熱血。（一家店門口有等身大小的初號機，可是我沒很喜歡 Eva..）    [2011-09-23 05:30:53 +0100]
  83. 中午吃旅館對面、晚上不開的拉麵店。販賣機上看到「味噌 XXX 半 XXXX」600 元，上來竟然是一碗味噌拉麵（這很難猜錯）+ 一盤炒飯！單看麵或飯的份量還好，加在一起就有點嚇人，幸好有吃完。這次拉麵的味道有達到想像中的鹹度了（上次和 scm 老師去吃的那家沒很鹹）。    [2011-09-23 05:19:46 +0100]  [ 1 人說讚！]
  84. My first ICFP ends tonight and nicely concludes my first year as a DPhil student. Heading back to Oxford tomorrow.    [2011-09-23 13:50:52 +0100]  [ 4 人說讚！]
  85. It took me quite a while to determine which route to take to reach Narita airport..    [2011-09-23 15:53:19 +0100]  [ 1 人說讚！]
  86. Now at the boarding gate. Will need to explain to UK border control 14 hours later why I have an unstamped visa (in my previous passport) but in fact am not entering the UK as a student for the first time.    [2011-09-24 01:06:54 +0100]
  87. The flight is.. er.. what is the antonym for delay? Anyway, we will depart 10 minutes earlier than scheduled. I suspect this is an extremely rare situation?    [2011-09-24 01:11:37 +0100]
  88. As expected, I needed to "discuss" with the immigrations officer about my visa.    [2011-09-24 16:56:19 +0100]  [ 1 人說讚！]
    • J************* ⇒ Nothing too awkward, I hope?    [2011-09-24 21:36:28 +0100]
    • Josh Ko ⇒ Yeah, I think it's okay. Basically he (and all other officers I encountered) somewhat complained that the visa sticker should have been put on the new passport. Anyway, I don't really care as long as I can get in..    [2011-09-24 21:46:12 +0100]
  89. 到家了。觸鍵果然都跑掉了，光第一聲彈下去還以為鋼琴被掉包了！    [2011-09-24 18:54:34 +0100]  [ 1 人說讚！]
  90. Just booked FOUR concerts!    [2011-09-24 21:28:10 +0100]
    • Josh Ko ⇒ Friday 7 October 2011: Tchaikovsky Symphony No. 6
      http://ticketing.southbankcentre.co.uk/find/tickets/london-philharmonic-orchestra-56529    [2011-09-24 21:29:30 +0100]
    • Josh Ko ⇒ Friday 10 February 2012: Chopin Piano Concerto No. 1
      http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56715    [2011-09-24 21:30:17 +0100]
    • Josh Ko ⇒ Friday 17 February 2012: Rachmaninoff Piano Concerto No. 2
      http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56721    [2011-09-24 21:46:44 +0100]
    • Josh Ko ⇒ Wednesday 22 February 2012: Brahms Violin Concerto
      http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56664    [2011-09-24 21:47:22 +0100]
  91. Bought ¥60,000 but only spent less than ¥14,000.    [2011-09-25 07:59:05 +0100]  [ 1 人說讚！]
    • 陳** ⇒ 快去找模型店XD    [2011-09-25 08:05:37 +0100]
    • Josh Ko ⇒ 已經回牛津啦 XD。    [2011-09-25 08:34:42 +0100]
  92. Physics is different from Maths (and Computing) in that the theory has to be validated by empirical experiments. If a language is developed for physical reasoning, would that become some kind of effects? (Just guessing.)    [2011-09-25 18:08:32 +0100]
  93. Is there any essential difference between a natural-scientific experiment and a survey? (I am still thinking about Wadler's comment on making programming language design a science.) ↦ Wadler's Blog: An experiment about static and dynamic type systems    [2011-09-25 18:18:16 +0100]

--
Real articles to follow. XD

Labels:

posted by Josh Ko @ 8:08 am   0 項意見