【モナド編】本書いたら数学愛好者の中級レベルのプログラマーからマウンティングを試みられた話

ken-okabe.hatenablog.com

のつづきです。多分中編

qiita.com

がトンデモ素材。

FunctorとMonadは二項演算か？

型と集合でnLabのどこに書いてありますか？と中級者が本・記事をろくに読まないままTwitterで聞いてきたのは呆れましたが、これも「読めよ」のレベルの話です。

HaskellのFunctorやMonadはそれぞれ

 

(<$>) :: Functor f => (a -> b) -> f a -> f b
(>>=) :: Monad m => m a -> (a -> m b) -> m b

という二項演算を持ちます。Monadはこのほかに単位射 return :: a -> m a を持ちます。Monadについてはこの時点で「二項演算」だけじゃないだろって感じですが。

Haskellでいうならば、悪名高いMonad laws のページに

wiki.haskell.org

とありますが、

これ、

Left Identity　左単位元

Riht Identity　右単位元

Associativty　結合則

という代数的属性について、まさにその

と定義されrた演算子が、左右のオペランドの間の中置記法で

二項演算子として使われている式になってるんじゃないの？っておもいますけどね。

と言うか、君、そのFunctorとかモナドの演算子とか二項演算子以外の使い方してるの？っておもう。

著作においては、

19. ファンクタ（Functor）すべてを包括するような代数構造

19.6. Functorをもっと厳密にTypeScriptで定義していく

において、

型定義だけを改めて抜粋すると、

type F<A> = A[]; // type constructor type map = <A, B> // function => function (f: (a: A) => B) => (Fa: F<A>) => F<B>;

このTypeScriptのコードで、かなり正確に、Functorの概念を表現できています。

(引用終わり)

とかさらに、そのHaskellでの定義そのものを引用している。

中級者はまたろくに読んでもいないから、書いてるものをまた、ほらね的にQiita記事に書いてる。

いや、著作でそれ引用した上で論じてるから（苦笑

（引用始まり）

ちなみに、Haskellでは、型定義にプレースホルダは積み増さない流儀なので、

fmap :: (a -> b) -> f a -> f b

とFunctorはよりスッキリと定義されてるのですが、全く同じ意味です。 TypeScriptではプレースホルダは逐一明示したほうが便利だ、という方針で、そのメリットは確かに大きいですが、こういう抽象度が高い概念になると、逆に見通しが悪くなるデメリットはありますね。 視覚的に表現するとこういう概念図になるでしょう。

19.7. 圏論（Category theory）のFunctor そもそも、Functorとは圏論（Category theory）で定義された概念なのですが、nLabのFunctorの項目によると、

この図をみると、ちょうど、

(f: (a: A) => B) => (Fa: F<A>) => F<B>

というコードの表現がそのまま書かれていることが感じられると思います。

（自分の本の引用終わり）

さて、中級者のQiita記事では、

HomF(c,d):HomC(c,d)→HomC′(F(c),F(d))$${\mathrm{H}\mathrm{o}\mathrm{m}}_F(c,d):{\mathrm{H}\mathrm{o}\mathrm{m}}_{\mathcal{C}}(c,d)\to {\mathrm{H}\mathrm{o}\mathrm{m}}_{{\mathcal{C}}^{\prime }}(F(c),F(d))$$

だそうです。

ここで、もしもHomが（プログラミング言語における）関数型のようなものであればこれはカリー化された関数、二項演算と思えるでしょう。しかし、 HomF(c,d)${\mathrm{H}\mathrm{o}\mathrm{m}}_F(c,d)$ の →$\to$ は集合の間の関数の意味なのに対し、行き先の HomC′(F(c),F(d))${\mathrm{H}\mathrm{o}\mathrm{m}}_{{\mathcal{C}}^{\prime }}(F(c),F(d))$ は圏 C′${\mathcal{C}}^{\prime }$ の射です。（C′=Set${\mathcal{C}}^{\prime }=\mathbf{S}\mathbf{e}\mathbf{t}$ でない限り）住んでいる世界が違うのです。

うん知ってる。

で、誰もそんな圏論における一般的なMonadの話なんてしていないよね。

そもそも君が、

って、その -> っていうのは、圏論の射（Morphism）ではなくて、

HaskellのコードでHaskellのFunctorとMonadの定義である時点で、

集合の圏（Category of sets）

https://ja.wikipediaorg/wiki/%E9%9B%86%E5%90%88%E3%81%AE%E5%9C%8F

の範囲で書いたんでしょ？

つまり、この中級者は最初

集合の圏（Category of sets）

