2012/01/29

[facebook digest] Home and back

  1. "[E]xcellence is a competitive notion, and that is not what we are heading for: we are heading for perfection." ↦ E.W.Dijkstra Archive: Introducing my fall 1987 course on Mathematical Methodology (EWD 1011)    [2011-11-08 23:30:37 +0100]
    • Josh Ko ⇒ But better not develop an aggressive personality like that of Steve Jobs or, indeed, Dijkstra..    [2011-11-08 23:34:01 +0100]
    • L********** ⇒ Sometimes a strong argument is necessary    [2011-11-09 01:54:31 +0100]
  2. Tom Melham mentioned today that a philosopher did propose something like whatever can be expressed in a language is/should be correct. He said Spinoza but wasn't sure. (I guess it's not Spinoza.) Does anyone has a clue?    [2011-11-08 23:39:39 +0100]
    • Josh Ko ⇒ Can it be Wittgenstein? I am not familiar with his work (yet) and cannot be sure.    [2011-11-08 23:41:37 +0100]
  3. Mail2000 just solved the IMAP problem. Good!    [2011-11-09 11:56:59 +0100]  [ 1 人說讚！]
  4. There's a generic programming course at Utrecht, which requires students to present published papers and design problem sets about the papers. I looked forward to doing the problems on OAOAOO, but they turned out to be just about Conor's ornaments (i.e., Section 2).. well.

    http://www.cs.uu.nl/wiki/pub/GP/Exercises/Set4.pdf ↦ http://www.cs.uu.nl/wiki/pub/GP/Exercises/Set4.pdf    [2011-11-11 10:10:35 +0100]  [ 1 人說讚！]
  5. It just occurred to me that I can apply for funding from the College instead of just draining Jeremy's project fund. Just wrote to the academic office to ask some questions.    [2011-11-11 16:26:58 +0100]
    • J********** ⇒ Can't be terribly much though?    [2011-11-11 17:50:06 +0100]
    • Josh Ko ⇒ No. But three hundred pounds are worth applying for, right? XD    [2011-11-11 18:16:50 +0100]
    • J********** ⇒ which is worth around 50 plates of pad thai, absolutel!    [2011-11-11 19:31:08 +0100]
    • Josh Ko ⇒ XD    [2011-11-11 21:15:24 +0100]
    • J************* ⇒ Even if the money isn't very good, you can add to your CV another source of funding.    [2011-11-11 23:56:12 +0100]
    • L********** ⇒ Is it open to students from other colleges?    [2011-11-12 02:09:38 +0100]
    • Josh Ko ⇒ It's for Univ students only, set up specifically for funding travels (maximum £300 per student per annum). St Catz might have something similar?    [2011-11-12 10:09:54 +0100]
    • L********** ⇒ Yes, we do.    [2011-11-12 12:59:53 +0100]
  6. Don Knuth will give a departmental seminar on next Tuesday.    [2011-11-11 18:18:18 +0100]  [ 2 人說讚！]
    • L************** ⇒ I'd like to see it as well!!    [2011-11-11 18:34:05 +0100]
    • Josh Ko ⇒ You'll need to be in the lecture theatre by 4pm.    [2011-11-11 21:14:45 +0100]
  7. Curious: While lots of efforts are putting into suppressing the second components of Sigma types, what I need is probably a way to suppress the first components.    [2011-11-13 20:46:00 +0100]
  8. Ralf is right: Okasaki's numerical representations is likely to be closely related work. I wonder if the ornament framework will be able to subsume that?    [2011-11-14 11:22:33 +0100]
    • Josh Ko ⇒ Okasaki didn't make the connection between the implementations of number systems and containers explicit (he just pointed out the similarity informally), which is what the ornament framework can offer and even generalise.    [2011-11-14 11:25:37 +0100]
  9. Just finished reading Steve Jobs' biography. He certainly should have been awarded a PhD - he had a clear thesis and developed strong arguments (the products) for it. The biography can be regarded as his dissertation (written by someone else, which is convenient!).    [2011-11-15 00:25:18 +0100]  [ 2 人說讚！]
  10. Finished reading the /Hound of the Baskervilles./ Now there's only the /Valley of Fear/ that I haven't read (in English) among all Holmes' cases.    [2011-11-17 23:53:45 +0100]  [ 2 人說讚！]
  11. Got the best poster award (from Jim Davis).    [2011-11-18 18:24:52 +0100]  [ 4 人說讚！]
    • D******** ⇒ 太強了！    [2011-11-18 18:25:32 +0100]
    • J********** ⇒ Jim Davies. Jim Davis is the cartoonist of garfield.    [2011-11-18 20:09:01 +0100]
    • Josh Ko ⇒ XD    [2011-11-18 20:09:50 +0100]
    • T************** ⇒ 你喜歡加菲貓    [2011-11-18 23:37:26 +0100]
    • Y********** ⇒ Congratulations!!!    [2011-11-19 01:12:11 +0100]
  12. 看來我的船歌會比第一號敘事曲更快練到可以聽的地步。後面有第四號敘事曲和幻想波蘭舞曲在排隊，不用擔心沒大曲子練 XD。    [2011-11-19 01:08:25 +0100]
  13. Checked-in online. Departure in 48 hours.    [2011-11-27 23:13:34 +0100]  [ 4 人說讚！]
    • J******************* ⇒ 你要去哪？    [2011-11-27 23:15:01 +0100]
    • Josh Ko ⇒ 回國 XD。    [2011-11-27 23:48:55 +0100]
    • M*********** ⇒ 你會待到農曆年嗎??!    [2011-11-28 02:23:34 +0100]
    • Josh Ko ⇒ 選舉結束就走 XD。    [2011-11-28 09:35:36 +0100]
    • M*********** ⇒ XDD 莫非你回來有特別目的!!! 這樣的話,就要看大家的時間了~~    [2011-11-28 16:48:39 +0100]
  14. 逃出生天⋯    [2011-11-28 22:00:27 +0100]  [ 2 人說讚！]
    • L******** ⇒ 哈哈 我大概知道是什麼！    [2011-11-28 23:58:53 +0100]
  15. With only my glasses and watch I still managed to make the metal detector beep..    [2011-11-29 20:49:52 +0100]  [ 2 人說讚！]
  16. At Hong Kong airport.    [2011-11-30 10:37:30 +0100]  [ 4 人說讚！]
    • 翁** ⇒ 是要學成歸國嗎XD    [2011-11-30 10:46:08 +0100]
    • Josh Ko ⇒ 欸，算 1/4 成好了 XD。    [2011-11-30 16:56:46 +0100]
  17. 到啦，看這次時差要調幾天。    [2011-11-30 17:02:42 +0100]  [ 4 人說讚！]
    • L************** ⇒ 去買褪黑激素 ..    [2011-11-30 17:08:59 +0100]
    • L********** ⇒ If possible, can you please buy me some pearl for making milk tea?    [2011-11-30 18:33:03 +0100]
    • L********* ⇒ 回來剛好台灣要變冷 XD    [2011-12-01 00:29:16 +0100]
    • Josh Ko ⇒ 不會比英國冷 XD。    [2011-12-01 00:54:21 +0100]
    • Josh Ko ⇒ I'll try to bring some to you, but you can buy some in London if you cannot wait.    [2011-12-01 00:56:19 +0100]
    • L********** ⇒ Thanks. I will probably stay here for the holiday as I've got some work to do...    [2011-12-01 01:25:41 +0100]
    • 周** ⇒ 我到今天才發現原來有翻譯喔~    [2011-12-01 05:45:46 +0100]
  18. Hammers of the piano at home (to be reconditioned). ↦ http://www.facebook.com/photo.php?fbid=278765245509353&set=a.126799950705884.40277.100001276392360&type=1    [2011-12-01 04:11:02 +0100]  [ 2 人說讚！]
    • W************ ⇒ 哈，我下禮拜五要回家，可以找你吃飯嗎 XD?    [2011-12-01 05:43:11 +0100]
    • Josh Ko ⇒ 可啊 XD。    [2011-12-01 10:44:38 +0100]
  19. 家裡的鋼琴已經老得不太聽話了⋯    [2011-12-01 14:25:55 +0100]
    • Josh Ko ⇒ 剛才彈船歌，那音色讓我頭好痛⋯    [2011-12-02 05:27:11 +0100]
  20. Found an interesting paper (by people at NCKU!) in SIGGRAPH 2008 about generating patterns that cause illusory motion (which has been quite popular recently). ↦ http://graphics.csie.ncku.edu.tw/SAI/    [2011-12-02 02:07:50 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ Is there any evolutionary explanation of this kind of illusion?    [2011-12-02 02:08:19 +0100]
    • Josh Ko ⇒ It's probably "overcompensation". An excerpt from Wade and Swanston's "Visual perception: an introduction": "Our species, like all others, has evolved to process motions that occur in the natural environment and to compensate for the consequences of our own biological motions. These latter involve rotations of the eyes, and translations of the head produced by walking, running, jumping, and turning." And indeed I seem to perceive motion if and only if my eyes are rotating. As for how to design an experiment to show more convincingly that this is indeed overcompensation I have no idea..    [2011-12-02 02:40:48 +0100]
  21. Luke Palmer on rationality and science as a religion (which is a position I'm taking). ↦ The Culture of Reason    [2011-12-03 19:27:54 +0100]
    • Josh Ko ⇒ My jetlag still persists, apparently..    [2011-12-03 19:48:04 +0100]
  22. I feel that I was deceived for a long time about what omega means. Now knowing the definition, somehow the problem doesn't seem to be that interesting anymore. ↦ The Meaning of Omega    [2011-12-04 00:11:41 +0100]
    • Josh Ko ⇒ It's a very delicate play with the distinction between variables and constants, for sure.    [2011-12-04 00:18:41 +0100]
  23. I just came up with the idea that I might be able to avoid doing deep embedding via Agda reflection. Sadly, the reflection API is not rich enough at the moment.    [2011-12-05 15:03:10 +0100]  [ 1 人說讚！]
  24. 早上竟然出現一群陽明國中的學生！    [2011-12-06 03:46:06 +0100]  [ 4 人說讚！]
    • 賴** ⇒ 英國?    [2011-12-06 05:50:31 +0100]
    • Josh Ko ⇒ 墾丁福華 XD。    [2011-12-06 06:01:24 +0100]
    • 賴** ⇒ 回來了喔~~~    [2011-12-06 06:01:39 +0100]
    • Josh Ko ⇒ 對啊 XD。    [2011-12-06 06:01:54 +0100]
    • 賴** ⇒ 有空來基隆玩枕頭，順便來基隆玩^^    [2011-12-06 06:02:27 +0100]
    • Josh Ko ⇒ 再看看嘍 XD。    [2011-12-06 06:03:02 +0100]
    • 賴** ⇒ 他變超胖的    [2011-12-06 06:06:46 +0100]
    • 洪** ⇒ 你回來了ㄛ！要不要來台北玩阿？    [2011-12-06 07:03:05 +0100]
    • Josh Ko ⇒ 近期還沒有計劃 XD。    [2011-12-06 10:30:57 +0100]
  25. Finished presenting the DNF poster and put it online (along with the original version). Now I can finally get rid of the transfer dissertation..
    http://www.cs.ox.ac.uk/people/hsiang-shang.ko/DNF/ ↦ Department of Computer Science, University of Oxford: Publication - Datatype ornamentation and the D    [2011-12-06 12:42:47 +0100]  [ 2 人說讚！]
  26. Repost: http://www.youtube.com/watch?v=yL_-1d9OSdk ↦ Chicken chicken chicken    [2011-12-07 05:16:31 +0100]  [ 1 人說讚！]
  27. No one is obliged to accept any argument; otherwise, it's dogmatism. (Ah, formal systems do not help here, as one can still reject the validity of such systems.)    [2011-12-07 21:53:42 +0100]  [ 1 人說讚！]
  28. It seems the datatype I need is actually a first-order representation of dependent functions with finite domains.    [2011-12-13 04:38:54 +0100]  [ 1 人說讚！]
  29. Hm, a naive modification of vectors does not serve adequately as a first-order representation of dependent functions whose domain is the finite numbers.    [2011-12-14 02:32:11 +0100]
  30. 船歌終於背起來啦！    [2011-12-14 04:02:15 +0100]  [ 1 人說讚！]
  31. Now I have a "large" datatype that does the job for Fin, but of course I'd prefer a small one..    [2011-12-14 07:21:05 +0100]
    • Josh Ko ⇒ And I don't quite see how to generalise the construction yet..    [2011-12-14 07:23:23 +0100]
    • Josh Ko ⇒ The problem is just the opposite of generic modalities as in Chapter 7 of Peter Morris' thesis, where an indexing datatype and a lookup function are derived from a container type. I need to be able to derive a container type whose elements can be indexed by a given datatype.    [2011-12-14 07:34:38 +0100]
    • Josh Ko ⇒ Shouldn't be that hard..    [2011-12-14 07:40:27 +0100]
    • Josh Ko ⇒ It's very much like generic enumeration, except that the usual approach to generic enumeration is coinductive, whereas I need it to be inductive.    [2011-12-14 07:56:33 +0100]
    • Josh Ko ⇒ (So I can get a fold operator for the derived containers.)    [2011-12-14 08:05:37 +0100]
  32. Unlocked my Wildfire S for use in Taiwan.    [2011-12-14 11:59:16 +0100]
  33. Would it be too picky to comment that "a tie is needed after 'et al.' "?    [2011-12-14 15:43:24 +0100]
    • Josh Ko ⇒ And functions names which are typeset like $er$ instead of $\mathit{er}$..    [2011-12-14 15:46:57 +0100]
    • M*********** ⇒ Reviewing?    [2011-12-14 16:16:48 +0100]
    • Josh Ko ⇒ Yeah, basically - I am producing some comments which will be sent to the authors directly.    [2011-12-15 00:45:43 +0100]
  34. Argh, it's just so hard..    [2011-12-15 12:26:48 +0100]
  35. This post starts to convince me that homotopy type theory is worth the effort: http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/ ↦ Just Kidding: Understanding Identity Elimination in Homotopy Type Theory    [2011-12-17 01:28:00 +0100]
  36. Failure to make the trie types small now leads to very serious predicativity problems..    [2011-12-19 08:17:02 +0100]
    • 楊** ⇒ 你昨天打給我？    [2011-12-19 08:18:01 +0100]
    • Josh Ko ⇒ 對啊：這週末或下週末你要不要和香香許博肥傲笑等人看福爾摩斯二？    [2011-12-19 08:27:42 +0100]
    • 楊** ⇒ 在哪？    [2011-12-19 08:28:37 +0100]
    • Josh Ko ⇒ 彰化吧。    [2011-12-19 08:28:55 +0100]
    • 楊** ⇒ 不會在英國吧…    [2011-12-19 08:29:06 +0100]
    • Josh Ko ⇒ 你可以飛過去看沒字幕的 XD。    [2011-12-19 08:29:33 +0100]
    • 楊** ⇒ 這星期應該可以    [2011-12-19 08:35:04 +0100]
    • Josh Ko ⇒ 再下週不行？    [2011-12-19 08:37:47 +0100]
    • 楊** ⇒ 突然發現這週不行 要下星期才行    [2011-12-19 08:39:32 +0100]
    • Josh Ko ⇒ 你果然跟傲笑有串通 XD。    [2011-12-19 08:40:13 +0100]
    • Josh Ko ⇒ 你有在用 hotmail 嗎？我要把討論串轉給你。    [2011-12-19 08:42:57 +0100]
    • 楊** ⇒ 我都用gmail    [2011-12-19 08:48:09 +0100]
    • Josh Ko ⇒ c102570?    [2011-12-19 08:49:53 +0100]
    • 楊** ⇒ 嗯    [2011-12-19 08:54:01 +0100]
  37. Now I've managed to type segs, though requiring --type-in-type..    [2011-12-19 08:31:45 +0100]
    • Josh Ko ⇒ Still far away from the goal.    [2011-12-19 08:32:45 +0100]
    • Josh Ko ⇒ At least there's progress..    [2011-12-19 08:34:24 +0100]
  38. Ignoring the size problem and the lack of relationship between the container datatype and the indexing datatype, there's still the crucial question "what is the type of the fold operator for potentially heterogeneous lists?"    [2011-12-25 02:54:19 +0100]
    • Josh Ko ⇒ Well, of course, we always get the standard elimination operator. The type, however, is large and complicated. The size problem is more severe than I had imagined..    [2011-12-25 08:15:31 +0100]
  39. Few papers have good discussions about, e.g., why their results really are interesting, what insights their solutions provide, etc. I consider the lack of such discussions unacceptable (but (reluctantly) accept that it has become the norm and that some might even argue against their significance).    [2011-12-29 14:11:57 +0100]  [ 2 人說讚！]
    • L********** ⇒ Very true indeed    [2011-12-29 15:32:28 +0100]
    • J************* ⇒ I think that's what the "conclusions" section should be for. (Most use it just for a summary.)    [2011-12-29 17:49:12 +0100]
  40. Not satisfied with the new Holmes movie.    [2011-12-31 12:31:12 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ But of course, as Anton Ego in Ratatouille said: "In many ways, the work of a critic is easy. We risk very little yet enjoy a position over those who offer up their work and their selves to our judgment. [...] But the bitter truth we critics must face, is that in the grand scheme of things, the average piece of junk is probably more meaningful than our criticism designating it so."    [2011-12-31 12:34:24 +0100]
    • Josh Ko ⇒ And I wouldn't describe the movie as junk..    [2011-12-31 12:34:38 +0100]
  41. foldr f e . concat = foldr (flip (foldr f)) e, if I eventually wish to fake doubly indexed collections.    [2012-01-01 08:26:26 +0100]
    • Josh Ko ⇒ Er, no, it does not generalise. That's unexpected..    [2012-01-02 02:45:55 +0100]
  42. The red-black tree datatype is surprisingly "dissectable!"    [2012-01-02 13:05:04 +0100]  [ 1 人說讚！]
  43. Ornament fusion, though conceptually simple, is indeed very helpful. The search tree property and the red-black balancing property can now be separately stated; moreover, the latter can be further dissected into two lines of ornamentations, one about the "red property" (there are no consecutive red nodes) and the other about the "black property" (every path from the root to a leaf contains the same number of black nodes). This will be a very nice example.    [2012-01-02 14:13:21 +0100]  [ 2 人說讚！]
    • J************* ⇒ I'm looking forward to a progress update...    [2012-01-02 18:57:18 +0100]
    • Josh Ko ⇒ Just sent one!    [2012-01-03 01:28:12 +0100]
  44. We can probably design a GUI development environment, so the programmer can, for example, right-click on a field in a datatype and select "specialise"; the constructors would be rearranged accordingly, and, more interestingly, all existing declarations/expressions referring to (elements of) the datatype are automatically rewritten.    [2012-01-02 14:36:12 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ This will definitely not be in my thesis, though.    [2012-01-02 14:36:35 +0100]
    • P************* ⇒ are you developing a new IDE?    [2012-01-02 15:58:33 +0100]
    • Josh Ko ⇒ No, this is just a very rough idea and I don't plan to produce an implementation in the near future. (It's still too premature: We don't really understand how to program with full dependent types yet.) But I hope my thesis will serve as a foundation for such development environments.    [2012-01-03 00:05:52 +0100]
  45. You should not quantify so boldly..    [2012-01-04 03:53:24 +0100]  [ 1 人說讚！]
  46. Yes, the ornament framework easily subsumes data types á la carte.    [2012-01-07 10:39:35 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ It goes in the "opposite direction" and coexists with the refinement interpretation very nicely - and there's no need to expand the universe.    [2012-01-07 11:02:47 +0100]
    • Josh Ko ⇒ And there is no need for smart constructors at all, if datatypes are presented simply as codes - we can calculate composite datatypes such that they have proper constructors.    [2012-01-07 11:03:28 +0100]
    • J************* ⇒ Time to start thinking about ICFP?    [2012-01-07 19:46:23 +0100]
    • Josh Ko ⇒ Would it be somewhat weak to say only that "we can do data types á la carte with ornaments"? And somehow this is "cheating" if compared with Wouter's solution, as he aimed to solve the problem for Haskell, which has limited datatype-manipulating capabilities. (Indeed, there's no practical language which has enough datatype-manipulating capabilities yet. We would need Epigram 2, which is still hypothetical, though.)    [2012-01-08 04:48:50 +0100]
    • P************* ⇒ I "Like" this statement, but I would like a constructive proof better ... Code, or it didn't happen!    [2012-01-08 12:22:13 +0100]
  47. A problem I've just realised is that ornament fusion is actually not a pushout (or pullback, depending on how you assign directions to ornaments)...    [2012-01-07 10:53:31 +0100]
    • Josh Ko ⇒ But perhaps it still is if interpreted in a "weaker" category.    [2012-01-07 12:41:51 +0100]
  48. The SICP course at MIT resurrected. ↦ 6.S184 - Zombies drink caffeinated 6.001    [2012-01-10 10:21:40 +0100]  [ 2 人說讚！]
  49. Impressive experiment result - Russell's paradox was comprehensible to a six-year-old girl! ↦ The Universe of Discourse : Elaborations of Russell's paradox    [2012-01-11 01:47:10 +0100]
  50. Free monad to the rescue!    [2012-01-12 14:39:26 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ Didn't really make use of the monadic structure, though.    [2012-01-12 19:45:19 +0100]
  51. Liskov: "I don't actually believe in functional programming." !!    [2012-01-16 04:20:58 +0100]  [ 4 人說讚！]
    • Josh Ko ⇒ "Because the purpose of programs is to manipulate states."    [2012-01-16 04:22:08 +0100]
    • L************** ⇒ I don't actually believe in listing a talk. XD    [2012-01-16 04:27:59 +0100]
    • 陳** ⇒ 今天是打臉大會XD    [2012-01-16 04:47:08 +0100]
  52. Passed through Heathrow very smoothly for the first time.    [2012-01-17 22:23:09 +0100]  [ 4 人說讚！]
    • L********** ⇒ What happened before?    [2012-01-18 01:25:54 +0100]
    • F********* ⇒ Welcome come back!    [2012-01-18 09:44:41 +0100]
    • Josh Ko ⇒ I had to explain to the immigration officer about the visa, which looks as if it has never been used before, in my old passport.    [2012-01-18 09:54:16 +0100]
    • Josh Ko ⇒ Thanks, Frank!    [2012-01-18 09:54:19 +0100]
  53. My eyes hurt and cannot look at the screen anymore.. This is probably the most annoying consequence of long-haul flights. (So it's time to sleep.)    [2012-01-18 01:05:02 +0100]
  54. My eyes are still tired..    [2012-01-18 11:03:42 +0100]  [ 1 人說讚！]
    • 洪** ⇒ 熱敷可以幫助眼睛改善疲勞~小心溫度不要太燙!    [2012-01-18 11:12:31 +0100]
    • Josh Ko ⇒ 噢太好了，謝謝！    [2012-01-18 11:15:47 +0100]
  55. 家裡的琴太軟，現在回來彈 Knight 琴鍵都壓不下去⋯    [2012-01-18 20:22:05 +0100]  [ 3 人說讚！]
    • 楊** ⇒ 練口琴！    [2012-01-18 20:22:44 +0100]
    • Josh Ko ⇒ 口琴一個人吹沒 fu 吧 XD。    [2012-01-18 20:43:45 +0100]
    • 楊** ⇒ 練獨奏其實也很有fu    [2012-01-18 20:44:13 +0100]
    • 楊** ⇒ 要幫你介紹琴種嗎？xd    [2012-01-18 20:44:19 +0100]
    • Josh Ko ⇒ 沒關係，反正現在我有琴彈 XD。    [2012-01-18 20:46:22 +0100]
    • 楊** ⇒ 真有錢！    [2012-01-18 20:47:14 +0100]
  56. Summoning relations, the great weapon for specification!    [2012-01-20 10:52:40 +0100]
  57. String diagrams for today's AoP meeting. Amazing indeed!    [2012-01-20 14:41:32 +0100]  [ 2 人說讚！]
  58. So the hypothesis is that it's a good idea to relate the indices with the underlying data via an explicit relation.

    Questions to be answered:

    1) Would it be more "meaningful" to manipulate relations than dealing directly with ornaments?

    2) Can we actually manufacture datatypes that we want to program with (and at the same time get properties of these datatypes for free)?

    3) What composable structures of relations can be transferred to datatypes? (And how?)    [2012-01-21 23:17:38 +0100]
    • Josh Ko ⇒ For the first question I think the answer is positive. I may have had a preliminary answer to the second one. The third one is harder.    [2012-01-21 23:22:18 +0100]
  59. The video of my WGP talk is online. Haven't got the courage to watch it, though.. ↦ SOURCE MATERIALS - Modularising inductive families    [2012-01-21 23:28:36 +0100]  [ 1 人說讚！]
  60. Hadn't expected that I can do field swapping with deletion.    [2012-01-22 10:33:53 +0100]
  61. And with deletion it seems I can get a stronger pushout (or pullback) property (the original one I had in mind, actually) for parallel composition. Great!    [2012-01-22 11:05:37 +0100]
    • Josh Ko ⇒ I really underestimated the power of deletion.    [2012-01-22 11:06:35 +0100]
  62. Extending the universe of descriptions to cover general products, in case that I eventually decide to do levitation of ornaments in the future.    [2012-01-22 11:22:21 +0100]
  63. "Too good to be true" does not apply to the Barcarolle. It's good, and it's true.    [2012-01-22 16:16:04 +0100]  [ 4 人說讚！]
  64. Deletion, however, seems to prohibit the universe of ornaments from being levitated. Well, I'm not eager to do this anyway..    [2012-01-22 17:47:17 +0100]
  65. C++ is indeed far away from me - I can now use // as an operator in Agda without regarding everything after that as irrelevant.    [2012-01-22 21:07:18 +0100]  [ 4 人說讚！]
    • L********** ⇒ Still a useful skill to have though    [2012-01-22 21:35:44 +0100]
  66. Extensional equality of the induced forgetful maps - that should be an adequate equality for ornaments.    [2012-01-23 09:16:30 +0100]
  67. I need a convenient way to reason about pullbacks..    [2012-01-23 11:12:21 +0100]  [ 1 人說讚！]
    • 楊** ⇒ 你在學微分幾何？    [2012-01-23 11:22:41 +0100]
    • Josh Ko ⇒ 不用到那麼複雜的東西就已經有 pullback 了 XD。    [2012-01-23 11:32:44 +0100]
    • 楊** ⇒ 我只知道微分幾何裡面要用而已    [2012-01-23 11:34:50 +0100]
    • T************** ⇒ 就是拉回來    [2012-01-23 14:42:56 +0100]
    • Josh Ko ⇒ 也可以推出去 XD。    [2012-01-23 14:45:40 +0100]
  68. Fun in the Afternoon to take place at Oxford on 28 Feb. ↦ Fun in the Afternoon    [2012-01-24 17:31:49 +0100]  [ 1 人說讚！]
  69. Vertical composition is very difficult to tame, whereas properties of parallel composition keep jumping out naturally..    [2012-01-25 10:55:46 +0100]
    • Josh Ko ⇒ On the other hand, it's not that easy to get a natural and easily manipulable definition of parallel composition (because of the need to deal with pullbacks), whereas the definition of vertical composition is straightforwardly inductive.    [2012-01-25 10:58:22 +0100]

Labels:

posted by Josh Ko @ 10:00 am   0 項意見

2011/11/08

[facebook digest] Status transferred

  1. DNF Poster accepted to APLAS.    [2011-10-12 17:10:10 +0100]  [ 4 人說讚！]
  2. Dijkstra simply hated pictorial aids.. How did he do Euclidean geometry, then? ↦ E.W. Dijkstra Archive: Written in anger (EWD 696)    [2011-10-12 21:17:19 +0100]
    • Josh Ko ⇒ "[T]he role of the auxiliary variables in proofs of program correctness is very similar to the role of auxiliary lines or points in geometrical proofs, and their invention requires each time a similar form of creativity. This is one of the reasons why I as a computing scientist can only regret that the attention paid to Euclidean geometry in our secondary school curricula has been so drastically reduced during the last decades."
      So he liked Euclidean geometry..
      http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD641.html    [2011-10-12 21:22:01 +0100]
    • Josh Ko ⇒ I can now almost imagine how rude he was..    [2011-10-12 21:27:46 +0100]
    • J************* ⇒ He did it axiomatically, of course. But even EWD admits to the need for creative invention, which (surely) can benefit from pictures?    [2011-10-13 05:43:04 +0100]
  3. And he didn't think that functional programs can be reasoned about using algebraic laws is an advantage! So supposedly he would have attacked me fiercely had he read the first paragraph of my transfer dissertation.    [2011-10-12 22:59:42 +0100]
    • Josh Ko ⇒ "And then comes his fundamental complaint "In any case, proofs about programs use the language of logic, not the language of programs. Proofs talk about programs but cannot involve them directly [? EWD] since the axioms of von Neumann languages are so unusable." and he presents as an advantage --without questioning-- that in his system "Algebraic transformations and proofs use the language of the programs themselves, rather than the language of logic, which talks about programs." I am not quite sure what is meant by talking proofs and talking logic. But whereas machines must be able to execute programs (without understanding them), people must be able to understand them (without executing them). These two activities are so utterly disconnected --the one can take place without the other-- that I fail to see the claimed advantage of being so "monolingual". (It may appear perhaps as an advantage to someone who has not grasped yet the postulational method for defining programming language semantics and still tries to understand programs in terms of an underlying computational model. Backus's section "Classification of Models" could be a further indication that he still belongs to that category. If that indication is correct, his objection is less against von Neumann programs than against his own clumsy way of trying to understand them.)"

      http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD692.html    [2011-10-12 23:00:51 +0100]
    • Josh Ko ⇒ If I say that axiom postulation has to be based on the way we (mentally) execute programs, he probably would dismiss me by calling me an "integralist".

      http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD611.html    [2011-10-12 23:09:30 +0100]
    • Josh Ko ⇒ Eventually I would have to fight against formalism, I think..    [2011-10-12 23:10:04 +0100]
    • J************* ⇒ Nevertheless, the beauty of functional languages is that you can conduct your reasoning in the language, rather than having to step out of it into predicate calculus. If EWD had understood FP, I'm sure he would have seen this as a benefit; we agree that "the axioms of von Neumann languages are unusable".    [2011-10-13 05:47:15 +0100]
    • Josh Ko ⇒ Yes, that's what Backus said, but Dijkstra did not think that this advantage is obvious. Instead, he thought that using two different languages reflects that machine execution and human understanding are "utterly disconnected" activities, and then attacked Backus (rudely) for not knowing the correct (axiomatic) way to understand programs.

      I don't think Dijkstra caught the point, but I cannot come up with a counterattack yet..

      (I messed up the quote of EWD 692 by adding quotation marks at the beginning and end.. Everything except the first and the last quotation mark is Dijkstra's writing and his quote of Backus's words, so "the axioms of von Neumann languages are unusable" is Backus's comment, which presumably Dijkstra objected.)    [2011-10-13 08:43:21 +0100]
  4. I am confused by change-of-base and reindexing.. Are they related? (Or perhaps I should ask: How are they related?)    [2011-10-13 09:25:54 +0100]
  5. Changed the bulb of my desk lamp to an LED one. Now it's brightly white (instead of yellow).    [2011-10-13 19:21:36 +0100]
    • W************ ⇒ Do you like white light more than yellow light ?    [2011-10-14 03:35:01 +0100]
    • J******** ⇒ The street lights beside CGU have change to LED. If someone stand under it, the color of their clothes is kind of strange!
      But for reading, LED might be find~~    [2011-10-14 05:28:15 +0100]
  6. 如果我可以忍受再一個半月不剪頭髮，我就能回台灣再剪了！    [2011-10-13 19:25:43 +0100]  [ 4 人說讚！]
    • 柯** ⇒ 回台灣我幫你剪~免費唷！    [2011-10-14 08:20:50 +0100]
    • T************** ⇒ 你要帶幾磅來臺灣    [2011-10-15 10:35:31 +0100]
  7. There are only 7 posters in APLAS...    [2011-10-14 08:28:49 +0100]
  8. A spider in my shoe.. Fortunately it didn't bite me. (I've sent it out of the window.)    [2011-10-14 19:26:34 +0100]  [ 1 人說讚！]
  9. Again a particular cold day for matriculation.    [2011-10-15 09:23:12 +0100]
    • L********** ⇒ It is quite warm in Marston.    [2011-10-15 11:15:12 +0100]
  10. Jackie 最後的午餐。 ↦ Wall Photos    [2011-10-17 14:16:30 +0100]  [ 3 人說讚！]
    • Y********** ⇒ 是"十月"的最後午餐啦XD    [2011-10-17 14:22:02 +0100]
    • J********** ⇒ :)    [2011-10-17 16:30:15 +0100]
  11. "But the point is that fibrations have a great organisational strength. They provide appropriate ways of layering mathematical structures, by making explicit what depends on what." (Jacobs, p70)    [2011-10-17 20:27:53 +0100]
  12. Just updated Agda to the latest (development) version and there are now unsolved meta-variables when typechecking OAOAOO.agda..    [2011-10-17 22:20:54 +0100]
  13. From: Ralf Hinze
    Subject: Transfer viva: date
    Date: 18 October 2011 07:50:55 GMT+01:00
    To: Josh Ko

    Hi Josh,

    Tom and I can make it in week 5. Would
    12:00, Tue, 8th Nov, 2011
    suit you?

    Cheers, Ralf    [2011-10-18 08:19:15 +0100]  [ 1 人說讚！]
    • Y*********** ⇒ Finally......    [2011-10-18 09:30:57 +0100]
  14. Getting lost in the category of fibrations.. (The category Fib of fibrations can be seen as fibred over the category Cat of categories, so the functor Fib -> Cat sending a fibration to its base category is a fibration itself. There should be some size problems we should avoid, but it's not urgent..)    [2011-10-18 09:03:07 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ And Fib has a 2-categorical structure.. That's too much for me now!    [2011-10-18 09:05:52 +0100]
    • Josh Ko ⇒ Skipping to Chapter 2.    [2011-10-18 09:19:33 +0100]
  15. The NSC-RS joint grant application was unsuccessful... How I wished that Jeremy could visit Taiwan!    [2011-10-19 07:31:52 +0100]
  16. A1 is already small enough for a poster.. A2 would certainly be much too small!    [2011-10-20 11:55:30 +0100]
    • L********* ⇒ 看到A1我還以為是要說Audi A1咧 XDDD    [2011-10-20 12:02:18 +0100]
  17. prefixes [] = [ [] ]
    prefixes (x ∷ xs) = [] ∷ map (_∷_ x) (prefixes xs)

    The three conses really should have different meanings!    [2011-10-20 15:20:08 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ The meaning of the second one is particularly hard to pin down.    [2011-10-20 15:25:15 +0100]
    • Josh Ko ⇒ (Of course, there is also an implicit one in the first clause.)    [2011-10-20 15:26:22 +0100]
  18. Received the payment for doing practicals demonstration for the UNIQ summer school.    [2011-10-21 10:24:37 +0100]
  19. Now I think that the structure of my poster is indeed rather too "modernist". Will rework the structure completely.    [2011-10-25 22:35:08 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ But then I'm not so sure if I can do it in a classical way..    [2011-10-25 22:47:58 +0100]
    • Josh Ko ⇒ The current modernist version is no doubt very space-efficient.    [2011-10-25 23:29:48 +0100]
    • Josh Ko ⇒ I'll finish this version anyway, and then see if I can manage to produce a classical version..    [2011-10-25 23:41:43 +0100]
  20. Bought Steve Jobs' biography.    [2011-10-26 13:56:28 +0100]  [ 4 人說讚！]
    • L********* ⇒ eBook version?    [2011-10-26 13:58:16 +0100]
    • Josh Ko ⇒ Hardcover.    [2011-10-26 14:01:43 +0100]
  21. The "modernist" version. Even though I may not use this one for the conferences, I'd still like to have an A1 sized copy of it. ↦ Wall Photos    [2011-10-26 19:12:20 +0100]  [ 4 人說讚！]
    • H************ ⇒ very creative!!    [2011-10-26 21:48:31 +0100]
    • W********* ⇒ 真是太漂亮惹 請寄給我一份XD    [2011-10-27 00:05:58 +0100]
  22. In fact, as I somewhat anticipated, I now feel that the modernist version is fine and hesitate to do a classical version. XD    [2011-10-27 08:47:07 +0100]
  23. Found a small error in the code on the poster, which however means that the same error is present in my transfer dissertation..    [2011-10-27 10:39:41 +0100]
    • Josh Ko ⇒ Oh, it's just a typo in an auxiliary definition, so no harm to validity.    [2011-10-27 15:24:36 +0100]
  24. Look at the two functions 'forget' and 'initialise' used in my solution to the Dutch National Flag problem: The former is a left inverse to the latter, but not vice versa; the latter is some kind of canonical injection, however, and we do have 'initialise . forget . initialise = initialise'. So there is likely to be an adjunction!    [2011-10-27 22:31:17 +0100]
    • S************ ⇒ A Galois connection?    [2011-10-28 00:45:58 +0100]
    • Josh Ko ⇒ Yes, indeed. (But some day I hope I can find a nontrivial adjunction! (No concrete ideas yet..))    [2011-10-28 08:15:14 +0100]
  25. If we recall that types are specifications, then it becomes clear that practically it's not possible (thanks to typechecking) to write wrong (or buggy) programs but only imprecise or wrong specifications.    [2011-10-27 23:14:57 +0100]
  26. Brouwer's proof of ¬¬¬p ↔ ¬p.    [2011-10-28 14:03:41 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ Theorem. Absurdity of absurdity of absurdity is equivalent to absurdity.

      Proof. When property y follows from property x, then from the absurdity of y follows the absurdity of x. Therefore necessarily, since truth implies absurdity of absurdity, absurdity of absurdity of absurdity implies absurdity.

      Conversely, because the correctness of an arbitrary property implies the absurdity of the absurdity of that property, so must absurdity of truth, that is absurdity, imply absurdity of absurdity of absurdity.    [2011-10-28 14:06:31 +0100]
    • Josh Ko ⇒ I simply cannot successfully pronounce three consecutive 'absurdity's..    [2011-10-28 14:07:00 +0100]
  27. Really, I'd have liked to say simply "page 2 needs to be rewritten".    [2011-10-28 16:06:43 +0100]
    • 陳** ⇒ 學長加油Q.Q    [2011-10-28 17:09:57 +0100]
  28. The abstract I reviewed probably took the author(s) only, say, 30 minutes to finish by copy-and-paste — the writing quality is definitely not good. Anyway, it's just an abstract for a student conference.. The work described looks sound so there is no reason to reject it!    [2011-10-28 21:22:48 +0100]
    • Josh Ko ⇒ Or can I give it a lower grade because I don't think it's well-written?    [2011-10-28 21:26:56 +0100]
    • L************** ⇒ Definitely you can.    [2011-10-28 21:43:42 +0100]
    • Josh Ko ⇒ I finally decided to still give it an accept but mentioned in the "remarks for the programme committee" section that I'd have given it a weak accept had writing quality been taken into consideration seriously.    [2011-10-28 21:50:48 +0100]
    • Y************* ⇒ So right now, you are a reviewer and have the authority to reject a paper. Oh my god, it sounds so cool, my friend.    [2011-10-29 00:12:20 +0100]
    • Josh Ko ⇒ It's just a student conference held in our department, so there's no substantial influence.    [2011-10-29 00:31:32 +0100]
    • Y************* ⇒ All right but it still cool.    [2011-10-30 01:56:50 +0100]
  29. The Barcarolle simply has an amazingly golden colour..    [2011-10-29 13:02:23 +0100]  [ 2 人說讚！]
  30. It seems that Dijkstra had a bad influence on me: I now tend to make ruder arguments. Fortunately I don't need to read his work intensively now as I have had a reasonable understanding of his philosophy.    [2011-10-30 19:09:41 +0100]  [ 1 人說讚！]
  31. "Nobody cares."    [2011-10-30 21:52:13 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ http://sneezy.cs.nott.ac.uk/darcs/DTP08/slides/Lennart.pdf    [2011-10-30 21:52:56 +0100]
  32. 不經意與此文重逢。 ↦ http://www.hgjh.hlc.edu.tw/~chenli/chopin.htm    [2011-10-30 22:41:00 +0100]
  33. There's no way to do implicit existential quantification in Agda now, I believe? (I wish to use a (Σ ℕ (Vec A)) as if it's just a (Vec A n) for some n.)    [2011-10-31 10:27:08 +0100]
    • Josh Ko ⇒ (without having to write trivial constructors and projections.)    [2011-10-31 10:31:43 +0100]
  34. Argh, Tarjan's Strachey lecture will be in December..    [2011-11-01 09:10:17 +0100]
    • L********** ⇒ Will be away in a conference that day...    [2011-11-01 11:26:41 +0100]
    • J********** ⇒ Great! I will be arriving in the morning of the 8th... Thx for the info:-)    [2011-11-01 13:54:10 +0100]
  35. I have not been able to receive emails from Mail2000 smoothly ever since I upgraded to Lion. (I have to dismiss "password rejected" dialog boxes every time Mail tries to login.) After observing the discussions about this problem on the Apple forum for a long time, I decided that it might well be a server-side problem and wrote to Mail2000, attaching two particular messages from the forum that might be helpful.    [2011-11-02 12:26:11 +0100]
    • Josh Ko ⇒ Their reply was a long list of forum entries and suggested that I switch to, e.g., Thunderbird while waiting for Apple to solve the problem.    [2011-11-02 12:26:20 +0100]
    • Josh Ko ⇒ I was a bit annoyed. Today I used telnet to connect to the IMAP server and discovered that the same authentication process had to be repeated twice to login, which just didn't make sense. So I wrote to them again, attaching the telnet log and this time asking explicitly how Apple violates RFC in this case.    [2011-11-02 12:29:07 +0100]
    • Josh Ko ⇒ Really, if they cannot give me a satisfactory answer this time, there doesn't seem to be any point paying for their service anymore.    [2011-11-02 12:31:50 +0100]
  36. > I am confused by change-of-base and reindexing.. Are they related? (Or perhaps I should ask: How are they related?)

    Right, change-of-base is reindexing in the category of fibrations.    [2011-11-03 09:59:52 +0100]  [ 1 人說讚！]
  37. Now Mail2000 seems to be interested in solving the problem, but not quite at the right level yet. (They recommended that I change the settings in Mail.) I pointed out that this is no longer a problem with Mail but with how the server responds to the AUTHENTICATE command since the experiment results were produced by telnet/openssl, and asked them to look at the case again.    [2011-11-03 11:35:04 +0100]
    • Josh Ko ⇒ I thought the telnet session I sent them should be a quite obvious hint to them (who are supposed to be experts) about what goes wrong.    [2011-11-03 11:37:22 +0100]
  38. "A category C has a terminal object if and only if the unique functor C -> 1 from C to the terminal category 1 has a right adjoint." Never thought of this..    [2011-11-04 10:36:55 +0100]
    • L************** ⇒ Now, you can think of universal and existential quantifiers in this way...    [2011-11-04 10:46:02 +0100]
    • Josh Ko ⇒ As right/left adjoints of a weakening functor?    [2011-11-04 10:49:25 +0100]
    • L************** ⇒ I overlooked your message. It seems different to what I thought. This is stated in the second section of adjunction in MacLane's book...    [2011-11-04 11:03:28 +0100]
    • Josh Ko ⇒ As a special case of limits/colimits expressed as right/left adjoints of the diagonal functor.    [2011-11-04 11:16:28 +0100]
  39. Simplified version of the DNF poster. The text size is more readable, but now it would be very difficult (if possible at all) for the reader to understand the poster by him/herself since the explanations (among other things) are left out. ↦ Wall Photos    [2011-11-05 01:13:45 +0100]  [ 4 人說讚！]
    • L********** ⇒ I would probably prefer the "unsimplified" version    [2011-11-05 03:31:25 +0100]
    • Josh Ko ⇒ I like that one too, but it can't be denied that the texts are too small - it works ok for one or two people but less effectively for more than three, I guess.    [2011-11-05 10:05:55 +0100]
    • Josh Ko ⇒ I might print both of them out, however. XD    [2011-11-05 10:07:33 +0100]
  40. While Dijkstra complained that Hilbert's formalism (and Leibniz's dream) was ignored by the maths community, I wonder how he could possibly ignore Gödel's incompleteness theorems?

    (I would say that he had his own "reality distortion field".) ↦ E.W.Dijkstra Archive: Under the spell of Leibniz's Dream (EWD 1298)    [2011-11-07 23:08:24 +0100]  [ 1 人說讚！]
    • J******************* ⇒ But the Reality Distortion Field usually works on others lol    [2011-11-07 23:59:09 +0100]
  41. Hm, transfer viva is apparently very daunting. The assessors' questions sounded not to be in English even to a (presumably) native speaker!
    http://clamorousvoice.wordpress.com/2011/06/01/prs-dphil-oxford-english-transfer-viva/ ↦ PRS to DPhil: the transfer viva    [2011-11-08 11:24:11 +0100]
    • Josh Ko ⇒ And if you google for "transfer viva", the first entry is this: http://www.postgraduateforum.com/threadViewer.aspx?TID=9368    [2011-11-08 11:25:04 +0100]
    • Josh Ko ⇒ Jeremy was right about the result. XD    [2011-11-08 13:54:50 +0100]
  42. Alright, I think I will shortly be a proper DPhil student!    [2011-11-08 14:03:18 +0100]  [ 4 人說讚！]
    • Josh Ko ⇒ (Just passed my transfer viva.)    [2011-11-08 14:04:04 +0100]
    • A*********** ⇒ congrats@    [2011-11-08 14:05:16 +0100]
    • G*************** ⇒ congratulations    [2011-11-08 14:44:29 +0100]
    • D******** ⇒ 恭喜啦！！    [2011-11-08 14:55:26 +0100]
    • M************ ⇒ cool!!!!!!!!    [2011-11-08 15:32:50 +0100]
  43. I presented the internalist position, although Ralf and Tom were not convinced. I believe that their job at this stage is only to check that I have something to say, so they didn't push it further, but I will certainly need to offer a complete argument in the thesis.    [2011-11-08 14:41:03 +0100]
    • Josh Ko ⇒ That is, I really cannot take internalism for granted - its validity will have to be justified in the thesis.    [2011-11-08 14:43:30 +0100]
  44. My verbal arguments tend to be rather unstructured. This weakness will have to be taken care of..    [2011-11-08 21:48:50 +0100]

--
It is really about time to write a review of the previous academic year now that I've transferred status..

Labels:

posted by Josh Ko @ 10:17 pm   0 項意見

2011/10/12

[facebook digest] Entering Michaelmas Term 2011

  1. OAOAOO has appeared in ACM Digital Library. (No video yet.) ↦ Modularising inductive families    [2011-09-26 10:42:38 +0100]
  2. Hm, perhaps what I need is a higher-order pivot table..    [2011-09-27 23:22:53 +0100]  [ 2 人說讚！]
  3. Implementation rate of my Clarendon Scholarship for the last academic year: 93.02%（上學年獎學金執行率）    [2011-09-28 09:26:35 +0100]
    • Josh Ko ⇒ 只算經常門的話，執行率僅 82.12%，看起來不錯。    [2011-09-28 09:46:10 +0100]
  4. Now I believe I have a working accounting table, but I have no good explanation of why it works yet.    [2011-09-28 10:42:10 +0100]  [ 1 人說讚！]
  5. And I wish Excel has support for monads..    [2011-09-28 10:43:24 +0100]  [ 2 人說讚！]
  6. Hm, 會計確實是需要腦筋轉一下的東西。    [2011-09-28 10:53:36 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ 如果網路上的會計學就是一般在學的會計，那還真的滿慘的 — 說明方式之落後模糊令人驚訝。    [2011-09-28 11:01:23 +0100]
    • 陳** ⇒ 所以學長正在oxford修會計學嗎? XD    [2011-09-28 11:23:35 +0100]
    • Josh Ko ⇒ 沒，我在設計自己用的會計學 XD。    [2011-09-28 11:27:49 +0100]
    • 柯** ⇒ 真的很麻煩的東西厚~爸爸一直炫耀說當初他一手抱著我，一手算會計還能all pass    [2011-09-28 14:18:14 +0100]
  7. Some day I might write a blog post on "the essence of accounting" (from my perspective), but I don't think it will be in the near future.    [2011-09-28 11:14:43 +0100]  [ 1 人說讚！]
  8. HelloUK 竟然出現一個 MSc in Computer Science 新生！    [2011-09-29 20:32:53 +0100]  [ 2 人說讚！]
  9. Russell O'Connor posted his story about publishing his WGP paper. ↦ The ACM and me    [2011-09-30 09:20:24 +0100]  [ 3 人說讚！]
  10. 熟練度（速度）有差不多達到最低限度了。副音群應該想成主音的延續，用它們做音量變化和彈性速度。
    https://sites.google.com/site/joshkos/Ocean_20111002.mp3    [2011-10-02 17:07:28 +0100]
    • Josh Ko ⇒ 可是接下來幾天不能彈太猛，手有點痠⋯    [2011-10-02 17:29:45 +0100]
  11. Week 0 starts in about 4 hours. As a computing scientist, this means that my second year will start shortly.    [2011-10-02 20:16:51 +0100]  [ 3 人說讚！]
    • M*********** ⇒ Josh, I need to remind you that in Oxford it's Sunday that is the first day of the week (or maybe I should say 0th day of the week?). In any case, week zero is already on for more that 24 hours.    [2011-10-03 01:53:05 +0100]
    • Josh Ko ⇒ Argh, you're right. I start working on Monday, however, so it feels that, practically, Week 0 starts today. XD    [2011-10-03 08:04:15 +0100]
    • J********** ⇒ 老大, 這個麻糬擺明在嗆你, 要不要幫你打爆他的頭??    [2011-10-03 19:32:11 +0100]
    • Josh Ko ⇒ 可是他說得很對呀，考試規則確實是這麼寫的 XD。    [2011-10-03 19:34:26 +0100]
    • J********** ⇒ 我不管啦><    [2011-10-03 19:49:32 +0100]
  12. 彰中換了新校長。一查，竟然是和苗栗苑里高中的校長互換？！    [2011-10-02 20:56:42 +0100]
    • W************ ⇒ 苑里高中 XD? 沒聽過就是了 XD    [2011-10-03 02:49:58 +0100]
    • 陳** ⇒ 據說是舊任校長的養老計劃，去山上養老種菜? XD    [2011-10-05 09:57:13 +0100]
    • Josh Ko ⇒ 他在苑里高中網頁上的照片還是以彰中為背景 XD。
      http://www.ylsh.mlc.edu.tw/principal/menu1/index.php    [2011-10-05 10:08:11 +0100]
    • Josh Ko ⇒ 還做 SWOT 分析，看起來很認真不像要養老呀 XD。    [2011-10-05 10:09:01 +0100]
  13. £426 for a LHR-TPE round trip, really competitive price.. (Er, I jet got up and will go back to sleep very soon.)    [2011-10-04 04:19:18 +0100]
    • L************** ⇒ Ours travel?    [2011-10-04 04:32:15 +0100]
    • Josh Ko ⇒ No, directly on the website of British Airways!    [2011-10-04 04:43:07 +0100]
    • Josh Ko ⇒ Tax and surcharges are included in £426, so it's really attractive.    [2011-10-04 04:44:42 +0100]
    • Josh Ko ⇒ s/jet/just/    [2011-10-04 04:46:33 +0100]
    • Josh Ko ⇒ It turns out not to be that cheap — £426 is for a single trip only...    [2011-10-04 12:08:45 +0100]
  14. It seems that Tim Cook is giving a bad presentation.

    "18:20: This is a lot like a financial briefing so far Tim.
    "18:22: iOS now. It's popular says another pie chart slide. That's about 57 pie charts and graphs so far. *sigh*"

    http://www.techradar.com/news/internet/iphone-5-launch-what-to-expect-1031146 ↦ TechRadar: iPhone 5 launch: what to expect    [2011-10-04 19:05:55 +0100]  [ 3 人說讚！]
  15. Which category does ". -> ." stand for? ↦ Wall Photos    [2011-10-05 09:03:20 +0100]
    • J************* ⇒ The category with two objects and three arrows (two identities, of course, and one additional arrow from one of the objects to the other), presumably.    [2011-10-05 09:33:20 +0100]
    • Josh Ko ⇒ Ah, right. I misinterpreted the dots as places for arguments instead of unnamed objects (and thus was utterly confused). Thanks!    [2011-10-05 09:39:54 +0100]
    • Josh Ko ⇒ So it's a category "which looks just like that" (ref. Mac Lane p66).    [2011-10-05 09:43:19 +0100]
  16. Still stuck at: "A Cartesian map above an isomorphism is an isomorphism. Especially a vertical Cartesian map is an isomorphism."    [2011-10-05 09:20:10 +0100]
  17. "Mythology."
    A great artist whose works are worth studying.
    http://www.apple.com/stevejobs/ ↦ Wall Photos    [2011-10-06 03:09:27 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ Suddenly I noticed that in "1955-2011" they used a hyphen instead of an en-dash..    [2011-10-06 03:53:58 +0100]
    • Josh Ko ⇒ But well, the length of en-dash is not standardised..    [2011-10-06 04:00:43 +0100]
  18. Thesis proofreading is highly challenging. But well, thesis writing is presumably even more difficult than that..    [2011-10-07 11:16:50 +0100]
    • Josh Ko ⇒ It's almost like limited co-authorship, I think.    [2011-10-07 11:22:45 +0100]
    • L********** ⇒ Indeed    [2011-10-07 17:19:52 +0100]
  19. Got an email from a fourth-year undergraduate Japanese student enquiring about getting a DPhil position in the AoP group. Discussing with Jeremy what to do.    [2011-10-09 09:54:50 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ Eventually I found myself unable to give helpful answers and simply relayed the email to Jeremy.    [2011-10-09 16:46:52 +0100]
  20. Registered as a referee for the student conference.    [2011-10-09 17:15:30 +0100]  [ 1 人說讚！]
    • L********** ⇒ Thank you Josh!    [2011-10-09 17:40:25 +0100]
  21. "At present they have very few abstract submissions and for the [student] conference to be a success many more are needed."

    I just submitted my abstract and it is the third submission.. Well, it's (slightly) better than WGP! XD    [2011-10-11 10:40:45 +0100]  [ 1 人說讚！]
    • L********** ⇒ Hi Josh, if you could remind students in the AoP group the submission deadline which is this Friday, that would be great help (probably no need to forward the message again, just talk to them when you meet in the department). Many thanks!    [2011-10-12 11:10:58 +0100]
    • Josh Ko ⇒ OK!    [2011-10-12 11:12:37 +0100]
  22. I think I need to set myself some short-term goal. Hm.. How about getting a reasonably good idea about Chapters 1 and 2 of Jacobs in this term?    [2011-10-11 15:07:36 +0100]  [ 1 人說讚！]
  23. Hm, calling it the French National Flag problem is in fact more suitable, and I would be able to cite the famous painting by Delacroix. (But anyway..) ↦ File:Eugène Delacroix - La liberté guidant le peuple.jpg - Wikipedia, the free encyclopedia    [2011-10-11 20:59:33 +0100]
  24. Received an email from ANSI that ISO/IEC 14882:2011, i.e., the latest version of C++ standard, has been released. (I received this email because I bought ISO/IEC 14882:2003 from their web store when I was in high school.)    [2011-10-12 07:49:38 +0100]
    • Josh Ko ⇒ Now I have little interest in understanding C++11, I'm afraid..    [2011-10-12 07:51:39 +0100]
    • 林** ⇒ Just reviewed C++ recently... XD    [2011-10-12 13:16:53 +0100]
  25. Booked my flight: outbound 29 Nov / inbound 17 Jan. Need to extend the length of stay a bit and skip presumably the last AoP meeting of this term because of, naturally, the ticket price.    [2011-10-12 10:54:33 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ Came across this article on air ticket pricing: http://www.maa.org/devlin/devlin_09_02.html    [2011-10-12 10:58:20 +0100]
    • L************** ⇒ How much is the ticket?    [2011-10-12 11:07:43 +0100]
    • Josh Ko ⇒ £630. I believe this is the standard price?    [2011-10-12 11:08:20 +0100]
    • Josh Ko ⇒ In fact, if I book the ticket directly on the website of Cathay Pacific, the price is £629.73..    [2011-10-12 11:09:33 +0100]
    • L************** ⇒ I got £580, but the outbound is in January.    [2011-10-12 11:09:56 +0100]
    • L************** ⇒ Try Ours Travel to see if it could be cheaper...    [2011-10-12 11:13:05 +0100]
    • Josh Ko ⇒ I think the inbound date also matters. And that's indeed the result I got from Ours Travel..    [2011-10-12 11:13:58 +0100]

--
啊，不要再拖稿了啦⋯！

Labels:

posted by Josh Ko @ 2:06 pm   0 項意見

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 項意見