[temp] 一堆還沒看的網頁

[agda 教學]
http://www.cs.nott.ac.uk/~txa/g53cfr/
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Modules
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records

[types in agda]

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.SimpleInductiveTypes

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ParameterizedInductiveTypes

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.UniversePolymorphism

[category]
http://www.haskell.org/haskellwiki/Category_theory
http://en.wikibooks.org/wiki/Haskell/Category_theory

[monad]
http://www.haskell.org/haskellwiki/Category_theory/Monads
http://en.wikibooks.org/wiki/Haskell/Understanding_monads

[monad transformer]
http://en.wikibooks.org/wiki/Haskell/Monad_transformers
http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Monad_transformers/
http://www.randomhacks.net/articles/2007/03/05/three-things-i-dont-understand-about-monads
https://github.com/copumpkin/categories/

[Agda] Instance Arguments

出來跑，遲早都要還的... XD

最近在試著使用 agda 裡面的 record，尤其是用來模擬 haskell 中的 type class。不過，用起來一直怪怪的，到處都綁手綁腳的。剛好前兩天看到 josh 的文章，裡面提到今年的 ICFP 有人在弄 type classes in agda。哪裡還有客氣的，趕快去找來看 XD。

大概看過去，看起來相當不錯的感覺，不過就是他沒有寫清楚實作上的細節。稍微查了一下發現 agda 號稱 2.2.12 就會有開始提供這個東西：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments
也有講到如何用 instance argument 來做 type class：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments

不過不過，現在 stable agda 才 2.2.10；development version 也才不過 2.2.11！看來只好慢慢等了。

另外，agda 的 instance arguments 畢竟還是和 haskell 裡面的 type class 不一樣。type class 基本上會自動遞迴地去試圖找出一個 instance，但是 instance argument 設計上限制我們必須要真的給它一個 instance。老實說，這邊目前還不是了解，看看以後能不能多懂一點。附上參考資料：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Non-recursiveResolutionForInstanceArguments

[Notes] Semantics, Category and their Implementation 1

此篇為彼篇之後續...

主要涵蓋了 denotational semantics 以及 fixed point iteration。

[Notes] Domain and Fixed Point

此篇大量參考 FLOLAC 08' 的 Denotational Semantics 講義。

A poset(partially ordered set) is a set D with a binary relation ⊑ s.t. the following properties hold:

1. reflexive: x ⊑ x 
2. anti-symmetric: x ⊑ y and y ⊑ x -> x ≡ y 
3. transitive: x ⊑ y and y ⊑ z -> x ⊑ z 

For a poset D, a set X ⊆ D is directed if:

1. X ≠ { } 
2. ∀ x,y ∈ X, ∃ z ∈ X s.t. x ⊑ z and y ⊑ z 

For a poset D, D is a cpo(complete partial order) if:

1. ∃ ⊥ ∈ D s.t. ∀ x ∈ X, ⊥ ⊑ x
2. Every directed set X ⊆ D has a least upper bound denoted as ⨆X

A cpo D is called domain as well.

---

Let D be a poset with ⊑ and f be a total function from D to D.

• x ∈ D is a fixed point of f iff f x = x
• x ∈ D is a least fixed point of f iff x is a fixed point of f and for every fixed point y of f, x ⊑ y.

**The Least Fixed Point Theorem**

Let D be a domain.

• ∀ f : D -> D, ∃ a least fixed point 
• ∃ fix : (D -> D) -> D, s.t. ∀ f : D -> D, fix f is the least fixed point of f.

For a function f : (D -> D), we can define a directed set Xf ⊆ D by

• Xf = {⊥,f ⊥,ff ⊥,fff ⊥,...}.

By the continuity of f,

