代数的データ型はF-始代数的データ型

もーひずむ @yuwki0131

@public_ai000ya すみません。。間違いですね。。。Cons a (List a)は直和ではなく直積です。

テクノショック @karrym_

@public_ai000ya F代数の始対象aでF(a)~=aが成り立ってFの最小不動点になるので再帰的なデータ(リストや木)の定義に使えるという感じかと

もーひずむ @yuwki0131

@public_ai000ya 「NilはF始代数における始対象」も「NilはF始代数における始対象からの任意の射」です。。。

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya F(X)=1+Xなら1→X←Xという構造を対象として類似の1→A←Aな対象の間で可換となるような図式を射とする。 するとF(X)=1+XのF代数における始代数は自然数型になる。 Aを固定してF(X)=1+Aとすると始代数はMaybe A型でF(X)=1+A*XならAのリスト型。

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya データ型を組み合わせて新たな型を作る事と1→X←Xみたいなセットを決める事がほぼ対応するんだと思います。 似たような構造を持つ物の中で始対象は何かというとそれがデータ型で、そのような複合型を引数にとる関数が1→A←A(この関数の返値)みたいなF代数との間の射(可換図)。

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya 始代数の場合は帰納的データ型になってて構成的に値を考える。 つまりzeroはNatでNatなnがあるならsucc nもNat。 終余代数だと余帰納的データ型になってて破壊的？に考える。 つまりこいつがNatなら皮を剥いて中からNatなnが出てくるか剥けなきゃzeroだ、と。

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya そのため、始代数の場合は構成するので有限の自然数や有限のリスト有限の木になるけど、終余代数の時はどうやって作るかではないので剥ける限り延々剥くことができてしまうので無限リストや無限の広がりのある値が考えられる。 余談だけどHaskellではこの区別はしてないという理解。

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya なぜ代数と言うのだろうか？ F:C→Cの関手としてF代数とはFA→Aの射のこと。 Aを台集合と呼ぶ。 例えば自然数と加算の代数(Nat,+)はFA=A*AとFh=h*hの代数。 こう言われると分かりやすかった。

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya まさに代数だった。 FA→Aは閉じてる演算でFの形によって代数構造はマチマチだけど代数の始対象とか終対象に鎮座してるのは計算ではなく型であるってことで、いかにデータ型が重要かがわかる気がする。

あいや🐕 @public_ai000ya

@yuwki0131 Nilが射なんですか！？

あいや🐕 @public_ai000ya

@karrym_ なるほど、そこがFの最小不動点っていうんですね……

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 F(X) = 1 + A がMaybe Aだ……というのは、FがMaybeで1がNothingでAが……なんだろ？？

cutsea110 @cutsea110

@yuwki0131 @public_ai000ya リストであればfoldrが始代数から他の代数への一意な射で、こいつの引数はまさに帰納的というか構成的で、終余代数から他の余代数への射はunfoldrだけど、こいつの引数なんかはまさに剥いてみて(破壊してみて)どうか？と振り分けてるのか型に現れてるんじゃないかと思ったり。

cutsea110 @cutsea110

@public_ai000ya @yuwki0131 Aは固定してるのでIntならJust 3とか

cutsea110 @cutsea110

@public_ai000ya @yuwki0131 FがMaybeというよりFはこのような代数構造で、1→X←Aなパターンのやつを対象とみなす。 そいつらの準同型を射とみなす。 そういう圏における始対象Xにあたる者はなにか？それがMaybe A型だね。 ということです。多分。

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 あ！ もしかして data Maybe a = Nothing | Just a というデータ型と F(X) = 1 + A というF-代数的構造が一致している、という感じですか？

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 ここの「射」って、F-代数準同型写像f f : X -> A F(f) : 1 -> 1 ですか？ α : 1 -> X, β : 1 -> Aがあると、可喚になると思うのですが。

cutsea110 @cutsea110

@public_ai000ya @yuwki0131 g T ← FT h↓ ↓ Fh A ← FA f という図式でh.g = f.FhとなるとF準同型ですかね. 1 → X ← X をパタンと両側閉じ合わせてやると X← 1 + X となってこれが X ← FX と見るわけですが.

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 ！？ 1 -> X <- X を「閉じ合わせる」ことができるんですか？

cutsea110 @cutsea110

@public_ai000ya @yuwki0131 あーいや単に書き方の問題だと思ってください. でも射や合成の定義を合わせれば別に問題ないというだけです. 1+Xから1+Aへの射の部分がFhつまり1+hになるので1のときはそのままパスしてXの時にはhに適用するようなのを射と見做すだけです. そう特別な操作をしてるわけでなく.

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 1+hはつまりF(h)ですか？

cutsea110 @cutsea110

@public_ai000ya @yuwki0131 g T ← FT h↓ ↓ Fh A ← FA f ここでF(X)=1+XとなるF代数を考えている場合には. Fh=1+hです.

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 あれ、もしかしてFTはF(T)ではなかったりしますか？

cutsea110 @cutsea110

@public_ai000ya @yuwki0131 すみません. カッコ付けたり付けなかったりしてます. 同じものを意味しています. その辺り結構適当です.

あいや🐕 @public_ai000ya

@cutsea110 @yuwki0131 ありがとうございます、直感まで落とし込めました！ data Maybe a = Nothing | Just a 固有の値（値構築子）を消してやると、ちょうど F(X) = 1 + X になってるところまで直感が追いついてきた。 圏論の意味に落とし込むぞー