日々の流転

λ. gtk2hs-0.9.4

をWindowsマシンにインストールしてみる。FFIのインターフェースが変更されたらしく、GHC-6.2ではそのままではコンパイルが通らず、newForeignPtrの引数の順番の入れ替えと、ForeignPtrToPtrのunsafeForeignPtrToPtrへの置き換えが必要だった。あと、生成されるlocalpackage.confのgtk2のエントリのextra_ld_optsがおかしかったので、["-Wl,--subsystem,windows"]に書き換えた(生成してるのはmk/library.mkなんだけど、こっちはどう直せばいいか良くわからなかった)。

使ってみたところ、とりあえず日本語はちゃんと通るようだ。wxHaskellは(wxhaskell-bin-msw-ghc6.2-0.6-1.zipを試した限りでは)日本語がまともには通らなかったので、とりあえずgtk2hsを使っていこうと思う。

λ. IO#readpartial

[ruby-dev:23247]でIO#readpartialの実装が出てきたので、iconv-ioで試しに使ってみる。うん、確かに便利そうだ。

λ. Calculational Proof っぽい書き方

等式の証明は大抵は A=B=C=D といった等式の連鎖で表されるが、これはAgdaでは書きにくい。Agdaでは普通は以下のような感じで書くことになるが、式が複雑になることを考えるとBやCの式が複数回出現するのが嫌。また、lem1等と名前を付けずに直接tranIdの引数として書いてしまうことも出来るが、そうすると今度は読みにくくなってしまう。

let lem1 :: Id A B
       = ?
    lem2 :: Id B C
       = ?
    lem3 :: Id C D
       = ?
in lem1 `tranId` lem2 `tranId` lem3

そこで、通常の calculational proof 風の書き方をDSLとして実現できないかと考え、次のようなものを用意してみた。

calc (|X::Set) (x::X) :: Id x x
  = refId x

(:=) (|X::Set) (|x,|y,|z::X) (id1::Id x y) (id2::Id y z)
  :: Id x z
  = tranId id1 id2

by (|X::Set) (|x::X) (y::X) (id::Id x y) :: Id x y
  = id

triv (|X::Set) (|x::X) :: Id x x
  = refId x

これを使うと例えば以下のような書き方が出来る。 演算子の優先順位やらの関係でちょっと不恰好だが、結構便利だ。 「型理論での形式的証明記述の技法について」(20050917#p01)で紹介されていた Chain を使う方法よりもずっと便利なのではないかと思う。

add_assoc (a,b,c::Nat) :: Id (a+(b+c)) ((a+b)+c)
  = ?

distl (a,b,c::Nat) :: Id ((a+b)*c) (a*c + b*c)
  = case a of 
    (zer   )-> refId (b*c)
    (suc a')->
      calc ((a+b)*c)
       :=( (((succ a')+b)*c)    `by`  triv )
       :=( ((succ (a'+b))*c)    `by`  triv )
       :=( (c + (a'+b)*c)       `by`  triv )
       :=( (c + (a'*c + b*c))   `by`  mapId (\x-> c+x) (distl a' b c) )
       :=( ((c + a'*c) + b*c)   `by`  add_assoc c (a'*c) (b*c) )
       :=( ((succ a')*c + b*c)  `by`  triv )
       :=( (a*c + b*c)          `by`  triv )

λ. デスノートネタ

<URL:http://etc4.2ch.net/test/read.cgi/wcomic/1143480199/213> のネタがツボだった。

page.103「宣伝」

照「…37」
月「…」
照「…38」
月「…」
照「…39」
月（パチ）
照「後手、３五角」

照「…じゅーびょ〜」
ニア「…」

照「…にじゅーびょ〜」
ニア「…」

λ. 証明書発行

就職先に提出する修了証明書と成績証明書を発行してもらいに学校へ。23日までに申し込んでいれば学位授与式で学位記と一緒にもらえたのだが、申し込むのを忘れてたので。あと、明日までは即日発行可能なのに、30日に申し込むと4/2以降の発行になってしまうというのが不思議。

λ. Edyが使えるコピー機

生協のコピー機を使おうとしたら、Edyが使えるやつがあってビックリした。