2023-07-05

論理と哲学とプログラミング言語

プロトタイプベースのオブジェクト指向言語について、哲学の方面から議論したエッセイを読んだ。クラスベースなのは古典的なアリストテレス的な分類の考え方に基づくもので、プロトタイプベースなものはヴィトゲンシュタインっぽい考え方に基づくとのこと。

アリストテレス的な考え方では、物事は分類できて、しかもいろんな分類があったとしても最高の分類みたいなものがある、みたいに捉えるそう。分類の中でその類を象徴する代表みたいなものも取れてしかるべきみたいな。一方でヴィトゲンシュタインっぽい考え方ではアリストテレス的なのには割と無理があって、そんな考え方が通用するのは数学の概念くらいとしていて、分類は観察する主体に依るし、文化とかの影響を受けるもので「科学」みたいに自然に導かれるようなものではない、みたいな考え方をするらしい。

リアルワールドを表現、分類しようと思うと確かにヴィトゲンシュタインの方がしっくりくるというか、矛盾が少なさそうな雰囲気がする。だけど、独自の世界を作ろうと思うとヴィトゲンシュタインの考え方に基づくのは骨が折れそう。

では、関数型言語とか意味論の人たちの視点だとどうなるだろうか。オブジェクト指向は哲学の話に基づいて議論しているみたいだが、型システムとか意味論は論理学をベースにしがち。型は命題でプログラムは証明。

ところで

型は命題でプログラムは証明。

この標語はしっくりきていない。型に入る_項_を僕は証明だとは思えない。依存型は項に依存する型だとは思えるけど、証明に依存する型と言われるとなんだかなと思う。まあ、その項にも型をつけるので、その型の証明にはなっているのだけど。Numみたいな型を命題というのがしっくりこないのと同じか。

依存型でも依存する項の型が関数型とかの命題っぽい型だったら証明に依存している雰囲気を味わえるかもしれない。帰着を考えればいいのかな。この命題が成り立つなら、これこれが成り立つ。これは依存型じゃないな。帰着は型をとって型を返すだけなので、type operatorだ。

ところでラフロイグの10年おいしい。

nが2より大きい、みたいな命題は依存型がないと表現できないか。簡単だ。

\Pi n: Nut. (n > 2 -> \Pi x,y,z: Nut. x^n + y^n != z^n)

ここで _ > _ は依存型。普通だね。

話を戻す（ラノベだったらここで閑話休題って言ってた）。オブジェクトと抽象化の話をしていたのだった。オブジェクト指向では、分類を動的な性質としてみるきらいがありそう。それに対して関数型っぽい世界では、分類は静的にできる型判断でしかないイメージ。型によって動的な振る舞いは変わったり変わらなかったりするけど、とりあえず型は静的につけるものだと思う。その情報を実行時まで持ち越すかは好きにすればいい、くらい。

お気持ち

動的メソッドディスパッチはいまだにしっくりこないし、メタプログラミングに関しては勝手にやってくれって思ってしまう。

Hugoについて

ディレクトリの構造で投稿の分類を決めるのはよくないと思う。分類なんて書いているうちに変わるのだし、その方が便利そうなので全てはフロントマターにお任せしてしまえばいいと思った次第。そんなこという子はhugoユーザには要らないのだろうから、そのうち独立するのがいいんだろうな。

今日は7月5日

明後日が七夕だ。花金なので会社の人と七夕のみをできるかもしれない。

七夕のみ

七夕は織姫と彦星が一年に一回逢瀬を重ねられる日。天の川に橋がかかるんだったか川の水が引くんだったかで会える。ここでは皮の水が引く説を採用する。

旧暦では時期的に川の水が引いたかもしれないが、現代では7月の頭はまだまだ梅雨みたいなもので川は元気だ。このままでは織姫と彦星は約束の日に会えない。かわいそう。なのでいつも夏の大三角に心を癒してもらっている僕たちは、せめてもの恩返しに川を飲み干して、逢瀬を支援することにした。これが七夕のみ。幸いなことに梅雨の雨で薄まった川はアルコール度数が比較的低く、ほろ酔いくらいのイメージ。だからこの日は梅雨がもたらす潤沢な量のほろ酔いを飲む。

エンジニアリングの幸せ

エンジニアリングは手段でしかないと今は本心で思っている。とはいえ、プログラミングやエンジニアリングをしていて幸せを感じるタイミングもある。このギャップはエンジニアリングの成果を確かめることにあると思う。

例えば家に電気が通っていることは感動的なことだと頭ではわかるが、その恩恵を享受することは特に幸せだとは思わない。それに対して、新しくプログラミング言語を学んで、これまではできなかった表現でこれまではできなかった解決策を実現するのはとんでもなく楽しい。さらにはこれまでは明らかではなかった解決の方法を明らかにするのは結構な幸せだ。

このギャップは成果を確かめること、差分を観測することにあると思う。微分係数が大きいときが一番やりがいを感じる、みたいな話に通じる気がする。

今日良かったこと

• 会社の人の親切に触れたこと
  • 一人だけじゃなくて4,5人くらい
• 会社じゃない知り合いとちょっと仲良くなれたこと
• ラフロイグがおいしいこと
• オブジェクト指向の話が面白かったこと
• 権八に行けたこと

あとがき

こんなしょうもないことを書いていたせいで、今日の元気が終わってしまった。ラフロイグに完敗。またこんなことをインターネットで公開するおかげで恥の概念がなくなってきた。これは良し悪しありそう。