f ⨆Xf
= f ⨆{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆f{Xf}
= ⨆f{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆Xf.

Thus, for any function f : D -> D, there exist a fixed point ⨆Xf of f. For least, we can support x is a fixed point as well. Then

⊥ ⊑ x,
f ⊥ ⊑ f x,
ff ⊥ ⊑ ff x,
...
fn ⊥ ⊑ fn x, (we write fn for applying f n times)
...

Because x is a fixed point of f, fd x will be x obviously. Collecting both sides as set we will obtain

{⊥,f ⊥,ff ⊥,fff ⊥,...} and {x},

then taking least upper bound of both set, 

⨆Xf ⊑ x

Thus, for any function f : D -> D, there exist a least fixed point ⨆Xf of f. Finally, we can define fix by 

fix f = ⨆Xf

for any function f : D -> D.

---

Relevance to (denotational) semantics:

The semantics of program g is a function g. For example, a program can be defined as follow:

g args = h (g args') : A -> B

This is not a simple case that we can find a corresponding g easily. However we can define another program/function f/f that can help us to define g. For example, we define

f : (A -> B) -> (A -> B),
f g = \args -> h (g args') = g.

Obviously, g is the least fixed point of f and the ⨆Xf as well. In this case, the domain D = (A -> B).

[Book] Logicomix

日前在 PL11 上面聽到這本 LOGICOMIX。覺得似乎蠻有趣的，也有點厭倦從硬梆梆的角度去看邏輯和數學，所以就找了一下資料想去弄一本來看。猶豫了一陣子以後，還是決定不要虐待自己，買中文版來看就好了。

整本書有三條線：
1. 編輯會議(?)
2. 羅素的演講
3. 羅素演講中的黑頁

用這三條故事線去描述了二戰之前羅素的回顧、二戰當時羅素的想法和二戰之後的人的看法。故事說得蠻精彩的，不過我覺得1.的篇幅太多了，而且相對於其他兩條線而且，沒什麼特別的東西值得提起。2.很精彩的描述了羅素這個人的價值觀，而3.則演繹了他的一生和成就，而且是以第一人稱在進行。

這不免會忽略一些對於主角的糟糕性格的批判：剛好我前兩天「是邏輯，還是鬼扯？」的系列總序中看到有關偉大哲學家(蘇格拉底)對於家庭的失格。一個「偉大」的哲學家是怎麼對於家庭的不負責任而寡情。剛好最近自己也在想類似這些的事情，「成就」究竟是怎麼定義出來的呢？錢？名？崇高的自我滿足？完成其他人所不能？現在我看到一個「偉大」的成就和人物的時候，心裡都難免會為其背後真正付出犧牲的人所嘆息。如果你/妳是一個「準偉人」的家人，你/妳會願意他/她去偉大還是平凡？

這問題或許可以上綱到「人究竟要遵循理性或人性？」完全人性其實應該就是另一種獸性、完全理性就又無異於機械。也許人生就是在這樣的兩種思維中拉鋸吧。所以應該來研究人是怎麼選擇的才對？好吧，這就等我看完下一本書再說吧。

回到主題，整個故事我覺得與其實在說邏輯和數學的歷史，我覺得我會把這本書的內容定位在「羅素對於自我和真理的探索之旅」。覺得看到的不是「數學邏輯的奇幻之旅」，裡面的那些定理那些數學都不重要，重要的應該是那個過程那個思維那個人生。因此，再一次，我覺得1.的部份實在是有些雞肋。

---

收藏指南：
相對於原裝的厚重雪桐(還是特桐?)的豐富質感
翻譯版的紙磅數太低，所以合理推測他的彩度也不高

翻譯的人對於少數專業詞彙的翻譯沒有很到位
有部份那種模擬兩可的翻譯還可以接受
但是「套套邏輯」的廣泛使用這點我實在是難以忍受

不過，就閱讀而言，翻得品質其實相當不差，看起來很通順
但是我就是覺得那些過於方正嚴肅的中文字體實在很礙眼

Shortcuts do not work

一直以來，我的OS X一直都被一個問題困擾。那就是「與 F1~F1x 有關的 shortcuts」都不理人。只有原本預設的特殊功能可以用。換句話說，我的 F3 按下去就等價於 Show All Windows。不過這就有個問題，沒有 show desktop 可以用。但是我很常用這個功能。 所以我就都去打開 system preference 裡面關於 Expose 的那三個 shortcuts：
F9 -> All Windows
F10 -> Application Windows
F11 -> Desktop

其實一開始 mac 剛灌好的時候，上述這些 special function 和 shortcuts 也確實都是預設使用的。不過問題就出在，原因不明地，dock 有時候會出現點問題，所以 F1~13 都會壞掉不能用。長年以來都是用滑鼠或是其他按鍵組合去取代，可是最近因為換鍵盤，所以變的非常不便利。也因此花了一些時間去找/試怎麼修復。最後還是 google 到人家的作法：殺掉整個關於 Dock 的 process，讓它重開並重設。

> killall Dock

[note] Pygments, a review

因為被抱怨說看以前我那篇 [reStructuredText] Pygments Intro. & Install 東西還是跑不出來，所以就重裝一下順便看看現在有啥搞頭。

總之，我現在沒有在用 macport，而 homebrew 中沒有 pygments 可以裝。所以稍微奮鬥了一下看能不能暴力裝進 /usr/local/cell/pygments/1.4/ 裡面去。最後發現說，pygments 被當作 python 的一個 package，而硬是給我裝到 /Library/Python/2.6/site-packages 裡面去。好吧，既然 cabal 下面灌的 agda 我沒做 brew link，這個我看也算了。一方面是懶惰，另一方面是想說趕快看是為什麼不能用。

前言結束

---

補充一點

首先，為了避免有人和我說沒有 twilight 可以用，先扯一下 style 的事情：
請在 /Library/Python/2.6/site-packages/Pygments-1.4-py2.6.egg/pygments/styles/ 下面開一個檔案叫做 twilight.py。然後把這篇裡面最下面的那一塊 twilight.py 的內容複製並且貼進去自己的 twilight.py 檔案中。

---

正文開始

基本上和以前沒差多少嘛，到底是哪哩不能用 T▽T

> pygmentize -f html -o out.html -O full,style=twilight,linenos=1 p.hs
-f html ≡ 指定輸出格式為 html [1]
-o out.html ≡ 指定輸出檔名
-O ≡ lexer 和 formatter 額外的設定
full ≡ 產生完整的 HTML 4 檔案
style=twilight ≡ 指定 style [2]
linenos=1 ≡ 開啟line number
p.hs ≡ 輸入的檔名

PS.
每個 formatter 可以用的參數不一樣
可以翻翻 formatter 的 source code
禮面會有寫，而且寫的蠻清楚的 [1]

不過上述的方法對於想要把 style 和 code 分開來的用的人來說，比較麻煩一點。因為變成要手動去把 html 中無關 code layout 的部份刪掉。因此就可以利用下面這種方式來輸出：

> pygmentize -f html -o skeleton.html p.hs
然後用 browser 打開 skeleton.html 以後會發現是黑白的。
而且用 editor 打開的話會發現他根本只有
換句話說這只是一個 html 的"片段"

所以我們可以用
> pygmentize -f html -S twilight > style.css
來取得名為twilight的style的css檔

然後打開之前輸出的 skeleton.html
補上 html, head, body 和 css 的 link
這樣就可以看見顏色了
(不過看不到 background color)

---

[1]
關於可以輸出的格式還有相對應的參數可以去這裡看看有哪些東西
/Library/Python/2.6/site-packages/Pygments-1.4-
py2.6.egg/pygments/formatters
[2]
關於可以 style 可以去這裡看看有哪些東西
/Library/Python/2.6/site-packages/Pygments-1.4-
py2.6.egg/pygments/styles

[Note] about reduction and normal form

[Redex]

我們知道，可以繼續簡化的 term 叫做 redex (reducible expression, reducible subterm)。
例如說

(λx.x+1) 10
(λxλy.x*y) 1
square (square 5)
1+4*5

[Reduction Strategies]

對一個 redex 我們可以優先從最裡面(innermost)或是最外面(outermost)來做拆解。兩種不同的方式即稱為 innermost reduction 和 outmost reduction。另一種解釋是： innermost reduction 會一直挑 innermost redex (不包含任何 redex 的 redex )來簡化，而outermost reduction 則相對會一直去選 outermost redex (不被任何 redex 包含的 redex)來簡化。

fst (square 10, root 100) -- outermost reduction
=> square 10
=> 100

fst (square 10, root 100) -- innermost reduction
=> fst (100, root 100)
=> fst (100, 10)
=> 100

[Non-strict and Lazy]

Non-strict reduction(evaluation) 是指只有在出現必須簡化(運算)的情況才去簡化(運算)。non-strict 是一種抽象的性質，實際上存在有若干種不同的實作方式：

<1> Normal order reduction
即是 outermost + leftmost。

(λx.x (λy.id y)) (λzw.fst (z,w))
=> (λzw.fst (z,w)) (λy.id y))
=> (λw.fst ((λy.id y),w))
=> (λy.id y)
=> (λy.y)

<2> call-by-name
基本上 call by name 關鍵的概念在於將 arguments 直接貼入 function body 而沒有任何先行運算這件事情上。(相對於 call by value 會先算好 arguments 再放到 function 中) 也就是說 call by name 是將 arguments 以 capture-avoiding substitution 的方式直接貼進 function body，等到非要算不可才去開始計算那些 copies。這些 argument 的 copies 被稱為 thunk，一個"尚未被運算的值加上如何運算它的描述"。

(λx.x (λy.id y)) (λzλw.fst (z,w))
=> (λzλw.fst (z,w)) (λy.id y))
=> (λw.fst ((λy.id y),w))

不過 call by name 也有個缺點：如果 argument 被用到不只一次，就會因為同一個 argument 被貼了很多份 thunks，所以變成要重複計算這些 thunks 的值。也因此，以這種方式做出來的 non-strict evaluation 在效率上會比較慢一些。

P.S.
從 evaluation 的角度來看，normal order 和 call by name 之間的一個差別在於：normal order 比 call by name 還要貪心一點：call by name 如果碰上一個 λ-abstraction (尚未拿到 arguments 的 function) 就不會去 reduce。但是 normal order 還是會試圖多做幾步。

(λfλg.f g) (λx.id x) (λx.x+2*3-5)
=> (λx.id x) (λx.x+2*3-5)
=> id (λx.x+2*3-5)
=> (λx.x+2*3-5) -- call by name will stop here! and, view this term as a normal form (..weak head normal form?)
=> (λx.x+1) -- only normal order will achieve here! this is a "real" normal form

所以另外有種說法是說：call by name 是 "normal order" + "停在 λ-abstraction 時"。

<3> call-by-need
是 call-by-name 的變體：原本 call-by-name 中 arguments 的 re-evaluation 不會發生。也就是說，所有會用到的 arguments 都只有第一次被使用的時候會被算一次。也因此 reduction 不是以 tree 的方式在進行，而是以 (directed) graph 的方式在處理。

call-by-need 即是一般所謂的 lazy evaluation。也就是說 lazy 是 non-strict 的一個實作。

[Normal Form]

而一個 term 如果不包含任何 redex，則被稱為 normal form。換句話說， normal form 就是一個無法再套用任何 reduction rule 來簡化的 term。

(λx.x+1) 10 => 10+1 => 11
(λxλy.x*y) 1 => λy.1*y
square (square 5) => square 25 => 625
1+4*5 => 1+20 => 21

[β-Reduction/Redex/NF]

在 λ-caululus 中我們用 β-reduction 來描述 application 的概念，也就是說，我們用

(λx.t) u =β t[u/x]

來描述「將 t 中出現的 x 都以 u 來取代」。

而，一個可以套用 β-eduction 的 redex 稱為 β-redex。換個說法就是：一個具有

(λx.t) u

這種長相的 term。

如果一個 term 不能再做任何的 β-reduction，則稱為 β-normal form。

[η-Conversion/Redex/NF]

Extensionality (extensional equality) - 如果兩個 function 對所有相同 input 都會產出一樣的 result。而在 λ-caululus 中我們用 η-conversion 來描述這個性質如下

(λx.t) x =η t , if x ∉ FV(t)

與 β-reduction 同樣地, 也有 η-redex 以及 η-normal form 的存在。更甚者，還有 βη-reduction 以及 βη-normal form 等等。

[Head Normal Form]

如果在一個 term 的最外層既不是 redex 也不是一個 reducible λ-abstraction，則此 term 被稱為一個 head normal form。換句話說，一個 head normal form 的 top-level 必定是

• 變數 (variable)
• 數值 (data value)
• 參數不足的內建函數 (build-in function applied to too few arguments)
• 不可簡化的 λ 函數 (lambda abstraction whose body is not reducible)

例如說

• x
• 11
• zipWith (*)
• (λxλy.x+y) (10)
• (λxλy.x+y) (length [1..10]) -- HNF 中的 argument 可以是 redex, 但是 normal form 不行
• (λx.id x) (λy.sum y) -- Not a HNF, because (λx.id x) could be reduced to (λx.x)

[Weak Head Normal Form]

weak head normal form 是 head normal form 或者 top-level 處是任何的 λ-abstraction。換個說法，weak head normal form 就是「把對 λ-abstraction 的限制拔掉的 head normal form」。

• (λxλy.x+y) (length [1..10])
• (λx.id x) (λy.sum y) -- in WHNF but not HNF

[Normalization Properties]

若一個 rewriting system 中所有 term 不管經由哪種 sequence of rewrites 都會產生出 normal form，則該系統被認為具有 strong normalization property。相對地，如果所有的 term 至少存在有一個 sequence of rewrites 可以產生出 normal form，則稱為 weak normalization property。例如

fst (square 10, length [1..])
=> square 10
=> 100

和

fst (square 10, length [1..])
=> fst (100, length [1..])
=> fst (100, 1+length [2..])
=> fst (100, 1+1+length [3..])
=> ...

只有第一種 reduction 會產生出 normal form，第二種則不會。所以這個 system 一定只具有 weak normalization property。

有趣的是，pure untyped λ-calculus 既沒有 strong 也沒有 weak normalization property。因為在 pure untyped λ-calculus 裡面我們可以寫出類似

(λx.xx)(λx.xx)

這樣的 term。而這種 term 不會 terminates，所以不會存在一個 normal form。
但是某些 typed λ-calculus 就具有 strong normalization property，例如說 simply typed λ-calculus 和 System F。換句話說這些 system 保證上面所有寫出來的 term 都會 terminates。

-- 後記 --
這篇前前後後斷斷續續寫了應該快三天吧
期間一直被事情打斷
不然就是因為一堆名詞問題卡住
然後開始無限翻書地獄
終於大概寫完了
還不知道有多少混淆和錯誤呢

[mac] The "gettext"

Mac OS X provide a BSD-gettext. When I build some software needed GNU-gettext, however, I will need to install a GNU-gettext by, for example, homebrew. But, because system gets confused if both are in the library path, the homebrew will NOT symlink GNU-gettext to /usr/local .

Due to the reason showed above, I have to add path by myself when I build some software by myself. e.g.

LDFLAGS="$LDFLAGS /usr/local/Cellar/gettext/0.18.1.1/lib"
CPPFLAGS="$CPPFLAGS /usr/local/Cellar/gettext/0.18.1.1/include"

[gtk2hs] re+install !

早上6:30就爬起來弄 XD

不知道是第幾次弄 gtk+
但是記得應該是第四次很認真的弄 gtk2hs

很久以前 gtk+ 就可以裝好了
不過我記得這邊還是會有點小問題
會需要自己去稍事調整, 例如說,
我記得我手動 brew install gdk-pixbuf 過
然後卡過 32/64 bit 的問題
也卡過 ghc 6.12 不相容的問題
不過這次隨著 ghc 7 的更新
似乎就兜起來了沒有問題

依序安裝 gtk+, ghc(x86_64) 和 haskell-platform

> brew install gtk+
> brew install ghc --64bit
> brew install haskell-platform

因為 ghc 改用 64bit 版
所以 haskell-platform 會需要 re-build
因此整體過程會比較花時間一點
需要多一點耐心 (不過完全比不上當年手動 build ghc 6.10 來的痛苦 XD)

接著參考上篇把 cabal 舊有東西清掉

接著就開始灌全套 gtk2hs

> cabal install gtk2hs-buildtools
> cabal install gtk

至此, 隨便去找個 gtk2hs 的 example 來跑就知道會不會 work
不過, 額外有一件事就是
我之前為了某個被我遺忘的原因而裝了 XQuartz
好像是因為原本 glib 還是 什麼 lib 之類的某些東西有問題
所以裝了XQuartz
是說 XQuartz 似乎真的比較好(完整)
但是因為它是 .pkg 所以這真的是有點囧
我現在沒辦法讓 gtk2hs 出來的程式用原本的 X11.app 去開
是說用 XQuartz 直接跑也沒有不好(似乎這樣才好?)
不過, 感覺如果拿到別的mac上去就葛屁了...

---

時代真的日新月異
以前這些都麻煩到翻天
每件事情都要自己手動去苦幹實幹
幹不下去了就只好投降
現在這些府住的東西真的越來越發達了
雖然說問題還是很多啦
例如說我一直可以看到 cabal install 時會顯示：
「warning: #warning Setup.hs is guessing the version of Cabal.」
這樣的警告訊息, 或是看到一些警語說「ooxx is experimental!」
這真的看了很抖呀...
感覺哪天會在哪裡突然出包然後解決不了..

[ghc] Upgrade to 7.0.3 !!

upgrade my ghc into 7.0.3 via homebrew.

1. updating homebrew
> brew update

2. upgrade all package you installed
> brew upgrade
or, install lastest ghc only
> brew install ghc
> brew cleanup ghc

3.
kill cabal .. XD
> cd ~/.cabal
> rm -R *
> cd ~/.ghc
> rm -R <path>
path is, for example, i386-darwin-7.0.3

restart cabal by
> cabal update

now, you could install any lastest package you want. XD
> cabal install <any package you want>

---

There was a weird problem when I want to install the bindings to the LLVM compiler toolkit. I got a error message about pattern matching:

..skipped..
/var/folders/KU/KUdrsAaeFWOIeZoa4Zhsqk+++TI/-Tmp-/llvm-0.9.0.145987/llvm-0.9.0.1/Setup.hs:102:70:
Couldn't match expected type `[PackageDB]'
with actual type `PackageDB'

Well, this problem is due to the error of source code...
so, the thing to do for salving it is to modify that code.

> cabal unpack llvm
> cd ~/.cabal/packages/hackage.haskell.org/llvm-<version>
for example my llvm source code is
~/.cabal/packages/hackage.haskell.org/llvm-0.9.0.1

and then, open Setup.hs with any editor, and replace packageDb by [packageDb] on the line#102 .

now, you must config, build and install by yourself:
> cabal config
> cabal build
> cabal copy

PS, if you cannot config this package
plz google for more info.
there is a big problem about 32/64-bit ghc and/or llvm...
(seems could be solved by rebuild ghc/llvm)

[android] Install and HelloAndroid Step by Step

[3-1] Selecting packages to install

1. install via homebrew
> brew install android-sdk

2. initialization about Android SDK and AVD.
> android

3. setup the SDK and AVD management.

3-1. switch to "Available" page to select packages you want to install, click button:"install selected"

3-2. switch to "Installed" page to update packages by click button:"Update All..."

[3-2] Updating packages

[3-3] "Virtual devices" page

[3-3] new AVD window

3-3. To create a new AVD(Android Virtual Devices): switching to "Virtual Devices" page and clicking button:"new".
(Picture - [3-3] "Virtual devices" page)

On the popped window, we could decide what properties of AVD we want. Select your target carefully, and, remember which target version you select.
(Picture - [3-3] new AVD window)

After clicking button:"Create AVD", this AVD will be showed on the AVD list. now, select a AVD you want to run and click button:"start". There will pop a "Launch Option" window, you could just clicking the button:"Launch".
(Picture - [3-3] "Virtual devices" page)

4. After Init. of Android opening, you could see a nice look.

[4] AVD with waiting for turn-on

[4] readied screen

5. Create hello world project via native example.
Do NOT close the AVD. switch to console:
> android create project --package com.example.helloandroid --activity HelloAndroid --target target id --path project-path

Hint: the target id have to be matched with the AVD that we are running. To query the id of target:
> android list targets

for example, the target name of my AVD is Android 2.2, and, in the result of query, I could find out that "id: 4" matches what I need.

...skipped..
id: 4 or "android-8"
Name: Android 2.2
Type: Platform
API level: 8
Revision: 2
Skins: HVGA, QVGA, WQVGA400, WQVGA432, WVGA800 (default), WVGA854
...skipped..

now, my creating command will be
> android create project --package com.example.helloandroid --activity HelloAndroid --target 4 --path ~/haha

6. compiling and installing
> cd where-your-project-is
> ant install
wait a few seconds, you should see something like

...skipped...
BUILD SUCCESSFUL
Total time: 9 seconds

7. switch to AVD, you will find out the HelloAndroid app:

---

竟然寫了兩個小時.. 囧>
godfat大大, 夠詳細了..吧？ XD

[xkcd]Duty Calls

"What do you want me to do? LEAVE? Then they'll keep being wrong!"

[xkcd]Pointer

Every computer, at the unreachable memory address 0x-1, stores a secret.

I found it, and it is that all humans ar-- SEGMENTATION FAULT.

[xkcd]Compiling

"Are you stealing those LCDs?"
"Yeah, but I'm doing it while my code compiles."

[xkcd]Sandwich

以後決定把看到有趣的xkcd放在這邊 XD

"Proper User Policy apparently means Simon Says."

[Exer] Gray Code in Unfoldr

有點難記
寫在blogger方便記憶好了

seed :: pair of integer
fst seed = decimal number
snd seed = length of gray code

graycode = unfoldr g p
p = (==0) ◦ snd
g = (div ◦ (id × (2^) ◦ (-1)) × (flip (-) ◦ ((+1) × (2^)) × (-1) ◦ snd) ◦ dup) ◦ dup

dup x = (x,x)

實在是長到有點令人厭煩XD
接下來是 unfoldl