2010/08/07

[facebook digest] 亂碼再現

  1. 下次錄鋼琴的時候記得檢查「使用環境噪音降低功能」有沒有關掉。打開來錄，很多踏瓣效果都被濾掉了，聲音有點噁心。    [2010-08-01 11:47:19 +0800]   [ 1 人說讚！]
    • Josh Ko ⇒ http://joshkos.blogspot.com/2010/08/playing-mazurka-op-50-no-3.html    [2010-08-01 13:52:22 +0800]
  2. 現在用 Altec Lancing VS2620 聽自己的錄音，低音和聲的感覺還挺棒的。（無論 Apple 原廠耳機還是 MBP 內建喇吧，低音都不清楚呀 XD。） ↦ Trek through Pure Reason: Playing Mazurka Op. 50 No. 3    [2010-08-01 19:48:25 +0800]
  3. 就算有 Unicode characters 可以用，命名還是很痛苦的事情⋯    [2010-08-01 22:13:09 +0800]   [ 1 人說讚！]
  4. Good sign! 之前摸出來對付 free channels 的方法似乎和現在對付「加在 typings 尾巴的 channel」的方法彼此不衝突。    [2010-08-01 22:19:35 +0800]
  5. Binders 現在變成一塊塊的蛋糕了！    [2010-08-01 22:45:03 +0800]   [ 1 人說讚！]
    • Josh Ko ⇒ 講太快，是簡單的 binders XD。    [2010-08-01 22:45:34 +0800]
  6. 把 catch/throw 以外的 clauses 全部解決掉再睡應該也不遲 XD。    [2010-08-01 22:55:47 +0800]
    • Josh Ko ⇒ 解決了！    [2010-08-01 23:23:51 +0800]
    • Josh Ko ⇒ 可是明天不想跟 scm 老師 meeting 呀，會中腸病毒⋯    [2010-08-01 23:27:40 +0800]
  7. catch 也做掉了，剩下 throw 的四個子句。    [2010-08-02 10:25:57 +0800]
  8. 餓了，可是現在出去吃又稍嫌太早⋯    [2010-08-02 11:11:06 +0800]   [ 1 人說讚！]
  9. throw 果然恐怖⋯ type 轉來轉去頭都昏啦。    [2010-08-02 14:51:07 +0800]
  10. 我真的在昏了，定理的前提結論都亂寫一通⋯    [2010-08-02 15:22:54 +0800]
  11. 2 down, 2 to go. 可是已經恍神了⋯    [2010-08-02 15:34:28 +0800]
    • S************ ⇒ Take a break!    [2010-08-02 15:38:10 +0800]
    • Josh Ko ⇒ 去人文大道上晃了一下，應該可以繼續啦 XD。    [2010-08-02 16:00:45 +0800]
    • S************ ⇒ (還是很不習慣我們院裡的路開始有名字）    [2010-08-02 17:17:52 +0800]
  12. 今天投降⋯    [2010-08-02 16:57:54 +0800]
  13. 現在對 abs function 做 typecheck 都要好久，就算獨立成一個檔案也快不了多少。等 typechecker 的時候就只好來上上網啦 XD。    [2010-08-03 09:17:34 +0800]
  14. 一個 type 有 1,100 characters，facebook 都貼不下啦。早知道就不要把 module 取名為 EvenMoreHeavilyIndexedSyntaxRevisited...    [2010-08-03 09:31:13 +0800]   [ 1 人說讚！]
    • L************** ⇒ Agda 現在還是不支援 overloading 啊?    [2010-08-03 09:59:28 +0800]
    • Josh Ko ⇒ 好像還是只有 constructors 有吧⋯    [2010-08-03 10:02:53 +0800]
    • L************** ⇒ module 跟 function 也有的話就好玩了 ...     [2010-08-03 10:05:30 +0800]
  15. 自暴自棄開始寫這種 code: subst (λ Δ₀ → ∞ (IOπᴰ A Γ Δ₀ Δ')) (trans (remove-ν'c c m (proceed₁ c) (channel₁Type c , m) (≡ℓ++ (proceed₁-preserves-length c) (channel₁Type c , m) (channel₁Type c , m))) (remove-Δ (ν'c c m) (≡ℓ++ (proceed₁-preserves-length c) (channel₁Type c , m) (channel₁Type c , m)) (proceed₁-preserves-length (c ↗₁ (channel₁Type c , m))) (proceed₁++≡proceed₁↗ c (channel₁Type c , m)))) p    [2010-08-03 10:38:38 +0800]
    • Josh Ko ⇒ 好消息是 facebook 貼得下這段 code XD。    [2010-08-03 10:38:57 +0800]
    • 陳** ⇒ 這...比perl還要write only吧？orz    [2010-08-03 14:18:01 +0800]
    • S************ ⇒ 開始猛用 subst 和 trans 了..    [2010-08-03 19:47:28 +0800]
  16. Yeah! 1 to go!    [2010-08-03 10:50:11 +0800]
  17. 難得聽到 MBP 的風扇聲⋯    [2010-08-03 11:09:22 +0800]
  18. Only one sub-clause left!    [2010-08-03 11:23:45 +0800]
  19. 全部寫完了，不過現在 typechecker 已經努力跑好久了還不停⋯    [2010-08-03 11:46:36 +0800]
  20. 看來上次 postulate swap 之後 hang 並不是獨立事件⋯    [2010-08-03 11:49:00 +0800]
  21. 吃完飯還沒過 typecheck...    [2010-08-03 12:21:11 +0800]
  22. 難道我真的寫出讓 typechecker 跑不停的程式？    [2010-08-03 12:38:59 +0800]
  23. 從萊爾富出來有人問路，幸好問的剛好是物理所 XD。    [2010-08-04 09:08:48 +0800]
  24. 「寫 Srv S 不能 typecheck」的神祕問題原來是我忘了把 Term 的 module parameter M 拿掉的關係⋯    [2010-08-04 11:59:27 +0800]
  25. decidable term 不會 reduce，應該是 decision procedure 寫不好（吧）。    [2010-08-04 14:17:04 +0800]
    • Josh Ko ⇒ 真的是！    [2010-08-04 14:42:33 +0800]
  26. MAlonzo compiler 不吃 --allow-unsolved-metas 選項，就宣告編譯不出來啦。雖然懷疑可能是 abs 寫得不好讓 typechecker loop，可是加個 dummy hole 在那裡卻又可以 check 實在很奇怪。是檢查完沒有 unsolved metas 之後還有動作，而那個動作遇到不好的定義時會 loop？    [2010-08-04 16:54:56 +0800]
  27. 突然發現 Kindle DX 用 200% 大小看 two-column paper 時，在左欄按「往左」會直接跑到正確的右欄位置，不用往右移 1⅓ 格，方便不少。    [2010-08-04 17:55:02 +0800]   [ 1 人說讚！]
  28. 到天瓏，C++ Primer 4/e 中文版還排在第八名，JavaPL 4/e 中文版則停留在一刷（as expected）。    [2010-08-04 22:08:45 +0800]   [ 1 人說讚！]
  29. 算了一下，工作天好像只剩下 15 天左右⋯?!    [2010-08-04 23:22:06 +0800]
    • Josh Ko ⇒ 意思是和 scm 老師有重疊的天數。    [2010-08-04 23:22:59 +0800]
    • F************ ⇒ 只剩15天就要離開了!?    [2010-08-04 23:25:06 +0800]
    • Josh Ko ⇒ 八月下旬我出國，九月上旬他出國⋯ XD    [2010-08-04 23:27:27 +0800]
    • F************ ⇒ 所以八月只剩中旬能出去了!?    [2010-08-04 23:28:23 +0800]
    • Josh Ko ⇒ 不能再出去啦！要趕進度⋯    [2010-08-04 23:29:00 +0800]
    • F************ ⇒ 囧....加油.....    [2010-08-04 23:29:22 +0800]
  30. 把 {-# OPTIONS --no-termination-check #-} 拿掉，typechecker 就不會 hang 了！（But no idea why...）    [2010-08-05 11:55:24 +0800]
    • Josh Ko ⇒ 而且這樣還是不能編譯呀⋯    [2010-08-05 12:38:40 +0800]
    • L*********** ⇒ because termination check won't terminate?    [2010-08-05 14:14:08 +0800]
    • Josh Ko ⇒ 可是加上這個 option 應該是不跑 termination check 才對呀⋯    [2010-08-05 14:16:41 +0800]
  31. 新護照拿回來了。    [2010-08-05 20:49:29 +0800]   [ 3 人說讚！]
    • Josh Ko ⇒ 剛變成舊護照的那本裡面裝的剛好是我所有的英國簽證，不多也不少。    [2010-08-05 20:54:39 +0800]
  32. 今天下午寫 Haskell。寫完特別兇猛的 Agda program 之後就覺得 Haskell 怎麼寫都對呀 XD。    [2010-08-05 21:09:47 +0800]   [ 4 人說讚！]
  33. Julie 寄來 "introductory week" 的時間表，裡面有 "emergency first aid course"。欸，call-call-A-B-C?    [2010-08-05 22:21:50 +0800]
    • S************ ⇒ 會教你怎麼作 CPR 唷～    [2010-08-05 23:31:19 +0800]
    • Y********** ⇒ 也是去虐待安尼嗎? :p    [2010-08-06 07:45:56 +0800]
  34. 七部公車擠在中研院站牌旁邊⋯    [2010-08-06 09:04:16 +0800]
  35. JSON 的發音不是應該是「就送」（台語）嗎？    [2010-08-06 13:17:49 +0800]   [ 1 人說讚！]
  36. 總覺得 EvenMoreHeavilyIndexedSyntaxRevisited 還有起死回生的機會⋯    [2010-08-06 14:37:37 +0800]
    • Josh Ko ⇒ 好像又沒了 XD。    [2010-08-06 14:45:36 +0800]
    • S************ ⇒ 你比較喜歡 EvenMoreHeavilyIndexedSyntaxRevisited, 是嗎？    [2010-08-06 21:08:53 +0800]
    • Josh Ko ⇒ 一來寫得那麼辛苦竟然不能跑真是太傷心了，二來還是覺得「沒有定義出多餘的 terms」和「寫 terms 時 typing 一併到位」似乎比較好。雖然還沒有怎麼寫到 typeless terms 的 typing rules，也覺得現況而言分開寫的組合性應該會比較好（比方說換個 type system），但如果可以組合地定義出 heavily indexed datatypes 就太完美啦 — which happens to be my thesis topic, ya!!    [2010-08-06 21:20:40 +0800]
    • S************ ⇒ BTW, 我覺得只需要做 IOπ S A 0 xs 的 typing 就可以了。碰到 bound variable 都用 [_↦_] 變成 free variable.    [2010-08-06 22:24:00 +0800]
    • S************ ⇒ [_↦_] 的 argument x∉¿xs 用 False 可能沒什麼意義 .. 我本來以為可以自動推，不過似乎不行。    [2010-08-06 22:39:36 +0800]
  37. 突然發現如果維持隔週 meeting，今天是我最後一次耶。（下一次是 Coq summer school 第一天，再下一次 scm 老師去英國，再下一次我就離職了。）    [2010-08-06 16:06:49 +0800]   [ 1 人說讚！]
    • J******************* ⇒ 在你離開前我也開始學會用fb來記工作上的事了 噗    [2010-08-06 16:18:59 +0800]
    • L************** ⇒ scm 老師一直很難遇到 Q_Q    [2010-08-06 17:40:31 +0800]
    • S************ ⇒ 那我們多 meeting 一次好了...    [2010-08-06 21:07:15 +0800]

--
用 Network.Curl 和 offline_access 並記錄上次擷取的日期，把下載也自動化了！

Labels:

posted by Josh Ko @ 5:37 am   0 項意見