檜山正幸のキマイラ飼育記

ハイコンテキストな定数・記号の解釈

雑記／備忘 | 12:19 |

演算子オーバーロードに関する記事「コンピュータは「掛け算は足し算とする」を理解できるか」に対して、id:kmizushimaさんとid:matarilloさんが、それぞれScala、F#で対応するサンプルを書いてくださいました。ありがとうございます。

• https://github.com/kmizu/tropical
• https://gist.github.com/matarillo/7502d98b8d46f56b4546
  記事は http://haskell.g.hatena.ne.jp/matarillo/20151207/1449485837

Scala、F#でも、C++と同じことができるのが分かります。

でもね、まだ不満があるんですよ。

ソースコード内で 1 + 1 と書けば、さすがにこれは2になります。数値をmin-plus半環の要素だと思って書いても、コンパイラは心のなかまでは察してくれません。

ここが不満。1 + 1 と書いたら答が1になって欲しい。いや、もちろん「心のなかまで察してくれ」とは言いません。ヒントは与えますが、それが 1_mp + 1 のような接尾辞ってのはどうもなー、ということです。

我々人間がコミュニケーションしている状況では会話のコンテキストがあります。min-plus半環を話題にしている“トロピカルなコンテキスト”では、ホワイトボードに 1 + 1 と書けば、定数リテラル1はmin-plus要素と解釈されるはずです。

C++でも名前空間の宣言があります。using namespace std; とすれば、スコープを明示するstd::接頭辞を省略できます。つまり、名前の解釈が変わるわけです。であるなら、記号やリテラルの解釈も変わっていいじゃないか、と思うわけです。例えば、using context tropical; とかすると、定数リテラル1の解釈が1_mpとなる、とか。

Coqにはnotationとinterpretation scopeというメカニズムがあり、Open Scope tropical_scope のようにして記号の解釈を変えられます。しかし、厳密な型付けの都合から、同じ名前を同時に（同一文脈で）異なる型に割り当てることはできません。Coq型クラスのラベル名（フィールド名）を局所化できないという酷い話もあって、結局、名前の増加を防げません。

僕が名前（記号やリテラルも含む）のオーバーロードに拘るのは、名前の増加に耐えられないからです。

「Coqで半環：アンバンドル方式の例として」より：

名前の増加にはシンドイ思いをしたので、人間が使うシステムではいかにして名前の個数を減らせるかはとても重要な課題だと思っています。共通の性質・構造を持つモノを同じ名前で呼べることは、ものすごい節約・効率化・汎用化につながります。

文脈依存の多義語は、ときに混乱をもたらす弊害もありますが、有限少数の語彙を効果的に使ってジェネリックな記述や推論を可能にするというベラボーなメリットがあります。だから、コンピュータとのコミュニケーションにも文脈依存だが適切にコントロールされた多義語を使いたいのです。