関数型プログラミング言語Haskell Part34 (667ﾚｽ)
上下前次1-新
395: 2024/10/01(火)21:38 ID:Ig6Tf0ue(2/2) AAS
圏論をやりたいならまず代数学をやるべき
それだけでだいぶ見通しが違う
396(1): 2024/10/01(火)21:42 ID:4kH314XL(1/3) AAS
>>390
モナドの効用で自分の把握してるのは
・数学やHaskellの様な遅延評価の場合、逐次処理を表現できる
（これは変数を使いまわさない場合は、関数合成で十分だが、変数を使いまわすときはモナドじゃないと使いまわせない）
・副作用のある関数を使っても参照透明性は保たれている
・モナドは入れ物前提の概念なので、空の状態を使って例外処理をまとめることができる
正直、普通のプログラミング言語にも役立ちそうな3つ目は実感はしてないけど、ネットで例外処理よりモナドの方が優秀っぽい記事を読んだ
省2
397(1): 2024/10/01(火)22:05 ID:4kH314XL(2/3) AAS
圏論全体だと…当たり前のことを構造として研究してるだけなので、圏論というよりはHaskellの型クラスとの合わせ技で関手（Functor）の方がfmap的なのを他の言語にも導入すれば役に立つかも
圏論の関手を一言で言えば（関数も含めた）型変換
（Hakellだと入れ物前提にすることで、関数ごと型変換を実現。本来はもっと柔軟）
自然変換は一言で言えば単位変換とか、大文字小文字の変換
398(1): 2024/10/01(火)22:16 ID:4kH314XL(3/3) AAS
モノイドは条件が結合法則だけなので、ほぼ結合法則そのものがモノイド
（その割には繰り返しとか数え上げに現れる構造）
そしてモナドも構造はそっくりなので、入れ物前提のモノイドとも考えられる
（モナドの再帰はループ処理でスタックを消費しないし、数え上げは逐次処理と考えられる）
399(2): 2024/10/01(火)23:08 ID:KbL1rq/V(2/2) AAS
バグを無くすこと自体が目的になりがちなのが数学とプログラムなんだよね
真の目的のため、デバッグを二の次にするやつが正しいと言われても・・・
それって証明とかあるんですか
400(1): 2024/10/01(火)23:21 ID:syLuNokt(1/2) AAS
>>397
大文字小文字の変換が自然変換の部分kwsk
>>399
目的と手段を区別したら、手段は二の次だと言うのは予選敗退者のポエム
401: 2024/10/01(火)23:25 ID:syLuNokt(2/2) AAS
>>396
> 2番目もマルチスレッドとか最適化には役に立ちそうではある
それもう一人のsimonが取り組んだけどモナドは否定された
402(1): 2024/10/02(水)05:35 ID:OAhBXB+m(1) AAS
やっぱり数学的に表現してみただけってことか
まぁ実際のプログラミングに利益はないわな
403(1): 2024/10/02(水)07:50 ID:AFS53MaU(1/6) AAS
>>400
よくよく考えたら特別な事じゃないんだけど、普通のプログラミング言語でも大文字・小文字の変換関数を自作するってなったら、文字をInt型に変換して処理する。
それって文字の圏で直接大文字小文字の変換するを作れない場合、一旦整数の圏を経由する関数を作る。
A(a) → B(a)
↓ ↓
A(A) → B(A)
可換図のA(a) → B(a)の逆射が作れれば、B(a) → B(A)が作れる。
ほら、分かってみれば「なーんだ。そんなことか」でしょ？
404: 2024/10/02(水)07:53 ID:AFS53MaU(2/6) AAS
この場合、整数同士の足し算に対応する、文字同士の足し算が作れる。
（ただし、整数と文字列で集合の大きさを合わせる必要がある。0－25とか1－26とかで循環する集合）
405: 2024/10/02(水)07:55 ID:AFS53MaU(3/6) AAS
んで、プログラマーはいちいち集合を合わせないで、エラー処理だったり循環リスト作ったりで対応するわけだぬ。
406: 2024/10/02(水)08:30 ID:VSz9kg2E(1) AAS
数学の圏論テキストではカリー化の操作は良く使うが、カリー化の名前を付けて引用することはまず無いね。
407(1): 2024/10/02(水)08:47 ID:wonXK6QE(1) AAS
>>403
大文字小文字の変換が自然変換になる事を(Haskellの例で)証明して、と言う話
(自然変換が何かは分かっているで、直感的に違うと思ったから訊いた)
408: 2024/10/02(水)09:21 ID:ZmuRtoMU(1/3) AAS
大文字の文字列の型から小文字の文字列の型への変換と考えると簡単
409: 2024/10/02(水)09:24 ID:ZmuRtoMU(2/3) AAS
リスト関手から集合関手への自然変換も分かりやすい。
410: 2024/10/02(水)10:25 ID:xCLOcr8o(1) AAS
すまん嘘を書いた
自然変換では無くリストの圏から集合の圏への関手だった
411: 2024/10/02(水)10:27 ID:ZmuRtoMU(3/3) AAS
大文字列、小文字列も同様に間違い
412: 2024/10/02(水)16:24 ID:H02uk4bf(1) AAS
>>402
ただの記号で表現したら「0の逆数」とかいう表現を禁止するのが難しい
ただの記号ではない方がベター
413(1): 2024/10/02(水)20:27 ID:AFS53MaU(4/6) AAS
>>407
圏論の自然変換だと文字コード前提じゃないので、[0..25] = ['a'..'z'] = ['A'..'Z']ってする。
んで、大文字と小文字は同じ文字の圏、[0..25]は自然数の圏とする。
lCharToInt c = (length.takeWhile (c /=)) ['a'..'z'] -- 小文字からIntへの変換（関手）
uCharToInt c = (length.takeWhile (c /=)) ['A'..'Z'] -- 大文字からIntへの変換（関手）
toLChar = (['a'..'z']!!) -- Intから小文字への変換（関手）
toUChar = (['A'..'Z']!!) -- Intから大文字への変換（関手）
mytoLower = toLChar.uCharToInt -- 大文字から小文字への変換（自然変換）
mytoUpper = toUChar.lCharToInt -- 小文字から大文字への変換（自然変換）
でも、普通のプログラミング言語のtoLower, toUpperも、Char型を圏とみれば同じ。
省1
414(1): 2024/10/02(水)20:45 ID:AFS53MaU(5/6) AAS
可換図にすると
Char（小文字）
⇗
Int ⇑toL ⇓toU
⇘
Char（大文字）
ここで、小文字→Int, 大文字→Intが作れればtoLower, toUpperを直接作らなくても、関手の合成で作れる。
415: 2024/10/02(水)20:53 ID:4E8lSXKR(1) AAS
出番ですよ >>399
416: 2024/10/02(水)21:03 ID:AFS53MaU(6/6) AAS
圏論の地平線でも書かれていたけど、圏論は直接的に役に立つというより、発想の転換の源泉になるそうな。
（なので、別に圏論分かったから偉いとかない）
417: 2024/10/02(水)21:18 ID:JUMm5MLB(1/2) AAS
数学の研究には有用かも知れないが
プログラミングで
直接役に立つようなことはまず無い
418: 2024/10/02(水)21:42 ID:Xrjxo4NT(1) AAS
どっ白け
419: 2024/10/02(水)21:51 ID:OPLMo7z3(1/8) AAS
プログラミング言語もどんどん数学に寄せているし、上のカキコみたいにプログラムの記述を
そのまま数学的対象とみなせるように改造していってると思う。本来は別物と考えるべきだと思う。
数学の研究といってもプログラム意味論の研究で、プログラムを数学の世界に写像したら
どう表現できるかということを研究していると言えるんじゃないかと思う。
数学の世界には、式の評価途中に発生する副作用といった概念がないので、現実のプログラムを
そのまま数学の世界に移そうと思ってもできないことの方が多い。
計算効果を圏論的に表現できたというのは、そういうプログラミング言語の数学化の一端みたいな
もんだと思う。
420: 2024/10/02(水)22:00 ID:YWEZQEUD(1/7) AAS
副作用ってどうでもよくね
Haskellとかだとそもそも副作用ないし
421: 2024/10/02(水)22:12 ID:OPLMo7z3(2/8) AAS
現実のプログラムだと式を評価する途中で発生する副作用というのは普通だけれど、
これを表示的意味論、操作的意味論で数学の世界に写そうと思うと途端に難しくなる。
数学で式の途中に文字列をディスプレイに映し出す、みたいな概念はないから。
それを整理して副作用と呼んでも差し支えない概念を提唱してHaskellに実装しているんだよ。
実際、ＩＯモナドの圏論的定式みるとこれが副作用？という表式してる。
全部後回しにしてフラッシュするというアイディアみたい。副作用をプログラムの最終局面で
実行しているから、式の評価途中の参照透明性も壊さない。なるほど、って感じ。
422(2): 2024/10/02(水)22:20 ID:sFAdPyYV(1) AAS
ID:OPLMo7z3 = ID:AFS53MaU 本人か同レベル
複おじってレベル
423(1): 2024/10/02(水)22:24 ID:YWEZQEUD(2/7) AAS
途端に難しくなるか？
副作用のない計算に変換する手順が教科書に書いてあるはずだが？
424(3): 2024/10/02(水)22:29 ID:OPLMo7z3(3/8) AAS
>>422
別の人。自分ならプログラムの記述を一回数学の世界に写すし。
>>423
副作用のある数学的関数ってある？
プログラム→数学
に変換するんだぜ。
副作用のない計算に変換する手順が数学の本に書いてあんの？
上下前次1-新書関写板覧索設栞歴
あと 243 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.025s