-
- いいね！0
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト書き直し 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)
2017-02-03 23:41:16
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト (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))))
2017-02-03 23:57:37
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト TX=P(X)べき集合 η:X→P(X), η(x)={x} ( )^#:(X→P(Y))→(P(X)→P(Y)) Φ^#(A)=⋃_{a∈A}Φ(a)のとき、 続く
2017-02-04 00:12:59
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト 続き P(X→Y)→(P(X)→P(Y)) Ψ↦(A↦⋃_{f∈Ψ}⋃_{a∈A}ηf(a)) ⋃_{f∈Ψ}⋃_{a∈A}ηf(a) =⋃_{f∈Ψ}f(A) 以上は「monad⇒applicative」とその例。
2017-02-04 00:15:59
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト ううむ。記号だらけで滅茶苦茶読み難いな。まるで暗号。suntax sugarはやはり大事ということか。でも砂糖をかけられちゃうと誤魔化された気分になることもときどきある。
2017-02-04 00:19:37
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト続ける。 (X→Y→Z)=(X→(Y→Z)) 共通 T:(X→Y)→(TX→TY) η:X→TX applicative T(X→Y)→(TX→TY) T(X×Y→Z)→(TX×TY→TZ) … 続く
2017-02-04 00:40:37
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き lax monoidal TX×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)) による像。
2017-02-04 00:48:03
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト続き lax monoidal⇒applicative T(X→Y)×TX→T((X→Y)×X)と評価写像ev:(X→Y)×X→Yから得られるT(ev):T((X→Y)×X)→TYの合成。 applicativeと直積をゆるく保つことは同値。
2017-02-04 00:56:11
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト続き monad bind:(X→TY)→(TX→TY) μ:TTY→TY bind⇒μ X=Yのとき μ=bind(1_{TY}):TTY→TY μ⇒bind (X→TY)→(TX→TY) f↦bind(f)=μ・Tf ここで・は合成
2017-02-04 01:19:50
黒木玄 Gen Kuroki
@genkuroki
#数楽 例：Kは体とする。 TX=K[X]=(不定元の集合とみなされたXから生成されたK上の多項式環)のとき、μ:TTX→TXはK[K[X]]の中で不定元とみなされているK[X]の元に対応する多項式としてのK[X]の元を代入する自然な環準同型写像になる。
2017-02-04 01:29:03
黒木玄 Gen Kuroki
@genkuroki
#数楽 もっと易しい例 TX=(Xから生成される自由モノイド) このとき、Xが文字集合ならTXは文字列の集合になります。一般にはTXはXの元を要素に持つリストの集合になる。μ:TTX→TXは複数の文字列またはリストを連結する写像になります。 一般に、代数系≈データ構造
2017-02-04 01:45:03
黒木玄 Gen Kuroki
@genkuroki
#数楽 以上の話は完全に専門外の話なのでそのつもりで読んで下さい。普通に数学を知っていれば言える話しか書いていません。特別な「専門知識」を含まない話。
2017-02-04 01:47:32
黒木玄 Gen Kuroki
@genkuroki
#数楽 例：Maybe monad TX=(Xのコピー)∪{Nothing} η:X→TXは包含写像。 μ:TTX→TXはTXのコピーをTXに恒等的に移し(η(x)をxに移し)、TTXに付け加えられた2つ目のNothingをTXのNothingに移す。
2017-02-04 02:21:28
黒木玄 Gen Kuroki
@genkuroki
#数楽 ググって見付けたHaskellの入門的解説を見ると、構文レベルの話と応用レベルの話と「それがどういうfunctor, applicative, monadなのか」に関する話が混合していて、私のようなタイプの人には滅茶苦茶わかり難いことが多い。抽象的に説明して欲しい(笑)。
2017-02-04 02:29:15
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト続き 例：Either monad X⊔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}の定義域の非連結和で得られる
2017-02-04 08:18:03
黒木玄 Gen Kuroki
@genkuroki
#数楽 テスト続き 非連結和X⊔Yは包含写像η:Y→X⊔Yと上で定義した写像μ:X⊔(X⊔Y)→X⊔Yによって、Yに関してモナドとみなせる。
2017-02-04 08:57:09
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き 「抽象的な説明」について Haskellの入門的解説をググって読むと、構文レベルの話(場合によっては単なるsyntax sugarの話)と応用の話と「それがどのような函手であるか」などなどの異なる事柄をすべてミックスした説明になっていて、私には分かり難い。続く
2017-02-04 10:22:52
黒木玄 Gen Kuroki
@genkuroki
#数楽 「抽象的」話の続き もっと抽象的に説明してくれればわかりやすいのになと思うことが個人的には多い。これはあくまでも私個人の問題なのですが、「抽象的」という言葉を使ったせいで誤解されることが多いので補足させて下さい。続く
2017-02-04 10:26:14
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。期待していることは、構文の詳細、実装の詳細、応用の詳細によらずに理解できることをざくっと解説してくれることである。いきなり完璧な理解は無理なので逐次近似的な理解を目指したいのですが、第0近似として「抽象的な説明」＝「実装の詳細によらない説明」があるとありがたいのだ。
2017-02-04 10:28:33
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。構文のスタイルを変えても、実装の仕方を変えても、応用先を変えても変わらない基本的な考え方を知りたい。それを一言で「もっと抽象的に説明して欲しい」と言っているのだ。これは「抽象」という言葉の意味的にも正しい言い方だと思います。続く
2017-02-04 10:32:11
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。まとめ：抽象的な説明によって、構文のスタイル、実装の仕方、応用先などなどを変えても変わらない基本的な考え方を説明してもらうことができれば、「どのように細かいことを気にしなくてもよいか」がわかって、逐次近似的な理解の出発点になる「第0近似」が得られる。
2017-02-04 10:36:06
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。数学の解説でも「どのように細かいことを気にしなくてもよいか」が不明瞭な説明は多いと思う。私もよくやってしまう。 これは個人的な意見なのだが、特に「他人によって与えられた定義から出発する」という発想になるとどんどんつらくなることが多いと思う。続く
2017-02-04 11:09:12
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。定義の背景にある考え方もしくは頭の使い方を理解することによって、定義から出発する必要が無くなるようにしないと、覚えなければいけないことが次々に増えて、自分の能力の限界を超えて永久に理解できない気持ちに陥る場面が増えると思う。
2017-02-04 11:14:44
黒木玄 Gen Kuroki
@genkuroki
#数楽 @beyondDNS usi-pl.github.io/lc/sp-2015/doc… をありがたくダウンロードしました。 ついでにリンクメモ disi.unige.it/person/MoggiE/… Moggiさんの有名なモナド論文(1989)
2017-02-04 13:41:26