日々の流転

λ. 人間の天敵はいつ開発が完了するだろう。

「ルドラの秘宝」みたい……

λ. Symmetric Haskell

今考えてること。

• Symmetric ML のアイディアをHaskellに対して適用してみる。 つまり、co-dataを通常のdataと同様に(対称的に)定義できるように文法を拡張する。
• ここで扱うco-dataはrecordによって表現できるはず。
• 拡張された文法からHakell98へのトランスレータを作成出来るか?
• 特にco-dataに対するパターンマッチングを用いた関数定義は翻訳できるか?
• Symmetric ML ではlazynessが問題になったが、 Haskellは最初からlazyなので、その辺りはシンプルになるはず。

試しに書いてみると、こんな感じか? 対称的なのは美しいかも知れないけど、全然面白くないなぁ……

codata (a,b) = Fst :: a & Snd :: b
 
pair :: a->b->(a,b)
pair a b = merge
             Fst <- a
             Snd <- b
 
codata InfList a = Head :: a & Tail :: InfList a
 
comb :: InfList a -> InfList a -> InfList a
comb l1 l2 = merge
               Head <- Head l1
               Tail <- comb l2 (Tail l1)
 
-- combの別の定義方法
Head (comb l1 l2) = Head l1
Tail (comb l1 l2) = comb l2 (Tail l1)

λ. 傘

また傘を盗られてしまった。少しの間とはいえあんな所に傘を置いてしまった僕の不注意なのだが、やはり腹が立つ。傘を盗むなんて最大級に卑劣な犯罪ですヨ。犯人は、良心の欠片もない卑劣な人間に違いない!

λ. 今日の向井研

新しい人が二人ほど来た。

ふむ「点の無い幾何学」か。

春学期はみんなバラバラの事をやってて、他人の発表にはついていけていなかったので、今期は何か共通のこともやりたいし、Topology via Logic を輪講するというのも悪くないと思うんだけどなぁ……

向井先生に『プログラム意味論』という本が教科書としてバランス良く丁寧に書かれていると聞いた。ラムダ計算や圏論、それにdomain theoryについても扱っているらしい。

λ. 借りた本

Intuitionistic Type Theory

P. Martin-Löf.