日々の流転

λ. 頭が冴えて眠れなくて、結局徹夜してしまった。朝食をとってからもう一回温泉に入って、それから旅館を後に。

λ. Re: functor category とデータ型

眠れなかったので、つまらないことでも考えてみた。

「data GRose f a = GBranch a (f (GRose f a))」というデータ型に対して「∀f g a b. (∀x. f x -> g x) -> (a -> b) -> (GRose f a -> GRose g b」という型のmap関数を定義するには、

type Hom{[  *   ]} a b = a -> b
type Hom{[ k->l ]} f g = ∀x. Hom{[l]} (f x) (g x)
map{| k->l |} t :: ∀a b. (Hom{[k]} a b) -> (Hom{[l]} (t a) (t b))

という型を考えれば良いと思ったのだけど、これだと「map{| (*->*)->*->* |} GRose :: ∀f g. (∀x. f x -> g x) -> (∀x. GRose f x -> GRose g x)」となってしまう。型構築子がカリー化されていることの当然の帰結でこれはこれで正しいのだけど、こんな型の関数があってもあまり役にはたちそうにない。最初の関数の型を得るには、

type Hom{[  *   ]} a b = a -> b
type Hom{[ k->l ]} f g = ∀x. Map{[l]} (f x) (g x)
type Map{[  *   ]} a b = Hom{[*]} a b
type Map{[ k->l ]} f g = ∀a b. (Hom{[k]} a b) -> (Map{[l]} (f a) (g b))
map{| k->l |} t :: Map{[k->l]} t t

とすれば良さそうな気がするけど、なんつーか、びみょー。

λ. 十国峠

「十国峠大声大会 - 富士山に吠えろ」というバカっぽい催しをやってて面白かった。ちなみに今年は第二回で、前回の優勝者は115ホンだったとか……

λ. SICPは、しくぷ? しっくぴー?

わたしも「えすあいしーぴー」と読んでましたが、うちの研究室には「しすぷ」と読んでる人もいました。

λ. ゼロ金利

今日の毎日新聞朝刊の、玉置和宏氏の「酸いも辛いも - 「最後の貸手」の麻薬」という論説によると、日銀のゼロ金利政策は「国債金利が急上昇したため政府の圧力で一時的に金利をゼロにした」ものだそうですよ(笑)

λ. 借りた本

『イリヤの空、UFOの夏　その1』

秋山 瑞人 [著] 駒都 えーじ[イラスト]

『虹の解体—いかにして科学は驚異への扉を開いたか』(UNWEAVING THE RAINBOW - Science, Delusion and the Appetite for Wonder)

リチャード・ドーキンス(Richard Dawkins) [著], 福岡 伸一 [訳]

『奇跡を信じて』

ニコラス・スパークス(Nicholas Sparks) [著], 天馬 龍行 [訳]

『文学部唯野教授』

筒井 康隆 [著]

『D - 双影の騎士 2』

菊地 秀行 [著]

λ. ハンニバル

論議をよんだあのシーンを楽しみにしてたのだけど、やっぱカットされちゃったのね。きたさんによると昨日の編集は最悪編集らしいし、やっぱ原作を読もうかあなぁ。