前回に続き、関数、値、圏論、モナド、評価戦略、純粋関数型、その辺りの「数学的基礎」を教えるの圏論について言及している部分について、内容を検証していきます。
「数」というものは、
数と論理操作が、まったく同一である、ということ、
「数」そのものが無限に自分を参照して自分自身となっている構造、
無限自己参照構造体とも表現できる「何か」です。
誤りです。圏論で扱うトピックではありません。
この非常に精緻な構造をガチで語ろうとするのが圏論なんですね。
まあだから、圏論の圏の定義とかどうでも良いです。
誤りです。むしろ圏論から定義をとると何も残りません。
今わたしがこうやって話したことを
難しい言葉で表現すると、
..以下略..
wikipediaの引用ですが、正しい内容です。
「数」というものは、
数と論理操作が、まったく同一である、
操作と数、数と操作の区別が一切ないっていう構造、
「数」そのものが無限に自分を参照して自分自身となっている構造、
無限自己参照構造体とも表現できる「何か」です。
誤りです。圏論で扱うトピックではありません。
数っていうのが何か？っていう本質的議論こそが「圏論」です。
誤りです。圏論で扱うトピックではありません。
って、数の本質を語ること＝圏論を語ることと同値なんです。
誤りです。
数と操作の区別なんてない、同じものだ、
それを論じるのが圏論で、
誤りです。
プログラミングの「ことば」、論理的にはまったく同じものを
勝手に違う言葉でいってるだけなんですが、言い換えると、値と関数の区別なんてない、同じものだ、
ってことになります。
誤りです。圏論の適用による結果ではありません。
関数型プログラミングの根本である「集合写像」の数学概念が、
そのままコンピュータによる計算という「物質化」にそのまま当てはめることが不可能であるから、
より「集合写像」をより抽象化した「圏論」をもってその
「計算」＝「物質化」を扱う必要があるということですね。
抽象化した、という記述は正しい内容です。圏論を利用する動機については誤りです。
を完全に論理的対象として扱えるようにした解決策としての「圏論」の具現化するならば、
実装は遅延評価でなければいけないし、遅延評価と不可分です。
誤りです。「a program is NOT a mapping」の解決策がモナドです。また、遅延評価にする必要はありませんし、圏論とは無関係です。
この圏論の導入は、
コンピュータのプログラミングが、
真に数学的と一致するような目的、
真に宣言的に記述できるようにするために導入されたのであり、
圏論を導入したコードというのであれば、宣言的にかけてアタリマエなんです。
誤りです。これは圏論ではなく、モナドを意味論に採用する理由です。
先行評価なら無限なんて宣言的に書けないんだから、そんなもんは圏論の実装ではない、ってことだし、
誤りです。遅延評価と圏論は無関係です。
純粋関数型を圏論が数学的基礎にあると語りながら、
純粋関数型と圏論は無関係です。Haskellが圏論の概念を多用しているだけに過ぎません。
これは、まさに圏論のことに他なりませんから、
遅延評価と圏論に関連はないため、誤りです。
IOモナドの理論的背景は圏論だ、ってことになります。
moggiの論文を元に実装されたものですから、正しい表明です。
ここまでの訳注
論理に対する記述は、圏論と直接関係があるわけではないので言及を避けています。
著者が頻繁に主張している「関数とは値」は、型無しラムダ計算のことを指していると考えられます。圏論の文脈ではCCCに $X \simeq X^X$ の同型を入れて作れますが、少なくともHaskellの理論的背景になっていません。
次回以降に続きます。