関数型プログラミング言語Haskell Part34 (691ﾚｽ)
上下前次1-新
459: デフォルトの名無しさん [sage] 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
>>428428(1): デフォルトの名無しさん [sage] 2024/10/02(水) 22:52:03.28 ID:YWEZQEUD(3/7) AAS
>>424
先に副作用のないプログラムに変換するって言ってるんですけど
Haskellなら最初から副作用がないからそのままでいいけど
プログラミング言語の理論の本ならどれにでも書いてないか？
Haskellの副作用については2つの解釈がある。
１．副作用も含めてアクションという単位で値としてみる。
（アクションを受け取って、アクションを返す関数）
２．Haskellは指示書を発行しているだけで、実際に実行するのは数学（Hakell）の外だから、Haskellそのものには副作用が無い。
（（末尾にHaskellに値を返す形の）マシン語を返して、ハードウェアに実行してもらうと考えるアウトソーシング方式）
461(1): デフォルトの名無しさん [sage] 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: デフォルトの名無しさん [sage] 2024/10/04(金) 06:07:02.79 ID:4jD3Hbcp(1) AAS
副作用が隔離できていることが大切
スレの基地外の隔離スレのように
464(1): デフォルトの名無しさん [sage] 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): デフォルトの名無しさん [sage] 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): デフォルトの名無しさん [sage] 2024/10/04(金) 20:18:31.78 ID:WSIC8Xt5(1/14) AAS
だから、副作用を隠してラムダ計算に変換する手続きは、世界をステートにする変換をした時点で達成されてるわけで、そんなの太古の昔から分かってたことだろ
IO aの定義読んでから出直せよ
473(1): デフォルトの名無しさん [sage] 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: デフォルトの名無しさん [sage] 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: デフォルトの名無しさん [sage] 2024/10/04(金) 20:57:28.69 ID:6lZW+X9H(1/3) AAS
こんなところで長文書くのはやめてもろて
読む価値があるものならzennとかnoteに書けば？
関数型言語界隈の人たちがクソミソにレビューしてくれるよ
478(2): デフォルトの名無しさん [sage] 2024/10/04(金) 20:58:08.93 ID:WSIC8Xt5(3/14) AAS
>>476
型付きラムダ計算の時点で数学的に表現されてるだろ…
意味不明すぎる
479(2): デフォルトの名無しさん [sage] 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: デフォルトの名無しさん [sage] 2024/10/04(金) 21:18:24.66 ID:WSIC8Xt5(4/14) AAS
>>480
アセンブルって何？
後半も何言ってるのかちゃんと分かるように書いて
483: デフォルトの名無しさん [sage] 2024/10/04(金) 21:25:06.50 ID:WSIC8Xt5(5/14) AAS
そうだよ、こんなとこじゃなくてzennとかに煽った感じのタイトルつけて炎上する記事書いてコメントもらって来いよ
上下前次1-新書関写板覧索設栞歴
あと 208 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.025s