#数楽 テストB→TBα↦η(α)(A→TB)→(TA→TB)ψ↦(α↦(α⇝x↦ψ(x)))T(A→B)→(TA→TB)φ↦(α↦(φ⇝f↦(α⇝x↦η(f(x))))(A→B)→(A→TB)f↦(x↦η(f(x)))

#数楽 テスト書き直しB→TBβ↦η(β)(A→TB)→(TA→TB)ψ↦(α↦(α⇝ψ))T(A→B)→(TA→TB)φ↦(α↦(φ⇝(f↦(α⇝ηf))))(A→B)→(A→TB)f↦ηf(A→B)=B^A=Hom(A,B)

#数楽 テスト(X→(Y→TZ))→(TX→(TY→TZ))ψ↦(α↦(α⇝x↦(β⇝y↦(ψ x y))))X=(A→B)、Y=A、Z=B、ψ=(f↦ηf)のとき、α⇝x↦(β⇝y↦(ψ x y))= α⇝f↦(β⇝x↦(η(f(x))))

#数楽 テストTX=P(X)べき集合η:X→P(X), η(x)={x}( )^#:(X→P(Y))→(P(X)→P(Y))Φ^#(A)=⋃_{a∈A}Φ(a)のとき、続く

#数楽 テスト 続きP(X→Y)→(P(X)→P(Y))Ψ↦(A↦⋃_{f∈Ψ}⋃_{a∈A}ηf(a))⋃_{f∈Ψ}⋃_{a∈A}ηf(a)=⋃_{f∈Ψ}f(A)以上は「monad⇒applicative」とその例。

#数楽 テストううむ。記号だらけで滅茶苦茶読み難いな。まるで暗号。suntax sugarはやはり大事ということか。でも砂糖をかけられちゃうと誤魔化された気分になることもときどきある。

#数楽 テスト続ける。(X→Y→Z)=(X→(Y→Z))共通T:(X→Y)→(TX→TY)η:X→TXapplicativeT(X→Y)→(TX→TY)T(X×Y→Z)→(TX×TY→TZ)…続く

#数楽 続きlax monoidalTX×TY→T(X×Y)TX×TY×TZ→T(X×Y×Z)…applicative⇒lax monoidalη(1_{X×Y})のT(X×Y→X×Y)→(T(X)×T(Y)→T(X×Y))による像。

#数楽 テスト続きlax monoidal⇒applicativeT(X→Y)×TX→T((X→Y)×X)と評価写像ev:(X→Y)×X→Yから得られるT(ev):T((X→Y)×X)→TYの合成。applicativeと直積をゆるく保つことは同値。

#数楽 テストなのにRTしているのは誰なんだろうか？

#数楽 テスト続きmonadbind:(X→TY)→(TX→TY)μ:TTY→TYbind⇒μX=Yのときμ=bind(1_{TY}):TTY→TYμ⇒bind(X→TY)→(TX→TY)f↦bind(f)=μ・Tfここで・は合成

#数楽 例：Kは体とする。TX=K[X]=(不定元の集合とみなされたXから生成されたK上の多項式環)のとき、μ:TTX→TXはK[K[X]]の中で不定元とみなされているK[X]の元に対応する多項式としてのK[X]の元を代入する自然な環準同型写像になる。

#数楽 もっと易しい例TX=(Xから生成される自由モノイド)このとき、Xが文字集合ならTXは文字列の集合になります。一般にはTXはXの元を要素に持つリストの集合になる。μ:TTX→TXは複数の文字列またはリストを連結する写像になります。一般に、代数系≈データ構造

#数楽 以上の話は完全に専門外の話なのでそのつもりで読んで下さい。普通に数学を知っていれば言える話しか書いていません。特別な「専門知識」を含まない話。

#数楽 例：Maybe monadTX=(Xのコピー)∪{Nothing}η:X→TXは包含写像。μ:TTX→TXはTXのコピーをTXに恒等的に移し(η(x)をxに移し)、TTXに付け加えられた2つ目のNothingをTXのNothingに移す。

#数楽 ググって見付けたHaskellの入門的解説を見ると、構文レベルの話と応用レベルの話と「それがどういうfunctor, applicative, monadなのか」に関する話が混合していて、私のようなタイプの人には滅茶苦茶わかり難いことが多い。抽象的に説明して欲しい(笑)。

#数楽 テスト続き例：Either monadX⊔Y=(XとYの非連結和)(X→Z)×(Y→Z)≅(X⊔Y→Z) 写像の定義域の非連結和X→X⊔Y、Y→X⊔Y 包含写像X⊔(X⊔Y)→X⊔YがX→X⊔Yと1_{X⊔Y}の定義域の非連結和で得られる

#数楽 テスト続き非連結和X⊔Yは包含写像η:Y→X⊔Yと上で定義した写像μ:X⊔(X⊔Y)→X⊔Yによって、Yに関してモナドとみなせる。