日々の流転

λ. デジカメ届いた。けど、思ってたよりもかなり画質が悪くて、いや〜ん。レンズ付きフィルムより悪そう。

λ. 醤油の「醤」と脳漿の「漿」が一瞬同じ字に見えた。「漿油」とか「脳醤」とか嫌すぎ。

λ. 家族で大谷美術館へ。ヴラマンクの絵を見るのは初めてだと思うが、気に入った。

λ. ロイヤルホストでタコスを食べた。

λ. 床屋

もう学校も始まるので、床屋に行ってスッキリしてきた。

λ. functor

MLにもfunctorがあるらしい。[ruby-dev:3777]のスレッドを見ると、圏論のfunctorと似たような感じか。

ところで、オブジェクト指向言語では関数オブジェクト(function object)の事をfunctorと呼ぶことがあるけど、あれは圏論のfunctorとは何か関係あるのかな?

λ. WEB+DB PRESS Vol.7 WebDAVバージョニング実装 Subversion

を読んだ。

λ. Collection Schemes For Distributed Garbage

「4.4 Hybrid collectors」に mark-and-sweep と reference counting を組み合わせる話があったけど、期待した内容ではなかった。

λ. 親知らず

消毒してもらってくる。もう痛みはほとんど無い。

λ. RHG読書会 Reloaded

市ヶ谷駅から間違えて反対側へ行ってしまい、靖国神社まで行ってしまった。どうせなら参拝していこうかとも思ったけど、すでに時間が過ぎていたので、急いで引き返す。地図を印刷していけばよかった。

これまで雲の上と思ってた人たちに会うことが出来て、ちょー感激。

λ. g_signal_override_class_closure() その2

メモ

• Chaining Class Closures (gtk-devel-list)

λ. hyさ〜ん

以前に、「Agdaの紹介Flash」というエントリに対するコメントで、hyさんという方に「Twelfでの証明行為」と「Coq-IDEでの証明行為」という動画を教えていただいたのですが、最近参照しようと思ったら消えていて残念でした。

これらの動画はこのまま見れなくなってしまうには非常に惜しい動画だと思います。 どなたか、hyさんの連絡先を知っている方や、これらの動画を保存している方はいらっしゃいませんでしょうか。もしいらっしゃいましたら、個人的に連絡を頂ければと思います。

λ. 先日交換したHDDを売却

先日交換したHDDをソフマップで売却。 不良セクタがあるのでジャンク扱いかと思っていたが、なんと満額の3,600円で売れた。 12,700円で購入したものだったので、2年で約9千円分償却したことになるか。

なお、HDDの使用期間や状態についての確認は一切無く、査定として検査を行っていた。一般に中古HDDは一定数以下の不良セクタは保証対象外として売られているようなので、それ以下の不良セクタしかなかったということかな。 ……後で気付いたのだけど、これって私には瑕疵担保責任は無いよね?

λ. Church-Rosser Theorem in Agda2

Haskell Hackathon in 2008 September に参加。やるネタは幾つか考えていたのだけど、結局、昔Agda1で書いたチャーチロッサーの定理の証明をAgda2で書き直すということをやっていた。

(詳しくは後で)

λ. Mの型付け

Mコンビネータ*1 λx. x x は多相型を適当に使うと型付け出来る。 例えばHaskell(GHC)ならば以下の通り。

m :: (forall a. a->a) -> (forall a. a->a)
m x = (x :: (forall a. a->a) -> (forall a. a->a)) x

これが出来るのは 型 forall a. a->a に属する真っ当な要素は id だけだから。

では、同様にすると、Yコンビネータ*2 λf. (λx. f (x x)) (λx. f (x x)) も型付け出来るだろうか?

λ. Introduction to Categorical Programming

Haskell Annual Meeting Autumn.jp 2009 (Hama.jp 2009) で、CPL とか Haskell での Categorical Programming の紹介をしたのだけど、テーマを絞りきれなかったのと、準備が間に合わなかったので、かなりグダグダな感じに。

このままというのはあんまりだと思ったので、修正版の資料を作成した。テーマが絞れていないという、根本的な問題は直ってないので、あまり変わらないけど……

資料(修正版)

ダウンロード(PDF)

資料(当日版)

ダウンロード(PDF)

参考資料や関連情報など

• Categorical Programming Language
• Categorical programming with inductive and coinductive types
  • ヒビルテ (2004-06-29)
• The Evolution of a Haskell Programmer
• CPLの処理系のダウンロード
• ヒビルテ [CPL]
• primrecの再帰を使った定義とiterを使った定義の等しさを QuickCheck で確認 (nwnさん)

その他 HAMA.jp 関係

• ログ
• Type level programming in Haskell (keigoiさん)
  • ustream.tv
• Haskellで圧縮 (smlyさん)
• #HAMA - Twitter Search
• nono weird science : HAMA.jp