随伴とカリー化とStateモナド

ちゅーん @its_out_of_tune

復習

ちゅーん @its_out_of_tune

関手F:C→DとG:D→Cを考える

ちゅーん @its_out_of_tune

c∈C, d∈Dとして、Hom_D(Fc→d) とHom_C(Gd→c)が同型である時、FをGの左随伴であるという。

ちゅーん @its_out_of_tune

ヲ級ちゃん可愛い

ちゅーん @its_out_of_tune

で、

ちゅーん @its_out_of_tune

あ、ちげぇ

ちゅーん @its_out_of_tune

訂正。c∈C, d∈Dとして、Hom_D(Fc→d) とHom_C(c→Gd)が同型である時、FをGの左随伴であるという。 こうか。

Jun Inoue @jun0inoue

@its_out_of_tune その同型射が c, d について自然、も追加

dif_engine @dif_engine

@its_out_of_tune Gを左にどっこいしょするとFになるときにFをGの左随伴と呼ぶ、とすると覚えやすい予感

ちゅーん @its_out_of_tune

で、F=(-)×A、G=(-)^Aとした時、Hom_D(c✕A→d) とHom_C(c→d^A)は同型になる。即ちcurryはuncurryの左随伴である。

ちゅーん @its_out_of_tune

で、良くわかってないんだけど、F○Gはモナドのreturnに相当するのだそうだ(´・ω・`)

ちゅーん @its_out_of_tune

また逆だorz

ちゅーん @its_out_of_tune

G○F

ちゅーん @its_out_of_tune

で、先ほどのカリー化の例で考えると、G○F=((-)✕A)^Aとなる。これがまさにStateモナドのrunState:s→(a,s)

ちゅーん @its_out_of_tune

このsにRealWorldを取ったのが、IOモナド。という事らしい(´・ω・`)

ちゅーん @its_out_of_tune

た、多分あってる(´・ω・`)

ちゅーん @its_out_of_tune

復習終わり(´・ω・`)なんとな〜く随伴わかってきたと思う。

ちゅーん @its_out_of_tune

なんかJoinはもーちょいわからん感じだった、GFGFcからGFcへの射が一意に定まるという話だけど…

ちゅーん @its_out_of_tune

とりあえず、Stateの定義が何で出てくんのかってのは思ってたけど、前提知識としてさっきのがあり、目の前にHaskellがあれば、そりゃやって見るよね、という話では在る。けど、RealWorldを状態に持たせちゃえば良いじゃんというアイディアはやっぱクレイジーだと思う。