型はオブジェクト（対象）であり集合の圏なら集合　カリー＝ハワード＝ランベック（同型）対応

b.hatena.ne.jp

 

「関数型プログラミングが『銀の弾丸』であるという非常識な常識2022」の感想 - Qiita

それな感。型はカリー・ハワード対応等で集合の様にも使えるけど、集合そのものではないよな。あとあの記事の理屈なんか全体的に対象がモノイドである事が普遍的な前提みたいなものを感じるんよな。何なんだろうアレ

2021/12/16 15:24

b.hatena.ne.jp

 

去年の年末に本書の超アルファ版をUPしたときに、冒頭に

ja.wikipedia.org

のことを書いた。

まさに冒頭に結構なウェイトをもって書いたので、すこぶる評判が悪かった。

結局の所、こういう関数型の本を書くときには、目線は初学者に向いていなければならないという根本的な方針を徹底することとした。

なぜならば、自分自身、これまでの経験として、ほんとうに鬱陶しい障害となるのは、こういうちょっとわかった風の中級者連中であり、人様の本への論評にかこつけて、なんか偉そうにドヤって、あたかも著述の内容が正確ではない、というような風評を流すことがあるので、彼ら除けの「お札」みたいに権威を貼り付ける、という最低限の作法だけにしようと思ったからだ。

 

それが、「型は集合」の章であり、このブログでもなんどもしつこいように貼り付けているnLabの項目だ。

ここでもう一度繰り返そう。ここで二つの言い分がある。

ひとつは、どこの馬の骨ともわからない中級者が匿名アカウントでハテなブックマークに殴り書きしたようなコメント

 

それな感。型はカリー・ハワード対応等で集合の様にも使えるけど、集合そのものではないよな。

 

もう一方は、数学の引用文献としてそこそこ権威がある

nLab記事から

nLab は、数学・物理学・哲学の研究レベルの内容について扱ったウィキである。nLabはMathOverflowにおいて、質問前にチェックするべき標準的なオンラインの数学文献の1つとしてリストされている。多くの質問と解答が、nLabを背景資料として用いている。また、nLabはバイエズがアメリカ数学会（American Mathematical Society）に投稿した数学ブログのレビュー記事の中で言及されている2つのウィキのうちの1つである。

Type theory versus set theory型理論 vs 集合論

Alternately, we could change our terminology so that what we have been calling “types” are instead called “sets”.あるいは、これまで「型」と呼んでいたものを「集合」と呼ぶように用語を変更することもできます。 Thus, words like “type” and “set” and “class” are really quite fungible. This sort of level-switch is especially important when we want to study the mathematics of type theory,このように、「型」や「集合」や「クラス」などの言葉は、実はかなり代替可能です。このようなレベルの切り替えは、型理論の数学を研究するときには特に重要です。

 

「集合そのものではないよな。」という漠然とした言及が、極めて具体的に「初学者」むけではない解説記事に詳細があるのに、なんでそれを上書きできると思ったのかよくわからない。

 

おそらく、

型はカリー・ハワード対応等で集合の様にも使える

というハッタリ文句が効くと思ったぽいのは想像にかたくない。

本書の前バージョンから、この「カリー・ハワード対応」というお札を引っ込めた途端に、その分だけ、なんか言ってくるんだな、ほんとうに鬱陶しいと毎度実感する。

 

今回、おそらく「チューリングマシン」だとか「計算理論」とか、グラフ理論のところで、「関係がある」とだけ書いたら、それについてはなーんもイチャモンつけてこない。

 

モナドと圏論については、それについて集合の圏では二項演算である、とまさにそれがせいぜい、HaskellのMonad則のページで書かれている全部の範囲なわけだが、そいつはその演算子の定義のコードを自分で出しておきながら、いきなり集合の圏に限らないモナドの定義の話をしだした。

結局の所、くだらない連中には、手間がかかってもお札を貼り漏らすことがあっては行けないということを再度確認しなければいけない。

 

型はカリー・ハワード対応等で集合の様にも使える

 

という言及に、こいつは、nLab引用した部分の言及以上にいったい何の価値を感じているのだろうか？


