2012/01/29

[facebook digest] Home and back

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

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

    Questions to be answered:

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

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

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

Labels: