Hちょびよみ勉強ノート(8回目)

代数的データ型と圏論の導入の導入。

代数的データ型

代数的データ型Xとは

X <- A + B

A + Bっていうのは集合Aと集合の重複の無い和との事。

┌── X───┐
│┌─┐┌─┐│
││ A││B ││
│└─┘└─┘│
└──────┘

javaで言うところのenumみたいなもの。
ただしJavaでは

enum X { // 型
  A, // 値
  B; // 値
}

だけど、代数的データ型では

 X  <- A   +  B
(型)  (型)   (型)

との事。

   -> (match, unapply Eitherをパターンマッチで分解する的な?)
 X   A  +  B
   <- (コンストラクタ eitherA = Left(a) みたいな事?)

圏論の導入の導入

今までの数学

  1. 集合(型)
  2. 集合と集合の対応(関数)
  3. 集合の元(値)

でいろんなことを考えるけど、圏論

  1. 対象(object, なんかしらのモノ)
  2. 射(対象と対象との間の関数)

でいろんなことを考えるらしい。
ざっくり言うと集合は対象、対応は射に対応していて、従来の数学と違うのは「元」と言う言葉を利用する事(言及すること)を禁止しているところとの事。
要するに集合の構成要素に触れないのでより抽象的(強い)ということっぽい。

圏論で「整数には足し算がある」という事を言う

Zを整数としたとき

「a, b ∈ Z に対して a + b ∈ Z が計算できる」(これが足し算だ)

↓が

「関数 add : Z × Z -> Z が存在する」(addが足し算だ。元a, bに対する言及が消えた)

こうなる。
しかし、足し算を言いたいときには「0を足しても変わらない」ということも言わないとダメ。

0 + a = a + 0 = a (a ∈ Z)

でもこれだと元(aとか0とか)が見えてるのでダメ

「0という特別な値がある」

「zeroと言う関数があるということにすればいいのでは??」*1

zero : 0Z -> Z が一つだけ必ず存在する*2
( 0Z = {0}, Z = {0, ±1, ±2 ...} と言うイメージ )


ぐるぐるのやつで足し算と言う計算を言う?

Z × Z  -> Z (最初に出てきた式)

Z × Z  -> Z

0Z × Z -> Z(0と計算しても変わらない的なことを言いたいやつ)

 Z × Z  -> Z
    / (行き先同じなのでまとめた)
0Z × Z 

    (ここがadd関数)
 Z × Z  -> Z
    /
0Z × Z

          add
   Z × Z  -> Z
※↑   /
  0Z × Z

※ここの関数は?
左側: 0Z -> Z -> zero関数だこれ
右側: Z  -> Z -> id関数(素通りさせるだけのやつ)だこれ
-> zero × id

                 add
          Z × Z  -> Z
zero × id↑   / right(左無視して右側を常に選ぶ)
         0Z × Z

可換図式っていうのは矢印の方向に歩くならどのルート通っても結果は同じになるらしいので

right = add ○ (zero × id) // 関数合成

が成り立つらしい。

具体的な元を当てはめて確かめてみると

                0 + a
                  ->
     (0,a)       add  a
          Z × Z  -> Z a
zero × id↑   / right
         0Z × Z
     (0,a)

矛盾ないっぽいので、Zには足し算という演算があるよ、と言えるらしい。

まとめ

この先Functorとか出てくるので道具立ての意味で圏論のさわりのさわりみたいな話聞いたけどまだ完全にフワッフワしています

*1:詐欺っぽいよねって言ってました

*2:一意に、とか存在する、とか可換、とかいう言葉は使っていいらしい