9.4. スーパーイディオム分野にまたがって、基本、同じ概念を違う用語で表現しています。

型理論（Type theory） 型（type） 関数（function）/ 写像（map）
集合論（Set theory） 集合（set）始集合（domain）と終集合（codomain） 写像（map）
解析学（Analysis） 定義域（domain）と値域（range）と終域（codomain） 関数（function）
代数学（Algebra） 集合（set）/ 被演算子（operand） 演算子（operator）
オブジェクト指向（Object-oriented programming） オブジェクト（object） メソッド（method）
圏論（Category theory） 対象（object）/ 圏（category） 射（morphism）

情報処理・プログラミング データ（data） 処理（operation）
このなかで、最も根底となる、すべての概念の包括的な枠組みが圏論（Category theory）で、これまで永らく数学の基礎であった集合論でさえも圏論の言葉で再定義されます（集合の圏（category of sets）における射（morphism）は関数（function）になる）。 型（Type）とは集合（Set）のこと。関数（Function）と演算子（Operator）は本当は同じもの。オブジェクト指向のオブジェクトは、数学の集合(Sets)に相当し、二項演算の左側の被演算子（Operand）になります。オブジェクト指向のメソッドは、数学の二項演算子(Binary operatior)に相当しており、オブジェクト指向のメソッドの引数は、二項演算の右側の被演算子（Operand）になります。 と既に明確にしたとおり、本稿の方針は、二項演算子(Binary operatior)を最大限に活用することなので、このなかでどの分野の言葉をもってコードを書いていくのか？となると、当然、代数学（Algebra）になります。

 

と書いているのだが、ここで

このなかで、最も根底となる、すべての概念の包括的な枠組みが圏論（Category theory）で、これまで永らく数学の基礎であった集合論でさえも圏論の言葉で再定義されます（集合の圏（category of sets）における射（morphism）は関数（function）になる）。

と、まず基底は、圏は集合であり、射は関数となる、集合の圏が基底であると示している。ただし、こんなもんは、イチャモンつけたいこういうごく一部の、まあどうせろくに読みもしない読者対象から外したい連中しか気にもとめないだろう。

いちおう初学者向けに将来にむけて、という意味は断固あるものの、半分くらいはこういう連中除けのお札であることは否めない。

上記の図では、型はオブジェクトに対応している。

これは、ある程度の偶然もあるが、

対象（object）/ 圏（category）

のオブジェクトにも対応している。集合の圏では、集合だ。

カリー＝ハワード同型対応 - Wikipedia

カリー＝ハワード＝ランベック対応

において、

このカリー＝ハワード＝ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる。ここでは

オブジェクトは型

あるいは命題に、モルフィズムは項あるいは証明に解釈される。

と書かれているそのものである。

 

元のQiitaのネガキャン記事では、型が集合ではない、とおもうという主張を、このブログ記事でも糞味噌に批判したが、TypeScriptの実装が、とかかなりトンデモな理路でやらかしているわけで、そういうトンデモにどのように「それな」と同調できるのか意味なんてわかるわけもない、まあこの人物がトンデモだという説明しか成り立たないが、せいぜい

型はカリー・ハワード対応等で集合の様にも使える

と、ボサーっとした意味不明なnLabの引用文を上書きするだけの論旨があるわけもない、

集合そのものではないよな。

ってのは、メタな観点ではこのような有用な観点で同一視されているものを、メタではない観点では、そりゃ

型理論

集合論

は、繰り返すとここで論じているメタな観点の同一視ではないレベルでは「そのものではない」のは自明なので、こういう主張の仕方するやつらって世の中で消えることはないけど、有害だよなあ、と思った次第。

 

基本的に、僕の書いたもんに文句つけてくる人間っていうのは、一様になんか思い込みが激しくて、最後には、自分の好きなPureScriptとかうAltJS使えとか、ML使えとか、自分の趣味領域の好みの発露をしてそれで満足みたいな、議論には適正のない、ましてや書評とかやってほしくない単に自己中心的な人種ばっかりで、迷惑だなあと思う。