を大前提に書き出していた。

というか今は関数型プログラミングの話なんで、暗黙に集合の圏のはなしで、自分も、

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

と書いたけど、圏論の話なんてこういう中級者がマウンティングしてくる素材としてしかおおよそ機能なんてしておらず、関数型の本筋ではないのでこの記述にとどめている。

で、その上で、中級者は、

とか書いてる。これは、

集合の圏（Category of sets）でない限り

って書いてるということ。

いや今は、集合の圏だろうが？Haskellのコードをしょっぱなに出すってことはそこの暗黙の了解はあるんですよね？

何いってんの？となる。

非常に中級者の誤魔化しぽいです。

僕がここで正さなければ、こういうごまかしが通用して、自分の腐ったメンツを保つのと引き換えに、こちらの書いたものが間違いだというデマを流すのと同時に、多くの入門者をあざむくことになります。非常に悪質です。

モナドの数学的な定義にはHaskellの >>= に相当するものは含まれていないのです。なので、モナドのことを二項演算と呼ぶのは不適切だと考えます。

Haskellの>>=は集合の圏のモナドで、これは「数学的」なの。

そして、集合の圏に限らない「数学的」なモナドが、集合の圏に限る「数学的」なモナドと一致しないのはあたりまえ。

だからといって、集合の圏であることがデフォルトの関数型プログラミングで扱う範囲のモナドは二項演算である事実を否定する正当化にはなるわけがないでしょ。

実際さ、Haskellのモナド則においても、モナドの演算で二項演算の演算子としてしか使われてない状態で、これがモナドです、って説明されている現状があるわけだろう？

あれで、どこにこれは集合の圏に限る、とか、

strong monadと呼ばれる構造を持つモナドであればお馴染みの (>>=) :: m a -> (a -> m b) -> m b に相当するものが定義できます。

人の本にイチャモンつけたいばっかりに、自分が普段普通にやってる範囲の概念で、いや、集合の圏ではない限り、違う、とかめちゃくちゃゴネてくるじゃねーよ、って思う。

モナドの数学的な定義にはHaskellの >>= に相当するものは含まれていないのです。なので、モナドのことを二項演算と呼ぶのは不適切だと考えます。

Haskellの>>=は集合の圏のモナドで、これはもちろん「数学的」ではあるが、この中級者が考えてる概念はデタラメで、たとえば、最初、

って書いたら、

プログラミング言語におけるモナドはそういう二項演算を持つのは確かですが、数学的なモナドにはそういう二項演算はあるのでしょうか？それとも、Kenさんは数学的なモナドはどうでもいいという立場でしょうか？

— mod_poppo (@mod_poppo) December 10, 2021

と　

プログラミング言語におけるモナドはそういう二項演算を持つ

という事実はようやく認めた。

というよりも

モナド＝代数構造＝二項演算

となるのだから「そういう二項演算を持つ」という表現は間違いで、あんまりわかってないぽい。

そんでゴネる中級者にたたみかける。

monadとstrong monadの違いが、
「プログラミングのMonad」なるものと
「数学のMonad」なるものと
モナドが二項演算という説明とどう不整合あるいは整合があるのか、まとめてごまかさずに書いてみて？
はいどうぞ。

— ken (@ken80297274) December 10, 2021

すると、　

Haskellのやつは「プログラミング言語におけるモナド」ですね。関数が第一級であるからこそ>>=のような演算が定義できます。一方、数学的なモナド（一般の圏上のモナド）では射が内部化できるとは限らないので、一般には>>=のような演算は定義できません。

— mod_poppo (@mod_poppo) December 10, 2021

「関数が第一級であるからこそ>>=のような演算が定義できます」

ってTweetされた。

>Haskellのやつは「プログラミング言語におけるモナド」ですね。関数が第一級であるからこそ>>=のような演算が定義できます

意味不明。なにこれｗ

もう一点
「関数が第一級であるからこそ>>=のような演算が定義できます」

集合の圏において
「関数がFirstClassObject」ってどういう意味？

プログラミングの概念が数学に逆適用されて、なんか数学とプログラミングは異なる、みたいな、トンデモ理論を聞いているようにしか思えなけど説明どうぞ

— ken (@ken80297274) December 10, 2021

もちろん、説明などできるわけもなく、この中級者はこの質問についてはダンマリきめこんで無視を続けています。

なんで、Monadの定義に、プログラミング実装の

「関数がFirstClassObjectである」というスペックが混入してくるのか、わけがわからず、ああこの中級者はトンデモなんだな、っていうことを確認しました。

つづき

ken-okabe.hatenablog.com