同じようなネタを繰り返し取り上げているってことは、それに興味があるってことでしょうね。
昨日、「例外処理の記述：あー大まちがい、でも面白いなーヤッパリ」というエントリーを書きました。直接的な動機は、さらにその前のエントリーの間違いを訂正することだったのですが、「面白いなー」と見出しにあるくらいなので、例外処理コードの同値書き換え問題に興味を感じているわけです。
僕は、データ型やプログラムを計算対象にした計算が好きです。プログラム“で”計算するんじゃなくて、プログラム“を”計算するのね。計算を足し算や掛け算のような演算と解釈すれば、部品となるデータ型やプログラムから、より大きなデータ型／プログラムを構成する話になります。計算を、a(b + b) = ab + bc のような等式変形と考えれば、意味（データ型の外延やプログラムの振る舞い）を変えない同値な表現を求めることです。
型構成子や制御構造が、基本演算になります。これに変数概念を導入すると、総称型やメタプログラムの概念になります。型やプログラムを値とする変数・関数を系統的に扱うなら、圏・関手・自然変換を道具立てにするのが便利です。
僕が圏論を使いたい一番の動機はコレですね。つまり、データ型やプログラムに対して計算を行うにあたっての、掛け算九九や筆算手順や解の公式が欲しい、基本となる計算手段が欲しい、と。圏を使わないにしても、背後になんらかの代数構造がないと計算はできません。
推論も一種の計算ですが、正しい命題をもとに正しい推論をすれば結論も正しいことが保証されます。同じように、正しい部品プログラムをもとに正しい組み立て方をすれば出来たプログラムも正しいことが保証できたらいいな、と思います。正しい部品を寄せ集めても出来上がりは悲惨だったりと、当たり前のことがなかなかできない。これは、プログラムで計算はできても、プログラムを計算することが十分にできてないってことじゃないでしょうか。
結論らしい結論はないのですが、関連エントリーを挙げておきます。
