日々の流転

λ. 夜型生活中。

λ. 数学得意?

あんまし数学得意じゃないというのは言い過ぎだったけど、少なくともそれほど得意なわけではないです。(ってか、もしそんなに数学得意だったら「総合政策学部」じゃなくて「理工学部」とかに進んでましたよー)

一応大学で一年間勉強したし、数学の先生とも割と話す機会があるので、表面的な知識はそれなりにあるけど、「数学が得意」というのはそういった表面的な知識の問題ではなくて、抽象的な対象に対する思考力/洞察力とでも言うべきものだと思う。僕はそういう点で僕はまだ非常に底が浅い(はず)。

なので、「12を2πで割るだけじゃん。なぜして、めんどくさい考え方をするのだろか」と即座に気づけるZOEさんのセンスは結構羨ましいのですよー

λ. bit別冊CLOS特集号

「一方artonさんにはbit別冊CLOS特集号を借りる。CLOS萌えるねー！」というのを見て、読んでみようかと思ったのだけど、[ruby-list:12525]によれば1989年1月のbit別冊のようだ。SFCのメディアセンタにはbit別冊は1990年以降のしか置いてないしなぁ……

【追記】 復刊.com 『bit別冊 Common Lisp オブジェクトシステム -- CLOSとその周辺』

λ. 金融数理 備忘録

阿部君の発表についていけるようにこれを読んでみようかな。

λ. momonga

ruby-fdiskなんてのがあるのか。以前に作りかけたまま放置してあるruby-partedもちゃんとするかなぁ……

λ. 巡回群とか指標群とか

n位の巡回群Gの指標群G^の指標群G^^がGとcanonicalな同型な事を理解するのに苦戦。指標群の元は準同型射(つまり関数)なので考えるのが面倒くさい。というか、こういう時こそλ記法で書いて欲しいのですよ。λ記法で書き直してようやく理解できた。

λ. tDiary国際化

そういえば、tDiaryの国際化ってどうなったんだろう。Accept-Language: を見てメッセージを切り替えれば良いのかな?

λ. 群から圏へ

ふむ。群は圏の特殊化として見れるのか。

λ. Ruby/DL

疑問。Win32 API を呼び出しているサンプルがあるけど、Win32ではcdeclではなくてstdcallを使うようになってるのかな? -fno-defer-popの効果?

λ. The Y Combinator

を読んだ。lambdaが沢山で目が回りそう。

ただ気になったのは (procedure procedure) という呼び出しがあること。単純型付きλ計算なんかだと、この手の呼び出しは不可能なはずなので、そういう場合はどうするのかな?

λ. 『ギルティ ギア ゼクス PLUS アンソロジーコミック 2』

を読んだ。

『ギルティ ギア ゼクス PLUS アンソロジーコミック 2』

せんのあき, 飛吉由耶, 銭形たいむ, 北神諒, D・キッサン, 夏代篤志, あんこきくちよ, 石見翔子, 水沢充, かわんちゃ, 多田乃伸明, 破弓翔, あきづき弥, ひせきりか, 秋霞種栄, NAO, ふしみゆうり [著]

λ. 博麗神社例大祭

行ってきます。

ちょっと朝ゆっくりしすぎて、会場の列に並んだのが11:20。40分入れ替え制になったそう。入場したのが13:10過ぎ。体験版はすでに完売していましたとさ。orz

戦利品(?)

「東方烈華伝」体験版

-

「anima I 東方」

-

「幻想電奏響」

-

「幻奏蓄音機」

「幻奏譜」

ドメインがkeioだったのに驚いた

「アリスといっしょ」

これは○○○さんへのお土産　;-)

カリスマ扇

「komkom.com 通信 vol.3」

komkom.com

グラス (アリス)

-

「東風味　参」

福交感神経

「はるのうたげ」

かぐらみずき＠かぐら堂

「御粗末」

羽毛布団

「五月バカ」

オレブリスカ
ページを開いてたまたま目に入ったパチュリーの絵が気に入って買ってしまった。

「住所不定夢職」

夢見ごこち

「my best friend」

graceful fool

時の旅人　個人サークルペーパー「壊れた時計はいりませんか?」

壊れた時計

「Mystic Wanderer」

川代 拓 (Mysticmaker)

「紫のないしょ」

ゐとはたかいき

「We are Prismriver」

みょふ〜会

「門番の仕事」

月見箱

λ. GHC ソースコードハッキング 2日目

2時過ぎに例大祭を抜けて四ツ谷へ。

Foreign.C.String 相当の関数をでっち上げた。I/O周りはかなり面倒そうなことが分かってきた。

鬼車(Oniguruma)を使ってText.RegexをUnicode対応にするパッチ を GHC-6.4 用に更新。鬼車の同梱は評判悪かったので、分離した。鬼車は別途インストールしてくれ。

[2005-05-06 追記] なんで以前に鬼車のソースを取り込んでいたのか理由を思い出した。GHCi対策だ。鬼車のライブラリは.soではなく.aにコンパイルされるが、GHCiのリンカがリンクできるのは.soや.oだけで、.aはリンク出来ないのだ。したがって、単にghc-6.4-oniguruma3-1.patchのようにすると、baseパッケージがGHCiで使えなくなってしまって致命的。

これを回避する一つの方法は、ld -r --whole-archive -o onig.o libonig.a として onig.o を作り、library-dirs のリストに含まれているディレクトリ(e.g. $prefix/lib/ghc-6.4)に置いてやること。別の方法はlibHSbase_cbits.aとHSbase_cbits.oにlibonig.aの中身を最初から取り込んでしまうこと。ただ、どっちもfptoolsのビルドシステムでやるにはどうしたら良いのか分からん。困った。

