関数型プログラミング言語Haskell Part34 (691ﾚｽ)
上下前次1-新
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とかに煽った感じのタイトルつけて炎上する記事書いてコメントもらって来いよ
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: デフォルトの名無しさん [sage] 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: デフォルトの名無しさん [sage] 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): デフォルトの名無しさん [sage] 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
横からというか >460460(2): デフォルトの名無しさん [] 2024/10/04(金) 05:46:29.14 ID:vLDssEdm(1/9) AAS
>>428
Haskellの副作用については2つの解釈がある。
１．副作用も含めてアクションという単位で値としてみる。
（アクションを受け取って、アクションを返す関数）
２．Haskellは指示書を発行しているだけで、実際に実行するのは数学（Hakell）の外だから、Haskellそのものには副作用が無い。
（（末尾にHaskellに値を返す形の）マシン語を返して、ハードウェアに実行してもらうと考えるアウトソーシング方式）
書いた者だけど、あなたの疑問は解釈1の「アクションを受け取ってアクションを返す関数」だとざっくりし過ぎて納得いかないって感じでしょうか？
でしたら、解釈2では納得出来ませんでしょうか？
解釈２は、モナドの効能の一つに追加して「数学の世界にアウトソーシングという概念を持ち込む」というものです。
モナドの例えとして、床下配線というのがありますが、MaybeやListの様な通常のモナドも、>>=の中に関数適用部分を押し込んで、表から見えないようにしています。
（これも、見ようによってはアウトソーシングです。同じ数学の世界なので、隣の席に頼んだ感じですが）
IOモナドは、>>=の中すら見えない状態で関数適用しているわけですが、 >460 でも書いたとおり、「数学の外（ハードウェア）」で関数適用されていると考えるわけです。
IOモナドの>>= は、外の世界と遣り取りする受付窓口というわけですね。
（実際、バッファの様な振る舞いをします）
main = do x <- return 0
_________x <- return (x + 1)
_________print x
494(1): デフォルトの名無しさん [sage] 2024/10/04(金) 22:14:36.08 ID:WSIC8Xt5(8/14) AAS
>>492
ラムダ計算も集合論上で展開されてるだろ
だから、Haskellも集合論の言葉で書かれてるじゃん
そんな誰もが分かってるけど、いちいち書いても何の得もないことを話したかったの？
上下前次1-新書関写板覧索設栞歴
あと 197 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.025s