CCCと直和がどうのこうの

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

うまってた。。。 / モナド基礎勉強会 vol.2 xbase.connpass.com/event/11252/?u… #monadBase

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

CCCについて話す人って誰かいらっしゃったりするのかしら。 #monadBase [うさみみ＊´×｀＊エンジニア]

ちゅーん @its_out_of_tune

CCCの話聞きたい

NaOHaq(苛性ソーダ) @NaOHaq

@its_out_of_tune っ ccc.co.jp

ちゅーん @its_out_of_tune

違うそうじゃない

ちゅーん @its_out_of_tune

特にCCCの定義に直和が含まれないのが前からすごく気になってる。

みょん @myuon_myon

@its_out_of_tune 入れた方が良い理由はありますか？

ちゅーん @its_out_of_tune

@myuon_myon 単純に、Haskellの型システムに直和型が備わってるので、入っているほうが自然に感じてしまうレベルの話ではあります。

みょん @myuon_myon

@its_out_of_tune 単純な理由としては直和には直積と冪のような綺麗な随伴が作れないことが挙げられますかね

ちゅーん @its_out_of_tune

@myuon_myon なるほど。直積と直和は双対なので、まったく意味がないとは思えないのですが、CCCに直和を加えたような圏が議論される事は無いのです？

みょん @myuon_myon

@its_out_of_tune 圏が直積と直和をもちかつそれらが一致する時その概念を双積(biproduct)といいます。同様に0=1なる対象をzero objectといい、zero objectとbiproductをもちHomに群構造が入る圏をadditiveといいます。

みょん @myuon_myon

@its_out_of_tune additiveにさらに条件をつけたAbel圏はホモロジー代数では特に重要です。(これはCCCとはあんまり関係無いですが)

ちゅーん @its_out_of_tune

@myuon_myon 「それらが一致する時」というのがよくわからなかったです。 A×B=A+Bとなるような圏という事ですか？

みょん @myuon_myon

@its_out_of_tune そうです 直積が直和の図式になっていて逆も然りということです

みょん @myuon_myon

Ab-enrichedでzero objectとbirproductをもつって言うべきであった

みょん @myuon_myon

0と直和だけからいい感じにならないかと思ったけど hom(a,b+c) = hom(Fa,c) っていう時点で射の濃度が一致しそうにないから無理だろうなって感じ

ちゅーん @its_out_of_tune

@myuon_myon なるほど、zero objectとbiproductはわかりました。Homの群構造もちょっと考えればわかる気がします。ありがとうございます。

ちゅーん @its_out_of_tune

@myuon_myon 例えばHask圏ってCCC＋直和＋αな気がするのですけども、そう考えると関数型の型システムの話をするのにCCC＋直和のシンプルな圏を考えても良いんじゃないかなぁと思いまして。んで、twitter.com/its_out_of_tun… みたいな事言ってたわけです。

みょん @myuon_myon

随伴の構成は一般に難しいけど存在しないことを示すなら0とか1とか直積とか直和とかを代入してhomの濃度を見るのが楽

ちゅーん @its_out_of_tune

直感的にA+B=A×Bとなる圏と聞いて「ふえぇ？」ってなったんだけど、何もおかしい事は無かった。

みょん @myuon_myon

@its_out_of_tune 有限limitと有限colimitの存在を仮定することはよくあるのでそういう圏で重要なものにはまた別の名前がつくと思います Haskの話で言うなら冪とhomが一致するのが異常なのでCCCであることはおまけに近いのではないかと

みょん @myuon_myon

Haskellと随伴 qiita.com/myuon_myon/ite… 随伴の話なら前に書いたよ

みょん @myuon_myon

@its_out_of_tune 典型的な例としてはAbel群の圏やベクトル空間の圏です biproductの構成には「射同士が足し算できること」を使います

ちゅーん @its_out_of_tune

@myuon_myon ふむーん。

ちゅーん @its_out_of_tune

カリー・ハワード同型対応の話で、論理と型の間を取り持つのに直和はあったほうが良い気がするとか、未だに考えてしまう。多分考え方がエンジニアに寄り過ぎ。