λ. filofax

一瞬firefoxに見えた。

λ. 禁煙席と喫煙席

GHCソースコードハッキングの後、某ファミレスで夕食を食べたのだけど、禁煙席がいっぱいなのに喫煙席がガラガラで驚いた。禁煙席と喫煙席の境界を適応的に変化させることが出来たら、より多くの客が利用できるのではないかと思った。

λ. ストリームの表現

ストリームの直観的な表現はsigを使った次のような表現だが、この定義はtermination checkerに怒られる。

Stream :: Set -> Set
Stream A = sig
             head :: A
             tail :: Stream A

別の定義として以下のようなものが考えられるが、今度はストリームを生成する関数がtermination checkerに怒られることになる。

data Stream (X::Set) = SCons (x::X) (xs::Stream X)

from :: Nat -> Stream Nat
from n = SCons n (from (succ n))

実のところ、agdaにはcodataを扱う機能がないので、ストリームのようなcodataを直接扱うことは出来ない。そこでストリームと同型でかつagdaで表現可能なデータ型を考える。ストリームの直観的な意味は無限個の直積 A^ω なので Nat -> A という関数型として表現することが考えられる。基本的な演算も同時に定義すると以下のようになる。

Stream :: Set -> Set
Stream A = Nat -> A

head (|A::Set) :: Stream A -> A
head s = s zero

tail (|A::Set) :: Stream A -> Stream A
tail s = \n -> s (succ n)

unfold (|A,|X::Set) :: (X -> A × X) -> (X -> Stream A)
unfold phi x n =
    case phi x of
    (a,x)->
        case n of
        (zer  )-> a
        (suc m)-> unfold phi x m

この表現で一つ嫌な点は外延性が成り立たない点。つまり Ext = (A::Set) -> (s1,s2::Stream A) -> ((n::Nat) -> Id (s1 n) (s2 n)) -> Id s1 s2 は要素を持たないし、双模倣(bisimulation)の関係にあるストリームが等しいことも一般には証明できない。内包的(intentional)な型理論の世界で作業している以上仕方がないところではあるが、これはやっぱし嫌な感じだし、ある程度の外延性を持った型理論がいいなぁ……

ところで、このストリームの表現は Representations of First order function types as terminal coalgebras. の対応を逆に使ったものなので、他のcodataにも同様の方法で表現できるものがある。しかし、νX. 1+A×X のように直和が入ってくるとこの方法では表現できないと思うし、やはり組み込みのcodata対応は欲しいところか。OTT(Observational Type Theory) と Observational Epigram (Codata参照) に期待。それから、IsabelleやCoqではcodataの扱いはどうなってるんだろう。Coqはcodataをサポートしているらしいが…

【2007-09-11追記】 直和が入ってくるような場合でも、20070905#p01のようにすれば表現可能。

λ. Last.fm

Last.fmのアカウントは少し前に作るだけ作って放置していたのだが、yaizawaさんが使っているのを見て、面白そうだと思い使ってみることに。 私の知り合いで Last.fm 使ってる人がいたら、Friend になりませんか?

ちなみに、私の再生履歴からこんなのがおすすめされてるらしい。
⇒ My Recommendations

iPodとiSproggler

社会人になってからPCで聴くよりもiPodで聴くのがずっと多くなったのだが、標準のクライアントだとiPodでの再生履歴が送られないようなので、iSprogglerに入れ替えた*1。 ただ、iPodをストレージとしても使っている場合、iPodを同期した後、ejectしないと再生履歴を送信しないようだ。mixi station ではそんなことはなかったので、何だか不思議。

λ. 藤沢で飲み会

藤沢で飲み会。 就職を祝ってもらったりとか、色々。 感謝。

λ. 東北旅行 (1)

北上市立公園展勝地。 桜はすっかり葉桜になってしまっていたけど、菜の花が綺麗だった。

角館。

安比高原温泉。

λ. 『本物のプログラマはHaskellを使う』読者の集い

参加した。(後で書く)

ustream.tvでの中継に初挑戦してみたが、どうも思うようにはいかなくてちょっと残念。

DoubleがBoundedのインスタンスになっていない話は、そういえば前も同じこと書いてたな。

Control.Monad.Errorで定義されている MonadPlus IO インスタンスは、Control.Monad のドキュメントにある m >> mzero == mzero の条件を満たさないのね。

mtlが現在のLazyバージョンとStrictバージョンの構成になった経緯について聞いてみれば良かったな。

JHCの存在型にまずい点があったというようなことを言ったが、どうも<URL:http://article.gmane.org/gmane.comp.lang.haskell.prime/436> のあたりの話と混同してた気がしてきた…… orz

m-a-oさんに初めてお会いした。

λ. "Do we Need Dependent Types?" by Daniel Fridlender, Mia Indrika

• <URL:http://www.brics.dk/RS/01/10/>
• <URL:http://www.citeulike.org/user/msakai/article/3140868>

Hindley Milner オンリーだから、型クラスも使わないのか。 アドホックすぎだけど面白い。

(<<) :: [a -> b] -> [a] -> [b]
(f:fs) << (a:as) = f a : (fs << as)
_ << _ = []

zero :: [a] -> [a]
zero = id

succ :: ([b] -> c) -> [a -> b] -> [a] -> c
succ = \n fs as -> n (fs << as)

one = succ zero :: [a -> b] -> [a] -> [b]
two = succ one :: [a -> b -> c] -> [a] -> [b] -> [c]

zipWith :: ([a] -> b) -> a -> b
zipWith n f = n (repeat f)

zipWith2 :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith2 = zipWith two

あと、(<<) は Applicative ZipList の <*> と同じかな。