[facebook digest] Dutch National Flag

1. 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]
2. This site is amazing! ↦ Bathrobe's "Harry Potter in Chinese, Japanese & Vietnamese Translation"    [2011-06-05 11:29:50 +0100]
3. 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]
4. So this is it! ↦ 公開徵求 2011 台英(NSC-RS)合作交流互訪計畫    [2011-06-07 08:38:39 +0100]
5. Celebration twice a day.. It's fortunate that I am on the third floor.    [2011-06-07 12:37:21 +0100]
6. 昨天學院舉辦「與老闆晚餐」，席間聊到醫生待遇，Jeremy 突然問我台灣情況如何。我用平均一秒講一個字的慢速破破爛爛地湊出一點東西，像是前一陣子才一個實習醫師工作壓力太大過世、雖然薪水和社會地位都高但是十分辛苦、家長普遍希望小孩讀醫等等。當三個人盯著你等你講完的時候，用這種速度講話實在無比尷尬 — 而且他們的語速都是一秒四、五個字吧⋯ 我竟沒想到可以講名駒醫師才在他個板上貼的「與第一線難纏病人接觸」的記錄（與情緒發泄），或描述更久以前我所身處的詭異氛圍（見連結）。只能說遇到這種場合我就整個慌了。 ↦ 摃龜了.............    [2011-06-07 20:09:33 +0100]
   • L*********** ⇒ 欸，背景雜訊這形容真貼切。旁人講中文偶爾會對我形成干擾，然英文完全不會，我得「認真」才有辦法聽進去，一恍神就會變雜訊。這個界線在哪呀...    [2011-06-08 08:56:14 +0100]
   • 柯** ⇒ 是不是從小我都沒有給你表達的機會，常常都是我一個人在講，所以沒有開發你閒話家常這方面的天賦呢？回台時姐姐給你最密集的特訓，看在可能元兇是我的份上，算你免費！    [2011-06-08 16:11:36 +0100]
7. 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]
8. 退伍一週年！    [2011-06-09 08:53:22 +0100]
   • L********* ⇒ 我還要好久才能講這句話 orz    [2011-06-09 17:54:31 +0100]
9. 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]
10. 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]
11. Always stuck at the last sentence..    [2011-06-09 15:57:24 +0100]
12. 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]
13. 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]
14. "[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]
15. 「一切藝術的問題都是節奏的問題，無論繪畫、雕刻或音樂都是一樣。既然美感就是動感，每一種形式都有隱含的韻律。就連建築方面亦然，歌德式的教堂彷彿在沈思。美學上甚至可以用「衝」「掃」「粗魯」等人格的形容詞，這些都是韻律的觀念。中國藝術的基本韻律觀是由書法建立的。中國批評家欣賞書法並不注重靜態的比例或調和，而是暗中追溯藝術家從第一筆到末一筆的動作，如此看完全篇，彷彿觀賞紙上的舞蹈。」（林語堂《蘇東坡傳》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]
16. 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]
17. 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]
18. Yes, typed syntax and evaluation is definitely a killer app of ornaments.    [2011-06-14 10:37:39 +0100]
19. 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]
20. 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]
21. 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]
22. 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]
23. 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]
24. Very difficult indeed... but that's research!    [2011-06-16 09:52:10 +0100]
25. 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]
26. It works...!    [2011-06-16 13:57:34 +0100]
27. Having the essential bits, now I need to think about how to package them.    [2011-06-16 18:24:24 +0100]
28. 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]
29. 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]
30. 寫完這程式有種吃到胡斐那口白菜的感覺 XD。    [2011-06-17 20:05:14 +0100]
31. 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]
32. 差點忘了今天（英國時間）是「水坑」四周年紀念日。（借 Yen3 的 SNG 連線報導一用 XD。） ↦ No title, no thinking, no meaning: 有人還活著    [2011-06-18 22:43:21 +0100]
33. 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]
34. 錦源經歷兩屆資優班摧殘，這次又要帶科學班啦⋯ ↦ 科學班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]
35. 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]
36. "There is a Haskell on the cloud / I like to go there in my sleep"...    [2011-06-20 14:32:57 +0100]
37. Lists indexed by a vector of natural numbers — hmm.. a hint of datatype-genericity?    [2011-06-20 23:25:36 +0100]
38. Too excited about the Dutch national flag program that I still cannot fall asleep...    [2011-06-21 00:29:47 +0100]
39. 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]
40. 「反正」好像就是 disjunction elimination 嘛？XD    [2011-06-22 10:54:03 +0100]
41. Less types!    [2011-06-22 12:59:52 +0100]
    • Josh Ko ⇒ No, the attempt failed.    [2011-06-22 13:05:06 +0100]
42. 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]
43. 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]
44. "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]
45. 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]
46. 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]
47. 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]
48. 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]
49. Making another attempt to attack adjunctions.    [2011-06-25 22:05:12 +0100]
50. Finally met Jeremy at Tesco!    [2011-06-26 11:41:35 +0100]
51. 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]