Trek through Pure Reason

GSS student report, Michaelmas Term 2011

2011-11-20T20:35:00.001Z

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

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

[facebook digest] Status transferred

2011-11-08T22:17:00.001Z

DNF Poster accepted to APLAS. [2011-10-12 17:10:10 +0100] [ 4 人說讚！]
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]
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]
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]
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]
如果我可以忍受再一個半月不剪頭髮，我就能回台灣再剪了！ [2011-10-13 19:25:43 +0100] [ 4 人說讚！]
- 柯** ⇒ 回台灣我幫你剪~免費唷！ [2011-10-14 08:20:50 +0100]
- T************** ⇒ 你要帶幾磅來臺灣 [2011-10-15 10:35:31 +0100]
There are only 7 posters in APLAS... [2011-10-14 08:28:49 +0100]
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 人說讚！]
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]
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]
"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]
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]
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]
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]
The NSC-RS joint grant application was unsuccessful... How I wished that Jeremy could visit Taiwan! [2011-10-19 07:31:52 +0100]
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]
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]
Received the payment for doing practicals demonstration for the UNIQ summer school. [2011-10-21 10:24:37 +0100]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
The Barcarolle simply has an amazingly golden colour.. [2011-10-29 13:02:23 +0100] [ 2 人說讚！]
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 人說讚！]
"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]
不經意與此文重逢。 ↦ http://www.hgjh.hlc.edu.tw/~chenli/chopin.htm [2011-10-30 22:41:00 +0100]
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]
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]
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]
> 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 人說讚！]
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]
"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]
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]
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]
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]
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]
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]
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..

[facebook digest] Entering Michaelmas Term 2011

2011-10-12T14:06:00.001+01:00

OAOAOO has appeared in ACM Digital Library. (No video yet.) ↦ Modularising inductive families [2011-09-26 10:42:38 +0100]
Hm, perhaps what I need is a higher-order pivot table.. [2011-09-27 23:22:53 +0100] [ 2 人說讚！]
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]
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 人說讚！]
And I wish Excel has support for monads.. [2011-09-28 10:43:24 +0100] [ 2 人說讚！]
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]
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 人說讚！]
HelloUK 竟然出現一個 MSc in Computer Science 新生！ [2011-09-29 20:32:53 +0100] [ 2 人說讚！]
Russell O'Connor posted his story about publishing his WGP paper. ↦ The ACM and me [2011-09-30 09:20:24 +0100] [ 3 人說讚！]
熟練度（速度）有差不多達到最低限度了。副音群應該想成主音的延續，用它們做音量變化和彈性速度。
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]
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]
彰中換了新校長。一查，竟然是和苗栗苑里高中的校長互換？！ [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]
£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]
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 人說讚！]
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]
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]
"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]
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]
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]
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]
"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]
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 人說讚！]
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]
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]
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]

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

ICFP 2011

2011-09-26T08:39:00.019+01:00

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

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

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

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

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

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

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

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

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

--
我也是很會拖稿⋯

[facebook digest] ICFP

2011-09-26T08:08:00.004+01:00

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]
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]
觸鍵要多下點功夫了⋯ [2011-09-01 19:06:05 +0100] [ 1 人說讚！]
「你必須愛上一塊石頭，」斯文嚴肅地說。「你看過成打的石頭，你說，啊！不對我的胃口。然後你看到那一塊，細緻又優雅的一塊，你就愛上它了。就和女人一樣。但接踵而至的婚姻卻很可怕。你拚命抵抗，但石頭堅硬無比。你好絕望，然後，剎那之間，彷彿蠟一般，石頭在你手裡融化了，於是你塑出一個形象。」 [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]
I guess I'll just stick to a slower Ocean.. [2011-09-02 16:36:39 +0100]
Pressing the "Intensify" button (à la iPhoto) for my music. [2011-09-02 20:02:03 +0100]
Ocean 這樣練下來，手應該是有比較強壯啦，可是愈彈愈快，每次彈完還是很痠⋯ [2011-09-03 18:11:50 +0100] [ 1 人說讚！]
Zimerman 那個線條之流暢靈動⋯ 真是無話可說。 [2011-09-03 21:58:15 +0100]
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]
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]
(Finally) reusing the slides for function upgrade and ornament fusion. [2011-09-05 20:37:36 +0100]
東京電玩展 17, 18 號開放參觀 — 17 號剛好是我到日本的第一天！可是我現在對電玩沒什麼興趣了⋯ [2011-09-05 21:36:35 +0100] [ 4 人說讚！]
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]
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]
Op 62 No 2 好像快熟了。 [2011-09-06 19:13:41 +0100]
Transfer application submitted! [2011-09-07 11:04:52 +0100] [ 4 人說讚！]
And I'll submit a poster on the Dutch National Flag problem to APLAS'11! [2011-09-07 11:52:25 +0100] [ 1 人說讚！]
我彈的時候聽到的東西和錄音聽到的東西愈來愈接近了，很好。 [2011-09-07 18:27:25 +0100] [ 4 人說讚！]
"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]
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]
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]
秋葉原是不可不逛的，應該就排在 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]
目前的 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]
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]
細讀一次 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]
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]
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]
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]
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]
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]
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]
"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]
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]
"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]
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]
Inverse Function Theorem.. ah, painful memories... ↦ The inverse function theorem for everywhere differentiable maps [2011-09-13 08:12:42 +0100] [ 1 人說讚！]
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]
東京電車有辦法弄得這麼複雜確實不簡單⋯ [2011-09-15 09:04:13 +0100] [ 2 人說讚！]
- P************* ⇒ 倫敦地鐵可以弄的這麼髒車上沒有空調空氣超差收費居然還這麼高也是非常不簡單 [2011-09-15 11:10:57 +0100]
目前唯一結論：到羽田先買張 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]
我對山手線的唯一印象是「扒手」：怪醫黑傑克有一集是山手線的扒手慣犯扒到黑道被切斷手指，長期追捕他的警官找黑傑克去把手指完美地接回去，讓他可以繼續偷，警官才可以繼續追捕他 (?!)。 [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]
這時候就有點後悔沒好好研究一下勇者特急裡的多款列車，去就不能享受指認拍照的樂趣了。 [2011-09-15 09:45:54 +0100]
從東京電玩展的海濱幕張站到神保町站好像要轉不少次。啊，不管啦，到時候按圖索驥了。 [2011-09-15 09:55:16 +0100] [ 2 人說讚！]
Now on board the X70 (again), leaving for the legendary ICFP. [2011-09-16 05:34:06 +0100]
這班早上五點到羽田的班機根本是為了要排東京電玩展的隊而設計得這麼早的嘛！經歷約三小時日曬雨淋風吹，十點十五分成功進入會場，現在是用免費提供的無線網路。 [2011-09-17 03:04:29 +0100] [ 4 人說讚！]
來到日本頓時覺得自己英文真好！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]
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]
早上六點多接到 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]
看到海龜按讚才想到：有個小小的攤位是 SIGGRAPH Asia 2011 的樣子，但是剛進場的時候看沒擺什麼東西。 [2011-09-17 03:58:04 +0100]
- C*********** ⇒ SIGGRAPH 2011 的時候也是這樣. 擺個桌子讓人拿傳單而已. [2011-09-17 04:15:54 +0100]
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]
想睡但是才中午，待會回飯店也應該再練習一下明天的 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]
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]
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]
連 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]
總覺得投影片到後段有亂流出現 — 可能是因為直接從 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]
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 人說讚！]
如果從日本搬一個免治馬桶座回去會不會太熱血了？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]
早餐吃得下，希望是好徵兆。待會再練一遍。 [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]
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 人說讚！]
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]
Met Oleg and finally the lengendary Ken (who looks much younger than I had expected) during lunch. [2011-09-18 06:07:22 +0100]
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]
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]
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]
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]
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]
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]
定風波．蘇軾

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

常羨人間琢玉郎，天應乞與點酥娘。自作清歌傳皓齒。風起。雪飛炎海變清涼。　　萬里歸來年愈少。微笑。笑時猶帶嶺梅香。試問嶺南應不好。卻道。此心安處是吾鄉。 [2011-09-20 23:42:35 +0100] [ 2 人說讚！]
- Josh Ko ⇒ 想回牛津的家，有感。 [2011-09-20 23:46:12 +0100]
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]
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]
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]
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]
Bump into a Japanese typhoon.. (Its direction is different from those of Taiwan!) [2011-09-21 00:54:08 +0100]
被困在 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]
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]
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]
Brightly sunny again today! Hope it's the same tomorrow. [2011-09-22 00:51:12 +0100] [ 1 人說讚！]
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]
美國腔很刺耳… [2011-09-22 06:19:39 +0100] [ 2 人說讚！]
- N*********** ⇒ 深有同感！！ [2011-09-22 11:55:49 +0100]
- 柯** ⇒ 你感染了英國病 [2011-09-22 13:10:13 +0100]
明天早上淺草寺，下午秋葉原好了，買模型比較方便 XD。（晚上有 continuation workshop 附設的 tutorial.） [2011-09-22 11:19:42 +0100] [ 2 人說讚！]
- 陳** ⇒ 學長準備好銀彈了嗎XD [2011-09-22 11:27:37 +0100]
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]
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]
結果淺草寺 + 秋葉原只逛了兩個多小時！淺草寺不大就算了，秋葉原的東西我都滿陌生，機器人只認得 Eva 和 Wing Zero。這樣自然沒什麼看頭，中午就回旅館了。 [2011-09-23 05:14:56 +0100]
- Josh Ko ⇒ 喔，是有看到 GaoGaiGar 和 Great Ganbarugar 啦，可是都小小隻的，一點都不熱血。（一家店門口有等身大小的初號機，可是我沒很喜歡 Eva..） [2011-09-23 05:30:53 +0100]
中午吃旅館對面、晚上不開的拉麵店。販賣機上看到「味噌 XXX 半 XXXX」600 元，上來竟然是一碗味噌拉麵（這很難猜錯）+ 一盤炒飯！單看麵或飯的份量還好，加在一起就有點嚇人，幸好有吃完。這次拉麵的味道有達到想像中的鹹度了（上次和 scm 老師去吃的那家沒很鹹）。 [2011-09-23 05:19:46 +0100] [ 1 人說讚！]
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 人說讚！]
It took me quite a while to determine which route to take to reach Narita airport.. [2011-09-23 15:53:19 +0100] [ 1 人說讚！]
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]
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]
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]
到家了。觸鍵果然都跑掉了，光第一聲彈下去還以為鋼琴被掉包了！ [2011-09-24 18:54:34 +0100] [ 1 人說讚！]
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]
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]
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]
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

[facebook digest] Transfer dissertation and DTP'11

2011-08-31T15:40:00.000+01:00

Migrating to lhs2TeX for formatting my Agda code in documents. [2011-07-31 23:46:28 +0100]
- J************* ⇒ Hurrah! [2011-08-01 10:31:39 +0100]
All of a sudden, the first ever and only cat that was once in my keeping for a few months is dying in a pet hospital back in Taiwan. [2011-08-01 10:12:49 +0100]
- Josh Ko ⇒ "Men have forgotten this truth," said the fox. "But you must not forget it. You become responsible, forever, for what you have tamed. You are responsible for your rose..." [2011-08-01 10:20:07 +0100]
- J************* ⇒ Sorry to hear this, Josh. [2011-08-01 10:28:44 +0100]
- J************* ⇒ But you're right - tamed or not, you don't own a cat, you merely look after it. [2011-08-01 10:30:17 +0100]
It turned out that I didn't get the Dutch vector ornament right. Fusing the ornament with itself produces an ornamented list type that has 4 cons constructors instead of 3! [2011-08-01 11:16:27 +0100]
Jackie has decided to finish his dissertation in 14 days, i.e., on 14 Aug. In the next two weeks I'll be with him in the lab to make sure he does not visit YouTube during work time. (As for me, I will also attempt to finish my transfer dissertation. I've just decided not to include the Dutch National Flag problem in the transfer dissertation, so it might take only a week.) [2011-08-01 19:21:22 +0100] [ 4 人說讚！]
Jackie's determination to finish his thesis in 13 days! ↦ Comeback Victory of Oxford Doctoral Thesis! [2011-08-01 22:02:16 +0100] [ 1 人說讚！]
Moving to Marlborough Road on Thursday. [2011-08-02 08:28:02 +0100] [ 1 人說讚！]
Beginning the dissertation by quoting Dijkstra looks thrilling. [2011-08-02 10:04:29 +0100]
Could it be that weakest precondition and strongest postcondition are adjoint? [2011-08-02 11:03:13 +0100]
- J************* ⇒ Sounds plausible! [2011-08-02 18:04:50 +0100]
So it seems I will still write about the Dutch National Flag problem in the transfer dissertation, but not in full detail. [2011-08-02 11:27:12 +0100]
- Josh Ko ⇒ Just to illustrate what I mean by "programs also serving as proofs." [2011-08-02 13:25:49 +0100]
Hot weather is making me reluctant to do the packing.. [2011-08-03 16:10:52 +0100]
- 洪** ⇒ 台北也熱翻了！ [2011-08-03 16:33:55 +0100]
- W********** ⇒ lol no worries. No summertime anymore XD [2011-08-04 13:26:57 +0100]
Now I have a concrete plan for my dissertation (see below). [2011-08-03 23:45:04 +0100]
- Josh Ko ⇒ The first paragraph quotes Dijkstra and introduces DTP; then comes a section on DTP in Agda (adapting the material from the appendix of the WGP paper and simple examples in the essay), after which the solution to the Dutch National Flag problem is presented in ordinary DTP terms without mentioning ornaments; finally contrast externalism and internalism, point out the reusability problem of internalism, and state the initial result recorded in the WGP paper. The thesis proposal follows naturally. Will refer the examiners to the appropriate parts of the essay and the WGP paper, which will be attached as appendices. [2011-08-03 23:45:33 +0100]
Just carried all my belongings from the third floor down to the ground floor, now waiting for Duen-Wei, who kindly agreed to help by taking me to the new accommodation by car, to show up. [2011-08-04 08:30:44 +0100]
所以要搞應用才回得了台大嗎…？唉，算了，先弄完 transfer 吧。 [2011-08-04 09:47:20 +0100] [ 2 人說讚！]
- L************** ⇒ ？ [2011-08-04 09:48:25 +0100]
- T************* ⇒ @@ [2011-08-04 12:11:41 +0100]
- Josh Ko ⇒ 小惇學長幫我載東西到新家，提到 scm 老師 2006 年把 CV 傳給陳文進老師看，後者說這種完全純理論的台大應該很難接受，大概只有中研院會收吧。（結果果然跑到中研院？）欸，反正還久嘛，先享受再說⋯ [2011-08-04 14:13:03 +0100]
- 柯** ⇒ 做自己愛做的吧！ [2011-08-04 15:43:45 +0100]
- L************** ⇒ Josh Ko 可能要在國外闖出個名堂來，才能回去「降級」（薪水變少，研究環境較差，外出交流不便） ... [2011-08-04 15:53:37 +0100]
- S************ ⇒ 啊，都忘了有這回事。
  實在感謝小惇一直很關心大家哩.. [2011-08-04 16:33:33 +0100]
