関数型プログラミング言語Haskell Part34 (692ﾚｽ)
上下前次1-新
498(1): デフォルトの名無しさん [] 2024/10/04(金) 22:28:17.05 ID:tixO3LDq(16/22) AAS
>>494494(1): デフォルトの名無しさん [sage] 2024/10/04(金) 22:14:36.08 ID:WSIC8Xt5(8/14) AAS
>>492
ラムダ計算も集合論上で展開されてるだろ
だから、Haskellも集合論の言葉で書かれてるじゃん
そんな誰もが分かってるけど、いちいち書いても何の得もないことを話したかったの？
モナドの原論文（Moggiの論文）の読書感想文を入出力の計算効果を題材に解説してみているんだって。
ブログに書いても今更突っ込むなんて恥ずかしいことができる人はいるわけないので、ここに書いている。
499(1): デフォルトの名無しさん [sage] 2024/10/04(金) 22:32:08.56 ID:WSIC8Xt5(9/14) AAS
>>498
その人はHaskellは数学的に正当化されてないけしからんって言ってたの？
500(1): デフォルトの名無しさん [sage] 2024/10/04(金) 22:34:04.82 ID:WSIC8Xt5(10/14) AAS
最低限、論文に書いてある正しいこととお前の妄想がはっきり区別できるように感想文を書けよ
501(1): デフォルトの名無しさん [] 2024/10/04(金) 22:44:05.60 ID:tixO3LDq(17/22) AAS
>>499
はっきりそうは言ってない。
プログラムをλ項に対応させて単純化させると、valueからvalueへの全域関数となるけれど、
そう考えると、非停止性とか非決定性、副作用といった現実のプログラムにある特徴が失われる（だからそれを何とかしようと読める）。
>>500
そんなことできるほど力量ないです。
502: デフォルトの名無しさん [] 2024/10/04(金) 22:46:51.98 ID:vLDssEdm(8/9) AAS
>>496496(1): デフォルトの名無しさん [] 2024/10/04(金) 22:21:54.69 ID:tixO3LDq(15/22) AAS
>>493
ごめんなさい。全然違う。入出力を題材にしているのはあくまで例で別に疑問はないです（実装をちゃんと知っているわけではないですが）。
モナドを導入する動機はMoggi論文読んだ読書感想文なので途中まで書いてますが、圏をなすかどうかです。
少なくともコマンド系のプログラムは圏をなしますね。
Haskellで作ると実感しますが、Haskellに限らず、
（ユーザーから見て）プログラムそのものが関数になります。
Linuxでコマンドをパイプライン処理するのは関数（射の）合成に相当しますし。
id相当のプログラムは作れますし。
・・・と考えると圏をなすと思うのですが。
（GUIプログラムもボタン単位とかで関数と言えますが、合成は…押した順序？）
例えば
{(x,2x+1) | x ∈ R} と 2x+1のグラフは同型だと直感的に分かりますが、その関数（射）は数式で表せません。
圏論では、可換図を受け取って可換図を返すとか出てきますので、{(x,2x+1) | x ∈ R} と 2x+1のグラフを結ぶ関数（射）が人間って言うのも有かな？とか、考えます。
（圏論では同型と分かれば（証明できれば）よくて、射の中身には言及しない）
503: デフォルトの名無しさん [sage] 2024/10/04(金) 22:50:56.01 ID:WSIC8Xt5(11/14) AAS
>>501
なんでラムダ項に対応させると全域関数になるわけ？ラムダ計算は停止しない計算も表現できるモデルでしょ
言ってることが意味不明なんだよ
504(1): デフォルトの名無しさん [] 2024/10/04(金) 22:52:29.23 ID:tixO3LDq(18/22) AAS
ただの圏じゃなくてクライスリ圏じゃないといけない（Moggiのアイディア１から）。
そして、クライスリ圏を定義するためにはクライスリ・トリプル（モナド）がいる
505: デフォルトの名無しさん [] 2024/10/04(金) 22:52:30.15 ID:tixO3LDq(19/22) AAS
ただの圏じゃなくてクライスリ圏じゃないといけない（Moggiのアイディア１から）。
そして、クライスリ圏を定義するためにはクライスリ・トリプル（モナド）がいる
506: デフォルトの名無しさん [sage] 2024/10/04(金) 22:54:07.35 ID:WSIC8Xt5(12/14) AAS
そもそもラムダ項は関数ではないし、集合ではあるということはできるけど、それは自然数1は集合であるみたいな話でそれに意義なんてないよ
507: デフォルトの名無しさん [] 2024/10/04(金) 23:02:32.42 ID:vLDssEdm(9/9) AAS
>>504
>398398(1): デフォルトの名無しさん [] 2024/10/01(火) 22:16:21.15 ID:4kH314XL(3/3) AAS
モノイドは条件が結合法則だけなので、ほぼ結合法則そのものがモノイド
（その割には繰り返しとか数え上げに現れる構造）
そしてモナドも構造はそっくりなので、入れ物前提のモノイドとも考えられる
（モナドの再帰はループ処理でスタックを消費しないし、数え上げは逐次処理と考えられる）
じゃ答えにならない？
508: デフォルトの名無しさん [sage] 2024/10/04(金) 23:02:43.19 ID:6lZW+X9H(2/3) AAS
流石にこれじゃ関数型界隈の人達にボコボコにされて終わるね
やめといた方がいい
509(1): デフォルトの名無しさん [] 2024/10/04(金) 23:04:12.66 ID:tixO3LDq(20/22) AAS
βη簡約するとλ項が別の簡約されたλ項になる。この対応関係を数学的関数とみなせると言ってると解釈してる。
510: デフォルトの名無しさん [sage] 2024/10/04(金) 23:12:30.87 ID:WSIC8Xt5(13/14) AAS
>>509
みなせるって何？
ようするにラムダ項は関数じゃないってことでしょ当たり前だけど
511(1): デフォルトの名無しさん [] 2024/10/04(金) 23:14:09.18 ID:tixO3LDq(21/22) AAS
全域関数となる理由はわからん。全域関数＝数学的関数ということを言いたいんだろうと思ってたけどそこから詰めてなかった。
512: デフォルトの名無しさん [sage] 2024/10/04(金) 23:22:52.03 ID:WSIC8Xt5(14/14) AAS
>>511
お前が言い出したんだろ
513: デフォルトの名無しさん [sage] 2024/10/04(金) 23:30:08.11 ID:6lZW+X9H(3/3) AAS
これがワードサラダか
514: デフォルトの名無しさん [] 2024/10/04(金) 23:41:03.02 ID:tixO3LDq(22/22) AAS
すまんね。準備不足だったわ。詰めるところわかったし、
詰めるところ詰めることができたらひっそりどっかに書くことにするわ。
いろいろコメント参考になったわ。
515: デフォルトの名無しさん [sage] 2024/10/05(土) 00:27:27.96 ID:aeHKoAMv(1/3) AAS
集合と写像の区別がついてないんだから、何を準備しようが時間の無駄
516: デフォルトの名無しさん [sage] 2024/10/05(土) 07:57:53.70 ID:jwoAd9Km(1/2) AAS
ZFでは集合しか無いから。写像だろうが、自然数だろうが何でも集合。全てを集合で実装する世界。
517: デフォルトの名無しさん [] 2024/10/05(土) 08:14:37.65 ID:JByJwyk5(1/4) AAS
圏論は逆で、対象（集合で言う元）を恒等写像と同一視して全てを射（写像）として扱うね。
518: デフォルトの名無しさん [sage] 2024/10/05(土) 08:53:09.61 ID:jwoAd9Km(2/2) AAS
対象Aに対しA=id_Aとする圏の定義は、射のクラスの上での全域的で無い結合的2項演算⚪︎を持つ代数系としての簡潔な定式化。この定義では圏には射しかなくて、対象とは恒等射の別名に過ぎない。
ただ、この圏の実装は入門者には分かり難い。
Aが圏Cの対象であることを古い文献はA in Ob(C)と書くことが多いけど、最近の文献はA in Cと書いてしまう。fが圏Cの射f:A --> Bなことはf in Hom_C(A,B)かf in Mor_C(A,B)。
519(1): デフォルトの名無しさん [sage] 2024/10/05(土) 10:51:32.56 ID:KE+ltgGd(1/2) AAS
普通のλはどの順序で適用しても同じ計算結果になる（Church-Rosserの定理）けど
副作用を伴うλは適用順序が入れ替わると副作用の順序も変わって同じ結果とは言えなくなるから
順序を保証する仕組みとしてモナドが応用されてるはず
IO a >>= (a -> IO b) -> IO b
は(a -> IO b)が(IO a)を受け取れないから
(IO a)からaを取り出せるところまで計算しないと(a -> IO b)を適用できない
仮に
IO a -> (IO a -> IO b) -> IO b
みたいな形だと(IO a)の計算を保留したまま(IO a -> IO b)を適用できる
圏論はよく分からないけど
圏Aに便宜的な時間軸をつけたA_t0, A_t1, A_t2, …を用意して関手
A_t0 → A_t1, A_t1 → A_t2, …
を作るとA_t0, A_t1…は全部AのクローンだからA_t0 → A_t1, …は自己関手になって
その自己関手の集合がなんやかんやでモナドに相当するみたいなイメージ
520: デフォルトの名無しさん [sage] 2024/10/05(土) 11:23:42.68 ID:KE+ltgGd(2/2) AAS
どうでもいいけど計算科学のside effect→副作用は誤訳だと思う
薬学のside effectは「随伴作用」（副作用）だけど計算科学のside effectは「側面作用」って感じ
521(1): デフォルトの名無しさん [sage] 2024/10/05(土) 11:40:17.86 ID:gdCH0E84(1) AAS
圏論のコンコルド効果について。
Haskellのコーティングの質をあげようと、
一生懸命頑張って勉強したのに実はほとんど役に立たない…
「大量の時間と労力を学習したのに悔しい！」
そのことを認めることができず、懸命に圏論のプログラミングでの有用性を力説し、学習布教に努める。
522(1): デフォルトの名無しさん [sage] 2024/10/05(土) 13:16:57.88 ID:AoKf42Y0(1) AAS
>>519
異なる順序でreductionする方法がある場合は、どの順序でreductionしても同じ結果になるだろ？
IO a >>= (a -> IO b) -> IO bなら当たり前だけど(a -> IO b) -> IO bをa -> IO bに先にreduction可能
上下前次1-新書関写板覧索設栞歴
あと 170 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.018s