関数型プログラミング言語Haskell Part34 (657ﾚｽ)
上下前次1-新
409: 2024/10/02(水) 09:24:29.51 ID:ZmuRtoMU(2/3)調 AAS
リスト関手から集合関手への自然変換も分かりやすい。
410: 2024/10/02(水) 10:25:28.13 ID:xCLOcr8o(1)調 AAS
すまん嘘を書いた
自然変換では無くリストの圏から集合の圏への関手だった
411: 2024/10/02(水) 10:27:20.94 ID:ZmuRtoMU(3/3)調 AAS
大文字列、小文字列も同様に間違い
412: 2024/10/02(水) 16:24:48.26 ID:H02uk4bf(1)調 AAS
>>402
ただの記号で表現したら「0の逆数」とかいう表現を禁止するのが難しい
ただの記号ではない方がベター
413(1): 2024/10/02(水) 20:27:37.99 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型を圏とみれば同じ。
可換にするのは面倒くさい上に効率悪いけど、そういう関手を作ろうと思えば作れる。
414(1): 2024/10/02(水) 20:45:45.19 ID:AFS53MaU(5/6)調 AAS
可換図にすると
Char（小文字）
⇗
Int ⇑toL ⇓toU
⇘
Char（大文字）
ここで、小文字→Int, 大文字→Intが作れればtoLower, toUpperを直接作らなくても、関手の合成で作れる。
415: 2024/10/02(水) 20:53:28.38 ID:4E8lSXKR(1)調 AAS
出番ですよ >>399
416: 2024/10/02(水) 21:03:02.82 ID:AFS53MaU(6/6)調 AAS
圏論の地平線でも書かれていたけど、圏論は直接的に役に立つというより、発想の転換の源泉になるそうな。
（なので、別に圏論分かったから偉いとかない）
417: 2024/10/02(水) 21:18:36.03 ID:JUMm5MLB(1/2)調 AAS
数学の研究には有用かも知れないが
プログラミングで
直接役に立つようなことはまず無い
418: 2024/10/02(水) 21:42:50.80 ID:Xrjxo4NT(1)調 AAS
どっ白け
419: 2024/10/02(水) 21:51:30.73 ID:OPLMo7z3(1/8)調 AAS
プログラミング言語もどんどん数学に寄せているし、上のカキコみたいにプログラムの記述を
そのまま数学的対象とみなせるように改造していってると思う。本来は別物と考えるべきだと思う。
数学の研究といってもプログラム意味論の研究で、プログラムを数学の世界に写像したら
どう表現できるかということを研究していると言えるんじゃないかと思う。
数学の世界には、式の評価途中に発生する副作用といった概念がないので、現実のプログラムを
そのまま数学の世界に移そうと思ってもできないことの方が多い。
計算効果を圏論的に表現できたというのは、そういうプログラミング言語の数学化の一端みたいな
もんだと思う。
420: 2024/10/02(水) 22:00:14.12 ID:YWEZQEUD(1/7)調 AAS
副作用ってどうでもよくね
Haskellとかだとそもそも副作用ないし
421: 2024/10/02(水) 22:12:34.31 ID:OPLMo7z3(2/8)調 AAS
現実のプログラムだと式を評価する途中で発生する副作用というのは普通だけれど、
これを表示的意味論、操作的意味論で数学の世界に写そうと思うと途端に難しくなる。
数学で式の途中に文字列をディスプレイに映し出す、みたいな概念はないから。
それを整理して副作用と呼んでも差し支えない概念を提唱してHaskellに実装しているんだよ。
実際、ＩＯモナドの圏論的定式みるとこれが副作用？という表式してる。
全部後回しにしてフラッシュするというアイディアみたい。副作用をプログラムの最終局面で
実行しているから、式の評価途中の参照透明性も壊さない。なるほど、って感じ。
422(2): 2024/10/02(水) 22:20:07.75 ID:sFAdPyYV(1)調 AAS
ID:OPLMo7z3 = ID:AFS53MaU 本人か同レベル
複おじってレベル
423(1): 2024/10/02(水) 22:24:19.37 ID:YWEZQEUD(2/7)調 AAS
途端に難しくなるか？
副作用のない計算に変換する手順が教科書に書いてあるはずだが？
424(3): 2024/10/02(水) 22:29:49.51 ID:OPLMo7z3(3/8)調 AAS
>>422
別の人。自分ならプログラムの記述を一回数学の世界に写すし。
>>423
副作用のある数学的関数ってある？
プログラム→数学
に変換するんだぜ。
副作用のない計算に変換する手順が数学の本に書いてあんの？
425: 2024/10/02(水) 22:43:26.42 ID:+kVmY7U4(1/3)調 AAS
>>424
別人とのことなので便乗
ID:OPLMo7z3 は ID:AFS53MaU が
> 大文字小文字の変換が自然変換になる事を(Haskellの例で)証明して
と問われて
>>413,414 を出してきたのは数学的証明だと思ってるの？
426: 2024/10/02(水) 22:46:45.28 ID:+kVmY7U4(2/3)調 AAS
>>424
或いはもっと直接的に、>>424は「大文字小文字の変換が自然変換」の真偽をどう考えているの？
427(1): 2024/10/02(水) 22:51:00.95 ID:OPLMo7z3(4/8)調 AAS
定義が何もないのに何も言えるわけないじゃん。
数学でこういうものを定義します、これをプログラムのこれこれと対応付けます。
てプロセスないじゃん。
428(1): 2024/10/02(水) 22:52:03.28 ID:YWEZQEUD(3/7)調 AAS
>>424
先に副作用のないプログラムに変換するって言ってるんですけど
Haskellなら最初から副作用がないからそのままでいいけど
プログラミング言語の理論の本ならどれにでも書いてないか？
429: 2024/10/02(水) 22:55:13.15 ID:+kVmY7U4(3/3)調 AAS
>>427
了解
>>422の指摘通りだと納得しました
430: 2024/10/02(水) 22:56:24.21 ID:OPLMo7z3(5/8)調 AAS
いや。プログラム意味論の本結構探し回ったけど副作用の記述は漠然としてて
扱えないわけじゃないらしいけど、具体的な変換なんて見たことない。
ちょうど伝統的なプログラム意味論で副作用どう扱われているか調べているんだ。
なんて本に書いてありましたか？
431: 2024/10/02(水) 23:02:49.62 ID:YWEZQEUD(4/7)調 AAS
どれにでも書いてあるだろ、whileプログラムをラムダ計算に変換する手順とか書いてないなんてことがあるわけがない
432: 2024/10/02(水) 23:06:08.21 ID:OPLMo7z3(6/8)調 AAS
なんだ。いや聞きたいのは入出力とかの副作用だよ。
433: 2024/10/02(水) 23:17:44.98 ID:YWEZQEUD(5/7)調 AAS
入出力なんて代入に比べたら自明だろ…
そんなのいちいち教科書に書くかよ
434: 2024/10/02(水) 23:26:30.50 ID:OPLMo7z3(7/8)調 AAS
書いてないのは自明だからではなくて、研究の方向性がどう転ぶかわからないからだと思う。
表示的意味論も出た当時の文献では副作用について語ってることが多い。
現代的な本になるほどD∞モデルつくってはいおしまいで数学的にきれいなところしかやらない。
435(1): 2024/10/02(水) 23:36:01.67 ID:JUMm5MLB(2/2)調 AAS
プログラムの仕様とその証明を数学で記述する本にあるだろうね。
436(1): 2024/10/02(水) 23:37:10.87 ID:YWEZQEUD(6/7)調 AAS
どこが非自明なのかさっぱりわからん
代入と違って入出力は垂れ流しだし、入出力は代入の特別な場合だろ
437: 2024/10/02(水) 23:46:11.64 ID:OPLMo7z3(8/8)調 AAS
>>435
ホーア論理とか公理的意味論か。いやそれはないな。あっても一般に適用できないし。
>>436
関数型プログラミングだとプログラムをλ式に対応させて、プログラムの実行をそのλ式の簡約に
対応させるというのが理想的なモデルとして想定されることが多いと思う。
でもλ式はλ項からλ項への対応でしかないから、λ項を値(value)と呼ぶとすると
value から valueへの数学的関数でしかない。これには入出力とかの副作用を表現する余地がない。
つまり、
入出力があるプログラム→value から valueへの数学的関数
という対応付けをすると、入出力という特徴が数学世界では失われてしまう。
という難問があった、けどモナドで一つ解答が出た。
438: 2024/10/02(水) 23:54:51.93 ID:YWEZQEUD(7/7)調 AAS
代入が書けるんだから、入出力なんて自明だろ…
こいつ何いってんだ…
439: 2024/10/03(木) 00:02:36.12 ID:B2Xmf+Xl(1/9)調 AAS
だから、入出力がある数学的関数なんてないだろって言ってんの。
数学的関数で入出力は非自明だと思うんだが。
440: 2024/10/03(木) 00:09:13.65 ID:B2Xmf+Xl(2/9)調 AAS
Haskellでいうと、
純粋関数は、λ式（valueからvalueへの数学的関数）
に対応付けられるけど、
IOモナド使ったプログラムは、その現実のプログラムが持つ特徴を表現できるλ式がないので対応付けられない
って言ってんの。
441: 2024/10/03(木) 00:21:32.37 ID:omgk7HiD(1)調 AAS
入出力なんてただの値のリストだろ…
442: 2024/10/03(木) 03:50:19.64 ID:KCHr29fD(1)調 AAS
圏論持ち出して愚にもつかないことをグダグダと…
それで何か効率良くなるならいいんだけど，何のメリットもないんだよね
443: 2024/10/03(木) 04:21:38.74 ID:zyXzLypu(1/6)調 AAS
圏論なんかより、遅延評価ならIOがwhnfの先頭に出てきたら実行すればいいって人類が気づいたのが本質なんじゃねーの
444: 2024/10/03(木) 08:29:58.17 ID:LNI2TnSo(1)調 AAS
最近の人類はseqのメリットを直接的に利用するコツに気づいとるんか
順調に進化しとるな
445: 2024/10/03(木) 14:31:37.97 ID:1wv2Oz28(1)調 AAS
コンパクトな言語仕様だが表現力は強力
数学をプログラミングに取り入れるメリットってまぁこんなもんでしかないでしょ
一方で静的に性質を決定しようとするやり方は一般的な人間の能力を簡単に超えてしまう
446: 2024/10/03(木) 16:46:40.39 ID:TkNlnb1D(1)調 AAS
急にポエマーだらけw
447: 2024/10/03(木) 19:56:29.70 ID:B2Xmf+Xl(3/9)調 AAS
入出力があるプログラムをどう数学的に整合する概念に対応させるかについて書いてみる。
こういう説明が通るものなのか興味があるし。
まず、仮想的なシェルスクリプト風の行番号付き手続き型言語を想定して、
その言語で入出力があるプログラムを定義するとする。
000 procedure prog1(int n) {
001 double res
002 （なにか込み入った計算）
....
020 echo "hogehoge"
021 （なにか込み入った計算）
....
050 echo "fugafuga"
051 （なにか込み入った計算）
...
100 return res }
このプログラムは実行 $(prog1) すると、行番号001版から順に評価していって複雑な計算をしつつ途中
hogehoge ← 行番号０２０の命令を評価
fugafuga ← 行番号０５０の命令を評価
と表示した上で、返り値 res を返す、という動作をする。
448: 2024/10/03(木) 19:57:08.78 ID:B2Xmf+Xl(4/9)調 AAS
現実のよくあるプログラムとはこういう感じのものだけれども、実行 $(prog1) をしてその結果が返ってくるという現実的に
必要な点だけを考えると、途中の行番号020を評価したとかそういう情報はいらなくて、結局 $(prog1) して
hogehoge
fugafuga
を表示して、複雑な計算の結果 res が返ってくれさえすればいいともいえる。
だったら、数学的に取り扱いがしづらい、式の評価途中で入出力が発生するみたいな部分を取っ払って
000 procedure prog2(int n) {
001 double res
002 （なにか込み入った計算）
....
020 ## echo "hogehoge" #コメントアウト
021 （なにか込み入った計算）
....
050 ## echo "fugafuga" #コメントアウト
051 （なにか込み入った計算）
...
100 return ("hogehoge"を表示する予約1、"fugafuga"を表示する予約2、返り値 res) }
というように、返り値の部分に全部まとめるということをするということが考えられる。こうしても、プログラムのユーザー側からすると
実行すると$(prog2)
hogehoge
fugafuga
と表示されて複雑な計算した結果 res が返ってくるということは変わらない。
449: 2024/10/03(木) 19:57:34.71 ID:B2Xmf+Xl(5/9)調 AAS
というわけで、入出力があるプログラムというのは、こういう返り値の部分というか評価の最終段階の部分に「入出力の予約情報と返り値の情報がまとめられたもの」だったんだ、と整理しよう。
ただ、こういう「入出力の予約情報と返り値の情報がまとめられたもの」と長い文で表すのはよろしくないので、何か名前を与えた方がいいということで
computationと呼ぶことにする。
そうすると、Haskellでいえば、
純粋関数は、valueからvalueへの数学的関数
に割り当てることができたけれど、
入出力付きのプログラムについては、valueからcomputationへの対応
に割り当てるということが数学的に正当化できそうだ、ということになるわけだ。
450: 2024/10/03(木) 20:00:39.07 ID:B2Xmf+Xl(6/9)調 AAS
訂正
computationというか、今でいう「入出力の予約情報と返り値の情報がまとめられたもの」を
数学的にうまく正当化するということが達成することができるのであれば、
入出力つきのプログラムを、valueからcomputationへの対応
に割り当てるということが正当化できるはずだ、と考えられる。
451: 2024/10/03(木) 20:23:28.46 ID:zyXzLypu(2/6)調 AAS
何言ってるのか全然わからん
ぶっちゃけ入力は関数の引数にして、出力は返り値にするように変換するだけでいいだろ
読み出し位置のカーソル管理が必要なら代入を使えばできるじゃん
452: 2024/10/03(木) 20:39:38.40 ID:B2Xmf+Xl(7/9)調 AAS
よくわかんないけど、そういう入出力プログラムがあったとする。
そしてそれを引数付きで実行することを考えると
$(prog n)
こうなる。ここで、引数の部分の n はプログラムの記述に属さないといけない。
なぜかというと現実世界の「入力」部分をそのまま引数のところには持ってこれないから。
引数部分を入力にするにしても、別途入力されたものをプログラムの変数に割り当てる概念
みたいなのが必要になるし、それは関数の引数だからということでは説明にならないと思う。
だから、少なくともprogの引数部分はvalueじゃないといけない。
453: 2024/10/03(木) 20:45:47.19 ID:zyXzLypu(3/6)調 AAS
ポエムすぎて意味わからん。値のリストはvalueじゃないと？
454: 2024/10/03(木) 20:59:58.72 ID:B2Xmf+Xl(8/9)調 AAS
値のリスト自体をそのまま持ってくればvalueということになるんだろうけれど、
$(prog n)
の実行結果として出てくるもので、計算効果の説明になるものであって、返り値の型を包含するもの
であればcomputationと判断せざるを得ないとかそういうことしか言えないです。
455: 2024/10/03(木) 21:11:15.46 ID:zyXzLypu(4/6)調 AAS
判断するって何言ってるの？
computationって定義は何なの？
ラムダ項を書き換えていく手続きが計算じゃないの？
456: 2024/10/03(木) 21:22:37.64 ID:B2Xmf+Xl(9/9)調 AAS
valueとcomputationの違いは微妙で$(prog n)の実行結果として出てくるかどうかとか
計算効果が発露しているかというところで見極めるしかない、と理解している。判断する
というのは専門用語としては使ってない。
computationの定義はまた微妙だけれど、$(prog n)の計算効果込みの実行結果みたいな概念。
最後は超個人的見解だけど、「λ項を書き換えていく行為」というのは、どういう方法で表現して
どういう方法で簡約していくか？というところが決まってない。λ計算じゃないけれど、
１＋１＝２
という計算を暗算でやるか、電卓でやるか、そろばんでやるかという違いを出しても計算することに
変わりない。
暗算でやると、脳内物質の分量が変わるし、電卓だと電位が変わる。そして、そろばんでやると
「ぱちぱち」という音が出る。
457: 2024/10/03(木) 21:30:24.72 ID:zyXzLypu(5/6)調 AAS
❌決まってない
⭕知らない
間違えるなよ
458: 2024/10/03(木) 21:31:19.82 ID:zyXzLypu(6/6)調 AAS
お前の脳内にしかないお花畑に巻き込むのやめてもらっていいですか？
459: 2024/10/03(木) 22:10:04.42 ID:/brOvmjG(1)調 AAS
おそらくメンタルヘルスに問題がある方なのかな？
自分の頭の中の映像をそのまま言葉にしたような感じを受ける
460(2): 2024/10/04(金) 05:46:29.14 ID:vLDssEdm(1/9)調 AAS
>>428
Haskellの副作用については2つの解釈がある。
１．副作用も含めてアクションという単位で値としてみる。
（アクションを受け取って、アクションを返す関数）
２．Haskellは指示書を発行しているだけで、実際に実行するのは数学（Hakell）の外だから、Haskellそのものには副作用が無い。
（（末尾にHaskellに値を返す形の）マシン語を返して、ハードウェアに実行してもらうと考えるアウトソーシング方式）
461(1): 2024/10/04(金) 05:52:21.21 ID:EogKDI3R(1/3)調 AAS
>>460
ようするに副作用はないってことじゃん
462(1): 2024/10/04(金) 05:57:16.46 ID:vLDssEdm(2/9)調 AAS
>>461
Javaは変数をクラスの外で作れないから、グローバル変数は存在しない。
けど、事実上のグローバル変数は作れてしまう。
ってのと、同じ。
アクションの中に副作用があろうが、マシン語を返していると解釈しようが、事実として副作用はある。
ただ、重要なのは副作用を伴っても参照透明性が保たれているってこと。
463: 2024/10/04(金) 06:07:02.79 ID:4jD3Hbcp(1)調 AAS
副作用が隔離できていることが大切
スレの基地外の隔離スレのように
464(1): 2024/10/04(金) 06:24:04.70 ID:EogKDI3R(2/3)調 AAS
>>462
それは例えばwhileプログラムから副作用のない言語に変換したあとの形式と同じ状態にすでになってるってことで、計算のルール上はもう副作用はないでしょ
465(1): 2024/10/04(金) 07:22:19.19 ID:vLDssEdm(3/9)調 AAS
>>464
そうなんだけど、結局普通のプログラミング言語を使ってる人にしてみれば屁理屈でしかない。
見た目そのままで伝えるなら、純粋関数型言語の定義のまんま、「副作用を伴っても参照透明性が保たれている」でいい。
466(1): 2024/10/04(金) 07:38:19.23 ID:EogKDI3R(3/3)調 AAS
>>465
まあそのほうがいいか
上の方にいた彼はなんか脳内にこだわりがあって、普通の型付きラムダ計算以上のことをやってると思ってるフシがあったね
467: 2024/10/04(金) 07:48:51.79 ID:vLDssEdm(4/9)調 AAS
>>466
そうそう。
副作用は無い！って、こっちが必死になって弁を述べれば述べるほど、屁理屈感が出てくる。
それよりは副作用を認めて、「副作用を分離」「副作用を伴っても参照透明性が保たれている」って言った方が、納得感がある。
468: 2024/10/04(金) 19:23:08.02 ID:tixO3LDq(1/22)調 AAS
とりあえず続きを書いてみる。
Haskellでいうところの
純粋関数は、valueからvalueへの数学的関数
入出力プログラムは、valueから（入出力）computationへの対応
に割り当てることで、数学上にプログラミング行為を写し出せそうだ、というところまで書いた。
ただ、やっぱり（入出力）computationって何？とか、valueと形式的にどう違うの？という疑問は拭い去ることができない。
そこでMoggiは、次のようなアイディアを２つ出して（結構ムリヤリに）疑問を解決した。
ただし、ここで入出力プログラム prog は A型の引数を取って（computationの整理をする前は）B型の返り値を返すとする。
469: 2024/10/04(金) 19:23:42.06 ID:tixO3LDq(2/22)調 AAS
Moggiのアイディア１
・返り値の型がBのcomputationは、何か型構築子をIOとすると、その型構築子を適用した型 IO B のvalueに対応する。
※Moggiの原理ともいう。
つまり、上で挙げた入出力プログラム prog の型は、具体的に A → IO B になると言っている。
IO B 型の実装で、入出力の予約だか、値のリストだか指示書だか表現はいろいろあるが、そういう機構を実装すれば、
prog :: A → IO B
は参照透過性を保ったまま入出力を行うプログラムになる。
もっと広がりが出そうなcomputation概念なのに、急に狭窄な感じがするアイディアだけれど、
実装と折り合いをつけるという観点からすると仕方ないともいえる。
なお、代数的効果のPlotkinとPowerが批判しているのはこのMoggiのアイディア１である感じがする（あんまわかってない）。
470: 2024/10/04(金) 19:24:13.18 ID:tixO3LDq(3/22)調 AAS
Moggiのアイディア２
・入出力プログラム（に対応する数学的概念）は、圏をなすはずだ。
Moggiのアイディア１の段階でもprog :: A → IO Bは参照透過性を保ったまま入出力を行うプログラムになるはずだが、
入出力プログラム同士の合成が考えられていない。入出力プログラム prog1、prog2と開発したら、できるだけ再利用するというのが
現実のプログラミングだと思う。わざわざprog1とprog2の合成として定義できそうなプログラムを得るために、イチイチいちから
開発するということを理論的に要請されるというのは不合理。
純粋関数は、λ式に割り当てられることになって、当然、圏をなすだろうに、
プログラムに割り当てられるものが圏を成さないというのはおかしい。
でも、入出力プログラムはMoggiのアイディア１から、
prog :: A → IO B
という特殊な返り値の型を持っているため単純な合成ができない。
471: 2024/10/04(金) 19:29:03.13 ID:tixO3LDq(4/22)調 AAS
Moggiのアイディア１の段階でcomputationの概念というのは解消してしまう。
PlotokinとPowerはそこが不満なんだろうか？
472(1): 2024/10/04(金) 20:18:31.78 ID:WSIC8Xt5(1/14)調 AAS
だから、副作用を隠してラムダ計算に変換する手続きは、世界をステートにする変換をした時点で達成されてるわけで、そんなの太古の昔から分かってたことだろ
IO aの定義読んでから出直せよ
473(1): 2024/10/04(金) 20:30:15.44 ID:SclsbEZF(1)調 AAS
日を跨ぐつもりならコテハンでも付けてくれんか
追えん
474(1): 2024/10/04(金) 20:44:30.01 ID:tixO3LDq(5/22)調 AAS
>>472
だからそれはわかっているって。評価途中では実際の入出力はせず指示書だか値のリストだけ作成して
参照透過性を保証して、参照透過性が要求されなくなったプログラムの最終段階でリストに従って
入出力を実行するような仕組みがあれば、参照透過性を保ったまま入出力はできるという話でしょ。
それを数学的にどう正当化するかという話を書いているんだって。
>>473
水曜日あたりからだからそんな分量ないよ。
475: 2024/10/04(金) 20:49:17.68 ID:WSIC8Xt5(2/14)調 AAS
>>474
どこが正当化されてないのか意味不明なんだけど
ていうか正当化って何？
476(1): 2024/10/04(金) 20:51:48.70 ID:tixO3LDq(6/22)調 AAS
だから、入出力がある数学的関数なんてないじゃん。
入出力があるプログラムを数学的に表現しようと思っても詰むからどうしようって話。
477: 2024/10/04(金) 20:57:28.69 ID:6lZW+X9H(1/3)調 AAS
こんなところで長文書くのはやめてもろて
読む価値があるものならzennとかnoteに書けば？
関数型言語界隈の人たちがクソミソにレビューしてくれるよ
478(2): 2024/10/04(金) 20:58:08.93 ID:WSIC8Xt5(3/14)調 AAS
>>476
型付きラムダ計算の時点で数学的に表現されてるだろ…
意味不明すぎる
479(2): 2024/10/04(金) 21:00:48.64 ID:qBjLuAvO(1/2)調 AAS
メインの入力とメインの出力は数学にもある
主じゃないやつを副作用といってる
480(1): 2024/10/04(金) 21:11:30.04 ID:tixO3LDq(7/22)調 AAS
>>478
なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。
でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？
>>479
よくわかんない。具体的に言うとどういうのある？
481: 2024/10/04(金) 21:11:31.21 ID:tixO3LDq(8/22)調 AAS
>>478
なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。
でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？
>>479
よくわかんない。具体的に言うとどういうのある？
482: 2024/10/04(金) 21:18:24.66 ID:WSIC8Xt5(4/14)調 AAS
>>480
アセンブルって何？
後半も何言ってるのかちゃんと分かるように書いて
483: 2024/10/04(金) 21:25:06.50 ID:WSIC8Xt5(5/14)調 AAS
そうだよ、こんなとこじゃなくてzennとかに煽った感じのタイトルつけて炎上する記事書いてコメントもらって来いよ
484(3): 2024/10/04(金) 21:28:05.10 ID:tixO3LDq(9/22)調 AAS
λ計算を機械語とかアセンブラと見立てて、λ計算ですべて数学世界を組み立てれば、
入出力がある数学的関数も定義できるだろうから、あえて数学的正当性なんて与えようとする
理由がわからない、ということだろうと思った。
プログラムの部分は全てλ計算で組み立てれば完全に同じものが作れると思っているということ
だけれども、じゃあ文字列をディスプレイに表示するというプログラムの構成要素である
ディスプレイはハードウェア部分だけれども、それはλ計算で組み立てるという範疇にはいるんですか？
入らないなら、なにか数学的概念を持ち出してきてそれに対応付けるということをしないといけないんじゃ
ないですか？
という趣旨のことを書いた。
485: 2024/10/04(金) 21:33:15.17 ID:tixO3LDq(10/22)調 AAS
これ読んだらわかるけどMoggi論文の読書感想文。いまさらの。
匿名以外でいまさら突っ込んでくるわけないじゃん。
486: 2024/10/04(金) 21:33:16.29 ID:tixO3LDq(11/22)調 AAS
これ読んだらわかるけどMoggi論文の読書感想文。いまさらの。
匿名以外でいまさら突っ込んでくるわけないじゃん。
487: 2024/10/04(金) 21:34:24.07 ID:qBjLuAvO(2/2)調 AAS
関数の「型」を見ろ
入力が何で出力が何かが宣言されている
488: 2024/10/04(金) 21:39:26.17 ID:tixO3LDq(12/22)調 AAS
>>484
ディスプレイに表示するまでの概念はよく考えたら既存の例でもなかったわ。
焦って変なこといったスマン。
ちょっと説明を考える。
489: 2024/10/04(金) 21:39:59.29 ID:WSIC8Xt5(6/14)調 AAS
>>484
意味不明すぎる
ラムダ計算は数学的に正当化されてるだろ
例えば合流性があるとか数学的に証明されてる
これのどこに非数学的要素があるんだって言ってるんだよ
すでに数学的な説明がされてるものに対して、数学的に正当化されてないとか言うのやめろよ
490(1): 2024/10/04(金) 21:48:55.49 ID:tixO3LDq(13/22)調 AAS
λ計算が数学的に正当化されてないというような話はしてなくて、
現実のプログラムをλ計算に反映させようと思っても入出力とか非決定計算の部分は表現しきれない
そのλ計算からはみ出す部分をどう正当化させようかという話。
491(1): 2024/10/04(金) 21:52:13.21 ID:WSIC8Xt5(7/14)調 AAS
>>490
じゃあHaskellは純粋にただの型付きラムダ計算なんだから、数学的に正当化されてない部分などない
おしまい
492(1): 2024/10/04(金) 22:03:12.33 ID:tixO3LDq(14/22)調 AAS
>>491
うーん。例えば、数学は集合論上で展開されているから、集合論があればその上で展開される
解析学とか、線形代数学とかいらない、みたいな論法じゃない？
この現象は、解析学でモデル化できるけれども、解析学は集合論上で展開できるから、
そんなモデル化はいらなくていちいち集合論の言葉で書けばいいじゃん的な。
みんなそこに興味あるわけじゃないと思いますよ。
493(1): 2024/10/04(金) 22:08:30.14 ID:vLDssEdm(5/9)調 AAS
>>484
横からというか >460 書いた者だけど、あなたの疑問は解釈1の「アクションを受け取ってアクションを返す関数」だとざっくりし過ぎて納得いかないって感じでしょうか？
でしたら、解釈2では納得出来ませんでしょうか？
解釈２は、モナドの効能の一つに追加して「数学の世界にアウトソーシングという概念を持ち込む」というものです。
モナドの例えとして、床下配線というのがありますが、MaybeやListの様な通常のモナドも、>>=の中に関数適用部分を押し込んで、表から見えないようにしています。
（これも、見ようによってはアウトソーシングです。同じ数学の世界なので、隣の席に頼んだ感じですが）
IOモナドは、>>=の中すら見えない状態で関数適用しているわけですが、 >460 でも書いたとおり、「数学の外（ハードウェア）」で関数適用されていると考えるわけです。
IOモナドの>>= は、外の世界と遣り取りする受付窓口というわけですね。
（実際、バッファの様な振る舞いをします）
main = do x <- return 0
_________x <- return (x + 1)
_________print x
494(1): 2024/10/04(金) 22:14:36.08 ID:WSIC8Xt5(8/14)調 AAS
>>492
ラムダ計算も集合論上で展開されてるだろ
だから、Haskellも集合論の言葉で書かれてるじゃん
そんな誰もが分かってるけど、いちいち書いても何の得もないことを話したかったの？
495: 2024/10/04(金) 22:16:42.74 ID:vLDssEdm(6/9)調 AAS
この場合、IOモナドを使って変数ｘを書き換えているのではなく、シャドーイングによって同じｘという名前の変数を新しく作って、古い x に +1 した値を束縛しています。
496(1): 2024/10/04(金) 22:21:54.69 ID:tixO3LDq(15/22)調 AAS
>>493
ごめんなさい。全然違う。入出力を題材にしているのはあくまで例で別に疑問はないです（実装をちゃんと知っているわけではないですが）。
モナドを導入する動機はMoggi論文読んだ読書感想文なので途中まで書いてますが、圏をなすかどうかです。
497: 2024/10/04(金) 22:27:08.92 ID:vLDssEdm(7/9)調 AAS
無理やりハードウェアも数学と言い張るなら、ハードウェアもチューリングマシンという計算モデルなので数学が元と言えなくはない？
そういうこじつけは置いておいても、IOモナドをアウトソーシングと考えると、じゃあ外の世界はめちゃくちゃか？と考えて、そうではないと気付く。
ハードウェアも一定の秩序がある。
数学だけが全てではないのかもしれない。
何かしらの秩序というか、法則性を持った世界（数学、数学以外含む）どうしのやり取りにモナドが橋渡しとして働いているのでは？とか、考えたりする。
498(1): 2024/10/04(金) 22:28:17.05 ID:tixO3LDq(16/22)調 AAS
>>494
モナドの原論文（Moggiの論文）の読書感想文を入出力の計算効果を題材に解説してみているんだって。
ブログに書いても今更突っ込むなんて恥ずかしいことができる人はいるわけないので、ここに書いている。
499(1): 2024/10/04(金) 22:32:08.56 ID:WSIC8Xt5(9/14)調 AAS
>>498
その人はHaskellは数学的に正当化されてないけしからんって言ってたの？
500(1): 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
>>496
少なくともコマンド系のプログラムは圏をなしますね。
Haskellで作ると実感しますが、Haskellに限らず、
（ユーザーから見て）プログラムそのものが関数になります。
Linuxでコマンドをパイプライン処理するのは関数（射の）合成に相当しますし。
id相当のプログラムは作れますし。
・・・と考えると圏をなすと思うのですが。
（GUIプログラムもボタン単位とかで関数と言えますが、合成は…押した順序？）
例えば
{(x,2x+1) | x ∈ R} と 2x+1のグラフは同型だと直感的に分かりますが、その関数（射）は数式で表せません。
圏論では、可換図を受け取って可換図を返すとか出てきますので、{(x,2x+1) | x ∈ R} と 2x+1のグラフを結ぶ関数（射）が人間って言うのも有かな？とか、考えます。
（圏論では同型と分かれば（証明できれば）よくて、射の中身には言及しない）
503: 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: 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
>398 じゃ答えにならない？
508: 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: 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: 2024/10/04(金) 23:22:52.03 ID:WSIC8Xt5(14/14)調 AAS
>>511
お前が言い出したんだろ
513: 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: 2024/10/05(土) 00:27:27.96 ID:aeHKoAMv(1/3)調 AAS
集合と写像の区別がついてないんだから、何を準備しようが時間の無駄
516: 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: 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): 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: 2024/10/05(土) 11:23:42.68 ID:KE+ltgGd(2/2)調 AAS
どうでもいいけど計算科学のside effect→副作用は誤訳だと思う
薬学のside effectは「随伴作用」（副作用）だけど計算科学のside effectは「側面作用」って感じ
521(1): 2024/10/05(土) 11:40:17.86 ID:gdCH0E84(1)調 AAS
圏論のコンコルド効果について。
Haskellのコーティングの質をあげようと、
一生懸命頑張って勉強したのに実はほとんど役に立たない…
「大量の時間と労力を学習したのに悔しい！」
そのことを認めることができず、懸命に圏論のプログラミングでの有用性を力説し、学習布教に努める。
522(1): 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可能
523: 2024/10/05(土) 13:51:21.32 ID:2BBo/yBe(1/2)調 AAS
数日程度で成果を出す戦略を採用したにもかかわらず何年も戦争が続く
こういうのは圏論に限定されない現象だ
順序を入れかえたら結果が変わる
数日後の情報が今ここに伝わるならそれは時間軸とは言えないぞ
524: 2024/10/05(土) 14:41:11.81 ID:hOtauQiF(1)調 AAS
>>522
IO a >>= (a -> IO b) -> IO b
は
(IO a >>= (a -> IO b)) -> IO b
であって
IO a >>= ((a -> IO b) -> IO b)
にはならないよ
(>>=)は演算子
525: 2024/10/05(土) 15:10:26.09 ID:u1hwkRNd(1)調 AAS
圏論の話題出すなよ
Haskellで何か書くにあたって利益があるわけじゃないんだから
526: 2024/10/05(土) 15:30:46.49 ID:2BBo/yBe(2/2)調 AAS
利益は道徳よりも軽い
これも、未来予知ができなければ利益を計算できないことに原因がある
527(1): 2024/10/05(土) 17:25:54.13 ID:JByJwyk5(2/4)調 AAS
>>521
役に立つなら、もっと色々入ってるかと…。
私はむしろHaskellより圏論そのものに興味の対象が移って、Haskellは圏論の概念を実際に動かしてみるための道具に成り下がってますね＾＾；
とはいえ、数学の知識不足なので群論やらトポロジーやらあっちこっち読み漁りながらなので、歩みは遅いですが…。
528(1): 2024/10/05(土) 20:22:21.95 ID:J2mQEu2j(1)調 AAS
>>527
面倒でも一般位相の基本、ホモロジーの初歩…と地道にやるのをおすすめします
529(2): 2024/10/05(土) 20:30:18.78 ID:aeHKoAMv(2/3)調 AAS
集合と写像の区別もついてないんだから、集合と位相からやらないとだめ
530(2): 2024/10/05(土) 22:07:16.25 ID:JByJwyk5(3/4)調 AAS
>>528
ありがとうございます。
手探りだったので、助かります。
重点的に勉強してみます。
（高卒にどこまで理解できるか…）
>>529
一応、区別付いてるつもりなのですが…。
指摘していただければ調べてみます。
531: 2024/10/05(土) 22:16:56.83 ID:aeHKoAMv(3/3)調 AAS
>>530
あー上で暴れてた人とは別人だったのね
でも、集合と位相は何をやるにしても必要だから頑張ってね
532(1): 2024/10/05(土) 23:30:55.73 ID:bPGp2ASj(1)調 AAS
>>373=396=530 っぽいから言うと、(数学に関して)「分かった」「理解した」の自己基準が不安しかない
> ほら、分かってみれば「なーんだ。そんなことか」でしょ？
> なるほど、って感じ。
と自分に言い聞かせていても、ポピュラーサイエンス書感覚で読んだってダメ
他人との議論では、逆に「こいつ分かってないな」と思われるだけだからな
533: 2024/10/05(土) 23:50:06.63 ID:JByJwyk5(4/4)調 AAS
>>532
独学ですしね＾＾；
こいつ分かってないなと思われても良いですよ？
それで指摘されたものも新しい知識になるので。
どうも定義を読むだけじゃイメージ湧かないので、ネット上や数学書の複数の例え話が全て真だと仮定して、共通の特徴からイメージを掴むパターンが多いんです。
534: 2024/10/06(日) 01:53:03.98 ID:6zQjUfx4(1/3)調 AAS
いま正常性バイアスを理解した
全て正常だと仮定する
なるほど
535(1): 2024/10/06(日) 10:54:18.58 ID:jCq2z3ec(1/2)調 AAS
本来Haskell使う上で必要のない数学の知識をかじらされるのかわいそう
こうやって無駄に間口狭めてなんの意味があるんだか
上下前次1-新書関写板覧索設栞歴
あと 122 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ
ぬこの手 ぬこTOP 1.144s*