- 柯** ⇒ 醬的話，就不用回來丫~留在英國就好了…只是胃不知道願不願意配合就是了 [2011-08-05 14:51:38 +0100]
I cannot fit even the most basic version of the declaration of the Dutch vectors into the page.. [2011-08-04 16:50:20 +0100]
Cannot believe they can perform Tchaikovsky's Piano Converting No 1 so badly! I was really reluctant to clap after it was over! [2011-08-04 21:00:36 +0100] [ 1 人說讚！]
- Josh Ko ⇒ s/Converting/Concerto/ [2011-08-04 23:24:08 +0100]
- L************** ⇒ Why clap if you don't like it? [2011-08-05 00:09:40 +0100]
The house is now online! [2011-08-05 11:40:41 +0100] [ 1 人說讚！]
Now extremely seriously considering renting a Steinway grand piano (for £75 per month)!!! [2011-08-05 22:49:07 +0100] [ 1 人說讚！]
- Josh Ko ⇒ Unfortunately the piano was already rented. And on second thought, perhaps the living room is still just too small to accommodate a grand piano.. [2011-08-06 00:29:57 +0100]
- Josh Ko ⇒ Lots of information to absorb: http://www.robertspianos.com/ [2011-08-06 00:30:19 +0100]
Sigh, I think the top priority is not to annoy our neighbours. That probably means I shouldn't consider a grand piano at all. [2011-08-06 01:24:24 +0100]
Renting a piano for two years costs 72% of its price, while pianos sold by Roberts Pianos below £9,000 is now 15% off. It seems buying one and then selling it might be a cheaper option... (Gosh!) [2011-08-06 09:22:06 +0100]
The pricing is attractive, at only £58 per month. ↦ Roberts Pianos - Oxford - Portsmouth - London | Piano Details [2011-08-06 10:28:03 +0100] [ 1 人說讚！]
I've started to imagine that I can give one or two home recitals during the next two years. XD [2011-08-06 10:39:12 +0100] [ 1 人說讚！]
The landlord brought the gardener here at about 1.30 and we asked him what he thought about renting a piano. He said "please do," a straightforward positive answer I had not really expected! Pan and I will depart for Roberts Piano at 2.30, and Eric will join us after 3.00. [2011-08-06 13:44:40 +0100]
- Josh Ko ⇒ s/Roberts Piano/Roberts Pianos/ [2011-08-06 13:51:00 +0100]
Hm.. If I really manage to give a home recital, I might have to give two (or more) performances of the same repertoire for different circles of friends (e.g., one for departmental friends and another for Taiwanese friends), as the living room is not big and cannot accommodate all of them at once. (It's certainly too premature to plan this, of course. XD) [2011-08-06 13:50:05 +0100] [ 3 人說讚！]
The piano I rented. Full story to be posted later.. (Hungry..) ↦ Roberts Pianos - Oxford - Portsmouth - London | Piano Details [2011-08-06 18:15:42 +0100] [ 1 人說讚！]
Repertoire for the first home recital: I think it will definitely include some selected nocturnes and mazurkas! [2011-08-06 21:34:00 +0100]
"Harry took the wand. He felt a sudden warmth in his fingers. He raised the wand above his head, brought it swishing down through the dusty air and a stream of red and gold sparks shot from the end like a firework, throwing dancing spots of light on to the walls." [2011-08-06 23:02:54 +0100] [ 1 人說讚！]
超 Q 的⋯ ↦ 『君達に最新情報を公開しようコトブキヤ D-スタイル勇者王ガオガイガーご紹介【でじたみん】』 [2011-08-07 11:40:49 +0100] [ 2 人說讚！]
- L********** ⇒ Looks cool! How much? [2011-08-07 18:33:47 +0100]
- Josh Ko ⇒ Much less expensive than I had expected..
  http://goods.ruten.com.tw/item/show?21107218693617 [2011-08-07 19:22:14 +0100]
The Dutch National Flag problem may occupy more pages than I expected.. [2011-08-07 21:15:08 +0100]
- Josh Ko ⇒ Well, the transfer dissertation will look more solid, which is not a bad thing.. [2011-08-07 21:16:28 +0100]
我在中興新村養過的貓情況緊急，需要輸血⋯ 有可能的話請幫忙！ ↦ 維康動物醫院: 與我們聯繫/交通資訊 [2011-08-08 07:32:07 +0100]
I'll try to finish the first complete draft of the dissertation in three working days. [2011-08-08 08:46:35 +0100]
Hm, I have decided the programme for the first home recital and just produced a draft of the programme sheet.. (The power of procrastination. XD) [2011-08-08 23:17:30 +0100]
The Knight piano will arrive at 8 am on Friday! [2011-08-09 10:47:51 +0100]
- Josh Ko ⇒ Or even slightly earlier on the same day! [2011-08-09 11:28:36 +0100]
- Y*********** ⇒ I can't wait...... Hope our door is big enough : ) [2011-08-09 12:23:21 +0100]
And we received email saying that "there is a strong likelihood of trouble in Oxford city centre this evening".. ↦ Oxford violence as unrest spreads [2011-08-09 17:37:06 +0100]
- W********* ⇒ Take care of yourself! [2011-08-09 17:40:56 +0100]
From the Thames Valley Police Twitter: "Despite rumours there aren't any problems in Oxford." [2011-08-09 19:51:21 +0100]
- J********** ⇒ Does that mean i can now go ahead and buy the zinger from kfc @ cornmarket? [2011-08-09 19:58:33 +0100]
- Josh Ko ⇒ There aren't any problems.. yet. XD [2011-08-09 20:08:47 +0100]
Indeed, this will be the first time that I gain constant, everyday access to a piano since I went to university and "systematically" fell in love with Chopin. It's just natural to get excited! [2011-08-09 20:13:53 +0100] [ 1 人說讚！]
I think 25 minutes is a good estimate of the time needed to get to the lab from my new home. [2011-08-10 08:22:26 +0100] [ 1 人說讚！]
- L********* ⇒ Walking? [2011-08-10 12:03:19 +0100]
- Josh Ko ⇒ Yes. [2011-08-10 13:24:58 +0100]
I have basically the texts for the Dutch National Flag problem. Now I am reading the TikZ tutorial to draw some illustrative pictures. [2011-08-10 11:02:48 +0100] [ 1 人說讚！]
- L******* ⇒ Josh, is the area you stay in affected by the riots? Take good care of yourself! [2011-08-10 11:37:52 +0100]
- Josh Ko ⇒ No, Oxford is still as peaceful as usual. Thanks! [2011-08-10 13:25:57 +0100]
- W********* ⇒ 天呀你什麼時候偷偷加了皮卡! XD [2011-08-10 13:43:38 +0100]
- Josh Ko ⇒ 是 Peacock 加我的！XD [2011-08-10 13:47:54 +0100]
The red case for the Dutch National Flag problem (drawn with TikZ). ↦ Wall Photos [2011-08-10 14:24:23 +0100]
Now arrive at the last paragraph, which will briefly state the reusability problem and the initial result of the WGP paper. Expecting to send an email to Jeremy tomorrow! [2011-08-10 20:18:55 +0100]
Dijkstra's sad remark on p202 of A Discipline of Programming (see below). [2011-08-10 20:50:49 +0100]
- Josh Ko ⇒ "Sad remark. Since then we have witnessed the proliferation of baroque, ill-defined and, therefore, unstable software systems. Instead of working with a formal tool, which their task requires, many programmers now live in a limbo of folklore, in a vague and slippery world, in which they are never quite sure what the system will do to their programs. Under such regretful circumstances the whole notion of a correct program — let alone a program that has been proved to be correct — becomes void. What the proliferation of such systems has done to the morale of the computing community is more than I can describe. (End of sad remark.)" [2011-08-10 20:50:53 +0100]
Dijkstra on abstract machines vs. physical machines and computing science vs. computer science, from p201 of A Discipline of Programming. [2011-08-11 07:48:56 +0100]
- Josh Ko ⇒ Eventually, there are two "machines". On the one hand there is the physical machine that is installed in the computer room, can go wrong, requires power, air conditioning, and maintenance and is shown to visitors. On the other hand there is the abstract machine as defined in the manual, the "thinkable" machine for which the programmer programs and with respect to which the question of program correctness is settled.
  
  Originally I viewed it as the function of the abstract machine to provide a truthful picture of the physical reality. Later, however, I learned to consider the abstract machine as the "true" one, because that is the only one we can "think"; it is the physical machine's purpose to supply "a working model", a (hopefully!) sufficiently accurate physical simulation of the true, abstract machine.
  
  This change in attitude was accompanied by a change in terminology: instead of "computer science" the term "computing science" came into use and we no longer gave courses in "Programming for Electronic Computers" — we could not care less whether the physical machine worked electronically, pneumatically or by magic! But it was of course more than a mere play with words; it was the symptom that slowly the programming profession was becoming of age. It used to be the program's purpose to instruct our computers; it became the computer's purpose to execute our programs. [2011-08-11 07:49:02 +0100]
- Josh Ko ⇒ It's perhaps part of the reason that I am reluctant to approach parallel or distributed programming — I see no urgent need to move to this paradigm except to instruct the newly built machines, which shouldn't be the main driving force of the studies of computing! (You would be right if you call me an extremist.) [2011-08-11 07:59:00 +0100]
- Josh Ko ⇒ Natural scientists, however, do not have this luxury to shift the emphasis from the "reality" to the model. [2011-08-11 08:04:57 +0100]
- Josh Ko ⇒ Still, we are modelling (capturing) our intuition about computations using abstract machines, i.e., formal systems. In this respect, the critique made by empiricists should not be forgotten — we should not forget that formal notations must ultimately reflect our intuition, instead of becoming merely games of symbols. [2011-08-11 08:14:16 +0100]
- J************* ⇒ Natural science is the study of pre-existing physical systems in order to understand them; natural scientists don't build the systems they study, and they don't have the luxury of designing those systems to have desirable properties. If you think the objects of CS study are pre-ordained physical systems over whose design we have no influence, then perhaps "computer science" is the right term. But if you believe that we're in the business of designing our objects of study in the first place, then perhaps natural science isn't a good comparator, and "computer science" not the right term. [2011-08-11 11:13:17 +0100]
Indeed I need to write about the Dutch National Flag problem — now I have a bit more justification for the hypothetical "canonical upgrade" section. [2011-08-11 09:06:30 +0100]
Now I have all the contents of the dissertation. Will do formatting and revision in the afternoon. [2011-08-11 11:53:14 +0100] [ 1 人說讚！]
Transfer dissertation sent to Jeremy! [2011-08-11 17:44:05 +0100]
Finishing writing the dissertation on the day before the piano arrives - perfect timing! [2011-08-11 18:13:17 +0100]
The Knight piano arrived at 8 am! Quite sure it's the same piano after a bit of initial testing. The stool was forgotten, however. Will take photos after the stool is delivered. [2011-08-12 08:26:24 +0100] [ 1 人說讚！]
Is playing the piano at 9 am acceptable..? [2011-08-12 08:35:29 +0100]
- Y*********** ⇒ You can play Chopin in the morning and leave Beethoven in the afternoon : ) [2011-08-12 09:19:44 +0100]
這架騎士鋼琴錄起來的音色和家裡的滿接近的。
挑戰三天練成 Schubert's impromptu D 899 No 3? [2011-08-12 11:16:25 +0100]
- Josh Ko ⇒ 突然忘記，周六日要去 lab 啦 XD。 [2011-08-12 11:20:37 +0100]
- J********** ⇒ 辛苦你ㄌ! [2011-08-12 11:39:48 +0100]
Schubert 的這首 Impromptu No 3 in G-flat major, D 899 有種神祕但是很平靜的柔光。 [2011-08-12 20:10:48 +0100] [ 2 人說讚！]
- T************** ⇒ 就是那首很像紅磨坊那首xd [2011-08-20 05:58:32 +0100]
(Okasaki's Exercise 3.1) We can instead prove its converse: A leftist tree with a right spine of length n has at least 2^n - 1 elements. This can be proved by a simple induction on n. [2011-08-14 11:04:15 +0100]
Got an email response to the WGP paper, which was classified as junk mail and I was not notified of its existence until this morning. I got a follow-up message on Friday from one of the other receivers and was confused then. Now trying to work out a proper response.. [2011-08-15 08:07:23 +0100] [ 1 人說讚！]
- 陳** ⇒ 有發現就好，沒發現的話就囧了XD [2011-08-15 09:02:55 +0100]
Got my own copy of A Discipline of Programming! [2011-08-15 21:51:50 +0100] [ 3 人說讚！]
The stool will be delivered some time between 1.30 and 2.00! Will take some photos after that. [2011-08-16 12:41:53 +0100]
騎士鋼琴的音色超適合彈德布西⋯ [2011-08-16 19:35:03 +0100] [ 2 人說讚！]
Learned some basic accounting (after leaving the Department of Accounting for more than a year!). The idea is basically data refinement (assigning different meanings ("accounting subjects") to money so flows between subjects can be traced and each subject can be individually managed, etc.), and thus might be better explained in the category-theoretical language! (I'll leave this as a low-priority future work, however. XD) [2011-08-17 10:48:09 +0100]
- Josh Ko ⇒ The typical symptom of viewing every problem as a nail when you have a hammer? XD [2011-08-17 10:57:18 +0100]
- W********* ⇒ 猴子夠多的話什麼都能看成莎士比亞 [2011-08-17 13:51:54 +0100]
I had regarded "Programming Languages meets Program Verification" as grammatically incorrect, until I suddenly realised today that "Programming Languages" should perhaps be considered as the name for the research area (so it means that two areas meet each other, instead of that a bunch of programming languages meet the area Program Verification). [2011-08-18 10:56:04 +0100]
Don't forget this: "In fact, I think contemporary society is all mixed up in its concept of 'boredom': People often say to each other that they are bored, but to me this is almost a shocking, shameful admission. Why should it be somebody else's duty to entertain us? People who can't find anything of interest in what they are doing, who constantly need external sources of stimulation and amusement, are missing most of life's pleasures." - D.E. Knuth, Digital Typography [2011-08-20 07:36:40 +0100] [ 4 人說讚！]
- L*********** ⇒ oh, true, but i feel it's hard [2011-08-20 10:19:01 +0100]
- Josh Ko ⇒ As I always tell myself: No one says it's easy.. XD [2011-08-20 11:23:46 +0100]
- L*********** ⇒ yeah, i shall try harder... XD [2011-08-20 11:26:54 +0100]
(Hopefully) the final version of my transfer dissertation, which cites Dijkstra in the beginning (!), presents an incremental development of an internalist solution to the Dutch National Flag problem, and uses that to motivate a study of composable structures for dependently typed programming. ↦ Datatype ornamentation and the Dutch National Flag problem [2011-08-21 09:18:32 +0100] [ 1 人說讚！]
- Josh Ko ⇒ Er, just discovered a misalignment in Appendix A... [2011-08-21 09:36:11 +0100]
- Josh Ko ⇒ Corrected. [2011-08-21 09:50:24 +0100]
Must remember not to use excessive rubato. [2011-08-22 21:49:55 +0100]
- Josh Ko ⇒ Especially for Schubert's Impromptu No 3, D899, constant tempo is part of its texture. [2011-08-22 21:51:38 +0100]
- Josh Ko ⇒ Can be more explicit about the colours (e.g., dark and bright). [2011-08-22 21:53:21 +0100]
- Josh Ko ⇒ Op 55 No 1 was not bad! [2011-08-22 22:00:23 +0100]
- Josh Ko ⇒ (Even better than Op 9 No 2.) [2011-08-22 22:02:18 +0100]
- Josh Ko ⇒ Op 50 No 3 was still not as good as the recording I put on my personal webpage, but better than those I did with the piano in College. [2011-08-22 22:28:49 +0100]
- Josh Ko ⇒ Alright, perhaps just a liiiiittle bit of rubato for Schubert. [2011-08-22 22:34:38 +0100]
Ocean etude (Op 25 No 12) 已經達到練一練手會痠的速度了。 [2011-08-23 11:52:21 +0100] [ 1 人說讚！]
- L********* ⇒ 功力大增 XD [2011-08-23 11:59:23 +0100]
Should have discovered this earlier. ↦ Free Worldwide Travel Guides - Wikitravel [2011-08-23 14:32:22 +0100]
- Josh Ko ⇒ And it's fun to see the travel guide for Taiwan. "In mid-sized and smaller cities, your main reference point is going to be the train station. If you're having trouble finding English speaking people, try looking for college or high school students." These are helpful remarks! [2011-08-23 14:34:14 +0100]
Dijkstra was even more radical than I had imagined.. Compared to him, I am certainly an empiricist! [2011-08-23 20:44:33 +0100]
- Josh Ko ⇒ (EWD1036: On the cruelty of teaching computing science) [2011-08-23 20:46:49 +0100]
- Josh Ko ⇒ Dijkstra proposing what the first introductory programming course should look like: "[W]e teach what looks like the predicate calculus, but we do it very differently from the philosophers. In order to train the novice programmer in the manipulation of uninterpreted formulae, we teach it more as a boolean algebra, familiarizing the student with all algebraic properties of the logical connectives. To further sever the links to intuition, we rename the values {true, false} of the boolean domain as {black, white}."
  
  This might work, actually, in order to expose students to the "radical novelty" of formal systems, but I do not think it should go on for the entire course - one or two lectures/homework on this perspective might be reasonable, and then we bind it to the natural interpretation. [2011-08-23 21:07:03 +0100]
- Josh Ko ⇒ Dijkstra's second proposal that an imaginary language be used in order to force students to reason about their programs - as opposed to try to run and correct them blindly - sounds good, however. I think we can spend more time on this, say at least half of the course. [2011-08-23 21:12:38 +0100]
- Josh Ko ⇒ Dijkstra's approach, taken to the extreme, would be like teaching school children group theory before addition and subtraction, which is simply not the right order - group theory is merely an abstraction and has to come after what it abstracts. In exactly the same way, a formal system is merely an abstraction of our intuitive reasoning patterns. We can teach students in Dijkstra's way, but only to highlight the concept of formal systems, not to imply that computing is purely symbol manipulation. We should only be interested in *meaningful* symbol manipulation, i.e., formal systems that correspond to our intuition. (Even Dijkstra himself introduced the concept of state space using a concrete computing device in A Discipline of Programming, i.e., abstracting the concept from our intuition.) [2011-08-23 21:37:39 +0100]
- W********* ⇒ 老K 針對死D 的純粹理性嘴砲是說, "他覺得不必要的, 自己可都有經歷過, 也許這些經驗對於像他一個這麼優秀的程式員有其必要而他不知道." (大意) "他自己可不是那樣學的." (關鍵吐槽)
  
  我自己是覺得, 其實跟教法沒啥關係, 一種米養百款人XD [2011-08-24 19:19:51 +0100]
Updated the interests section on my personal webpage: "Shortly after I moved from college accommodation to a share house in August 2011, I rented a Knight K10 piano for two years and can now practise regularly, thanks to the support of my dear housemates." [2011-08-24 08:59:11 +0100] [ 3 人說讚！]
The problem with this set of slides is that lots of practice is required, much like performing an intricate piece of music.. [2011-08-25 22:22:43 +0100] [ 1 人說讚！]
Got past security. The gate will open in about 2 hours.. [2011-08-26 06:56:54 +0100]
Reviewed the slides and got a little bit more confident. [2011-08-26 07:59:24 +0100] [ 2 人說讚！]
And I forgot something important - I think Jeremy will need to sign my expense claim forms in Tokyo.. [2011-08-26 08:07:31 +0100]
- J************* ⇒ We can see if finance will accept an email from me instead... [2011-08-26 16:26:22 +0100]
Arrived at the hotel after a short tour in Nijmegen. (As Wikitravel commented, there are not many things left to see, despite that Nijmegen is the oldest city in the Netherlands.) Will (try to) do more practice in the evening. [2011-08-26 16:26:30 +0100] [ 4 人說讚！]
Delivered the talk. Epinephrine did its job well, although my Mac did not react to the projector properly in the beginning, I overran a slide in the middle, and people had to suffer my discontinuous sentences. Fortunately, the two questions raised after the talk were all addressed by the paper, one by the subsection "Realisability predicates for algebraic ornaments" and the other by footnote 2. And during lunch, Kai Trojahner told me he liked my talk! [2011-08-27 12:17:12 +0100] [ 3 人說讚！]
- Josh Ko ⇒ And Conor helped to answer both questions, one directly and the other indirectly. [2011-08-27 12:17:26 +0100]
- J********** ⇒ 老大, you're my hero! 電死他們!! [2011-08-27 12:28:50 +0100]
- Josh Ko ⇒ 我沒被電到就很好了 XD。 [2011-08-27 12:30:37 +0100]
- W************ ⇒ 聽起來很不錯! [2011-08-27 12:34:15 +0100]
- L********** ⇒ Sounds good! [2011-08-27 15:55:55 +0100]
- J************* ⇒ Well done! [2011-08-27 17:20:13 +0100]
Three more people - Conor, Cezar Ionescu, and a guy whose name I forgot to ask - told me that my talk was good, or at least the slides were good. (They were particularly impressed by what I did using Keynote's animations.) [2011-08-27 21:32:22 +0100]
- Josh Ko ⇒ Jeremy, Cezar asked me to say hi to you! [2011-08-27 21:33:46 +0100]
- J************* ⇒ Thanks! Too late now to ask you to say hello back... [2011-08-29 14:44:06 +0100]
The next task would be restructuring the slides for WGP. [2011-08-27 21:45:38 +0100]
- Josh Ko ⇒ into a more conventional structure - with motivations, backgrounds, etc. [2011-08-27 21:46:22 +0100]
- L********** ⇒ Hi are you at Oxford next week? [2011-08-27 23:47:05 +0100]
- Josh Ko ⇒ Yes, I'll be back today (but very late). [2011-08-28 07:43:14 +0100]
Almost forgot something very worth noting: Google Maps and GPS are *GREAT* inventions!! [2011-08-28 08:31:17 +0100] [ 4 人說讚！]
Arrived at the Schiphol airport, 3 hours before the flight. The security checks are distributed just outside every boarding gate. Hm.. I've never thought about this before. Does this increase the checking efficiency? [2011-08-28 17:37:40 +0100]
Can't wait to get back home.. [2011-08-28 17:38:21 +0100] [ 3 人說讚！]
- 翁** ⇒ 學成歸國嗎XD [2011-08-28 17:42:55 +0100]
- Josh Ko ⇒ The home in Oxford! [2011-08-28 17:43:11 +0100]
- Josh Ko ⇒ The home in Taiwan will have to wait for a few more months.. [2011-08-28 17:44:16 +0100]
Turns out I might do non-trivial adaptation to my slides.. [2011-08-29 10:15:29 +0100]
- J********** ⇒ 沒在怕的啦>< [2011-08-29 10:33:08 +0100]

New house and the Knight K10

2011-08-07T08:05:00.009+01:00

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

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

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

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

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

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

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

[facebook digest] Slides

2011-07-30T10:16:00.002+01:00

床前明月光，疑是地上霜；舉頭望明月，低頭思故鄉。 [2011-07-13 23:20:28 +0100] [ 4 人說讚！]
- W************ ⇒ You can listen to "登彼岸" [2011-07-18 15:38:17 +0100]
Dare I not raise the big question at the beginning of my talk? [2011-07-14 23:18:54 +0100]
- Josh Ko ⇒ I have to do so for WGP, I think; but for DTP it might be possible just to tell a story. Will do some experiments. [2011-07-14 23:23:33 +0100]
- Josh Ko ⇒ (Because not asking a question at the beginning can make the talk disorienting. The audience at DTP can be assumed to have more relevant backgrounds, though, so this might work for them.) [2011-07-14 23:42:08 +0100]
Not sure if internalist dependently typed programming will succeed. If programs and proofs are to be composed simultaneously, wouldn't that violate the principle of separation of concerns? Is there some way to defend internalism (against the principle)? [2011-07-15 21:46:44 +0100]
- Josh Ko ⇒ Perhaps we just need both internalism and externalism. Program in the internalist way to show that the program is constructed with some sort of correctness in mind; prove afterwards in the externalist way that the program has other properties. [2011-07-15 22:01:53 +0100]
- Josh Ko ⇒ This is not entirely convincing, though.. I hope I won't have to make the conclusion in my thesis that internalism should be abandoned. [2011-07-15 22:18:39 +0100]
- J************* ⇒ Best of both worlds? [2011-07-16 18:21:15 +0100]
- Josh Ko ⇒ Yeah.. I guess that's the way to go. [2011-07-16 19:36:05 +0100]
《悲愴》的震撼至今尚未消散。 [2011-07-15 23:37:08 +0100]
- W************ ⇒ 為何？ [2011-07-18 15:36:42 +0100]
- Josh Ko ⇒ 可看我 blog. [2011-07-18 15:37:51 +0100]
Gattai - sorted vectors! [2011-07-16 15:28:27 +0100]
Killer effect of Keynote. ↦ Sorted vectors = sorted lists + vectors [HQ] [2011-07-16 19:43:02 +0100] [ 3 人說讚！]
- 曾** ⇒ Magic Move! [2011-07-16 20:07:51 +0100]
- L************** ⇒ Cool! [2011-07-16 21:00:12 +0100]
Kant's justification of faith (or the lack thereof) is comparable to the introduction of extensional substitution in observational type theory.. [2011-07-17 21:27:48 +0100]
谷歌翻譯可以正確翻譯「傑瑞米長臂猿」耶 XD。 [2011-07-18 16:52:53 +0100] [ 2 人說讚！]
"Haskell Curry (1900-1982): He worked in combinatory logic. There is a programming logic named after his first name! (see here). Sane!"

... "programming logic?" Interesting choice of term.. ↦ Computational Complexity: Disproving the Myth that many early logicians were a few axioms short of a [2011-07-18 19:58:56 +0100] [ 1 人說讚！]
The word "reify" does not appear in LDOCE (and spell checker)! Oxford dictionary includes it, though, and says it originated in mid 19th century — no wonder! [2011-07-19 09:33:35 +0100]
Hmm.. Ornament composition is not yet a pushout in the present ornament language. Permutations of fields need to be taken into consideration. That can be messy... [2011-07-19 19:37:58 +0100]
I dare not use the title "One more thing"... [2011-07-19 21:36:49 +0100]
- Josh Ko ⇒ But it's tempting! [2011-07-19 21:38:44 +0100]
Fitting the third paragraph of the discussion section as the special slides for DTP. (For WGP it would be... datatype-generic implementation details?! Er.. will think about that later.) [2011-07-19 22:34:58 +0100]
Great! I believe I have an adequate set of slides now. The remaining work is to make sure I can give a good performance. (The control of timing and expressions is less demanding than that required for performing a piano piece, but the principles are similar, I think.) [2011-07-19 23:55:24 +0100]
Title page. ↦ Wall Photos [2011-07-20 00:18:31 +0100] [ 4 人說讚！]
- Y********** ⇒ 右上角那個好俏皮呀 XDD [2011-07-20 08:27:51 +0100]
- Josh Ko ⇒ 旋轉 10 度，效果就不一樣 XD。
  （另外，擺那個是要提示聽眾有 paper 可以看。） [2011-07-20 08:42:51 +0100]
Read a bit more fibred category theory, waiting for the installation of Lion to complete. [2011-07-20 14:17:42 +0100] [ 2 人說讚！]
- Josh Ko ⇒ It was estimated to take 33 minutes. [2011-07-20 14:20:52 +0100]
- Josh Ko ⇒ In Lion! [2011-07-20 14:38:08 +0100]
- Josh Ko ⇒ It can take some time to get used to the opposite scrolling direction and different gestures. [2011-07-20 14:50:29 +0100]
The UI design of the new OS X is not (yet) perfect this time... (Leopard was a success.) [2011-07-20 18:47:24 +0100]
- Josh Ko ⇒ Integration of the UI of Keynote into Lion is particularly crappy. [2011-07-20 18:56:29 +0100]
TeXShop for Lion, supporting Resume, Auto Saving (and Versioning), and Full Screen Mode! ↦ TeXShop [2011-07-21 14:42:04 +0100] [ 1 人說讚！]
- L********* ⇒ How's OpenVanilla? Will it work in Lion? [2011-07-21 15:02:21 +0100]
- Josh Ko ⇒ I use the built-in input method. XD [2011-07-21 15:03:26 +0100]
- L********* ⇒ But, I don't like it! XD
  I still remember that I trying to use simplified chinese IM on Lion DP2 version few month ago... [2011-07-21 15:11:07 +0100]
這隻 King J-Der 也太夢幻！要是可以變型就真的是極品了啊。（轉自 ptt BraveSaga 板 #1E86XoUK） ↦ http://www.amiami.jp/blog/2011/07/fes_01cgk/11.jpg [2011-07-21 21:01:52 +0100] [ 1 人說讚！]
- Josh Ko ⇒ 不過網上有人指出如果為了變型而照原比例做的話看起來滿慘的⋯ [2011-07-21 21:04:27 +0100]
- Josh Ko ⇒ http://tieba.baidu.com/f?kz=325206746 [2011-07-21 21:07:14 +0100]
Developing my "interpretation" of the slides. [2011-07-21 23:03:25 +0100]
30 + 4 slides for a 25-minute talk, the additional four slides being special slides for DTP, which might not fit into the talk due to the time limit, however. 30 slides, then, which seems to be a reasonable number, taking into account that a few of them are transitional. Will know more exactly how much time is needed after I rehearse the presentation. [2011-07-22 00:06:58 +0100]
I will go to this one. ↦ Stephen Hough and Oxford Philomusica | Oxford Philomusica [2011-07-23 23:00:59 +0100] [ 1 人說讚！]
I think I did better than I had expected as a demonstrator for the first time (for the UNIQ summer school). (Three days to go.) ↦ UNIQ summer schools at Oxford - University of Oxford [2011-07-25 18:59:30 +0100] [ 3 人說讚！]
ICFP is expensive... [2011-07-25 19:12:35 +0100]
- Josh Ko ⇒ About £360 for ICFP, WGP, and Haskell Symposium (student price). [2011-07-25 19:13:28 +0100]
- J********** ⇒ ㄑ, 還好啦我去 QSIC ㄉ註冊費要 £485 ㄉ說 [2011-07-25 19:14:44 +0100]
- J********** ⇒ 當然沒 funding 就另一個故事ㄌ [2011-07-25 19:15:29 +0100]
- L************** ⇒ CALCO costs over £500 ... [2011-07-25 19:16:48 +0100]
- Josh Ko ⇒ I had better keep all the receipts very carefully.. [2011-07-25 19:18:30 +0100]
- L************** ⇒ I think the school can pay them directly... [2011-07-25 19:19:42 +0100]
- Josh Ko ⇒ It doesn't seem to be easier, though. [2011-07-25 19:27:22 +0100]
Visa exemption! It's great to be a citizen of Taiwan. [2011-07-25 19:31:48 +0100]
Second day. The part in my brain that handles English didn't work quite well in the morning, but it became normal in the afternoon. Dealt with a lot of parsing errors - teaching syntax *is* important.. [2011-07-26 18:11:49 +0100]
Fire alarm at 6 in the morning. Whoever forgot about his/her toast didn't (dare to?) show up. [2011-07-27 06:19:03 +0100]
Jeremy is now Professor Gibbons!!! [2011-07-27 16:39:33 +0100] [ 3 人說讚！]
- T************** ⇒ 手很長 [2011-07-28 07:02:33 +0100]
- Josh Ko ⇒ 很好。 [2011-07-28 08:16:31 +0100]
Practised the presentation again. Cannot believe I could do it so badly.. [2011-07-27 21:55:39 +0100] [ 1 人說讚！]
- J********** ⇒ Wanna present it to me tmw? [2011-07-27 22:36:42 +0100]
- Josh Ko ⇒ Thanks, but tomorrow is definitely too soon - I need more practice! [2011-07-27 22:47:36 +0100]
- J********** ⇒ That's exactly the point though, cuz if you keep practicing in the same manner, the same shortcomings, if any, would stay... but certainly no pressure, let me know if feel like~~ [2011-07-27 22:49:40 +0100]
- Josh Ko ⇒ You're right, but now I cannot satisfy even myself - it might be said that the presentation is still in an early draft form, so it's just premature to ask for comments from others. [2011-07-27 23:02:49 +0100]
- Josh Ko ⇒ More precisely: I am still thinking about what to say and how to say them.. [2011-07-27 23:05:24 +0100]
- J********** ⇒ cool... my offer is upon your request~ [2011-07-27 23:18:26 +0100]
Managed to see one kid cracking the Caesar cipher and another cracking RSA. [2011-07-28 18:36:26 +0100]
- Josh Ko ⇒ However, I think some of them suffered from my non-proficient English.. [2011-07-28 18:41:39 +0100]
MS (Research) now does dependent types. ↦ Fstar: Secure Distributed Programming with Value-Dependent Types - Microsoft Research [2011-07-28 21:56:21 +0100]
那時候做白色版社會司中辦團體服的設計理念是不要太顯眼，結果到牛津這裡已經被問好多次那塊 QR code 的內容是啥⋯（用英文寫「社會司中辦」到這裡也變成很自然看得懂的字⋯） [2011-07-29 19:34:08 +0100] [ 1 人說讚！]
The phenomenon Jackie is experiencing. ↦ PHD Comic: The Repulsor Field Explained [2011-07-29 20:09:20 +0100] [ 2 人說讚！]
- J********** ⇒ What the hell is wrong with Jackie? [2011-07-29 20:10:11 +0100]
- Josh Ko ⇒ Nothing: It's a natural phenomenon, as explained by the comics! [2011-07-29 20:12:34 +0100]
- J********** ⇒ 傑瑞米, 千萬不能跟吉姆講這件事ㄡ!! [2011-07-29 22:31:02 +0100]
Oxford has appeared on the screening list! ↦ The PHD Movie! [2011-07-29 20:50:16 +0100]
Wow, this is very democratic... "all participants are given 5 minutes for a quick “advertisement” of their proposed talk in the morning of 14th Sep. Participants then vote for talks they would like to listen to, and the programme is scheduled accordingly." ↦ Dependently Typed Programming [2011-07-29 22:41:31 +0100] [ 1 人說讚！]
- Josh Ko ⇒ And there are lots of familiar names.. I suppose they will stay for ICFP too? (Thrilling.) [2011-07-29 22:46:20 +0100]
- Josh Ko ⇒ Shonan 是湘南；湘北比較有名吧？XD [2011-07-29 22:57:46 +0100]

--
Updated the extraction program so the "like" counts are restored.

倫敦悲愴

2011-07-17T14:39:00.006+01:00

《悲愴》的震撼至今尚未消散。

六月三十日在 Royal Festival Hall，Christian Vásquez 指揮 Philharmonia Orchestra，上半場以白遼士的《羅馬狂歡節》序曲開場（Overture, Le carnaval romain, Op. 9），然後與臨時代班的 Nikolai Demidenko 演出拉赫曼尼諾夫《第三號鋼琴協奏曲》。Demidenko 風格嚴謹，每一句都刻畫得相當仔細，雖然少了點狂野奔放，但也得以清晰呈現拉赫曼尼諾夫曲子那種精巧繁複的紋理。

然而，要找到能和《悲愴》同擺在曲目裡而不相形失色的曲子實在不容易。（在我目前相當有限的已知曲單裡是找不到的。）下半場《悲愴》登台，再次將我席捲其中。特別是晦暗中透著光明的第四樂章，樂團合奏竟能表現深沈的孤寂！儘管中間一段極其溫暖，但那是夾在更長的寒冷之間 — 孤寂才是常態⋯。尾奏，低音大提琴踏著沈重但穩定的腳步邁向死亡，上層旋律逐漸崩解，只剩下那穩定的腳步聲，低沈而分明，遠去，停止。指揮的右手停在結束手勢，全場靜默。

啊，那時彷彿在場的人都同感那深沈的孤寂，整個音樂廳裡的意志合而為一，為無止盡的黑暗所震懾。那不再是我自己的孤寂，而是一個群體的孤寂 — 不是群體內個別孤寂的聚合，而是整個群體因為知道自己是唯一得以感受此一震撼的群體（as the audience of that particular concert, or as human beings that are able to perceive the emotions）而共同領悟到的孤寂。整曲的悲喜冷暖，特別是第四樂章自無止盡黑暗中透出而更顯珍貴的光亮，得以感受這些情感正是我（們）的特質！

掌聲、地鐵、牛津街道。我不覺得「第四樂章象徵死亡」是精確的說法，說是死亡前對生命的回顧或許更貼切。這樣的回顧可不限於哪個時候才做，畢竟死亡隨時可能登門造訪。以死亡為背景，這樣的回顧更顯真實深刻。

--
希望還有機會複習。

[facebook digest] Double acceptance

2011-07-13T18:17:00.001+01:00

I find that thinking about an adjunction in terms of the unit and counit (instead of the natural bijection) is easier, as they can be interpreted as saying that the left adjoint finds the least upper bounds and the right adjoint finds the greatest lower bounds in a certain sense. (The natural bijection is essential for calculation, of course. But I tend to express it with the unit and counit to see what's going on.) [2011-06-30 04:32:47 +0100]
- Josh Ko ⇒ > The natural bijection is essential for calculation, of course. But I tend to express it with the unit and counit to see what's going on.
  
  This is what we do to explain the meaning of the natural bijection anyway (deriving the unit and counit on the fly and stating their universal property). [2011-06-30 04:35:58 +0100]
- Josh Ko ⇒ I still haven't penetrated the symmetry of adjunctions, but I'll leave this mystery to a later time. (Yes, the form of the natural bijection is perfectly symmetric, but I am not satisfied with just a formal explanation.) [2011-06-30 04:43:54 +0100]
- L********** ⇒ We all stayed up late working, hehe [2011-06-30 18:04:28 +0100]
- Josh Ko ⇒ No, I got up early. ;) [2011-06-30 19:23:28 +0100]
Incredibly fine-grained Rach3! [2011-06-30 20:48:39 +0100]
Even if I, as an individual being, am not alone and can assume that human beings share the same way of thought, we humans as a collective being would still very likely be alone. (Some random thought after listening to another successful performance of Pathétique.) [2011-07-01 01:45:29 +0100]
Got a new HTC Wildfire S to replace my frequently crashing ZTE Racer. [2011-07-01 13:05:03 +0100]
- L************** ⇒ Try to sync it with your google account ...:p [2011-07-01 13:10:41 +0100]
- 王** ⇒ 我才剛拜了一臺Desire S [2011-07-01 13:25:50 +0100]
- Josh Ko ⇒ 也可以打中文！ [2011-07-01 14:08:46 +0100]
- Josh Ko ⇒ > Try to sync it with your google account ...:p
  
  This is definitely the worst part of it.. [2011-07-01 15:37:50 +0100]
- W************ ⇒ 我最近也想換智慧型手機 [2011-07-01 16:44:16 +0100]
- Josh Ko ⇒ 在外面可以上網、收信挺方便的，然後地圖導航功能特別實用！我這次去荷蘭就靠我的手機了 XD。 [2011-07-01 16:52:03 +0100]
- W************ ⇒ HTC Wildfire S 好用嗎? 雖然被評為入門機 [2011-07-01 16:56:47 +0100]
- Josh Ko ⇒ 到目前為止我覺得還不錯啊，上網上 FB 收信查地圖都滿順的，而且肯定比 ZTE Racer 好用 XD。 [2011-07-01 17:06:50 +0100]
- C************ ⇒ 我也爆想換的....Sensation啦!! [2011-07-02 04:50:43 +0100]
- W************ ⇒ 那台雙核機好像有問題聽說目前不穩 [2011-07-02 16:46:52 +0100]
Dear Hsiang-Shang,

We are happy to inform you that your paper

Modularising inductive families

has been accepted to the WGP'11 workshop. Congratulations!

[...] [2011-07-01 21:57:07 +0100]
- Josh Ko ⇒ Evaluation given by the second reviewer, who is obviously an expert:
  
  > This is an extremely well written but tense paper, so reading it was challenging but also very much fun.
  
  I am really flattered by this comment!
  
  > The research reported is clearly exploratory at this stage. It is difficult to conclude anything very deep or definitive from the paper,
  
  Indeed; however, the whole story is what my thesis will be about (hopefully)!
  
  > but I find the discussion of the methodology of DTP very insightful and valuable.
  
  It is also the part of the paper I like most. (I realised those points I made in that part only after I had an early draft of the paper, and was eager to share them.)
  
  > I must acknowledge that although I am familiar with McBride's work on ornaments broadly, I haven't seen his journal paper and hence cannot quantify the delta of this paper wrt what was already done by McBride. But the exposition is very strong.
  
  Again flattered. I am now more confident about my writing ability!
  
  Two strong accepts (one of which rated by the second reviewer) and one accept — I feel great right now! [2011-07-01 23:29:54 +0100]
- R*********** ⇒ Congrat.! [2011-07-02 02:13:16 +0100]
- 陳** ⇒ 恭喜學長呀~!!! [2011-07-02 05:08:30 +0100]
Bought the Longman Dictionary of Contemporary English (5/e) for my Wildfire S! [2011-07-03 00:05:35 +0100]
Should have guessed that the music room would look like this after the ball. (I managed to manoeuvre through this mess to reach the piano, though.) ↦ Wall Photos [2011-07-03 17:22:28 +0100]
Less vaguely, what the fourth movement of Pathétique told me this time was to learn to be lonely. [2011-07-03 19:50:25 +0100]
I'll do a bit of fibred category theory everyday in the morning (in principle XD)! [2011-07-04 09:45:14 +0100]
Had better go shopping before the predicted heavy rain arrives. [2011-07-05 09:49:51 +0100]
Travel arrangements... [2011-07-05 14:50:34 +0100]
- Josh Ko ⇒ very annoying! [2011-07-05 15:01:23 +0100]
- L************** ⇒ As annoying as arranging a meeting [2011-07-05 15:06:17 +0100]
- Y************* ⇒ Where are you going? [2011-07-05 15:58:16 +0100]
- Josh Ko ⇒ Nijmegen (The Netherlands) in August and Tokyo in September. [2011-07-05 16:03:01 +0100]
- Y************* ⇒ That's cool! [2011-07-05 16:03:23 +0100]
- Y************* ⇒ How long are you gonna stay in Japan? [2011-07-05 16:03:42 +0100]
- Josh Ko ⇒ 5 days, I think, but I'll be attending the conference and workshops for most of the time. [2011-07-05 16:06:29 +0100]
- Y************* ⇒ oh ~ do you go there by your own? [2011-07-05 16:07:10 +0100]
- Josh Ko ⇒ I guess so.. But my supervisor and ex-boss will be in Tokyo too! I am hoping that my ex-boss, who stayed in Tokyo for his postdoc, can give us a short tour then. XD [2011-07-05 16:10:42 +0100]
- Y************* ⇒ That's cool. [2011-07-05 16:11:52 +0100]
- 洪** ⇒ 你要去哪裡參加研討會阿？好可惜都不能盡興玩！ [2011-07-05 16:14:06 +0100]
- Josh Ko ⇒ 荷蘭一個老城市 Nijmegen（八月底）和東京（九月下旬）。我是沒特別喜歡玩啦，所以沒差 XD。 [2011-07-05 16:16:17 +0100]
- 洪** ⇒ 好羨慕你喔！真的！我去英國把錢燒光了只能再賺錢準備下一次的旅行，還有我回台灣後跟朋友講了你的善心事跡，喔•••大家好想認識你喔！hahaha [2011-07-05 16:22:30 +0100]
- S********** ⇒ Josh Ko 是好人 ^^ [2011-07-05 16:42:29 +0100]
- Y************* ⇒ 善心事蹟？我也要聽？他幹嘛了？ [2011-07-06 03:29:41 +0100]
- Josh Ko ⇒ 欸⋯ 可參考 http://www.facebook.com/100001276392360/posts/179924578726754 XD。 [2011-07-06 09:11:40 +0100]
- Y************* ⇒ I got it...so she is the one. [2011-07-06 15:28:16 +0100]
New word learned yesterday. ↦ Recumbent bicycle - Wikipedia, the free encyclopedia [2011-07-05 15:56:42 +0100]
莊老師寫的交通資訊多有誠意呀！ ↦ transport [The Ninth Asian Symposium on Programming Languages and Systems, APLAS 2011] [2011-07-05 16:04:28 +0100]
- Josh Ko ⇒ 還可以簽名 XD。 [2011-07-06 13:58:29 +0100]
- Y********** ⇒ 嗚嗚，我沒有 Jeremy 的書可以簽名 OQ [2011-07-06 18:01:44 +0100]
After reading Terence Tao's latest blog post (only the first paragraph, apparently), what he called "proof mining" is quite similar to the result I'd like to have, namely refinement of program types. (To me, what he said looks like turning a program that produces, say, a natural number to one producing a finite number.) ↦ Polynomial bounds via nonstandard analysis « What’s new [2011-07-06 09:45:40 +0100]
- Josh Ko ⇒ Quote: "In many cases, a bound can eventually be worked out by performing *proof mining* on the argument, and in particular by carefully unpacking the proofs of all the various results from infinitary mathematics that were used in the argument, as opposed to simply using them as “black boxes”, but this is a time-consuming task and the bounds that one eventually obtains tend to be quite poor (e.g. tower exponential or Ackermann type bounds are not uncommon)." [2011-07-06 09:47:50 +0100]
The city changes its character by replacing undergrads with tourists; DPhil students always stay, however. [2011-07-08 14:26:36 +0100]
Just sent out my registration form for ITP (with which DTP is affiliated). Air tickets booked, hotel rooms reserved, travel insurance applied for — I think I can start working on the slides.. [2011-07-08 15:39:12 +0100]
Oh my goodness, it's fortunate that I decided to print the paper and read it thoroughly again. I still spot little typographical errors... [2011-07-08 17:51:00 +0100]
- J************* ⇒ It's always a bad idea to read it after it's submitted :-). [2011-07-08 17:55:42 +0100]
Now I find myself making nontrivial revisions... [2011-07-08 22:17:18 +0100]
Every time I read the discussion section (of the OAOAOO paper) I invariably feel that this is indeed the kind of paper I'd love to write. [2011-07-09 10:59:28 +0100]
The hard decision I face now, after completing another revision: to submit the paper directly, or read it again tomorrow? [2011-07-09 11:44:58 +0100]
- Josh Ko ⇒ I'll just review those parts where I made nontrivial revisions.. [2011-07-09 15:09:51 +0100]
Submitted! (Meaning I should not read the paper again unless it is returned. XD) [2011-07-09 16:34:43 +0100]
- 陳** ⇒ AC~~~~~~~~~~ [2011-07-09 16:48:00 +0100]
- Josh Ko ⇒ This time (and for the first time) I submitted my work to the *real* ACM. XD [2011-07-09 16:53:23 +0100]
作者: ByKiss (白親) 看板: Gossiping
標題: Re: [新聞] 台語被稱閩南語學者明抗議教部
時間: Thu Jul 30 04:27:00 2009

[...]

另外補個大家也許不知道的東西，
有機會看到新加坡人名字的羅馬拼音時可以注意一下，
他們的姓氏，時常都是以閩南地區的方言下去拼音，
而不是用華語。

例如王先生的王，他們會拼做Ong，
這是蠻有趣的一個現象。 [2011-07-10 20:44:42 +0100]
- Josh Ko ⇒ Luke Ong!! [2011-07-10 20:44:52 +0100]
- M*********** ⇒ 其實他姓翁，不是王。 [2011-07-10 21:05:42 +0100]
- Josh Ko ⇒ 哎呀，好可惜 XD。 [2011-07-10 21:09:52 +0100]
- T************** ⇒ Ng BigPiece 給你猜這是誰 [2011-07-11 00:55:07 +0100]
- P************* ⇒ yes 遇到有個姓蘇的她是用Sow instead of Su [2011-07-11 00:57:53 +0100]
- T************** ⇒ 樓上...廣東話差不多也是這樣拼，不能當福建話的例子 [2011-07-11 01:01:47 +0100]
- P************* ⇒ BTW 她是新加坡人新加坡華人大部人是福建移民講閩南語 checked!
  如果連其他方言都要考慮才能舉例的話那豈不是要.很.忙.了 [2011-07-11 02:37:06 +0100]
- Josh Ko ⇒ @TS: 呃⋯ 直譯是大塊？ [2011-07-11 08:10:07 +0100]
- T************** ⇒ 是大塊 [2011-07-11 13:19:14 +0100]
Met the college cat of Hertford just outside the college's entrance yesterday. It was well cared for and very friendly to humans (which made me guess correctly that it's a college cat). ↦ Panoramic View [2011-07-11 15:03:55 +0100]
- L********** ⇒ There may be another one, which is blonde [2011-07-11 23:59:59 +0100]
- Josh Ko ⇒ Hm.. Perhaps you are referring to New College's cat?
  http://www.facebook.com/group.php?gid=348485626674 [2011-07-12 00:13:11 +0100]
- L********** ⇒ Not sure...I saw it in Hertford...very cute! [2011-07-12 00:18:12 +0100]
"The little prince went away, to look again at the roses. 'You are not at all like my rose,' he said. 'As yet you are nothing. No one has tamed you, and you have tamed no one. You are like my fox when I first knew him. He was only a fox like a hundred thousand other foxes. But I have made him my friend, and now he is unique in all the world.' " [2011-07-12 00:33:06 +0100]
- Josh Ko ⇒ It's hard to quote The Little Prince - I would have quoted the entire section about the fox if I could. [2011-07-12 00:41:20 +0100]
- 王** ⇒ 這和我之前跟你提過的花被吃掉的那段很像呀 [2011-07-12 08:26:39 +0100]
Being very inefficient when trying to work out the research proposal.. [2011-07-12 20:26:22 +0100]
- Josh Ko ⇒ Let's just produce something and send it to Jeremy tomorrow. I quite believe he will have better ideas. [2011-07-12 23:00:35 +0100]

[facebook digest] Dutch National Flag

2011-06-27T15:36:00.002+01:00

Kind of understood (or guessed) how observational equality works, finally. The missing details can wait until I meet the authors next time.. [2011-06-04 22:23:32 +0100]
This site is amazing! ↦ Bathrobe's "Harry Potter in Chinese, Japanese & Vietnamese Translation" [2011-06-05 11:29:50 +0100]
Got back from the Supervisors' Dinner. It's apparent that I am very bad at socialising with people, at least much slower than usual. Well, since long ago I have kind of accepted that, and I have decided not to try very hard to change that (except for a very short while). But perhaps I should say sorry to those people who have to tolerate the slow and usually irresponsive and thus monotone interaction with me. [2011-06-06 23:08:37 +0100]
- W************ ⇒ 加油 ! [2011-06-07 03:27:46 +0100]
- W************ ⇒ Maybe I will have the same difficult with you. I am tired to be social with people. [2011-06-07 03:28:51 +0100]
So this is it! ↦ 公開徵求 2011 台英(NSC-RS)合作交流互訪計畫 [2011-06-07 08:38:39 +0100]
Celebration twice a day.. It's fortunate that I am on the third floor. [2011-06-07 12:37:21 +0100]
昨天學院舉辦「與老闆晚餐」，席間聊到醫生待遇，Jeremy 突然問我台灣情況如何。我用平均一秒講一個字的慢速破破爛爛地湊出一點東西，像是前一陣子才一個實習醫師工作壓力太大過世、雖然薪水和社會地位都高但是十分辛苦、家長普遍希望小孩讀醫等等。當三個人盯著你等你講完的時候，用這種速度講話實在無比尷尬 — 而且他們的語速都是一秒四、五個字吧⋯ 我竟沒想到可以講名駒醫師才在他個板上貼的「與第一線難纏病人接觸」的記錄（與情緒發泄），或描述更久以前我所身處的詭異氛圍（見連結）。只能說遇到這種場合我就整個慌了。 ↦ 摃龜了............. [2011-06-07 20:09:33 +0100]
- L*********** ⇒ 欸，背景雜訊這形容真貼切。旁人講中文偶爾會對我形成干擾，然英文完全不會，我得「認真」才有辦法聽進去，一恍神就會變雜訊。這個界線在哪呀... [2011-06-08 08:56:14 +0100]
- 柯** ⇒ 是不是從小我都沒有給你表達的機會，常常都是我一個人在講，所以沒有開發你閒話家常這方面的天賦呢？回台時姐姐給你最密集的特訓，看在可能元兇是我的份上，算你免費！ [2011-06-08 16:11:36 +0100]
Now I think what I had in mind and didn't manage to express was that my high school classmates who did very well academically were encouraged to study medicine and congratulated for being admitted into the programmes; the atmosphere then is in sharp contrast with the almost cruel situations they face now, having started working. [2011-06-07 21:08:03 +0100]
- Josh Ko ⇒ The problem is that I need quite some time to express that in words. I guess I am just used to taking my time writing down these kinds of thoughts rather than talk about them on the fly (without having written them down). [2011-06-07 21:08:07 +0100]
- Josh Ko ⇒ Even if I manage to come up with a response, the topic is very likely to have already changed... I am just slower, to sum up. [2011-06-07 21:21:12 +0100]
- Josh Ko ⇒ Regarding the sharp contrast, actually I do not have further comments. I myself would not choose that path, but it's perfectly fine for others to do so. If I must conclude with something, then it's just "C'est la vie," i.e., 老師：「這就是人生啊 ( ′-`)y-～」 [2011-06-07 21:34:57 +0100]
- P************* ⇒ sorry I don't think this really matters.... It's worthless to guess others' thought. They might not even think about this matter. At least you had tried your best to sincerely express yourself. On the other hand, you may induce them to speak your mother tongue which is Mandarin or Taiwanese, and let's see who will be the slower. [2011-06-07 21:47:21 +0100]
- Josh Ko ⇒ Well, indeed this has little to do with what others think. (I may have to add that the three people, one of them being my dear supervisor, in fact listened very patiently to me when I spoke, for which I am very grateful.) It's just that I was once again reminded by myself of how awkward I am at expressing my own thoughts, so I reviewed the situation as I tend to. Besides, I am also slow even when I use Chinese, so it's a more fundamental issue than using foreign languages (although having to use foreign languages does have its negative effect). [2011-06-07 22:08:20 +0100]
退伍一週年！ [2011-06-09 08:53:22 +0100]
- L********* ⇒ 我還要好久才能講這句話 orz [2011-06-09 17:54:31 +0100]
I think the reviewers expected a student who is troubled by his illness and requiring advice regarding his slow progress. They looked surprised to hear that I've just submitted a paper for publication. They gave the advice anyway: suspension, even though the term has passed, but added that given that I and perhaps my supervisor feel I am back on track it may not be necessary. [2011-06-09 11:32:59 +0100]
- Josh Ko ⇒ The maths professor who came in place of my college advisor asked "is it going to be published?" and I answered yes. Was that the right answer? It seemed to imply that the paper has been accepted, since the professor later said something like "as you've already had a paper under revision...". [2011-06-09 11:36:33 +0100]
Submitted a dummy paper which was withdrawn immediately. It was numbered 10... [2011-06-09 11:45:48 +0100]
- Josh Ko ⇒ Not a good way to use the system, I admit. I'll never do this, forgive me... [2011-06-09 11:49:24 +0100]
Always stuck at the last sentence.. [2011-06-09 15:57:24 +0100]
WGP '11 hasn't been cancelled, nor is there a further extension. I take that as a good sign. XD [2011-06-10 15:06:56 +0100]
Still amazed by Op 50 No 3. Just look at this delicate weaving of the theme and contrapuntal ornamentation! ↦ Wall Photos [2011-06-11 09:47:35 +0100]
"[M]ost of us experience (even if we do not analyse) music as a 'flowing state', shaping time through tension and release, growth and decline, intensifying and resolving impulses. [2011-06-12 10:14:41 +0100]
- Josh Ko ⇒ These operate, moreover, on different structural levels, so that material which is unstable or 'dissonant' at the foreground (the level of the phrase, for example) may be stable or 'consonant' at the background (the level of the paragraph or of the entire piece). The relationship of such intensity curves to the static external pattern or design of a piece, in itself perceivable only after the event or, more precisely, gradually revealed as the music unfolds, may be one either of correlation or of counterpoint." (Jim Samson, The Music of Chopin, pp 75–76.) [2011-06-12 10:14:45 +0100]
「一切藝術的問題都是節奏的問題，無論繪畫、雕刻或音樂都是一樣。既然美感就是動感，每一種形式都有隱含的韻律。就連建築方面亦然，歌德式的教堂彷彿在沈思。美學上甚至可以用「衝」「掃」「粗魯」等人格的形容詞，這些都是韻律的觀念。中國藝術的基本韻律觀是由書法建立的。中國批評家欣賞書法並不注重靜態的比例或調和，而是暗中追溯藝術家從第一筆到末一筆的動作，如此看完全篇，彷彿觀賞紙上的舞蹈。」（林語堂《蘇東坡傳》p 279，宋碧雲譯。） [2011-06-12 10:40:12 +0100]
- 陳** ⇒ 寫程式也是一種節奏！ [2011-06-12 10:48:48 +0100]
- Josh Ko ⇒ Original text: "All problems of art are problems of rhythm, whether in painting, sculpture, or music. As long as beauty is movement, every art form has an implied rhythm. Even in architecture, a Gothic cathedral aspires, a bridge spans, and a prison broods. Aesthetically, it is possible even to speak of the "dash" and "sweep" and "ruggedness" of a man's moral character, which are all concepts of rhythm. The basic concept of rhythm in Chinese art is established by calligraphy. When a Chinese critic admires calligraphy, he does not admire it for its static proportions or symmetry, but rather follows the artist mentally in his movement from the beginning of a character to the end and so on to the end of the page, as if he were watching a dance on paper." [2011-06-12 10:58:07 +0100]
Completed the reports (the termly GSS report and the annual scholarship report, the latter of which is just a questionnaire and is much lighter than I expected). Will play with some data structures in the afternoon! [2011-06-13 11:05:05 +0100]
- L********** ⇒ What kind of data structures? [2011-06-14 02:16:13 +0100]
- Josh Ko ⇒ Purely functional, of course, with all the invariants expressed. [2011-06-14 08:47:04 +0100]
The very first example looks like a good one for ornament composition (or whatever it will be called) — "Leftist heaps are *heap-ordered* binary trees that satisfy the *leftist property*[.]" (Emphases mine.)
It's rather obvious that heaps are a generalisation of sorted lists. It would be interesting to see later if they can be unified somehow. [2011-06-13 14:50:19 +0100]
Yes, typed syntax and evaluation is definitely a killer app of ornaments. [2011-06-14 10:37:39 +0100]
Hmm, just discovered that I used \sqcup to mean minimum in the paper, which should have been \sqcap... [2011-06-14 15:06:55 +0100]
- P************* ⇒ ctrl+f & replace all [2011-06-14 15:09:28 +0100]
- Josh Ko ⇒ Just did that and updated the paper & code on my webpage. But that gives the reviewers one more thing to say.. [2011-06-14 15:24:41 +0100]
Got some likely-to-be-interesting idea about constructing imperative programs in dependently typed functional languages. Hope I can develop it to something presentable soon. [2011-06-15 08:35:07 +0100]
- Josh Ko ⇒ It was inspired by the Dutch national flag problem, of course. [2011-06-15 08:36:14 +0100]
- S************ ⇒ Is that related to the work of Wouter Swierstra? http://www.cs.ru.nl/~wouters/publications.html [2011-06-15 11:32:09 +0100]
- Josh Ko ⇒ Indeed! Jeremy said it might be interesting to improve the reusability of his program with ornaments, and it would be a good example for my talk in DTP '11 if I could work it out in time. Right now, however, I am not satisfied with his verificationistic approach and have been thinking about how to do it in a more correct-by-construction manner. [2011-06-15 12:24:14 +0100]
Will this work? ↦ Wall Photos [2011-06-15 09:20:15 +0100]
- 翁** ⇒ ok~but why?what's that mean? [2011-06-15 09:47:20 +0100]
- Josh Ko ⇒ That's a long story... No, rather, there is no story to tell at the present stage! [2011-06-15 12:25:15 +0100]
It's going to be awesome if this works. I do hope it will work! But now I really need to get some rest... [2011-06-15 21:56:55 +0100]
data DVec (A B C : Set) : (n : ℕ) (i j k : Fin (suc n)) → ∀ {m} (d : Diff j k m) → MaybeTri m → Set
Even just the index type of the Dutch vector inductive family is already intimidating.. [2011-06-16 08:39:55 +0100]
- Josh Ko ⇒ It's not necessary to use Fin actually; Nat suffices! [2011-06-16 10:18:03 +0100]
Very difficult indeed... but that's research! [2011-06-16 09:52:10 +0100]
I refuse to believe I need proof irrelevance here! [2011-06-16 10:24:12 +0100]
- Josh Ko ⇒ Indeed I do not need it! Ya! [2011-06-16 10:37:33 +0100]
It works...! [2011-06-16 13:57:34 +0100]
Having the essential bits, now I need to think about how to package them. [2011-06-16 18:24:24 +0100]
Hilbert: "The art of doing mathematics consists in finding that special case which contains all the germs of generality." (One of the first quotes that inspired me.) [2011-06-16 19:49:41 +0100]
My first correct-by-construction solution to the Dutch National Flag problem. The main program, reduce, is a functional program, but it was designed with loop invariant maintenance in mind, so it's tail recursive, and it should be straightforward to convert the program to a state-monadic program if one wishes. I haven't expressed that the only possible updates are swaps, though. ↦ http://www.cs.ox.ac.uk/people/hsiang-shang.ko/DutchFlag.agda [2011-06-17 19:25:33 +0100]
- Josh Ko ⇒ Notice that there are no separate logical proofs. (Well, a very few of them might be controversial..) Or rather, the programs are simultaneously read as proofs. (Well, in fact I am still practising reading them in that way...) [2011-06-17 19:25:53 +0100]
寫完這程式有種吃到胡斐那口白菜的感覺 XD。 [2011-06-17 20:05:14 +0100]
You know what? I think I can eliminate those auxiliary functions by adding more indices to the dutch vector type! [2011-06-17 21:18:24 +0100]
- Josh Ko ⇒ Since they are folds, all folds. Algebraic ornaments come to the rescue! [2011-06-17 21:19:50 +0100]
- Josh Ko ⇒ Encountered some difficulties, though. [2011-06-17 22:28:29 +0100]
差點忘了今天（英國時間）是「水坑」四周年紀念日。（借 Yen3 的 SNG 連線報導一用 XD。） ↦ No title, no thinking, no meaning: 有人還活著 [2011-06-18 22:43:21 +0100]
Yesterday I tried to play the F-sharp major prelude (Op 28 No 13). It was wonderful. In the middle "più lento e molto espressivo" section, I could precisely control the colour and intensity I wish to express. 以武俠小說比喻，感覺彷彿內勁直透劍尖，隨手一揮都劍意十足。The moral is that I should sleep very well before I go to the music room. [2011-06-19 19:14:12 +0100]
錦源經歷兩屆資優班摧殘，這次又要帶科學班啦⋯ ↦ 科學班100學年度高一師資群 [2011-06-19 21:49:34 +0100]
- Josh Ko ⇒ FAQ 還特地列一條「就讀科學班可以選擇考醫學院嗎？」⋯ [2011-06-19 21:50:10 +0100]
- Josh Ko ⇒ 咦，只有兩屆嗎？'05 一屆、'08 第二屆，連著帶的話今年應該要送走第三屆？ [2011-06-19 22:12:46 +0100]
One reason to teach functional programming, I think, is that it easily leads to intuitionistic logic (or at least the concept of deduction systems), which is very helpful for doing logic proofs. But then, for those subfields in CS that are not interested in proofs (at all), this is perhaps not a strong reason.. [2011-06-20 00:45:46 +0100]
- L************** ⇒ I think another reason is to help programmers understand the meaning of a program rather then a correct program. Once being trained in this way, the meaning of imperative programs might be easier to understand and to have a correct program. [2011-06-20 01:00:40 +0100]
- L************** ⇒ BTW, Richard Stallman will come to Birmingham in 25th August. Are you interested at this? The title of his talk has not been finalised, though. [2011-06-20 01:11:50 +0100]
- Josh Ko ⇒ Not sure I get what you mean.. For Java and C++ we know what they mean without having to know functional programming, because we have the standards to read. That does not help very much to construct a correct program, though.
  
  Hmm, I am not particularly interested in Stallman's work. So his topic has to be very interesting to convince me to be there. [2011-06-20 09:10:44 +0100]
- D****** ⇒ It suffices for me to know that it is a good toy. [2011-06-20 11:08:35 +0100]
- L*********** ⇒ I guess for me regarding understanding the meaning of imperative programs is that, it helps me to understand that even a simple instruction, say, raising exceptions (ok, this is not simple at all, is it?), could have far more impact than my imagination. [2011-06-20 11:20:21 +0100]
- L************** ⇒ Functional programming is very close to usual mathematics, so it might be easier to learn programming from something we are familiar with. Then, from a mathematical viewpoint the notion of states should be clear to programmers, and side effects can be explained rigorously if they keep FP in mind. As for the standard, it is ususally not the one people read to learn a language.... [2011-06-20 17:42:01 +0100]
- L************** ⇒ But my point might be very weak. I'm struggling if people would think of imperative languages in this way or not ... [2011-06-20 17:48:33 +0100]
- L********** ⇒ CS still remains as a practical subject though [2011-06-20 22:34:50 +0100]
- 黃** ⇒ 話說你們牛津大學的Wykeham講座邏輯學教授Timothy Williamson好像不太喜歡intuitionistic logic，但他的理由有些奇怪，大概是說intuitionistic logic一直處在主流數學邊緣。有趣的是前前任Wykeham講座邏輯學教授Michael Dummett(Elements of intuitionism的作者)卻一直為intuitionistic logic做辯護(他是基於哲學上反實在論的理由) [2011-06-24 09:43:01 +0100]
"There is a Haskell on the cloud / I like to go there in my sleep"... [2011-06-20 14:32:57 +0100]
Lists indexed by a vector of natural numbers — hmm.. a hint of datatype-genericity? [2011-06-20 23:25:36 +0100]
Too excited about the Dutch national flag program that I still cannot fall asleep... [2011-06-21 00:29:47 +0100]
The fact is that I do not really understand the program, in the sense that I cannot explain it well, even though it looks surprisingly straightforward. Hope I'll get some feedback in the forthcoming AoP meeting! [2011-06-22 02:11:47 +0100]
- Josh Ko ⇒ It does not seem that I can get more out of the program before then, so I'll turn to reviewing adjunctions later today (i.e., after I get up). [2011-06-22 02:18:02 +0100]
「反正」好像就是 disjunction elimination 嘛？XD [2011-06-22 10:54:03 +0100]
Less types! [2011-06-22 12:59:52 +0100]
- Josh Ko ⇒ No, the attempt failed. [2011-06-22 13:05:06 +0100]
Right, let's get the reflexive transitive closure.. [2011-06-22 18:46:17 +0100]
- Josh Ko ⇒ Still somehow there's something missing.. [2011-06-22 18:54:41 +0100]
How is education justified? [2011-06-23 11:42:28 +0100]
- S************ ⇒ Are you talking about compulsory education for children and teenagers, or something else? [2011-06-23 12:24:41 +0100]
- Josh Ko ⇒ Yes, more about that. [2011-06-23 13:38:37 +0100]
- Josh Ko ⇒ And especially ethics.. [2011-06-23 14:09:31 +0100]
- P************* ⇒ Philosophy! I think it's unjustifiable. Education is more like an imposed public value to an individual. On the other hand, ethics is nothing more than a mental rule for stablizing a society. Once you have got education, you are in this game. Justification for education in some sense is meaningless since the value is decided by the public. And the public are capricious. [2011-06-23 14:38:11 +0100]
"It is useful to know something of the manners of different nations, that we may be enabled to form a more correct judgement regarding our own, and be prevented from thinking that everything contrary to our customs is ridiculous and irrational[.]" — Descartes, A Discourse on Method. [2011-06-23 13:46:40 +0100]
- Josh Ko ⇒ My interpretation: Upon encountering new customs, it's not the addition of facts (say, to one's database of "acceptable behaviour") that is important, but the refutation of the belief that what one thinks are good/correct are universally so. [2011-06-23 15:36:05 +0100]
I feel that I still have not gone very far from where I started in my first year in senior high school, still utterly puzzled by all the same big questions. I have made a bit of progress, maybe, but just a bit. [2011-06-23 14:03:38 +0100]
- 翁** ⇒ don't think to much,just believe yourself! [2011-06-23 14:13:25 +0100]
- Josh Ko ⇒ I believe I should think more! [2011-06-23 14:21:28 +0100]
- B*********** ⇒ i guess thats why you go all the way to uk. if it aint tough, it aint worth fighting for! [2011-06-23 14:33:16 +0100]
- L********* ⇒ "Much farther you go, much smaller you feel." It's a normal feeling when you walk on any research path. [2011-06-23 14:37:20 +0100]
I will allow myself to reread Descartes' Discourse on Method this afternoon, and then in the evening I will plan my Dutch National Flag story to be told tomorrow. [2011-06-23 15:14:55 +0100]
- S************ ⇒ Any new thoughts on the topic of ethics and education? [2011-06-25 02:13:58 +0100]
- Josh Ko ⇒ There are some, but justifications are still to be found. I think I will first write about just some observations. (Now there are five blog posts waiting in the queue to be written.. If I decide to write about the Dutch National Flag then there would be six...) [2011-06-25 08:52:09 +0100]
- S************ ⇒ I want to see the Dutch National Flag too! :) [2011-06-26 03:50:52 +0100]
- S************ ⇒ (Could it be that there's just no justification?) [2011-06-26 03:52:26 +0100]
- Josh Ko ⇒ It could, but in any case I'd like to have something to say about the subject.
  
  After the AoP meeting, I think I can summarise my approach as formulating the invariant inductively so it can be proved by induction, the proofs taking the form of simple functional programs (so simple that there are only pattern matches!) since the invariant is integrated into the list type. (Perhaps that has given you enough hints to work it out!) Hmm, I can write about it in the morning.. [2011-06-26 07:08:15 +0100]
I am offered "one of the new ensuite rooms at 132/133 Walton Street" by graduate accommodation. It would have been a very tempting offer had I not agreed to live with the Oriel Musketeers. I'll decline the offer but ask graduate accommodation to put me on the queue for the next year, as a backup plan (as Frank did). [2011-06-23 17:45:47 +0100]
- J********** ⇒ 果真是義薄雲天! [2011-06-23 18:52:20 +0100]
- Josh Ko ⇒ 這是那時決定搬進去就得先連帶做好的決定呀！ [2011-06-23 18:55:04 +0100]
- J********** ⇒ 不管啦, 成語用了歹收回... [2011-06-23 18:56:48 +0100]
- Y*********** ⇒ Don't go......Josh
  我還沒走出失去Wilson的傷痛.... [2011-06-23 19:06:53 +0100]
- F********* ⇒ 老潘....說不定你們下一位新室友是正妹喔!　我看你到時可樂到不行吧! [2011-06-23 19:34:49 +0100]
- Josh Ko ⇒ 其實今天中午才跟可能是新室友的人吃飯，北京男 XD。 [2011-06-23 20:07:23 +0100]
- L************** ⇒ 那 Josh 妳還是留下吧。 [2011-06-23 23:16:06 +0100]
- S************ ⇒ 我住過 Walton St. 唷～地下室那間。頭幾週每天早上從牆壁裡發出敲擊聲，讓我以為是鬧鬼了... [2011-06-25 02:20:33 +0100]
- Josh Ko ⇒ 噢，故事我還記得！不過我忘記是什麼時候講的了 XD。 [2011-06-25 08:46:13 +0100]
Re: DTP '11 submission: Modularising inductive families

Dear Josh,

I'm pleased to inform you that we would like to accept your proposed talk for the workshop on Dependently Typed Programming 2011.

[...]

See you in Nijmegen,

Ana Bove
Matthieu Sozeau
Wouter Swierstra [2011-06-24 16:45:35 +0100]
- L************** ⇒ Oh, I'd like to read reviews! [2011-06-24 20:39:38 +0100]
- Josh Ko ⇒ Only the abstract was submitted, so there are no reviewer comments. (However, the result of WGP will come out in a week..) [2011-06-24 21:06:57 +0100]
- T************* ⇒ Congratulations! [2011-06-26 13:22:00 +0100]
Making another attempt to attack adjunctions. [2011-06-25 22:05:12 +0100]
Finally met Jeremy at Tesco! [2011-06-26 11:41:35 +0100]
Somehow I guess we need even more radical generic programming techniques to acquire true reusability of dependently typed programs — the scheme proposed by OAOAOO is rather shallow. Well, that's going to be reflection..? In any case, to be able to do useful generalisations I certainly need to look for more interesting dependently typed programs which not only shows that proofs can be done but can also be done *well*. [2011-06-26 20:09:47 +0100]

The Dutch National Flag Problem, inductively

2011-06-26T08:59:00.017+01:00

Jeremy suggested that I look into Wouter Swierstra's Agda solution to the Dutch National Flag problem, which Shin has also written about in his Chinese blog using Dijkstra's guarded command language. There are two things that I'd like to improve:

In Agda every program has to be terminating, and one (perhaps the most obvious) way to show that is to make a program structurally recursive. Wouter did it by introducing an explicit tree-shaped call structure on which the program recurses, which is a general technique (the so-called Bove-Capretta method) for expressing well-founded general recursion in a total language. For this problem, however, it is obvious that the difference between the two indices j and k is decreasing, so we should be able to just do structural recursion on the difference. It would be a counterexample against using a total language if we could not express that directly and had to invent a tree structure that does not seem necessary.
Wouter then wrote additional proofs to verify the program in the traditional index-based style. That is, he worked in the externalist way. I would like to see an internalist solution, i.e., the proof being integrated into the program.

It turned out that there is an arguably cleaner solution — a few functional programs that use exclusively pattern matching!

First we look at the problem of expressing the program as structurally recursive. Wouter used the finite numbers as indices into vectors (naturally), and he defined a Difference relation on finite numbers as

data Difference : forall {n} -> (i j : Index n) -> Set where
  Same : forall {n} -> (i : Index n) -> Difference i i
  Step : forall {n} -> (i j : Index n) -> 
    Difference i j -> Difference (inj i) (Next j)

The reason that the program cannot be made structurally recursive using this type is that the section of unknown colour can shrink either leftwards or rightwards, i.e., the pair of indices inj i and Next j can proceed to either inj i and inj j or Next i and Next j. For the latter case, we need a separate function to tweak the difference, but then Agda cannot see that the tweaked difference is smaller than the given one. We do know, however, that the "size" of the difference, i.e., the number of Steps, is smaller, so all we need to do is expose that size, i.e., the underlying natural number, as an index in the type, using (ornamental-) algebraic ornamentation:

data Difference : forall {n} -> (i j : Index n) -> (m : Nat) -> Set where
  Same : forall {n} -> (i : Index n) -> Difference i i Zero
  Step : forall {n} -> (i j : Index n) -> forall {m} ->
    Difference i j m -> Difference (inj i) (Next j) (Succ m)

Now the program can just do structural recursion on m. No matter how the difference is tweaked, the size (reflected in the index of its type) can always be shown to be smaller, so Agda accepts the program as structurally recursive and thus terminating. This datatype will also appear in my program below (with a different syntax).

The second problem is whether we can make the program manifest its own correctness (so separate proofs are not needed) by making the types more precise. The crucial property we wish to express is the invariant that the array is always divided into four sections such that pebbles in the first/second/fourth section are all red/white/blue while those in the third section can be arbitrarily coloured (in red, white, or blue). It turned out that this invariant can be formulated inductively and baked into the list type. Assume there is a three-element datatype for the colours,

data Colour : Set where
  red white blue : Colour

and the type of pebbles is a type family Peb : Colour → Set. The Dutch vectors are defined by

data DVec : (i j k : ℕ) → Set where
  []   : DVec 0 0 0
  _R∷_ : (x : Peb red) →     ∀ {i j k} (xs : DVec i j k) → DVec (suc i) (suc j) (suc k)
  _W∷_ : (x : Peb white) →   ∀ {  j k} (xs : DVec 0 j k) → DVec 0       (suc j) (suc k)
  _A∷_ : ∀ {c} (x : Peb c) → ∀ {    k} (xs : DVec 0 0 k) → DVec 0       0       (suc k)
  _B∷_ : (x : Peb blue) →              (xs : DVec 0 0 0) → DVec 0       0       0

It is easy to see from the indices that once we use the arbitrary cons _A∷_ it is no longer possible to use the blue cons _B∷_ (since the index k in the type of a Dutch vector constructed by _A∷_ is nonzero but _B∷_ expects k in the type of its tail to be 0), and once we use the white cons _W∷_ it is no longer possible to use _A∷_ and _B∷_, etc. Thus these constructors necessarily appear in the desired order. Moreover, the indices in the type of a Dutch vector are exactly the values of the variables indexing into the corresponding array satisfying the invariant. And interestingly, we can simply use natural numbers instead of finite numbers as the indices; in the type of a successfully constructed Dutch vector, the indices are necessarily within bounds.

Next we need to expose two more pieces of information in the indices, both of which are algebraic ornamentations. The first one is the termination measure, i.e., the difference of k and j. We redefine the datatype Difference as

data _-_≈_ : ℕ → ℕ → ℕ → Set where
  zero : ∀ {j} → j - j ≈ zero
  suc  : ∀ {j k m} → k - j ≈ m → suc k - j ≈ suc m

The difference can then be computed by the fold,

diff : ∀ {i j k} → DVec i j k → Σ ℕ (λ m → k - j ≈ m)
diff []        = _ , zero
diff (x R∷ xs) = _ , adjustLeft (suc (proj₂ (diff xs)))
diff (x W∷ xs) = _ , adjustLeft (suc (proj₂ (diff xs)))
diff (x A∷ xs) = _ , suc (proj₂ (diff xs))
diff (x B∷ xs) = _ , zero

where the function adjustLeft is defined by

adjustLeft : ∀ {j k m} (d : k - j ≈ suc m) → k - suc j ≈ m
adjustLeft {m = zero } (suc zero) = zero
adjustLeft {m = suc _} (suc d) = suc (adjustLeft d)

One can see that the definition is a bit tricky as it is structurally recursive on m instead of d. This will turn out to be useful later. After the algebraic ornamentation, the signature of the DVec type becomes

DVec : (i j k : ℕ) → ∀ {m} (d : k - j ≈ m) → Set

Another information we need is the colour of the first pebble in the arbitrarily coloured section, as it determines what kind of swap we will do. There may or may not be such a colour, depending on the size of the arbitrarily coloured section, which is m. So we define

MaybeColour : ℕ → Set
MaybeColour zero = ⊤
MaybeColour (suc _) = Colour

and perform algebraic ornamentation using the fold

firstArbitraryColour : ∀ {i j k m} {d : k - j ≈ m} → DVec i j k d → MaybeColour m
firstArbitraryColour []              = tt
firstArbitraryColour (x R∷ xs)       = firstArbitraryColour xs
firstArbitraryColour (x W∷ xs)       = firstArbitraryColour xs
firstArbitraryColour (_A∷_ {c} x xs) = c
firstArbitraryColour (x B∷ xs)       = tt

So the signature of the type of the Dutch vectors becomes

DVec : (i j k : ℕ) → ∀ {m} (d : k - j ≈ m) → MaybeColour m → Set

Now we are ready to write the swaps. First we consider the case where the first arbitrary coloured pebble is actually red, i.e., we need to complete the program

reduceRed :
  ∀ {i j k m} {d : k - j ≈ suc m} →
  (xs : DVec i j k d red) → DVec (suc i) (suc j) k (adjustLeft d) (nextColour xs)
reduceRed xs = ?

where nextColour computes the first colour of the arbitrarily coloured section after it is reduced. Note that in the type of reduceRed, the size of d is suc m, so we are allowed to specify that the first colour of xs is red. Asking Agda to perform case analysis, we get

reduceRed :
  ∀ {i j k m} {d : k - j ≈ suc m} →
  (xs : DVec i j k d red) → DVec (suc i) (suc j) k (adjustLeft d) (nextColour v)
reduceRed (x R∷ xs) = ?
reduceRed (x W∷ xs) = ?
reduceRed (x A∷ xs) = ?

In the red cons case, we should go past x and reduce the rest, so the goal is solved by x R∷ reduceRed xs. Here the typing works directly because of how we defined adjustLeft: Matching the input vector with red cons unifies d with adjustLeft (suc d') for some d' (of size suc m) appearing in the type of xs, so the difference in the goal type becomes adjustLeft (adjustLeft (suc d')), while in the type of x R∷ reduceRed xs it is adjustLeft (suc (adjustLeft d')), so we need the emphasised subterm in the goal type to compute further. We could have done case analysis on d' but that messes up the program; instructing adjustLeft to look at the size instead of the difference itself, however, directly makes the emphasised subterm compute.

reduceRed :
  ∀ {i j k m} {d : k - j ≈ suc m} →
  (xs : DVec i j k d red) → DVec (suc i) (suc j) k (adjustLeft d) (nextColour v)
reduceRed (x R∷ xs) = x R∷ reduceRed xs
reduceRed (x W∷ xs) = ?
reduceRed (x A∷ xs) = ?

In the white cons case, we need to swap x with the first arbitrarily coloured pebble, which we assume to be red, and change the constructor to a red cons, extending the red section. We thus need to define a function to lookup the pebble

firstPeb : ∀ {j k m} {d : k - j ≈ suc m} → DVec zero j k d red → Peb red
firstPeb (x W∷ xs) = firstPeb xs
firstPeb (x A∷ xs) = x

and a function that substitutes the white pebble x for that pebble in xs.

substWhite :
  ∀ {n j k m} {d : k - j ≈ suc m} →
  Peb white → (xs : DVec n zero j k d red) →
  DVec n zero (suc j) k (adjustLeft d) (nextColour xs)
substWhite x (y W∷ xs) = y W∷ substWhite x xs
substWhite x (y A∷ xs) = x W∷ xs

The case is then solved by firstPeb xs R∷ substWhite x xs.

reduceRed :
  ∀ {i j k m} {d : k - j ≈ suc m} →
  (xs : DVec i j k d red) → DVec (suc i) (suc j) k (adjustLeft d) (nextColour v)
reduceRed (x R∷ xs) = x R∷ reduceRed xs
reduceRed (x W∷ xs) = firstPeb xs R∷ substWhite x xs
reduceRed (x A∷ xs) = ?

For the last goal we simply replace the arbitrary cons with a red cons.

reduceRed :
  ∀ {i j k m} {d : k - j ≈ suc m} →
  (xs : DVec i j k d red) → DVec (suc i) (suc j) k (adjustLeft d) (nextColour v)
reduceRed (x R∷ xs) = x R∷ reduceRed xs
reduceRed (x W∷ xs) = firstPeb xs R∷ substWhite x xs
reduceRed (x A∷ xs) = x R∷ xs

Similarly, reduceWhite and reduceBlue can be defined by just pattern matching, although reduceBlue is slightly more complex. The three functions can be assembled into a tail-recursive function

reduce :
  ∀ {i j k m} {d : k - j ≈ m} {c} →
  DVec i j k d c → Σ[ i' ∶ ℕ ] Σ[ j' ∶ ℕ ] DVec i' j' j' zero tt
reduce {m = zero} {d = zero} v = _ , _ , v
reduce {m = suc _} {c = red  } v = reduce (reduceRed   v)
reduce {m = suc _} {c = white} v = reduce (reduceWhite v)
reduce {m = suc _} {c = blue } v = reduce (reduceBlue  v)

which is structurally recursive on m. We can package reduce so it works on ordinary lists:

fuel : ∀ {k} →  k - zero ≈ k
fuel {zero } = zero
fuel {suc n} = suc (fuel {n})

initialise :
  (xs : List (Σ Colour Peb)) →
  let n = length xs in Σ[ c ∶ MaybeColour n ] DVec zero zero n fuel c
initialise [] = tt , []
initialise ((c , x) ∷ xs) = c , x A∷ proj₂ (initialise xs)

forget : ∀ {i j k m} {d : k - j ≈ m} {c} → DVec i j k d c → List (Σ Colour Peb)
forget [] = []
forget (x R∷ xs) = (red   , x) ∷ forget xs
forget (x W∷ xs) = (white , x) ∷ forget xs
forget (x A∷ xs) = (_     , x) ∷ forget xs
forget (x B∷ xs) = (blue  , x) ∷ forget xs

dutchFlag : List (Σ Colour Peb) → List (Σ Colour Peb)
dutchFlag = forget ∘ (proj₂ ∘ proj₂ ∘ reduce) ∘ (proj₂ ∘ initialise)

The whole development is available here. I think the novelty of the approach is that the invariant is formulated inductively and integrated into the list type, so the proofs that certain swaps preserve the invariant can be written inductively in the form of simple list-manipulating functional programs. Also it demonstrates how algebraic ornamentation can be used to tidy up dependently typed programs.

--
Still five more blog posts in the queue, argh..

GSS student report, Trinity Term 2011

2011-06-13T23:00:00.002+01:00

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

--
Uneventful. XD

[facebook digest] Paper submitted

2011-06-04T14:46:00.002+01:00

週末試著把積好久的 blog posts 出清吧⋯ 然後就可以繼續寫 reading course 的小論文了。 [2011-04-29 20:29:38 +0000]
Preparing to go to the legendary May Day. [2011-05-01 02:37:56 +0000]
- 王** ⇒ 是五月天嗎XDD [2011-05-01 02:54:33 +0000]
補眠到剛剛。八點多吃的 double sausage & egg McMuffin meal 應該是會當早午餐了。 [2011-05-01 11:27:10 +0000]
There are really two kinds of ornament composition: vertical and horizontal. The horizontal one is the one introduced in the paper; the vertical one seems to be less interesting. The implementation of projection & integration, however, relies on converting horizontal composition to vertical composition. That's more interesting... [2011-05-02 19:05:28 +0000]
「這不是正確與否的問題，而是規約問題。目前我們只能說，在一個規約下，就得到一個明確的答案。到底是採用那一種規約較方便、好用與合理呢？這就必須作進一步的考察與比較，從比較中作選擇。」 ↦ 先算乘除後算加減 - 數學解惑四則 [2011-05-04 13:34:36 +0000]
- Josh Ko ⇒ 我也是這樣覺得呀。「相鄰」和「星號」是兩個不同的算符，語意上行為一樣，語法上前者優先度較高。（說不定學 lambda-calculus 的人都會這麼覺得？）真的怕歧義、不想加括號（確實有點醜）然後不嫌麻煩的話⋯ 有篇 functional pearl "Enumerating the Rationals" 裡面是特地把 1/2 的 1 打成上標、2 打成下標，可以考慮？ [2011-05-04 14:09:34 +0000]
- S************ ⇒ 用上下標的想法不錯，等下試試看 [2011-05-04 14:19:49 +0000]
It seems that realisability is always talked about relative to a more complete notion, e.g., provability, and there is always an adequacy theorem (which is the realisability transformation in the paper) saying that, e.g., provability implies realisability. [2011-05-04 15:19:48 +0000]
- Josh Ko ⇒ When Kleene introduced realisability, proofs were still *mental* constructions and did not have a concrete form. He defined realisability to say that natural numbers, interpreted "recursively", can be considered concrete proofs which reflect the mental proofs. [2011-05-04 15:46:37 +0000]
- Josh Ko ⇒ So an adequacy theorem is needed, because the realisability view should faithfully reflect the proving view. However, the realisability view can be incomplete, so realisability does not imply provability. [2011-05-04 15:50:27 +0000]
- Josh Ko ⇒ For Kleene's original intention, he certainly wished the realisability view was incomplete, because he wished to talk about intuitionistic logic in classical logic. [2011-05-04 15:51:24 +0000]
This should be the argument that realisability implies consistency: Let Γ denote some consistent axioms and φ a realisable proposition.

Γ ∧ φ → ⊥ provable
⇒ { adequacy }
Γ ∧ φ → ⊥ realisable
⇒ { Γ and φ realisable }
⊥ realisable
⇒ { which is not the case }
contradiction.

Hence from Γ ∧ φ we cannot derive ⊥, i.e., Γ ∧ φ is consistent. This can be developed into an induction on the number of axioms in Γ. [2011-05-04 15:33:21 +0000]
Used \section*{Acknowled\smash gements} to squeeze the last reference entry into the last page. [2011-05-04 18:57:26 +0000]
Paper now reached the closed-beta stage! [2011-05-04 22:26:33 +0000]
- Josh Ko ⇒ 翻譯：論文進入封測階段！ [2011-05-04 22:26:49 +0000]
- Y********** ⇒ 瞄了一下, 好難好難好難 XD [2011-05-05 13:38:20 +0000]
- Josh Ko ⇒ 蛤，不會啦⋯ [2011-05-05 14:49:15 +0000]
A weakness that just came to my mind: The realisability interpretation cannot be straightforwardly extended to function types. Specifically, the adequacy theorem does not hold for functions, i.e., not all complete functions have a realiser. This does not undo the contribution of the paper, but in the worst case we would have to rename the realisability transformation to something else. [2011-05-05 18:19:24 +0000]
Almost forgot that an even more fun & exciting part of writing a paper is responding to comments! [2011-05-06 17:03:22 +0000]
Borrowed Jacobs' Categorical Logic and Type Theory. But as "[t]he reader is assumed to be familiar with the basic notions of category theory, such adjunctions, (co)limits and Catesian closed categories" and the chapter on **first-order** dependent type theory starts on page **581**, it's going to be a very tough read... [2011-05-06 19:35:12 +0000]
剛才和 Frank 一塊晨間散步時想到 Mazurka Op 59 No 1 的這一句，琢磨著前四個小節的顏色與鬆緊時，突然發現這種質地和那些極其精煉的古詩句是完全相通的。交響曲用完整的主線支線發展交織去鋪敘情感（如同小說一般），馬厝卡則是用精煉的句式、藉著細緻的音色與節奏變化在一瞬間表現一切。 ↦ http://www.facebook.com/photo.php?fbid=186698124716066&set=a.126799950705884.40277.100001276392360&type=1 [2011-05-08 08:05:27 +0000]
- Josh Ko ⇒ 對啊 XD。 [2011-05-08 14:13:10 +0000]
- S********** ⇒ 我喜歡chopin的nocturne :D [2011-05-08 20:32:56 +0000]
Relational ornaments? [2011-05-09 19:54:08 +0000]
- Josh Ko ⇒ Gosh, can it be the realisability predicate for the ornamentation from Desc to Orn?! [2011-05-09 20:01:11 +0000]
- Josh Ko ⇒ It turns out to be the algebraic ornament of Orn using the algebra of its decoding function (basically)! [2011-05-09 20:36:55 +0000]
"Interestingly, in Chinese philosophy yin symbolizes open and hence corresponds to the open world of coSQL, and yang symbolizes closed and hence corresponds to the closed world of SQL." Never heard of that... [2011-05-11 08:48:58 +0000]
- L************** ⇒ hahahaha. [2011-05-11 09:18:50 +0000]
- L********** ⇒ Do you also study semantics of database querying languages? [2011-05-11 10:53:31 +0000]
- Josh Ko ⇒ It's a paper we are going to read in a Haskell reading club. [2011-05-11 11:14:16 +0000]
- L********** ⇒ Interesting. What's the name of the paper? [2011-05-11 11:15:19 +0000]
- Josh Ko ⇒ A co-relational model of data for large shared data banks.
  http://portal.acm.org/citation.cfm?doid=1924421.1924436
  I find it rather too sketchy, though... [2011-05-11 11:16:47 +0000]
General (horizontal) composition is working... XD [2011-05-11 14:37:21 +0000]
This is the key to victory! (A tribute to GGG, of course.)

-- fibre product
data _⋏_ {A B C : Set} (e₁ : A → C) (e₂ : B → C) : Set where
_,_ : ∀ {c} → e₁ ⁻¹ c → e₂ ⁻¹ c → e₁ ⋏ e₂ [2011-05-11 15:19:32 +0000]
Interesting... It is nontrivial to express the datatype of relational algebraic ornaments as an ornamentation of the datatype of the relational ornaments, if possible at all. [2011-05-12 08:57:00 +0000]
Some candidate concerts. [2011-05-12 19:23:39 +0000]
- Josh Ko ⇒ Rachmaninoff: Piano Concerto No 3 + Tchaikovsky: Symphony No 6 (Pathétique)
  30 June - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/philharmonia-orchestra-53788
  Chopin: Piano Concerto No 1
  4 Dec - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/philharmonia-orchestra-56505
  Rachmaninoff: Piano Concerto No 2
  23 Oct - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/royal-philharmonic-orchestra-58985
  14 Feb 2012 - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56718
  Brahms: Violin Concerto
  25 Sep - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/philharmonia-orchestra-56421
  22 Feb 2012 - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56664
  12 June 2012 - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/royal-philharmonic-orchestra-58970 [2011-05-12 19:23:43 +0000]
- Josh Ko ⇒ Tchaikovsky: Piano Concerto No 1
  4 Aug - http://www.oxfordplayhouse.com/ticketsoxford/?event=12255 [2011-05-12 19:26:03 +0000]
- W********* ⇒ 通通去了阿 [2011-05-13 02:08:19 +0000]
Conclusions: 1. I am offered more freedom regarding the research direction than I had expected. 2. Let's keep developing stories based on universe encodings, and also start learning about fibred categories, about which Jeremy can provide more help. [2011-05-13 22:17:08 +0000]
- Josh Ko ⇒ I won't put particular emphasis on the categorical approach, though, at least in the near future, because it can take quite some time for my categorical maturity to catch up with my dependently typed programming skills. [2011-05-13 22:17:11 +0000]
Stuck on a special case of the adjoint functor theorem for a while (but got through eventually): For a partial order, prove that "every subset has a least upper bound" implies "every subset has a greatest lower bound". [2011-05-14 22:44:39 +0000]
- Josh Ko ⇒ Suddenly not very confident whether it is a special case of the adjoint functor theorem. Is it? [2011-05-14 22:56:50 +0000]
- L************** ⇒ A monotone function (functor) preserves greatest upper bounds (colimits) if and only if it has a right adjoint. The solution set condition is automatically satisfied since poset is a set. [2011-05-14 23:23:32 +0000]
- Josh Ko ⇒ Yes, but it says nothing about the existence of (co)limits... [2011-05-15 07:40:23 +0000]
- L************** ⇒ in (meet-)complete lattice ... [2011-05-15 13:37:02 +0000]
退役快一年才打上役政署發的領帶（和領帶夾）XD。 [2011-05-15 20:41:29 +0000]
Impressed by how much can be achieved by using fibre products. [2011-05-15 23:25:08 +0000]
- T************** ⇒ 纖維積是啥 [2011-05-16 01:04:27 +0000]
- Josh Ko ⇒ 給兩個 functions f : A -> C and g : B -> C, 它們的 fibre product 是 { (a, b) \in A * B | f(a) = g(b) }.
  http://en.wikipedia.org/wiki/Pullback_(category_theory) [2011-05-16 07:07:48 +0000]
When Delta and nabla clash — Δ S O' ⊙ ∇ s O = O' s ⊙ O. [2011-05-16 08:08:41 +0000]
- T************** ⇒ While Ita and alpha clash -- +.+ @@ = T^T QQ [2011-05-16 14:50:49 +0000]
"Martin Campbell-Kelly is emeritus professor in the Department of Computer Science at the University of Warwick, where he specializes in the history of computing." 有人專門研究計算史耶！香香可以考慮一下 XD。 [2011-05-16 15:30:06 +0000]
- W********* ⇒ 真的有唷XD [2011-05-17 02:28:14 +0000]
「寫於 1845 年的作品 59 向來是諸多鋼琴名家最愛的一組馬厝卡，三曲旋律出色又有蕭邦晚期獨到的轉調手法；特別是第一曲，其轉調之繁複巧妙讓人嘆為觀止，幾乎每一拍都可有所變化，聽者卻不覺其勉強古怪，只能感受無窮無盡的色調光影與心理層次。而搭配如此和聲的，卻是旋律線條相當明確，在庫加維亞克與馬厝爾兩者間徘徊的舞曲，更可見蕭邦的巧思。」（焦元溥《聽見蕭邦》p 297。） [2011-05-16 17:25:44 +0000]
- Josh Ko ⇒ 唉，重聽四首即興曲也覺得好想練啊。 [2011-05-16 18:01:31 +0000]
"èe-téks ding~~" XDD ↦ Don Knuth - An Earthshaking Announcement - Transcription [2011-05-16 21:16:29 +0000]
7 am - Morning walk with Frank
8 am - Breakfast
9 am - Essay
12 pm - Lunch
2 pm - Piano playing
4.30 pm - Departmental seminar
6 pm - Dinner
7 pm - Essay
10 pm - Bedtime reading

Wonderful schedule! ↦ SpongeBob SquarePants - The Best Day Ever [2011-05-17 05:16:54 +0000]
- J********** ⇒ Are you saying that you'll play piano for nearly 2 hours?! [2011-05-17 08:42:46 +0000]
- Josh Ko ⇒ I am! [2011-05-17 08:51:14 +0000]
I suspect the reason that the inverse realisability transformation is not available in, say, the Calculus of Constructions is simply that we are not allowed to inspect the realisability proof and accordingly produce a complete object because the former resides in Prop and the latter in Set... [2011-05-17 08:53:54 +0000]
Interesting — trying to explain dependently typed programming to an audience who I cannot even assume to know what first-order logic is. [2011-05-17 21:36:30 +0000]
- Josh Ko ⇒ and what types are! [2011-05-17 21:37:03 +0000]
- Josh Ko ⇒ strictly speaking, not even what proofs are... [2011-05-17 21:40:33 +0000]
- L************** ⇒ ............ tell me if you can make it. If it is possible, there is no reason why we can't teach category theory to the same audience (via Curry-Howard-Lambek isomorphism). [2011-05-17 21:59:28 +0000]
Abstract submitted to Oxbridge Taiwan Science and Technology Symposium. [2011-05-17 22:50:43 +0000]
- Josh Ko ⇒ Introduction to dependently typed programming
  
  It is desirable to be able to check whether the dynamic behaviour of a program satisfies a certain property just by examining the static structure of the program, without actually executing it. To state what property a program should satisfy, we assign an appropriate type to the program. Type checking — the process of finding a proof that a program has a certain type — can then be done mechanically, because the structure of such proofs are designed in such a way that they can be synthesised by following the structure of the program being checked. Modern programming languages thus employ type systems to help programmers to check properties of programs. The more sophisticated a type system is, the more properties can be expressed and checked. Since the last decade of the last century, dependent types have come into play — they are a family of type systems that are strong enough to specify exact behaviour of programs. Programming language researchers are still actively finding ways to fit this powerful type system for practical programming. In this talk I will attempt to sketch how dependently typed programming might change the way we program fundamentally. [2011-05-17 22:50:51 +0000]
- S************ ⇒ Oh, is that an event organised by the Taiwanese student society? Must be fun, good luck! [2011-05-18 05:39:23 +0000]
- S************ ⇒ You should come and give a talk in my lecture. :) [2011-05-18 05:41:21 +0000]
- Josh Ko ⇒ Then I can assume much more background! On the other hand, I do not think I can do better than you... (Yesterday I just reviewed your correspondence with Conor on observational equality back in March 2009!) [2011-05-18 05:49:29 +0000]
- S************ ⇒ Was there such a conversation? It must be asking Conor lots of questions and still feel puzzled... [2011-05-18 05:52:07 +0000]
- S************ ⇒ BTW, I believe that the OTSTS series was initiated by Duen-Wei, and I was one of the 1st generation speakers. :) Arrr.. sweet memories~ [2011-05-18 05:53:17 +0000]
- Josh Ko ⇒ And you talked about... relational derivations?! [2011-05-18 07:39:36 +0000]
- S************ ⇒ Something more general --- about 1. how programs could go wrong and why we need to prove the correctness of programs (and that by correctness we mean being correct w.r.t a specification), and 2. in proofs we work purely symbolically. I am not sure how many of them understood 2. [2011-05-18 09:53:17 +0000]
- Josh Ko ⇒ They sound like reusable ideas for my talk.. XD [2011-05-18 10:11:56 +0000]
- S************ ⇒ Haha... I will send you my old slides. :) [2011-05-18 10:13:45 +0000]
- Josh Ko ⇒ Thanks a lot! [2011-05-18 10:16:18 +0000]
About time to get a haircut... [2011-05-18 13:29:59 +0000]
My head becomes considerably lighter after having a long awaited haircut. Now I can stuff more things about equalities in my head. [2011-05-18 15:56:49 +0000]
After listening to the recording, I found that my Mazurkas Op 50 were not as awful as I thought. [2011-05-18 17:47:00 +0000]
I shall focus on these pieces in the near future:

Mazurkas Op 50
Mazurka Op 59 No 1
Mazurkas Op 63 No 2 & 3
Ballade No 4, Op 52
Impromptu No 1, Op 29
Nocturne No 15 in F minor, Op 55 No 1

Only Op 59 No 1 and Op 63 No 3 are completely new to me. [2011-05-18 17:54:03 +0000]
- Josh Ko ⇒ At the current rate, however, I expect that Ballade No 4 would take at least another year... [2011-05-18 17:55:52 +0000]
- J********** ⇒ Seriously, any intent of switching your dphil to musicology? Or at least, a double major of cs and music? ^^ [2011-05-18 18:11:54 +0000]
- Josh Ko ⇒ I think music will always be more like an excursion rather than a destination to me. Earning a DPhil in that is too much for an excursion... [2011-05-18 19:54:31 +0000]
- J************* ⇒ Besides, it's good to hang on to at least one passion that's not also a job... [2011-05-19 11:36:40 +0000]
Streicher's habilitation thesis is very helpful for understanding the equality issue in type theory. [2011-05-18 19:53:07 +0000]
- L************** ⇒ Thomas Streicher? [2011-05-18 20:00:21 +0000]
- Josh Ko ⇒ That's him. [2011-05-18 20:05:31 +0000]
Reluctant to write about equality... [2011-05-19 21:18:37 +0000]
"Your Graduate Review will be with the Master, Dean of Graduates and your College Advisor and last 5 minutes." ... So it's like "hello/how're you doing/good/keep up with it/bye"? [2011-05-20 12:53:03 +0000]
Got my first rejection: My abstract submitted to the Taiwanese Oxbridge Symposium wasn't selected. (Hope my next submission — which is more important — won't have the same fate.) [2011-05-20 13:10:04 +0000]
- J********** ⇒ 厚, 那個 committee 是看到鬼ㄡ>< [2011-05-20 13:36:26 +0000]
- Josh Ko ⇒ I posted the abstract here, in case you didn't notice:
  
  https://www.facebook.com/Josh.HS.Ko/posts/189165994469279
  
  I do not know which part went wrong. Too trivial? Too hard? Too abstract? Too boring? [2011-05-20 13:49:56 +0000]
- J********** ⇒ actually, i just noticed that the deadline for that was May 12. Or it's been extended? [2011-05-20 13:51:28 +0000]
- S************ ⇒ Hmm.. my guess is that they have a limited number of slots and have to give priority to those who about to graduate soon. After all, it's not a serious peer review! [2011-05-20 14:12:13 +0000]
- F********* ⇒ Hi Josh: You are doing very well actually. Sometime referees don't understand how important of our research are. We still love our research and will definitely have great impact on Science and human society. That's for sure! [2011-05-20 14:12:53 +0000]
- J********** ⇒ Target for the upcoming comlab student conference in November!
  
  Might you be interested in volunteering a softeng talk? (They're not holding it regularly anymore, used to be on Fridays, but it's worth asking!) [2011-05-20 14:15:09 +0000]
- P************* ⇒ Getting used to rejections is a part of PhD training. cheers. [2011-05-20 14:30:06 +0000]
- S************ ⇒ Well, don't take this too seriously. It's just a social event and a rejection has nothing to do with the quality of your work. [2011-05-20 14:56:29 +0000]
- Josh Ko ⇒ Indeed, and it's not really my work after all. XD For the comlab student conference, I can just talk about my real work! (No longer need to presume no one knows what types are.) Max and Oege seemed to hint that they intend to hold the Programming Languages Seminar regularly from now on. In any case, I think I will surely get lots of chance to give talks. [2011-05-20 15:04:52 +0000]
Received the second comment, which is long and nice. Feeling thrilled to answer it! [2011-05-20 16:51:14 +0000]
- Josh Ko ⇒ Spent three hours replying. [2011-05-20 20:16:15 +0000]
If we do not need to avoid confusion, realisability is actually a good term... [2011-05-21 07:55:08 +0000]
Helicopter taking off again. [2011-05-23 19:08:10 +0000]
This excerpt from "The Humble Programmer" by Dijkstra, which I am rereading, forcibly reminds me of C++. [2011-05-24 07:41:46 +0000]
- Josh Ko ⇒ And if I have to describe the influence PL/I can have on its users, the closest metaphor that comes to my mind is that of a drug. I remember from a symposium on higher level programming languages a lecture given in defence of PL/I by a man who described himself as one of its devoted users. But within a one-hour lecture in praise of PL/I, he managed to ask for the addition of about 50 new "features," little supposing that the main source of his problems could very well be that it contained already far too many "features." The speaker displayed all the depressing symptoms of addiction, reduced as he was to the state of mental stagnation in which he could only ask for more, more, more.... [2011-05-24 07:41:53 +0000]
Got my copies of Categorical Logic and Type Theory, Categories for the Working Mathematician, Purely Functional Data Structures, and Computation and Reasoning from Amazon.co.uk. It is about time to embrace more category theory... [2011-05-26 14:14:53 +0000]
- W********* ⇒ 在英國也要疊滿床嗎 [2011-05-26 16:23:16 +0000]
- Josh Ko ⇒ 一時之間湊不起來吧 XD。 [2011-05-26 16:51:45 +0000]
Now that the descriptions and ornaments form a proper category, the construction of horizontal ornament composition looks very much like a pushout... [2011-05-26 14:28:57 +0000]
Came across the proceedings of SIGCSE in the basement communal area. ↦ SIGCSE [2011-05-27 21:20:41 +0000]
Very tricky, this whole business about equality. [2011-05-28 08:33:30 +0000]
Revising the paper again, watching the reference entries happily crossing the page limit... [2011-05-29 09:20:50 +0000]
Nice... Not only the 15 references but also the last four lines of Acknowledgements have gone into page 13, and I've just started revision... [2011-05-29 14:33:19 +0000]
Perhaps I should study a bit of music composition so I can learn to write beautiful papers! [2011-05-30 18:41:29 +0000]
Everything was good before a sentence was inserted in page 5. Keep squeezing... [2011-05-30 21:12:39 +0000]
- Josh Ko ⇒ Successful after transforming a displayed definition to an inlined one. [2011-05-30 21:18:18 +0000]
The title of the paper is reduced to only three words now, having to de-emphasise the connection with realisability. [2011-05-30 21:45:06 +0000]
- W************ ⇒ Only three words ... XD [2011-05-31 01:36:14 +0000]
I think I am very close to the first release candidate, but I should go to bed now... [2011-05-30 23:20:07 +0000]
I was wrong: I am still making quite a few revisions here and there... [2011-05-31 14:49:32 +0000]
Submission deadline of WGP has been extended by two days, indicating there may not be enough submissions...? [2011-06-01 09:20:08 +0000]
- J******************* ⇒ 不管submission夠不夠再延個幾天是很多個conference的傳統阿 [2011-06-01 09:24:30 +0000]
- Josh Ko ⇒ WGP 這種小眾 workshop 特別令人擔心 XD。 [2011-06-01 09:56:44 +0000]
- J******************* ⇒ 小眾work shop吃個best paper拿來用阿XD [2011-06-01 10:03:56 +0000]
- S************ ⇒ 呵呵，現在還不知道 submission 有多少（雖然通常不多啦），是因為有人問，往年也都會延，所以就延了。延期通常不可以是 deadline 之前最後一刻，不然拼死趕進了 deadline 的人會不高興... [2011-06-01 12:25:37 +0000]
- Josh Ko ⇒ 有點像「lecture/seminar 的開始時間照慣例比公告慢五分鐘」的感覺⋯ [2011-06-01 13:21:10 +0000]
Paper submitted! But it is shown as Paper 1... (Please do let the workshop have other papers!) [2011-06-01 18:28:51 +0000]
- Josh Ko ⇒ Resubmitted, correcting "signaling" to "signalling." [2011-06-01 21:42:24 +0000]
- W************ ⇒ Could you submit your paper until the conference's deadline ? [2011-06-02 01:32:18 +0000]
- Josh Ko ⇒ Yes, we can always resubmit before the deadline. [2011-06-02 05:38:28 +0000]
Finally gained access to the webpage database (after writing to the IT staff) and can update my own page. ↦ Department of Computer Science: Hsiang-Shang Ko [2011-06-03 14:53:45 +0000]
- J************* ⇒ Weren't you given access automatically? [2011-06-03 19:58:03 +0000]
- Josh Ko ⇒ No! My SSO account was not linked to the database account until today. [2011-06-03 19:59:04 +0000]
Undergrads happily chatting on Merton Street, presumably having just finished their exams. [2011-06-03 16:34:38 +0000]
- Josh Ko ⇒ With occasional "Whoo~~~!!!" sounds. [2011-06-03 16:35:21 +0000]
- Josh Ko ⇒ Now "happy birthday to you"... [2011-06-03 16:38:15 +0000]
- Josh Ko ⇒ Peace has returned. [2011-06-03 16:58:48 +0000]
Err... The word "laboratory" in "Ideas that were ﬁrst developed in the laboratory environment of functional programming have proved their values in wider settings" was wrongly replaced by "Department of Computer Science"... XD ↦ Department of Computer Science, University of Oxford: Publication [2011-06-03 21:37:49 +0000]
Bought a £40 book on Chopin for £3.99 at Oxfam. ↦ The Music of Chopin (Clarendon Paperbacks) [2011-06-04 09:41:10 +0000]

--
現在已經累積五篇 blog posts 等著出清了⋯

Harasiewicz

2011-05-22T20:35:00.003+01:00

五年前與 Adam Harasiewicz 的蕭邦第一號鋼琴協奏曲第一樂章相遇，今天終於找到他的整套蕭邦錄音。Harasiewicz 風格比較接近 Arthur Rubinstein，線條質樸、不如 Zimerman 華麗，但是清雅回甘，仔細品味餘韻無窮。以下收錄服役時一篇談音樂的每月作文。

我聽西洋古典音樂
我與西洋古典音樂的關係始於我練彈鋼琴的經驗。除了演奏上必需的少數概念，我從未接觸任何正式的音樂理論，因此我認得的音樂結構與情感絕大部分是沒有名字的，少數獲知的概念名稱也可能誤用於不適當的語境。不過正如語言的流利使用源於自然培養的語感、數學論證的熟練來自對數學物件的舒適掌握，音樂理論也只是音樂感的表現與延伸。對一般無精確交流需求的人而言，培養音樂感遠比研讀音樂理論重要許多。換句話說，非音樂專業的人只要用心聽就對了。
雖然我從國小到高中學琴十餘年，我對音樂的感受是從大學才真正敏銳起來。觸發我的那首曲子是蕭邦的第一號鋼琴協奏曲第一樂章，長達二十分鐘卻讓我一遍遍重覆再聽。一開始我被溫柔的第二主題所吸引，漸漸整首曲子都對我產生意義。旋律記住了、和聲認出了、結構浮現了，每次和弦轉變都閃耀不同的色彩，每個樂句都勾動細緻的情感。慢慢地我擴張聆賞範圍，從高貴帶著憂鬱的蕭邦第二號鋼琴協奏曲、波蘭舞曲、即興曲和敘事曲，跨到絢麗近乎狂野的拉赫曼尼諾夫第二、三號鋼琴協奏曲，再到濃烈乃臻偉大的柴可夫斯基第六號交響曲《悲愴》。我仍記得快兩年前在國家音樂廳第一次聽悲愴交響曲的巨大震撼。在那五十分鐘，作曲家透過樂團帶我經歷重大哲學問題的情境、推理、與解答，步出場外時我心情異常沉重，一句話也說不出來，之後數月沒有勇氣重聽。雖然這裡所謂的問題、推理與解答本質上比較貼近文學的感性處理方式，但其中包含的一聲聲詰問卻同時也是一切理性思考的起點。這或許是我的理性和情感最接近交融的一次經驗。（JK 注：完整版見〈倫敦愛樂完整心得〉。）
無論是什麼音樂，如果只把它當作背景音樂被動地聽，往往無法領會其精神。甚至可以說聽音樂的重點在於聽者的主動唱和，外在的音樂只是引導聽者在心中演奏，因此樂器演奏的經驗對於音樂聆賞確實有很大助益。以我彈琴的經驗來說，即使一首曲子彈起來結結巴巴，也得以讓我形成自己的詮釋，並更深刻體會作曲時諸般細緻的考量──這些細節在名家手中很可能一閃即逝而難以覺察。另外像西方音樂一種常見的結構是「對位」，即兩道以上的旋律個別行進又互相唱和，花式相當多變。演奏時，對位的多道旋律常被賦予不同輕重，而使對位結構不那麼明顯。聽者（和演奏者）必得讀譜找出各道旋律，慢慢揣摩其間關係，才能更由衷讚嘆其複雜與美妙。
近來我發現音樂的表現手法也常見於其他的藝術領域，例如現代舞。「舞者身體的展延」和「音符的展延」拉扯情感的力度是一樣的，兩位舞者共舞的獨立與互補也和兩道旋律的對位是同一件事。比較可惜的是，我看過的極少數舞蹈表演當中，音樂都屈居陪襯地位，舞者和音樂之間沒能產生共鳴，使得效果大打折扣。我期待欣賞一場舞者與舞者、旋律與旋律、以及舞蹈和音樂之間全部完美唱和的表演。
古典音樂的一個特質是「望之儼然、即之也溫」，這點和數學、哲學等抽象學門出奇地類似。音樂、數學、和哲學各有不同的抽象過程，抽象後的產物儘管內涵豐富，其型式卻不若一般感官經驗來得直接，構成入門門檻。然而正如數學教育的動機，跨越門檻後所見的風景是如此綺麗，已得其門而入的人實在有義務幫助其他人跨越那門檻，至少讓他們知道有那樣的風景。且和數學相比，古典音樂顯得沒那麼生冷而較容易親近，相當值得在基礎教育階段推廣。可惜的是中小學音樂教育現未獲得足夠重視，想推廣古典音樂只能靠有心人士多加張羅了。

--
另可參考〈The Magic of Rachmaninoff〉。

Term algebra

2011-05-07T14:18:00.013+01:00

Jeremy 在昨天的 AoP meeting 重講 maximum segment sum，最後提出一個 datatype-generic version。（他寫在他最新的 blog post Horner's Rule。）中間我們拐到 T-algebras：令 T 是 monad，那麼我們稱 f : T a → a 是 T-algebra 的意思是它滿足 f . μ = f . T f 和 f . η = id。（μ : TT → T 和 η : Id → T 是伴隨 monad T 來的兩個 natural transformations，在 Haskell 裡面是 join 和 return 這兩個 polymorphic functions。）這時 Nick 問到：他一直看不出這裡說的 algebra 和我們一般講的 algebra（monoids, groups, rings, fields, ...）有什麼關係。Well asked! Jeremy 於是給了下面這一段 monad 循循善誘版介紹。

我們知道一個 monoid 是某個集合上面定義一個 associative binary operator 並且有一個 unit。比方說，List A 是一個 monoid，用的 associative binary operator 是 concatenation "++"，unit 則是 empty list []。它們的 type 是

[]   : List A
(++) : List A × List A → List A

稍微複雜一點的例子像是架在某個 field K 上的 vector space V，這時我們有 vector addition、unit、和 scalar product:

0   : V
(+) : V × V → V
(·) : K × V → V

這些 operators 必須滿足某些額外的條件。但無論那些 operators 的 signature 有多複雜，我們發現它們的 result type 都是那個底層的集合。Category theorists 於是用 sum types 把這些 operators 收集起來，list monoid 的話是

1 + List A × List A  →  List A

vector space 則是

1 + V × V + K × V  →  V

最後我們把箭號左邊的東西抽象成某個 "signature" functor F，上述兩個 type 就都能寫成 F X → X 的型式，其中 X 是底層的集合（List A 或 V）。（對於 list monoid 我們讓 F X := 1 + X × X，vector space 則是 F X := 1 + X × X + K × X。）於是 F X → X 這種型式的 arrows 我們就叫它做 F-algebra，只要適當定義 F 就能表現各式各樣的 operators，至於這些 operators 應該滿足的條件就還要另外陳述。以 monoids 為例，令 f : 1 + X × X → X，裡面藏的那個 binary operator (++) = f . inr 的 associativity 是

(x ++ y) ++ z = x ++ (y ++ z)

這可以繼續改寫成 point-free 型式：

  (x ++ y) ++ z = x ++ (y ++ z)
≡ ((++) . ((++) × id)) ((x, y), z) = ((++) . (id × (++))) (x, (y, z))
≡   { 令 assoc ((x, y), z) := (x, (y, z)) }
  ((++) . ((++) × id)) ((x, y), z) = ((++) . (id × (++)) . assoc) ((x, y), z)
≡   { extensionality }
  (++) . ((++) × id) = (++) . (id × (++)) . assoc

願意的話可以繼續畫成 commutative diagrams 之類的。如果描述的性質足夠泛化，甚至可以寫成「不須依賴 F 實際定義」的型式。

所以給一個 F-algebra f : F A → A，小學生可以用它列出算式然後求算 normal form。但國中生開始處理未知數的時候，事情就變得複雜一些，因為「列算式」和「求值」這兩個階段更明確地分開了。假設我們考慮整數加法和乘法，小學生看到的算式都是立刻可以求算出值的，在 Haskell 裡面就相當於用 + 和 * 直接列式，比方說 3 + 2 * 5，那直接是個 Int，小學生做的事情只是把它化簡成 normal form 而已。但國中生看到的式子含有未知數，那些式子沒辦法求算得一個整數值，所以更精確的說法是他們先定義一個 datatype

data Expr X = Var X | Add (Expr X) (Expr X) | Mult (Expr X) (Expr X)

其中 X 是未知數 x, y, z, ... 這些符號的集合（請忽略 Haskell 的 naming conventions XD），然後用 Var, Add, Mult 這些 constructors 列式，如 Var 'x' `Add` (Var 'y' `Mult` Var 'z')，另外再有一個求值函式把 X 上的賦值擴充到 Expr X 上：

eval : (X → Int) → Expr X → Int
eval σ (Var x)    = σ x
eval σ (Add a b)  = eval σ a + eval σ b
eval σ (Mult a b) = eval σ a * eval σ b

如果我們要把加法和乘法這兩個 operators 表示成 F-algebra，那麼我們會定義 F Y := Y × Y + Y × Y。顯然 Expr X 和 F 是有關聯的 — 前者乃導自後者，Expr X 其實是 μY. X + F Y！一個算式 Expr X 可能是個未知數，或是一個 F (Expr X)，也就是某一個 operator 下繼續裝更多算式。現在有兩件事情應該滿容易能接受：首先，給一個未知數 x : X，我們可以把它變成一個算式 Var x : Expr X。再來，Expr X 的 X 可以是任意的集合，也就是說我們所謂的未知數其實可以是各種奇怪的東西，就像高年級小學生可以寫 "□ + ▵ * ◯" 一樣。而其中一種我們可以當作未知數的東西就是 Expr X，像 "[x + y] + [y * z] * [z + x]"，方括號的意思是說括起來的部份其實我們看作是一個「未知數」，這個算式的 type 是 Expr (Expr X)。但絕大部份人看到這個算式都會覺得我們只是寫一個單純的算式，裡面有未知數 x, y, z，也就是說，他們看到的算式型別是 Expr X。因此給一個 Expr (Expr X)，我們可以把中括號抹去，讓它變成一個 Expr X。這兩件事情正是 monad 附帶的那兩個 natural transformations return : X → T X 和 join : T (T X) → T X，它們互動的時候會滿足某些看起來很自然的條件，比方說把一個算式看作是未知數（加上中括號）再把中括號抹掉會得到原來的算式（join . return = id）之類的。所以我們剛得知 Expr 是個 monad。再想一想，「抹括號」這件事情其實和 substitution 息息相關。如果我們有一個 Expr X 如 x + y * z，然後對於每個未知數我們都指定一個要取代它的 Expr Y，也就是說我們有一個 function X → Expr Y，那麼代換後我們會得到 [u + v] + [v * w] * [w + u] 這種東西，其中 u, v, w 是 Y 裡的未知數，算式型別是 Expr (Expr Y)，抹去括號後我們就得到一個 Expr Y。整個過程的型別是 Expr X → (X → Expr Y) → Expr Y，也就是 bind operator。

List monad 用算式觀點來看應該十分自然（因為正好只是 free monoid），比方說 concat : List (List A) → List A 確實是把第二層的中括號抹掉。IO monad 我相信一樣可以用算式來看，只是它的 operators 複雜一點。想法大概是 IO a 只是一段程式碼（syntax tree — 所以也是某種算式），我們寫 Haskell 程式去產生那些程式碼。至於程式碼的執行是高一層的事情，就好像外界有個 eval 在跑一樣。Expr 的 eval 只是把 Add 翻譯成 +，但 IO 的 eval 翻譯出來的東西比較複雜，得把某個 operand 的結果餵給別的 operand 讓那個 operand 算出更多程式碼，所以情況會像是跑一段程式碼把結果丟給 Haskell 程式產出更多程式碼再繼續跑一樣。Haskell 程式負責的永遠只是產出程式碼，那當然都是 pure data/computations 嘍。

--
先還個債，以後想到再寫清楚一點⋯ XD

Wordle for OAOAOO

2011-05-05T15:16:00.005+01:00

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

自傳

2011-05-01T22:23:00.005+01:00

重讀各個時期的自述。大學畢業的 Trek Begins 和服役完畢的〈畢業論文〉完成時間比較近，都還頗為可讀，高中申請入學的資料就不行了（雖然當作史料是不錯）。另有一份自傳是初至中辦時繳交的，和前三份相比，這份自傳比較精簡（好像有字數或頁數限制吧），最後一段的規劃也相當具體。（高中申請入學的規劃也很具體沒錯，但太過具體了。）

我出生於一個四人家庭，除了父母以外還有一個姐姐。[...] 家庭氣氛融洽，管教有方。回想起來，我的言行舉止深受家庭教育的影響。若將學校教育的成果比喻為地面上的建築，家庭教育所造的就是其下的地基了 ── 不起眼但相當深刻。
自幼即養成閱讀習慣，並學了十餘年的古典鋼琴，至今回家仍時常練彈。閱讀與古典鋼琴演奏都是比較需要定性的個人活動，或許因此塑造了安靜不擅言詞的個性。高中之後閱讀內容漸偏專業，一般的書籍就少碰了。對（古典）音樂的著迷則真正始於大學：在大學之前，音樂比較像是一項技能，是身外的東西；上了大學之後，音樂逐漸滲入我的人格，甚至成為我的感性（情緒）與外界最暢通的溝通途徑。特別喜愛蕭邦鋼琴曲中特有的高雅氣息，例如〈英雄波蘭舞曲〉在燦爛輝煌的和弦行進間透著憂鬱卻又堅決，這種憂鬱卻堅決的獨特氣味在〈第一號敘事曲〉兩段清麗主題當中更加明顯。現在因為技巧不足而難以彈出這些曲子的神髓，但練彈除了更能領會曲子的意境，也是一種受控制的情緒抒發，長期下來對於情緒管理的工夫甚有助益。
學業上我進展得相當順利，從國小到大學，成績都保持在一定水準。國中時接觸簡單的網頁程式設計，很快就產生濃厚興趣。程式設計和眾多其他創造性活動一樣帶給人實現構想的樂趣，但和其他創造性活動（如繪畫、建築）相比，程式碼是種毫無缺陷的理想素材，透過各種電腦硬體又得以製造出活生生的具體效果，「顯現出我們未曾見過、或在現實生活中不可能見到的事物，神話和傳說中的魔法在我們有生之年實現了」（摘自《人月神話》），被這樣的活動吸引相當自然。這份興趣到了高中更蓬勃發展，高二時已經需要購買原文書滿足求知慾，之後申請就讀台大資工系順利獲錄取。
上大學之後除了繼續充實資訊相關背景知識，受大一微積分課程啟蒙，我的關注焦點轉向數學，選擇輔修數學系。另外我也愈來愈希望能找到一些哲學問題的答案，於是選修哲學系的倫理學和知識論。哲學以理性辯證方法試圖回答各種問題，數學更將純粹理性的方法發揚光大，歸納、類推、抽象，建造出宏偉華麗的心智建築。由「心智建築」的觀點來看，程式編寫和數學理論的建構是十分相近的活動，只差在前者有實體的電腦協助讓效果表現於外在世界而已。和現在仍嫌粗糙的程式開發方法相比，數學理論經歷千百年錘鍊，留下的都是品質最精純的結晶，也難怪我當初會對數學心生嚮往了。大學四年下來，我根據研讀哲學、數學、和計算學的經驗為自己打造出一套初步的知識體系，過程和內容在我畢業後寫的一篇總結當中有詳細的描述。
大二升大三的暑假，我參加在中研院舉辦的第一屆「邏輯、語言與計算暑期研習營」，認識了中研院的穆信成老師。穆老師稍後來信邀我加入他的研究小組，我對他的研究主題十分有興趣，不假思索就答應了，成為中研院資訊所的工讀生。在這之前，我已經意識到自己有往學術界發展的傾向，但要等到這時真正接觸過研究工作，了解研究的方法、艱辛過程與必經的低潮、和最後一切水到渠成的狂喜之後，我才確定自己應該走向學術界。我們的研究領域主要由歐洲領導，在國內則相當冷門，就我所知沒有其他的研究團隊投入這個領域。因此我如果想沿著這條路走下去，方向其實相當明確：儘快服完兵役，然後出國攻讀博士。
所以這一年兵役生活就相當重要了 ── 除了盡應盡義務以外，必須善用時間補足基本的背景知識（例如相關的數學理論）、持續關心最新發展、擬出自己打算鑽研的主題、通過英語檢定、申請學校和獎學金。規律作息和運動更是培養體力、保持高效率的關鍵。現階段眼前的目標只需要有一個，而所有的努力都是為了這個目標，那就是為留學作好一切準備。希望明年秋天我能夠漫步於理想的學校，展開另一段探索之旅。

寫這種內容交給服勤單位是有點突兀，不過這就是我的作風吧 XD。現在回頭看，當時規劃的實現程度高得嚇人。一直以來總能遇上天時地利人和，我真的走得很順利（尤其和好多其他留學生的故事相比），好好把握，別在這裡鬆懈了。

--
明天開工，blog posts 密度大概又要下降了 XD。

一紙明信片

2011-04-30T15:27:00.017+01:00

本次回中辦最出乎意料的景象是這一幕（感謝琦皓提供相機及 Waiting 專業攝影）：

我在抵達牛津的第二週寫了兩張明信片寄回中辦，收件者分別是會計處和社發科，去年 10 月 11 號寄出、15 號收到，聽說會計處版還被影印放大成一張 A3 貼在公佈欄上（對每個人都寫一句話，字寫得太密啦 XD）。回辦公室已是將近半年後，我完全沒預料到明信片（原版）竟然還在公佈欄上，顯然我低估了這一紙明信片的份量。情誼維繫需要有些積極表示，這是中辦的人教我的，貼在公佈欄半年的明信片又幫我補上一課。

當然，和辦公室人們實際的熱情相比，那張明信片只算聊表象徵而已。我回去總有些不好意思，畢竟是「辦公」室，回去多少會干擾到眾人工作。但每次看到大家掩不住笑容噓寒問暖、臨走前問「下次什麼時候再回來」的模樣，就又覺得這趟走得值得。雖然情境不可能回到從前：簽到簿早已沒我的專屬頁，我進會計處坐的第一張椅子不在傳真機前、而是科長室會客用的竹椅，我也不可能再幫忙做多少事（一來大家客氣，二來我也不該搶別人的工作，比方說事情弄出差錯或有後續發展的話責任歸屬問題很麻煩），（還有大概也不太可能再吃到便當了 XD，）但這就是新的相處模式，回不去的話也就只有想想日後如何發展了。

回不去以往的情境，意味著我無以應對大家的好意。進辦公室只能陪大家聊天解悶、頂多帶點禮物（不過這次倉皇逃難回去沒準備⋯），幫不上什麼忙，於是像這次會計處和蔡專員盛情相請的中餐就實在難以回應。普通的禮物還不夠，我總覺得非得送點帶有個人意念、獨一無二的東西才算是真的傳達謝意，比方說明信片。但有什麼真正有趣的東西是帶有個人意念又獨一無二的呢？明信片終究稍嫌單薄，什麼東西的份量與深度才和我的謝意相稱？假設把我現在全心投入的東西 — 論文 — 當作禮物，就算把對方名字寫在致謝區（這也只有博士論文才勉強適合吧），但除了自己名字以外其他都是天書，這種禮物顯然不太對呀。於是答案出現了：科普書。科普的第一目標是讓讀者能夠接受，除非對方不閱讀，否則成功的科普書應該是很好的禮物（至少也有致謝區可以寫對方名字⋯）。猶記拉瑪錢德朗醫師說他寫科普是因為覺得虧欠納稅人，我想我或許可以體會一點他的心情。

唯一的缺點大概是科普不好寫，幸運至極（有時間寫、寫得出來、有得出版⋯等等）也恐怕得花個一、二十年才能把禮物送出去。看來近期只有博士論文能當作有份量的禮物，雖然內容對很多人是天書，但請相信內文的長度與符號量代表著我的感激之意 XD。（我相信致謝區應該格式長度不限吧！到時候有得寫了 XD。）

--
這篇拖了真久，總算出清啦 XD。

[facebook digest] Writing the first first-author paper

2011-04-28T22:00:00.001+01:00

Should perhaps explicitly introduce a notation of realisability transformation for functions. [2011-04-09 18:12:09 +0000]
Arrived at the boarding gate, where the destination shown is still Hong Kong (07:25). [2011-04-09 23:27:27 +0000]
It is reported that Oxford will be wonderfully warm and sunny - nice! [2011-04-09 23:31:53 +0000]
拚死在登機前吃了一客 NT$180 的紅燒牛腩飯套餐。其實不錯，除了牛腩飯以外，附三種小菜、貢丸湯（兩顆）、和一小塊巧克力蛋糕。有到讓我不敢照相的水準（免得日後望圖興嘆）。 [2011-04-10 00:22:31 +0000]
- 柯** ⇒ 哈！這次回台媽媽叫你練習煮飯你就不要… [2011-04-10 12:59:32 +0000]
今天機場比上次熱鬧很多，好幾個航班擠在同一個櫃台報到。 [2011-04-10 00:23:50 +0000]
- 翁** ⇒ good luck~ [2011-04-10 00:32:07 +0000]
- W************ ⇒ 一帆風順~ [2011-04-10 13:59:43 +0000]
登機嘍！ [2011-04-10 00:58:25 +0000]
- S************ ⇒ Farewell~ [2011-04-10 04:34:35 +0000]
Finally got on the coach, after helping a Taiwanese girl get on a coach to Cambridge. (She's attending a language school and does not speak English very well.) [2011-04-10 18:25:07 +0000]
Arrived at Oxford. 從海角又飛回天涯。 [2011-04-10 20:03:15 +0000]
Good morning! Spring really has come to Oxford, as the trees are now vibrantly green. (In Taiwan there's no such contrast.) [2011-04-11 07:39:49 +0000]
- M*********** ⇒ 沒圖沒真相,照片~~照片~~~~ [2011-04-13 16:24:51 +0000]
- Josh Ko ⇒ 真相已貼！XD [2011-04-13 16:37:19 +0000]
The immigration officer really asked for my CAS letter, even when I was entering the UK as a student for the second time. When she said "CAS letter, please", I replied "CAS letter?" and she said "acceptance letter" instead. But I was merely surprised to hear that a CAS letter was still needed. And of course I easily produced the letter, having brought it back to Taiwan. [2011-04-11 08:11:48 +0000]
- L********** ⇒ Useful information [2011-04-11 08:54:31 +0000]
- L************** ⇒ I have never been asked this ... [2011-04-11 20:26:50 +0000]
Finally discovered that option + '-' produces an en-dash and shift + option + '-' produces an em-dash. No need to search through the character map anymore! [2011-04-11 14:34:25 +0000]
The sun hesitating to fall, it is so easy to assume that it is still well in the afternoon while in fact the evening has come! [2011-04-11 17:15:13 +0000]
Classic FM: 101.3 MHz or www.classicfm.co.uk [2011-04-12 09:02:54 +0000]
What happened to the kitchen?! Leaving things in this horrible state, it's simply... illogical! And I guess the logical thing to do is to spend some time clean it all up, say tomorrow (allow myself some time to convince myself emotionally)... ↦ http://www.facebook.com/photo.php?fbid=180388995346979&set=a.126799950705884.40277.100001276392360&type=1 [2011-04-12 18:04:12 +0000]
- J******** ⇒ Dishwasher is your best friend!! [2011-04-12 22:07:08 +0000]
- Josh Ko ⇒ No such thing in our kitchen... [2011-04-13 05:42:41 +0000]
Suddenly realised why it is strange and inconvenient to publish a result heavily based on something which hasn't been published. [2011-04-13 15:47:16 +0000]
"Silver white winters that melt into springs" - now I know why it's one of her favourite things. ↦ http://www.facebook.com/photo.php?fbid=180612515324627&set=a.126799950705884.40277.100001276392360&type=1 [2011-04-13 16:36:30 +0000]
Hmm... I'd say it's really a paper from the AoP group, with lists, folds, and fold fusion! [2011-04-14 17:56:16 +0000]
The paper is definitely going to exceed the page limit... [2011-04-14 19:01:59 +0000]
- Josh Ko ⇒ Let's forget about fusion? [2011-04-14 19:02:43 +0000]
- J********** ⇒ Let's forget about submitting it? [2011-04-14 19:34:37 +0000]
- Josh Ko ⇒ No way! ICFP is too tempting! [2011-04-14 19:38:26 +0000]
- J************* ⇒ C'est la vie, I'm afraid. Short version for submission, long version with the full story in to go online. TeX conditionals are your friend! [2011-04-15 00:09:58 +0000]
When can we publish animated papers...? [2011-04-14 20:01:20 +0000]
- C*********** ⇒ We graphics guys really need that. [2011-04-18 00:46:49 +0000]
"The contribution of the realisability transformation, then, is pointing out the connection between the two different ways of expressing constraints --- realisability predicates for externalism and ornaments for internalism. [2011-04-17 18:43:48 +0000]
- Josh Ko ⇒ An ornament induces a realisability predicate, which is the manifestation of the ornament in the world of decoded datatypes, and moreover, composition of realisability predicates mirrors composition of ornaments. A bridge is formed between externalism and interalism, and subsequently, externalist modularity is brought into internalist datatypes." [2011-04-17 18:43:52 +0000]
- Josh Ko ⇒ A problem I encountered four years ago, now finally having an initial solution.
  http://joshkos.blogspot.com/2007/11/qsort-in-agda-round-4.html [2011-04-17 18:52:29 +0000]
- Josh Ko ⇒ It was actually mentioned by Shin in his fifth email to me (in Chinese):「有沒有可能模組化地證明程式的性質。例如我們能設計一個 type 證出 mergesort 之中的那個 merge 函數傳回的 list 長度是對的，也可以設計另一個 type 證出 merge 傳回的 list 是 sort 好的。但如果要同時證兩個性質，又要設計另一個 type. 有沒有可能模組化一點。」 [2011-04-19 20:17:59 +0000]
Writing up and revision of the paper in active progress. It reminds me vividly of how much hard work was required to produce the two AoPA papers, even though I had been just watching and didn't actually do the writing then. [2011-04-19 20:12:46 +0000]
Tulips or...? ↦ http://www.facebook.com/photo.php?fbid=182721041780441&set=a.126799950705884.40277.100001276392360&type=1 [2011-04-22 10:16:44 +0000]
- T************** ⇒ 這樣拍看不出來 [2011-04-22 12:37:58 +0000]
The Introduction will be finished tomorrow, which tells a specialised story about finite numbers with parity. (And the maximum page number is expected to reach 12.) [2011-04-22 22:04:17 +0000]
Just realised that paper writing is really comparable to music composing! (The example of finite numbers with parity appearing in the Introduction and never again reminds me of the first theme in the first movement of Tchaikovsky's first piano concerto.) [2011-04-23 10:10:42 +0000]
- Josh Ko ⇒ Cf. Remy: "Compose the salad like you were painting a picture!" [2011-04-23 10:17:35 +0000]
Making some very subtle points. The points are already hard by themselves, and naturally it is even harder to put them in words clearly! [2011-04-24 14:23:01 +0000]
- Josh Ko ⇒ On the other hand, that's what's so interesting about a paper. I hope the reader will find the discussion worth reading. [2011-04-24 14:24:11 +0000]
"Thus the use of realisability predicates, which is central to externalist compositionality, can in fact be regarded as an application of an internalist technique to solve the compositionality problem of internalist datatypes." [2011-04-24 15:38:44 +0000]
See if I can have the first complete draft of the paper before May starts. [2011-04-24 19:39:20 +0000]
$ detex OAOAOO.tex | wc
1009 9327 56566
(No, the paper has not been finished...) [2011-04-25 19:33:47 +0000]
人事物都在變，很快中興新村就要變得陌生了。 ↦ 中興新村將風華再現開發計畫有條件通過｜地方新聞｜中時電子報 [2011-04-25 21:17:26 +0000]
- W************ ⇒ 彰中的教室都有冷氣了 ... [2011-04-26 02:49:40 +0000]
New address from August: 45 Marlborough Road, Oxford, OX1 4LW. [2011-04-26 15:04:23 +0000]
So nice to be able to reach the Acknowledgements. [2011-04-26 21:49:59 +0000]
Finally arrived at a draft that counts basically as complete. XD [2011-04-27 21:23:20 +0000]
- Josh Ko ⇒ Err... I forgot the abstract. XD [2011-04-27 21:31:42 +0000]
- Josh Ko ⇒ It seems to be customary for the abstract to be excerpted from the introduction? [2011-04-27 21:43:28 +0000]
The abstract produced! [2011-04-28 10:15:17 +0000]
- Josh Ko ⇒ Dependently typed programmers are encouraged to use inductive families to integrate constraints with data construction. Different constraints are used in different contexts, which lead to different version of datatypes for the same data structure. How the common operations can be modularly implemented for these structurally similar datatypes has been a longstanding problem. We propose a datatype-generic solution based on McBride's datatype ornaments, exploiting an isomorphism which can be interpreted in terms of realisability. Relevant properties of the operations are separately proven for each constraint, and after the programmer selects several constraints to impose on a basic datatype and synthesises an inductive family incorporating those constraints, the operations can be routinely upgraded to work with the synthesised inductive family. [2011-04-28 10:15:24 +0000]
Twelve pages! [2011-04-28 15:13:23 +0000]
- Josh Ko ⇒ Further tweaking can change that easily, though. [2011-04-28 15:14:35 +0000]
Global refinement to be done tonight. [2011-04-28 17:17:06 +0000]
Just gone through the whole paper again. I'll ask Jeremy about some details and then the paper can be finalised! [2011-04-28 19:18:04 +0000]

寫作

2011-04-20T20:55:00.004+01:00

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

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

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

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

返台巡迴紀實

2011-04-11T15:25:00.013+01:00

說起來，我這次返台拜訪的站數其實不多。三月 8–9 號上台北找 scm 老師和台大幫、19 號星期六在台中慶祝替代役學長考上地方特考、21 號回中辦、24 號訪新竹清大幫然後隔天直取桃園、四月 4 號留在本陣彰化吃牛排、最後 8 號夥同 7 人再回中辦。本篇記錄發生事實，感想將另寫數篇。

三月 2 號回到家，4 號就想到如何以 realisability 詮釋 algebraic ornaments — 想法突然全部自己迸出來。那時還沒有實作，雖然自己覺得應該是有意思的東西，但還是需要講給別人聽看看，評估一下可不可行和有沒有搞頭。雖然難找 Jeremy 討論，但有 scm 老師在台北呀！於是敲定 8–9 號上台北，下午先到中研院，晚上混進台大宿舍借宿於神的吉里巴斯室友的床位，隔天下午聽 scm 老師上課，晚上搭車回彰化。中午到台北車站再到台大，和 Weijin 吃完懷念已久的老爺上菜後往南港去，接近下午兩點時我進資訊所，剛好遇到蔡益坤老師和當天的 distinguished lecturer Moshe Vardi 也正要搭電梯到七樓。因為別人都有事，聽眾只有 scm 老師和他的新助理，我就在 scm 老師研究室的小白板上寫了一堆 datatypes 比手畫腳講它們之間的關係（有趣的是我講的（還有現在正在寫的 paper 裡面寫的）全部是衍生自 natural numbers）。晚上三人到內湖的春水堂人文茶館吃晚餐，然後我搭捷運回台大找神（並在「勝利」補充兩隻搖搖筆）。他的室友是吉里巴斯人，似乎因為在外有親戚所以不常留宿，我就借佔他的床位。隔天早上我留在房間裡寫 Agda，中午和神去吃台大牛肉麵。那時肚子已經有點脹痛，但台大牛肉麵清燉的甘甜湯頭還是讓我忍不住多喝幾口，以致於吃完走回台大肚子脹得不太舒服，不過在神推薦的台大農場旁邊的桌椅睡一下之後就好了不少。與神暫別走回資管系，scm 老師已經抓好髮型準備開場啦。終於看到一門正宗的程式語言課開在台大，而且還用大教室耶！雖然不是開在資工系有點可惜 XD。課程才剛開始，scm 老師還在介紹基礎的 Haskell，真正有意思的部份還沒到，不過 scm 老師為了趕在下課前把程式變出來奮力和 Helium 一波波錯誤訊息搏鬥的娛樂效果還挺不錯的 XD。晚上和神、Weijin、施銘峰、秉毅、香香吃老莊作結。

至中辦服役一開始的管理幹部程哥經歷一年蟄伏苦讀，考上台北市地方特考三等，所以就有正當理由找大家吃飯啦！19 號週六中午十二點約在台中中友百貨前集合，我搭火車到台中讓琦皓接過去。地點選在中友附近一家隱密的咖啡簡餐館，是一般的民房裝潢而成，程哥訂了一個大得出奇的包廂，裡面除了沙發桌椅還有電視音響再加一張撞球桌！九個人（包括特地從台北下來的顯奕荐堯顯光兄弟）聊得很愉快，我也盡情把玩琦皓新購的單眼相機，一路加點飲料點心待到六點（（除了振弘有事中途先落跑）），到後來其中四人還拿起旁邊放的撲克牌打起小額賭錢的大老二。有趣的是最後出錢的人是已經找到好工作的顯光，只聽他一口爽快地把費用全包下來，毫不拖泥帶水。嗯，哪天能輪到我有理由出手呀？XD

早早就和程哥相約星期一返中辦，週六台中聚完的晚上 Waiting 正好也在 facebook 上問我週一有沒有空一起回去，也太有默契！早上十點鐘到辦公室，還沒進會計處大門就看到淑芬姐和蔚民從對面小倉庫出來，蔚民正擔心我要吃什麼。我的打算是重溫便當滋味，而蔚民早已特地開了皇上皇並幫我先訂好燒肉飯，貼心！這天辦公室全員到齊，和大家打招呼聊一下，也在科長室坐了一會。很快麗紋姐就發起中午到彰化吃佛跳牆，參加的人除了我以外有（逆時鐘順序）麗紋姐、秀霞姐（名言：吃飯相搶才好吃！）、嘉萱姐、林專員、吳專員、亞欣姐、惠如專員，八個人兩台車剛好圍一桌，科長因為隔天健康檢查不能吃油膩但慷慨解囊贊助，可憐的蔚民（因為肚子不舒服沒參加）只好處理退訂和退款，我原本以為繳了錢就萬無一失的便當也飛啦！XD（程哥笑說早就告訴我會計處的人不可能讓我吃便當 XD。）不過吃了以後證明佛跳牆一樣好吃一樣是正宗台灣味，60 元就有一碗精燉佛跳牆加一碗香噴噴的魯肉飯，我們又另外叫了一整桌小菜。吃飽後一行人再到隔壁的寶珍香餅店把科長的贊助款花完，麗紋姐又送了兩塊大餅給我。下午才進社發科找蔡專員，至圖書館尋人不遇的程哥也進來聊了一下然後先回去整理行李隔天上台北，隨後 Waiting 也和出納吃完飯回來了。蔡專員很懊惱我們回來她卻沒好好招待我們，於是責成琦皓和我們再約一天回來一起吃中飯。照淑芬姐吩咐向黃副座打聲招呼（前一陣子他找科長聊天的時候還提到我的畢業論文），然後我和 Waiting 到出納串門子（中間突然想到衝回會計處拿秉棋哥請客、蔚民硬開成的大苑子芋頭奶綠），聊到下班後三十分鐘欲罷不能，以為差點趕不上最後一班回彰化的車，結果車子六點才來。

24 號星期四中午吃飽飯後搭車上新竹，傲少等在車站載我到清大，兩人先在校園內散步一圈。晚餐小 Nate 加入，三人吃完甘泉魚麵，買三杯烏龍珍奶回小吃部繼續聊天，晚一點得腸胃型感冒的 CC 賢也來了。我用 iPhoto 講了一會英國故事，小 Nate 也拿出 iPod touch 讓大家玩一個神祕的拼圖遊戲。還在桃園 HTC 加班的許博肥十一點多說會過來，到的時候已經十二點多了，我們移師 CC 賢實驗室旁附設的娛樂間，裡面有台電子琴讓我玩了一會。兩點多，我們再移往「早餐店」（絕對是台灣特產）吃完消夜才散去。我想我的時差應該是從這天開始調的 XD。夜宿傲少房間，他驅離室友空出一張床（因為上次他室友也做過同樣事情）。新竹晚上極冷，不過傲少讓我蓋了三件被子，睡得不錯。

隔天和傲少多聊一下，接近中午時前往國光客運清大站，搭車到林口長庚。Yen3 已經安排好吃牛肉麵，許博肥又義氣搭計程車過來一塊吃，但才吃半小時就被緊急電話召回開會了。我和 Yen3 搬到麥當勞繼續聊，我用他的甜心卡買了一杯大的玉米濃湯（又是台灣特產）和大杯可樂。幾個小時後麥當勞響起火災警鈴，雖然是 false alarm 不過我們也藉機離開，我準備搭統聯回去。不過星期五交通繁忙，我只買到快七點的票，還要等兩個小時，Yen3 就帶我參觀長庚大學（嵌在國立體育大學裡面！），順便講了一下他的論文主題。統聯一班接著一班疏運人潮，雖然出發時間比預訂晚了約二十分鐘，但我覺得已經很厲害了。

四月 4 號中午傲少來訪，帶著他精雕的華麗紙摩天輪卡片送給我。我們聊到五點，傲少騎車把我交給香香後先走，我晚上和香香、許博肥（三度赴會！）、南宏、書佑吃大象牛排。話題大致圍繞在高中時期的霸凌和電研資訊社秘辛，還有牙醫內幕和 scm 老師的神鬼認證。我們聊到九點半才被趕走。

最後壓軸是 8 號星期五的十一梯（67–77T）役男演訓召集。我成功召到連我在內共八人，四人（顯光顯奕兩兄弟還有承賢和威廷 — 威廷這天假是硬請到的）遠從台北回來（可惜宣余有課未到），另外三人（俊元、啟禎、舉哥）都在台中（俊元似乎排開了一個有點規模的討論會）。十點多到辦公室，承賢已經先到了，十一點過後威廷、俊元、啟禎也陸續到齊，顯光顯奕在十二點抵達。一行人包括蔡專員、千莉視察和琦皓在中興小館圍成熱鬧的一桌，舉哥稍後也抵達了。蔡專員叫了整桌菜，光湯就三鍋，最後又加兩盤青菜續兩瓶麥茶。下午整群人拜會各科室，聲勢浩大，身為召集人的我不禁覺得很有面子！XD 三點多拜會完畢，我回到會計處和淑芬姐聊天，其他人四點多說要先走，但當我五點半到國光站前卻看到一群人還聚在那，原來是車位要等到六點。再聊一會，我的車先來了，就先這樣，大家下次再見啦。

--
如果你覺得這篇冷冰冰，that's intended effect. XD

[facebook digest] 返台六週

2011-04-09T14:13:00.001+01:00

Just a title and another line "Don Knuth (Stanford)". Is it real?! ↦ Oxford University Computing Laboratory: Long and skinny knight's tours [2011-02-14 11:03:49 +0000]
- Josh Ko ⇒ So close! But he is so intimidating... XD [2011-02-14 13:02:19 +0000]
- J************* ⇒ He's really quite friendly... [2011-02-14 19:21:22 +0000]
Perhaps Lansoprazole works better for me. Even if it is not the case, I still feel much better today anyway. [2011-02-14 13:57:38 +0000]
Knuth REALLY knows how to have fun! [2011-02-15 18:09:46 +0000]
- Josh Ko ⇒ His grasp of concrete mathematics is so clear and natural - certainly a real artist. [2011-02-15 18:39:13 +0000]
- Josh Ko ⇒ Concretely, he went through Chapter 42 of one of his latest books, Selected Papers on Fun and Games.
  http://www-cs-faculty.stanford.edu/~uno/fg.html [2011-02-15 19:40:32 +0000]
- L********** ⇒ You seemed to have great fun from his talk too! [2011-02-15 20:30:54 +0000]
- Josh Ko ⇒ I did, for sure! [2011-02-15 21:07:25 +0000]
- L********** ⇒ I can tell that your understanding of concrete maths is very concrete, dont you think? [2011-02-16 00:22:00 +0000]
- W************ ⇒ Although I can get the mean of concrete mathematics, i think it's very interesting for the grasp. [2011-02-16 01:02:40 +0000]
- Josh Ko ⇒ My understanding? No, I am not skilled in concrete math (specifically, all those techniques recorded in the book with the name). But I appreciate the concrete flavour in Knuth's work, and I am awed by how concrete he can get to. [2011-02-16 08:17:54 +0000]
- L********** ⇒ I see, Don is indeed quite passionated in concrete maths. [2011-02-16 10:54:22 +0000]
I need to make a major change to the direction of my essay... Otherwise it's bound to get too long and less focused. [2011-02-17 11:38:19 +0000]
- Josh Ko ⇒ I estimate the original plan can lead to a 50-page essay... [2011-02-17 11:54:37 +0000]
- C************ ⇒ Relax~There're three more years !haha [2011-02-17 14:55:59 +0000]
- Josh Ko ⇒ This essay, however, is due at the end of this term, merely 23 days away... [2011-02-17 15:39:05 +0000]
- S************ ⇒ Is that your transferring dissertation? [2011-02-18 00:28:08 +0000]
- Josh Ko ⇒ No, it's not, but it may form a part of the dissertation. [2011-02-18 07:45:47 +0000]
舉頭忽見，柔墨輕潑月暈渲，今夜又共嬋娟。 [2011-02-17 21:00:54 +0000]
看起來很容易操作的食譜，可以當新購（二手）電鍋的處女作。 ↦ 【反媽簡易食譜】香噴噴的魯肉飯..省錢方便又簡單的電鍋料理來囉.. @ 反嗑為主反推有理 :: 痞客邦 PIXNET :: [2011-02-18 20:15:11 +0000]
- J******** ⇒ 我也常做類似的
  簡單的豬肉醃一下放入電鍋
  飯好肉也好了，之後再炒個菜快速方便 [2011-02-19 00:30:44 +0000]
又以出清價向 Mark 收購一個完整版的大同電鍋，順帶拿了不少保鮮盒和幾件餐具，可料想日後的菜色應該會愈來愈多。需要保鮮盒的可以找我拿幾個，我一個人用不了那麼多⋯ [2011-02-21 18:03:55 +0000]
- 翁** ⇒ 原來牛津是餐飲大學XDDD [2011-02-22 00:46:00 +0000]
- W************ ⇒ 民以食為天啊XD 自己動手比較便宜咩~ [2011-02-22 09:15:30 +0000]
魯肉做成蒸肉，單吃還不錯，配麵就不夠鹹了。肉應該要先醃一下顏色才會比較深？ ↦ http://www.facebook.com/photo.php?fbid=168359006549978&set=a.126799950705884.40277.100001276392360 [2011-02-22 13:09:47 +0000]
- W************ ⇒ 應該不用吧，是要不要再煮久一點 ? [2011-02-23 03:17:53 +0000]
- J******** ⇒ 麵是指湯麵嗎？通常湯麵配抄過的料會比較香歐！
  配飯瓜子肉是個不錯的選擇(英國有華人超市吧！？) [2011-02-23 05:04:50 +0000]
- E******** ⇒ 醬油多一點，小火悶久一點，應該不用醃吧 [2011-02-23 12:27:41 +0000]
I need a good example for with-matching... [2011-02-23 16:01:11 +0000]
- S************ ⇒ Are you teaching someone Agda? [2011-02-23 17:00:44 +0000]
- L************** ⇒ (mod n) ? [2011-02-23 17:03:22 +0000]
- Josh Ko ⇒ @scm: Not exactly. I am describing dependent pattern matching in my essay.
  @LT: That's a view, right? I was seeking something more exciting but now I think I will use a view... [2011-02-23 19:02:24 +0000]
- Josh Ko ⇒ Small examples are boring, while interesting examples are too big... [2011-02-23 19:33:41 +0000]
Perhaps I have never been really aware that I have given up playing the piano seriously, in the sense that it is almost for sure that I will never succeed in playing the Polonaise-Fantaisie, or Ballades No 1 & 4, because I will never be able to reach the demanded technical level nor allocate much time for them. (There is a mutual implication between the two reasons.) The best hope is that the accumulated time I spend on them in my whole life will lead to an acceptable approximation. That's going to be one of the justifications for my exclusive interest in Chopin's works. ↦ http://www.facebook.com/photo.php?fbid=168714059847806&set=a.126799950705884.40277.100001276392360 [2011-02-23 23:03:03 +0000]
I have felt the ulcer again since last night. So far it has been relatively mild, but I have no idea whether it will become worse or go away quickly. (This time I had 4 days of peace, from Sunday to Wednesday.) [2011-02-24 10:32:12 +0000]
Prepared quite some steamed rice with vegetables with my electric cooker. It tastes ok but I don't have appetite... [2011-02-24 18:10:32 +0000]
肚子痛房間就一團亂⋯ [2011-02-24 20:19:39 +0000]
feel worse today... [2011-02-25 18:31:25 +0000]
- W************ ⇒ It sounds not good … [2011-02-26 09:01:58 +0000]
這兩天決定要不要回台灣吞胃鏡⋯ [2011-02-25 22:36:19 +0000]
- F********* ⇒ Josh 千萬要保重!!! 有需要任何幫忙的話, 隨時打電話給我! Any time!!! [2011-02-25 22:54:39 +0000]
- T************** ⇒ 你要來台大醫院嗎 [2011-02-26 00:26:47 +0000]
- T************** ⇒ 我比較好奇你喝urea的時候有停用PPI嗎？ [2011-02-26 00:31:13 +0000]
- 陳** ⇒ 學長保重呀@@ [2011-02-26 00:46:43 +0000]
- Y************* ⇒ 回來呀! 這樣就可以去找你了 [2011-02-26 04:27:22 +0000]
- Josh Ko ⇒ @Frank: Thanks a lot! 希望能快點再和你們一塊晨走呀⋯
  @TS: 大概不會去台大，現在待台北不太方便。（你有特別推薦的理由？）做呼氣測試前醫生確實沒叫我停藥，我後來看到有一種標榜不用特別停藥的但我也不是吃那種，所以開始對他不太有信心⋯我現在比較擔心療程長短，不知道如果回台灣的話得待多久？
  @小朋友：謝啦！考試結果還 OK?
  @YT: 唉，聽說你六月才回去？我現在是希望頂多一個半月可以回英國啦，所以應該待不到六月。（如果待到六月就是休學了⋯） [2011-02-26 06:23:46 +0000]
- W************ ⇒ 嗯 ... 不知道要說什麼，反正，身體優先。 [2011-02-26 09:01:32 +0000]
- L************** ⇒ 請保重！養病養好了再繼續會比較好 ... [2011-02-26 12:18:42 +0000]
- 王** ⇒ take good care [2011-02-26 13:52:21 +0000]
- T************** ⇒ 胃鏡頂多只要半小時，你可以看完就回彰化，又不是要開刀...
  台大有幾個醫生我覺得不錯，不然施銘gay應該可以有好的人選建議，
  應該是兩個星期左右吧然後停藥然後再測失敗再換別的藥再測
  
  while JoshKo.getUlcer == 1
  {
  JoshKo.takeExam()
  JoshKo.takeMed()
  JoshKo.stopMed()}
  } [2011-02-26 14:56:22 +0000]
- Josh Ko ⇒ 我媽剛才已經在彰基找比較熟的醫生約好星期四做胃鏡，明天打電話給旅行社，希望星期二回去。 [2011-02-26 14:59:29 +0000]
- T************** ⇒ 好禿我下下星期會回彰化再去看你 [2011-02-26 15:01:38 +0000]
- S************ ⇒ 希望早日康復！如果需要來台北的話可以住我這邊。 [2011-02-27 01:12:50 +0000]
- Y************* ⇒ So you are in Taiwan now? Oh ~ no [2011-02-27 05:27:04 +0000]
- Josh Ko ⇒ @scm: Thanks! 治療順利的話，還可以去聽一下你的課耶！
  @YT: 還沒但快嘍。如果我之後進度趕得回來的話，說不定九月可以有理由再回去勒！ [2011-02-27 18:15:06 +0000]
even worse today, unbelievable... [2011-02-26 19:55:51 +0000]
- T************** ⇒ 可以好的，看我現在這樣子就知道了XD
  不過你應該可以體會到我那時候的絕望了XD [2011-02-27 03:00:55 +0000]
- T************** ⇒ 你媽說要買軟便劑，我建議可以買MgO (magnesium oxide)，他也是鹼性的，附帶中和胃酸。我不確定會不會和PPI有交互作用，你可以問問看施銘gay [2011-02-27 03:27:13 +0000]
- T************** ⇒ 你可以變成餅乾怪獸，肚子比較不會痛 [2011-02-27 03:36:19 +0000]
倉皇準備逃回台灣，雖然狼狽不堪但也是段經歷。 ↦ Pollini plays Chopin Nocturne op.32 no.2 [2011-02-27 11:18:51 +0000]
- P************* ⇒ 祝福你 [2011-02-27 14:44:14 +0000]
- J******************* ⇒ 身體是革命的本錢! PHD慢慢讀就可以了! [2011-02-27 14:45:18 +0000]
Flights confirmed (and X70 bus tickets booked):
21:00, 1 Mar, LHR T4 - CI070 - 18:35, 2 Mar, TPE T1
09:25, 12 Apr, TPE T1 - CI069 - 17:05, 12 Apr, LHR T4 [2011-02-27 14:52:14 +0000]
GSS report done; don't forget the Census. [2011-02-27 15:23:48 +0000]
It cannot be related to what I am thinking?! My idea about "generic lookup with ornaments" has begun to take shape, but a moment ago when I tried to compare my (still rough) idea with the diamond modality and its associated find operation, I started to feel something in my stomach. [2011-02-28 20:21:28 +0000]
- S************ ⇒ At least there is now a clue worth following.. [2011-03-01 07:21:36 +0000]
Ever since I played in Chopin Nocturne Night I have never touched the piano again, except for the digital piano which is now owned by Liang-Ting. My original plan (formulated before Christmas) was to play daily! It is obvious how seriously the plan was disrupted. [2011-02-28 21:04:39 +0000]
Position this term.
(http://gaogaigar.wikia.com/wiki/Protect_Shade) ↦ http://www.facebook.com/photo.php?fbid=169907736395105&set=a.126799950705884.40277.100001276392360 [2011-02-28 21:14:10 +0000]
撤電腦、拔插頭、出發！ [2011-03-01 14:32:43 +0000]
- J******************* ⇒ welcome back to Taiwan [2011-03-01 14:55:07 +0000]
Checked in. Depart in three and a half hours. [2011-03-01 17:29:35 +0000]
No free wifi at Heathrow. Sigh, even Taoyuan airport provides that! [2011-03-01 18:49:22 +0000]
Now on board the aircraft. Turning off the mobile. [2011-03-01 20:27:35 +0000]
Finally arrived at home. [2011-03-02 14:10:21 +0000]
- Josh Ko ⇒ Tony Hoare's lecture(s) regretfully missed. [2011-03-02 14:14:23 +0000]
- J********** ⇒ I'm going there tonight @ Wolfson and tomorrow @ comlab! [2011-03-03 15:28:59 +0000]
- Josh Ko ⇒ Please give me a summary of what he says afterwards! [2011-03-03 20:05:02 +0000]
It seems the generic lookup problem has been satisfactorily solved by generic modality. I need to find another story to tell. [2011-03-03 13:27:14 +0000]
Just came up with a more ambitious idea than generic lookup, which looks promising in terms of potential, but I'm not sure how hard it will be to develop the idea yet. And safe indexing for lists can be a motivating example for it if it works. [2011-03-03 20:28:22 +0000]
Ornamental-algebraic ornaments turn out to be very worth investigating! [2011-03-04 00:53:56 +0000]
- Josh Ko ⇒ Wished I were at Oxford... [2011-03-04 00:56:02 +0000]
- 翁** ⇒ 可以寫中文嘛，應該入境隨俗喔XDD [2011-03-04 01:03:37 +0000]
- Josh Ko ⇒ 「結果裝飾代數式的裝飾很值得研究一番！」
  不要翻譯比較好啊⋯ XD [2011-03-04 01:52:38 +0000]
- 翁** ⇒ 恩，太學術的東西還是英文好!醫生看的如何? [2011-03-04 01:55:22 +0000]
- Josh Ko ⇒ 胃鏡照起來還滿正常的，現在感覺也正常，但之前那些痛就得不到完善的解釋。再觀察幾天看看。 [2011-03-04 01:57:28 +0000]
- 翁** ⇒ 恩，看來沒問題，那可以吃頂唐鋒了XD [2011-03-04 02:00:33 +0000]
- Josh Ko ⇒ 欸，吃那個好飽好痛苦喔，不能吃個皇上皇就好嗎？XD [2011-03-04 02:01:22 +0000]
- 翁** ⇒ XD可是我覺得吃燒臘飯很普通耶 [2011-03-04 02:02:10 +0000]
- Josh Ko ⇒ 一點也不⋯ 我好想念他的燒肉飯 XD。 [2011-03-04 02:02:53 +0000]
- W************ ⇒ 愛家啦 [2011-03-04 14:21:33 +0000]
Time to consider composition of ornaments, starting from the special (but already useful) case where one of the two ornaments is algebraic. [2011-03-04 02:21:45 +0000]
Why, ornamental-algebraic ornaments correspond perfectly to realisability! Why does "Vec A n" say that the natural number n realises List A? Because to expand n to a list of A's, we need to supply n elements of A, which is a vector of length n! [2011-03-04 02:28:38 +0000]
- Josh Ko ⇒ And this explanation works for all the examples I have in hand: Nat to Fin, Nat to List, List to Vec, and List to SortedList. [2011-03-04 02:31:51 +0000]
- Josh Ko ⇒ And we can prove that a realiser of some type A and a corresponding realisability proof can be integrated into a proof of A, echoing our intuition about realisability. [2011-03-04 02:34:20 +0000]
- Josh Ko ⇒ Conversely, we can of course separate a proof of A into a realiser and a realisability proof. Since the realiser is of a simpler type and the realisability predicate is one on the realisers, which are of the simpler type, we essentially factored a complex type into simpler ingredients. The potential for compositionality then shows up. [2011-03-04 02:38:57 +0000]
I think I now have a cute story to tell! [2011-03-04 14:41:39 +0000]
- Josh Ko ⇒ Bad timing. I really should have been in Oxford now. [2011-03-04 14:56:36 +0000]
- J************* ⇒ Feel free to tell me by email... [2011-03-04 18:42:16 +0000]
- Josh Ko ⇒ Just did that! [2011-03-04 23:39:56 +0000]
Everything just fits together and works! [2011-03-04 20:39:46 +0000]
My idea is more accurately described as "fusing an algebra into an ornament" instead of "fusing two ornaments where one of them is algebraic". The new description subsumes the original notion of algebraic ornaments, which is fusing an algebra into the identity ornament. [2011-03-05 12:39:08 +0000]
- Josh Ko ⇒ The algebras then form some kind of structure (with weak properties, I guess) which acts on the ornaments. [2011-03-05 12:42:54 +0000]
- Josh Ko ⇒ Not sure whether we should get rid of the original notion of algebraic ornaments. [2011-03-05 12:47:25 +0000]
- Josh Ko ⇒ The subsumption cannot be proved in Agda due to lack of extensionality. [2011-03-05 13:31:17 +0000]
A possible title might be "Ornamental algebraic ornaments, algebraic ornament ornaments". XD [2011-03-05 15:55:16 +0000]
Need to do the proofs on paper first. It is hopeless to try to work out the proofs directly in Agda... [2011-03-05 23:32:03 +0000]
Note on ornamental algebraic ornaments and algebraic ornament ornaments. (The names can be changed!) ↦ http://sites.google.com/site/joshkos/OAOAOO_note.pdf [2011-03-06 13:19:53 +0000]
Implementation is nontrivial. [2011-03-06 23:12:45 +0000]
- Josh Ko ⇒ Because doing datatype-generic induction is painful... [2011-03-06 23:37:46 +0000]
As suspected, the remember function and the recomputation lemma for algebraic ornaments are subsumed by the general facilities of the realisability framework. [2011-03-06 23:29:30 +0000]
6 goals, 6 inductions. Pretty scary... [2011-03-07 00:37:05 +0000]
有史以來做過最難的 induction，幾無頭緒，都快哭出來啦！ [2011-03-07 03:40:52 +0000]
- Josh Ko ⇒ 算是卡住了。也是該卡住，不然刷刷刷一下寫完不就沒什麼價值！ [2011-03-07 03:42:47 +0000]
- W************ ⇒ ... 加油 !! [2011-03-07 04:14:26 +0000]
There does not seem to be particular reason not to directly consider fusion of arbitrary ornaments. [2011-03-07 13:11:22 +0000]
- Josh Ko ⇒ Not very straightforward after a quick experiment. Let's stick to algebraic ornament ornaments for now. [2011-03-07 13:29:16 +0000]
Oops, fusion of arbitrary ornaments is successfully defined, which is more complex than algebraic ornament ornaments, of course. If the former really works then there's no point dealing with the latter anymore. [2011-03-07 17:40:08 +0000]
- Josh Ko ⇒ The good thing is that we can get rid of the awkward name "algebraic ornament ornaments". XD [2011-03-07 17:43:17 +0000]
- Josh Ko ⇒ Hmm... I like the word "composition" more than "fusion". [2011-03-07 17:45:52 +0000]
- Josh Ko ⇒ I anticipate there will be significant difficulties with substitution of equal indices... [2011-03-07 17:58:46 +0000]
- Josh Ko ⇒ My gosh, I just noticed that the new index set is actually a pullback! [2011-03-07 18:03:47 +0000]
Soon heading for Taipei and will try to sell the story to Shin in the afternoon. [2011-03-07 22:50:12 +0000]
Finally succeeded in my first datatype-generic induction! (More to come...) [2011-03-09 02:55:17 +0000]
- L********** ⇒ Any interesting result? [2011-03-09 20:06:20 +0000]
- Josh Ko ⇒ I think so, if I can succeed in implementing the ideas (which look plausible)! [2011-03-09 22:56:05 +0000]
- L********** ⇒ En...We all can not avoid coding at some point... [2011-03-10 23:18:15 +0000]
It is really absolutely necessary to record my own playing so defects can be identified and corrected afterwards. Keep in mind to sing and breath elegantly when playing Chopin! [2011-03-10 09:08:03 +0000]
Once again the goal type is too long to be pasted on fb as a status update. The length is actually not surprising; the problem is I don't know how to abstract variables to make induction go through. [2011-03-11 08:34:55 +0000]
If I just give up and postulate extensionality...? [2011-03-11 11:27:15 +0000]
- Josh Ko ⇒ Then we won't have practically working examples. That's bad. [2011-03-11 11:28:50 +0000]
Goal:
erase O
(mapFold ⌊ O ⌋ ⌊ O ⌋ (ornAlg O)
(erase (algOrn ⌊ O ⌋ (φ ∘ erase O))
(mapFold ⌊ algOrn ⌊ O ⌋ (φ ∘ erase O) ⌋
⌊ algOrn ⌊ O ⌋ (φ ∘ erase O) ⌋
(ornAlg (algOrn ⌊ O ⌋ (φ ∘ erase O)))
(isoF₂ O φ
(mapFold ⌊ algOrn' O φ ⌋ ⌊ algOrn' O φ ⌋
(<_> ∘ isoF₂ O φ) ds)))))
≡
erase (algOrn' O φ)
(mapFold ⌊ algOrn' O φ ⌋ ⌊ algOrn' O φ ⌋ (ornAlg (algOrn' O φ)) ds) [2011-03-12 10:30:42 +0000]
- Josh Ko ⇒ Still finding a way to suitably generalise this type. [2011-03-12 10:31:28 +0000]
- Y************* ⇒ what's the hell? [2011-03-13 04:52:35 +0000]
- Josh Ko ⇒ You're right, it's hell! Therefore I am trying to bypass this mess. [2011-03-13 04:59:47 +0000]
- Y************* ⇒ Ha! I know that's the devil you are facing now. My point is what's that? Is it a kind of mathematical issue? [2011-03-13 05:09:51 +0000]
- Josh Ko ⇒ It's some proposition I am trying to prove. You can see that there is a three-line equality sign in the middle, so what I'm trying to prove is that two things are equal, which have long and scary descriptions. [2011-03-13 05:12:35 +0000]
- T************** ⇒ ⌊ O ⌋ 感覺很強壯
  Orn' 小狗 [2011-03-14 10:15:02 +0000]
Perhaps try to perform fold fusion?! [2011-03-12 12:00:24 +0000]
Even just stating the fusion theorem is problematic... [2011-03-12 22:46:36 +0000]
Fusion theorem stated and proved (with an explicit application of subst)! [2011-03-13 03:58:01 +0000]
So now the hard work falls on proving the fusion conditions, which is still far from trivial. [2011-03-13 06:01:06 +0000]
Two ways to go: keeping staring at the fusion condition and trying to disentangle the parameters, or postulating extensionality and finishing the coding quickly, at the expense of losing a working implementation. [2011-03-14 00:25:03 +0000]
Un oh, the need to disentangle the parameters is not eliminated by postulating extensionality... [2011-03-14 01:03:47 +0000]
Good luck to Japan... (Just before the first ICFP ever held in Asia... sigh.) [2011-03-15 10:42:55 +0000]
- Josh Ko ⇒ Pollini plays Etude Op 25 No 12 (Ocean): http://www.youtube.com/watch?v=5M2PO4f5Y7k [2011-03-15 10:45:55 +0000]
Bought this from iTunes Store UK. A good recording to own. ↦ Fryderyk Chopin - The Complete Works of Fryderyk Chopin on historical instruments - NIFCCD 007. 24 E [2011-03-15 11:55:05 +0000]
After (finally) recognising the recursion pattern as accumulating parameters, now it seems I am on a right track to a suitable generalisation. [2011-03-16 00:39:15 +0000]
- Josh Ko ⇒ That also means I need to invent a nice and useful loop invariant... [2011-03-16 00:48:33 +0000]
Stomachache reappeared yesterday but has been relieving, indicating the real cause may have been identified. Meanwhile I am still having trouble proving the datatype-generic fusion condition. Perhaps I should start writing the easy part first. [2011-03-18 08:48:54 +0000]
I didn't know Robert Harper's writing is so "spicy"! ↦ Existential Type [2011-03-19 00:32:03 +0000]
- L*********** ⇒ Waiting for more posts, hahaha.. [2011-03-19 15:55:07 +0000]
默哀⋯ "We have now had the official clearance from Council that the department can change its name to The Department of Computer Science as of the 1st June 2011." [2011-03-24 00:09:04 +0000]
Unbelievable! Suddenly I managed to come up with a nice and working loop invariant and the proof of the fusion condition just went through effortlessly! (Three more to go...) [2011-03-24 01:07:59 +0000]
- L************** ⇒ That's really mathematical! [2011-03-24 01:09:25 +0000]
- Josh Ko ⇒ And then I realised I proved the wrong thing. That's also a common phenomenon, I think? XD [2011-03-24 01:14:55 +0000]
- L************** ⇒ Sometimes you find the right proof from a wrong one. :-) [2011-03-24 01:21:02 +0000]
Impressive! ↦ GaoGaiGar - Television Tropes & Idioms [2011-03-24 05:49:47 +0000]
Reduced the fusion condition to some kind of parametricity. Hope it will be easier to see how to melt and expand the structures involved. [2011-03-26 14:21:53 +0000]
- Josh Ko ⇒ Turns out to be the right direction. Now I can do induction without worrying about "parameter entanglement". [2011-03-26 15:40:20 +0000]
- Josh Ko ⇒ I believe I am close to my first projection. [2011-03-26 16:04:39 +0000]
First projection typechecked! It took me quite a few days to realise I needed to break things into pieces finer than I had anticipated. I think it was due to lack of experience. But well, now I have gained the experience. XD [2011-03-27 02:52:41 +0000]
- Josh Ko ⇒ Second projection should be similar. What's more interesting (meaning requiring some more work) is integration, which should be able to be tackled in time because we're looking at a special case (namely algebraic ornament-ornaments). [2011-03-27 02:59:27 +0000]
- Josh Ko ⇒ The code will require substantial tidy-up afterwards... [2011-03-27 03:09:09 +0000]
Second projection produced in minutes by copy-n-paste. [2011-03-27 05:41:30 +0000]
Integration (with six successive rewrites) also typechecked! Only the examples are left, which are easy. [2011-03-27 12:52:55 +0000]
- Josh Ko ⇒ And the paper, of course. [2011-03-27 13:10:33 +0000]
The solution looks quite straightforward - after it is found... [2011-03-27 13:48:45 +0000]
- L********** ⇒ This happens from time to time [2011-03-29 04:35:44 +0000]
I am not writing a pearl after all, so let's stick to the standard form, beginning with a standard introduction... [2011-03-29 15:45:56 +0000]
Suddenly not very sure how to sell my discovery... [2011-03-30 08:47:20 +0000]
- J******************* ⇒ 包裝也是一門技術阿XD [2011-03-30 08:48:38 +0000]
- 王** ⇒ 我發現寫科學文章腦中最長閃過的念頭就是如何自圓其說 [2011-03-30 10:06:04 +0000]
- L********** ⇒ Does it wok well in practice? [2011-03-30 23:10:45 +0000]
- Josh Ko ⇒ It is a solution to a practical problem and works well, I think, but what is the exact problem that it solves I am still not very sure (but not far away from it). [2011-03-31 07:16:55 +0000]
- S************ ⇒ Reminds me of the old 42 joke -- it's an answer taking millions of years to compute. However, the question was lost. [2011-04-01 01:37:06 +0000]
- S************ ⇒ Answer to the Ultimate Question of Life, the Universe, and Everything (42) [2011-04-01 01:37:08 +0000]
寫得又慢又爛，真討厭⋯ 不過還是只能先寫個大概再修了。 [2011-03-31 05:58:16 +0000]
- 翁** ⇒ 果然是太久沒寫作文了XDD [2011-03-31 06:04:36 +0000]
- Josh Ko ⇒ 應該叫學弟每個月交中英文論說文各一篇！XD [2011-03-31 06:05:58 +0000]
- 翁** ⇒ ......中文就要寫不出來了，還寫英文哩，我看辦公室也沒人會改XD [2011-03-31 06:06:47 +0000]
- Josh Ko ⇒ 編預算請老師來改好了 XD。 [2011-03-31 06:07:49 +0000]
- W************ ⇒ 我看用英文寫這條件一出來可能就沒人要進來了XDD [2011-03-31 08:53:49 +0000]
"Incidentally, had we proved AOE and AOE^{-1} from scratch, implementation of remember and recomputation can be made perfectly symmetric under the realisability view." I like this part because the symmetry comes out somehow surprisingly and looks beautiful. And it is much more justified to publish a paper which contains something beautiful. [2011-04-01 06:20:20 +0000]
- L************** ⇒ What does AOE mean? [2011-04-01 12:16:04 +0000]
- Josh Ko ⇒ Age of Empires... XD
  (Seriously, the initials of "algebraic ornament" and "equality".) [2011-04-01 12:31:48 +0000]
- Josh Ko ⇒ (The realisability predicate for an algebraic ornament can be reduced to an equality.) [2011-04-01 12:32:30 +0000]
- L************** ⇒ Cool! Are you giving a talk after you arrive? BCTCS? [2011-04-01 12:33:28 +0000]
- Josh Ko ⇒ You mean to you, right? I still did not sign up for MGS in the end. BCTCS, hmm... not sure whether it is worthwhile to stay for three days... [2011-04-01 12:39:51 +0000]
- L************** ⇒ Surely you can leave earlier! Don't worry about the registration fee. If you'd like, you can stay at my place to get £100 off. But, I think it will be paid from the project funding? [2011-04-01 12:41:50 +0000]
- Josh Ko ⇒ Whoo, I didn't notice the registration fee. Can I just sneak in for the talks and skip the lunches, banquet and stuff, and also skip the payment? XD [2011-04-01 12:47:36 +0000]
- L************** ⇒ Yes, I think so. But if you'd like to give a talk, of course you have to pay it! [2011-04-01 12:48:22 +0000]
- Josh Ko ⇒ Oh, I was thinking of giving a talk to you at your place. For now I am less interested in talking in BCTCS - it's safer to publicise it after I have some discussions with Jeremy, I think. XD [2011-04-01 12:56:00 +0000]
- L************** ⇒ I'd be quite happy to enjoy your talk! [2011-04-01 13:03:08 +0000]
Diagram for the first projection. ↦ http://www.facebook.com/photo.php?fbid=177814358937776&set=a.126799950705884.40277.100001276392360 [2011-04-01 18:37:03 +0000]
- Josh Ko ⇒ TikZ. [2011-04-02 10:47:21 +0000]
- L********** ⇒ Thx [2011-04-04 22:01:06 +0000]
Produced an insertion sort which emits a sorted vector carrying proof that it has a certain length and is sorted, but it can only sort at most **TWO** elements. Give it a three-element list and Agda just hangs. [2011-04-06 07:42:11 +0000]
- Josh Ko ⇒ This is the sorted vector [0, 1]:
  <
  true ,
  < false , refl > ,
  < false , refl > ,
  < false , < false , refl > , refl > ,
  < true , < false , refl > , refl > ,
  <
  true ,
  < true , < false , refl > , refl > ,
  < false , refl > ,
  < false , < true , < false , refl > , refl > , refl > ,
  < false , refl > ,
  < false , < true , < false , refl > , refl > , refl > , refl
  >
  , refl
  > [2011-04-06 07:51:31 +0000]
- Josh Ko ⇒ Hmm, it just takes a very long time to produce [0, 1, 2] (from [1, 2, 0]):
  <
  true ,
  < false , refl > ,
  < false , refl > ,
  < false , < false , refl > , refl > ,
  < true , < true , < false , refl > , refl > , refl > ,
  <
  true ,
  < true , < false , refl > , refl > ,
  < false , refl > ,
  < false , < true , < false , refl > , refl > , refl > ,
  < true , < false , refl > , refl > ,
  <
  true ,
  < true , < true , < false , refl > , refl > , refl > ,
  < true , < false , refl > , refl > ,
  <
  true ,
  < true , < false , refl > , refl > ,
  < false , refl > ,
  < false , < true , < false , refl > , refl > , refl > , refl
  >
  ,
  < false , refl > ,
  <
  false , < true , < true , < false , refl > , refl > , refl > , refl
  >
  , refl
  >
  , refl
  >
  , refl
  > [2011-04-06 08:00:47 +0000]
- L********** ⇒ Why does it take so long? [2011-04-07 04:39:44 +0000]
- Josh Ko ⇒ I think Agda implementors do not put emphasis on optimisation for speed (it is not necessary anyway, given that the language is an experimental one). Also I used a lot of rewrites which get translated to a large amount of code. [2011-04-07 07:39:40 +0000]
Acceptable, I think. [2011-04-06 15:14:55 +0000]
- Josh Ko ⇒ Barely acceptable, to be precise... [2011-04-06 15:18:40 +0000]
巡迴結束於今日的中興大聚餐，明天收一收後天回去嘍。（照片和 blog 後補⋯） [2011-04-08 11:38:10 +0000]
- Josh Ko ⇒ 琦皓你的相機時間慢了一年！XD [2011-04-08 11:44:46 +0000]
- 翁** ⇒ 抱歉，當初是相機店老闆設定的，我也沒特別注意XD [2011-04-08 12:04:35 +0000]
- Josh Ko ⇒ iPhoto 可以批次調整日期，所以按幾個鍵就搞定了 XD。 [2011-04-08 12:06:06 +0000]
- 翁** ⇒ 我把相機更新了XD [2011-04-08 18:07:34 +0000]
APLAS '11 (and CPP '11) to be held in KENTING! (So that was what they were secretly discussing last year.) Should consider submitting a... poster? XD ↦ start [The Ninth Asian Symposium on Programming Languages and Systems, APLAS 2011] [2011-04-09 00:24:01 +0000]
- S************ ⇒ Should I post the CFP on facebook? [2011-04-09 00:54:53 +0000]
- Josh Ko ⇒ Sounds like a good idea! More publicity does no harm. (Dunno whether this has been done before. Perhaps you'll be the first one to do so? XD) [2011-04-09 00:59:17 +0000]

GSS student report, Hilary Term 2011

2011-02-28T21:07:00.001Z

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

--
A somewhat discouraging report...