関数型プログラミング言語Haskell Part34 (667ﾚｽ)
関数型プログラミング言語Haskell Part34 http://mevius.5ch.net/test/read.cgi/tech/1639713446/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
452: デフォルトの名無しさん [] 2024/10/03(木) 20:39:38.40 ID:B2Xmf+Xl よくわかんないけど、そういう入出力プログラムがあったとする。 そしてそれを引数付きで実行することを考えると $(prog n) こうなる。ここで、引数の部分の n はプログラムの記述に属さないといけない。 なぜかというと現実世界の「入力」部分をそのまま引数のところには持ってこれないから。 引数部分を入力にするにしても、別途入力されたものをプログラムの変数に割り当てる概念 みたいなのが必要になるし、それは関数の引数だからということでは説明にならないと思う。
だから、少なくともprogの引数部分はvalueじゃないといけない。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/452
453: デフォルトの名無しさん [sage] 2024/10/03(木) 20:45:47.19 ID:zyXzLypu ポエムすぎて意味わからん。値のリストはvalueじゃないと？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/453
454: デフォルトの名無しさん [] 2024/10/03(木) 20:59:58.72 ID:B2Xmf+Xl 値のリスト自体をそのまま持ってくればvalueということになるんだろうけれど、 $(prog n) の実行結果として出てくるもので、計算効果の説明になるものであって、返り値の型を包含するもの であればcomputationと判断せざるを得ないとかそういうことしか言えないです。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/454
455: デフォルトの名無しさん [sage] 2024/10/03(木) 21:11:15.46 ID:zyXzLypu 判断するって何言ってるの？ computationって定義は何なの？ ラムダ項を書き換えていく手続きが計算じゃないの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/455
456: デフォルトの名無しさん [] 2024/10/03(木) 21:22:37.64 ID:B2Xmf+Xl valueとcomputationの違いは微妙で$(prog n)の実行結果として出てくるかどうかとか 計算効果が発露しているかというところで見極めるしかない、と理解している。判断する というのは専門用語としては使ってない。 computationの定義はまた微妙だけれど、$(prog n)の計算効果込みの実行結果みたいな概念。 最後は超個人的見解だけど、「λ項を書き換えていく行為」というのは、どういう方法で表現して どういう方法で簡約していくか？というところが決まってない。λ計算じゃ
ないけれど、 １＋１＝２ という計算を暗算でやるか、電卓でやるか、そろばんでやるかという違いを出しても計算することに 変わりない。 暗算でやると、脳内物質の分量が変わるし、電卓だと電位が変わる。そして、そろばんでやると 「ぱちぱち」という音が出る。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/456
457: デフォルトの名無しさん [sage] 2024/10/03(木) 21:30:24.72 ID:zyXzLypu ❌決まってない ⭕知らない 間違えるなよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/457
458: デフォルトの名無しさん [sage] 2024/10/03(木) 21:31:19.82 ID:zyXzLypu お前の脳内にしかないお花畑に巻き込むのやめてもらっていいですか？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/458
459: デフォルトの名無しさん [sage] 2024/10/03(木) 22:10:04.42 ID:/brOvmjG おそらくメンタルヘルスに問題がある方なのかな？ 自分の頭の中の映像をそのまま言葉にしたような感じを受ける http://mevius.5ch.net/test/read.cgi/tech/1639713446/459
460: デフォルトの名無しさん [] 2024/10/04(金) 05:46:29.14 ID:vLDssEdm >>428 Haskellの副作用については2つの解釈がある。 １．副作用も含めてアクションという単位で値としてみる。 （アクションを受け取って、アクションを返す関数） ２．Haskellは指示書を発行しているだけで、実際に実行するのは数学（Hakell）の外だから、Haskellそのものには副作用が無い。 （（末尾にHaskellに値を返す形の）マシン語を返して、ハードウェアに実行してもらうと考えるアウトソーシング方式） http://mevius.5ch.net/test/read.cgi/tech/1639713446
/460
461: デフォルトの名無しさん [sage] 2024/10/04(金) 05:52:21.21 ID:EogKDI3R >>460 ようするに副作用はないってことじゃん http://mevius.5ch.net/test/read.cgi/tech/1639713446/461
462: デフォルトの名無しさん [] 2024/10/04(金) 05:57:16.46 ID:vLDssEdm >>461 Javaは変数をクラスの外で作れないから、グローバル変数は存在しない。 けど、事実上のグローバル変数は作れてしまう。 ってのと、同じ。 アクションの中に副作用があろうが、マシン語を返していると解釈しようが、事実として副作用はある。 ただ、重要なのは副作用を伴っても参照透明性が保たれているってこと。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/462
463: デフォルトの名無しさん [sage] 2024/10/04(金) 06:07:02.79 ID:4jD3Hbcp 副作用が隔離できていることが大切 スレの基地外の隔離スレのように http://mevius.5ch.net/test/read.cgi/tech/1639713446/463
464: デフォルトの名無しさん [sage] 2024/10/04(金) 06:24:04.70 ID:EogKDI3R >>462 それは例えばwhileプログラムから副作用のない言語に変換したあとの形式と同じ状態にすでになってるってことで、計算のルール上はもう副作用はないでしょ http://mevius.5ch.net/test/read.cgi/tech/1639713446/464
465: デフォルトの名無しさん [] 2024/10/04(金) 07:22:19.19 ID:vLDssEdm >>464 そうなんだけど、結局普通のプログラミング言語を使ってる人にしてみれば屁理屈でしかない。 見た目そのままで伝えるなら、純粋関数型言語の定義のまんま、「副作用を伴っても参照透明性が保たれている」でいい。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/465
466: デフォルトの名無しさん [sage] 2024/10/04(金) 07:38:19.23 ID:EogKDI3R >>465 まあそのほうがいいか 上の方にいた彼はなんか脳内にこだわりがあって、普通の型付きラムダ計算以上のことをやってると思ってるフシがあったね http://mevius.5ch.net/test/read.cgi/tech/1639713446/466
467: デフォルトの名無しさん [] 2024/10/04(金) 07:48:51.79 ID:vLDssEdm >>466 そうそう。 副作用は無い！って、こっちが必死になって弁を述べれば述べるほど、屁理屈感が出てくる。 それよりは副作用を認めて、「副作用を分離」「副作用を伴っても参照透明性が保たれている」って言った方が、納得感がある。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/467
468: デフォルトの名無しさん [] 2024/10/04(金) 19:23:08.02 ID:tixO3LDq とりあえず続きを書いてみる。 Haskellでいうところの 純粋関数は、valueからvalueへの数学的関数 入出力プログラムは、valueから（入出力）computationへの対応 に割り当てることで、数学上にプログラミング行為を写し出せそうだ、というところまで書いた。 ただ、やっぱり（入出力）computationって何？とか、valueと形式的にどう違うの？という疑問は拭い去ることができない。 そこでMoggiは、次のようなアイディアを２つ出して（結構ムリヤリに）疑問を解決した。 ただ
し、ここで入出力プログラム prog は A型の引数を取って（computationの整理をする前は）B型の返り値を返すとする。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/468
469: デフォルトの名無しさん [] 2024/10/04(金) 19:23:42.06 ID:tixO3LDq Moggiのアイディア１ ・返り値の型がBのcomputationは、何か型構築子をIOとすると、その型構築子を適用した型 IO B のvalueに対応する。 ※Moggiの原理ともいう。 つまり、上で挙げた入出力プログラム prog の型は、具体的に A → IO B になると言っている。 IO B 型の実装で、入出力の予約だか、値のリストだか指示書だか表現はいろいろあるが、そういう機構を実装すれば、 prog :: A → IO B は参照透過性を保ったまま入出力を行うプログラムになる。 もっと広がりが出そ
うなcomputation概念なのに、急に狭窄な感じがするアイディアだけれど、 実装と折り合いをつけるという観点からすると仕方ないともいえる。 なお、代数的効果のPlotkinとPowerが批判しているのはこのMoggiのアイディア１である感じがする（あんまわかってない）。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/469
470: デフォルトの名無しさん [] 2024/10/04(金) 19:24:13.18 ID:tixO3LDq Moggiのアイディア２ ・入出力プログラム（に対応する数学的概念）は、圏をなすはずだ。 Moggiのアイディア１の段階でもprog :: A → IO Bは参照透過性を保ったまま入出力を行うプログラムになるはずだが、 入出力プログラム同士の合成が考えられていない。入出力プログラム prog1、prog2と開発したら、できるだけ再利用するというのが 現実のプログラミングだと思う。わざわざprog1とprog2の合成として定義できそうなプログラムを得るために、イチイチいちから 開発すると
いうことを理論的に要請されるというのは不合理。 純粋関数は、λ式に割り当てられることになって、当然、圏をなすだろうに、 プログラムに割り当てられるものが圏を成さないというのはおかしい。 でも、入出力プログラムはMoggiのアイディア１から、 prog :: A → IO B という特殊な返り値の型を持っているため単純な合成ができない。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/470
471: デフォルトの名無しさん [] 2024/10/04(金) 19:29:03.13 ID:tixO3LDq Moggiのアイディア１の段階でcomputationの概念というのは解消してしまう。 PlotokinとPowerはそこが不満なんだろうか？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/471
472: デフォルトの名無しさん [sage] 2024/10/04(金) 20:18:31.78 ID:WSIC8Xt5 だから、副作用を隠してラムダ計算に変換する手続きは、世界をステートにする変換をした時点で達成されてるわけで、そんなの太古の昔から分かってたことだろ IO aの定義読んでから出直せよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/472
473: デフォルトの名無しさん [sage] 2024/10/04(金) 20:30:15.44 ID:SclsbEZF 日を跨ぐつもりならコテハンでも付けてくれんか 追えん http://mevius.5ch.net/test/read.cgi/tech/1639713446/473
474: デフォルトの名無しさん [] 2024/10/04(金) 20:44:30.01 ID:tixO3LDq >>472 だからそれはわかっているって。評価途中では実際の入出力はせず指示書だか値のリストだけ作成して 参照透過性を保証して、参照透過性が要求されなくなったプログラムの最終段階でリストに従って 入出力を実行するような仕組みがあれば、参照透過性を保ったまま入出力はできるという話でしょ。 それを数学的にどう正当化するかという話を書いているんだって。 >>473 水曜日あたりからだからそんな分量ないよ。 http://mevius.5ch.net/test/read.cgi/tech
/1639713446/474
475: デフォルトの名無しさん [sage] 2024/10/04(金) 20:49:17.68 ID:WSIC8Xt5 >>474 どこが正当化されてないのか意味不明なんだけど ていうか正当化って何？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/475
476: デフォルトの名無しさん [] 2024/10/04(金) 20:51:48.70 ID:tixO3LDq だから、入出力がある数学的関数なんてないじゃん。 入出力があるプログラムを数学的に表現しようと思っても詰むからどうしようって話。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/476
477: デフォルトの名無しさん [sage] 2024/10/04(金) 20:57:28.69 ID:6lZW+X9H こんなところで長文書くのはやめてもろて 読む価値があるものならzennとかnoteに書けば？ 関数型言語界隈の人たちがクソミソにレビューしてくれるよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/477
478: デフォルトの名無しさん [sage] 2024/10/04(金) 20:58:08.93 ID:WSIC8Xt5 >>476 型付きラムダ計算の時点で数学的に表現されてるだろ… 意味不明すぎる http://mevius.5ch.net/test/read.cgi/tech/1639713446/478
479: デフォルトの名無しさん [sage] 2024/10/04(金) 21:00:48.64 ID:qBjLuAvO メインの入力とメインの出力は数学にもある 主じゃないやつを副作用といってる http://mevius.5ch.net/test/read.cgi/tech/1639713446/479
480: デフォルトの名無しさん [] 2024/10/04(金) 21:11:30.04 ID:tixO3LDq >>478 なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。 でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？ >>479 よくわかんない。具体的に言うとどういうのある？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/480
481: デフォルトの名無しさん [] 2024/10/04(金) 21:11:31.21 ID:tixO3LDq >>478 なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。 でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？ >>479 よくわかんない。具体的に言うとどういうのある？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/481
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 186 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.012s