圏論的プログラミング生活の勧め 1


前置き

今回は、完全にネタだと思って構いませんが、出来る限り分かりやすい説明を心がけたいと思います。

ま〇かマ〇カに例えてみる

まず、圏論を説明するのに一番都合の良い状態を示します。

dom --(f)-- x
            |
           (g)
            |
            y --(h)-- cod

圏の説明

このような単純な関数と値の関係を整理したものを 圏 と呼びます。

dom と書いたのは、始まりの値の事を言います (始域)ドメイン
cod は終わりの値です。 (終域)コドメイン

射の合成

そして、この状態は、実はとても都合がよく f g h を合成した状態を作り出すことが出来ます。

この時、然るべき掛け算の法則が、各々の関数にはあることを覚えておくと便利だと思います。

なので、関数は基本的に合成順序に関わらず、以下のような取り換えが可能です。

(f . g) . h === f . (g . h)

そして合成すると、何が起こるでしょうか?

答えは…

僕と契約して、魔法少女に殺されようよ(笑)

あれ?途中のストーリなし?

関手と自然変換

では、その上の図全体を括弧でくくり、それをCとします。

C --(F)-- D
  \       |
   \      |
   (Nat) (G)
      \   |
       \  |
          E

ここで、まず気が付いて欲しいのが、大文字になったってことです。

関手(Functor)は高階関数

Fには、CからDへ圏を計算して移すために必要な無名関数が取られます。
下のjavascriptのコードは、それが根拠です。

//F:C -> D
let D = C.map(d => d + 5);

そして、このような図の時に圏を説明する場合、の書き方は、

C = Hom(dom, cod)

というように書くみたいです。
こうすることで、原因と目的と結果が整理して書けるようになってきます。

自然変換は、関手を引数に取る高階関数

Natが示す線を自然変換と呼んでいます。
Natは、FとGの合成だとは限りません。
よって、

Nat(F, G)

となる場合の関係を示す関数の事を、自然変換と呼んでいるにすぎません。

本当の数学を知ってほしい

本当の数学は、算数で計算することではありません。
数学の構造すらも、自己言及的に証明することこそが、正に数学なのです。

気が向いたら、また投稿します。
それでは~