世界はHaskellプログラムが数秒前に写した説

屑軍師 @kuzugunshi

Haskellがすべて じゃなく すべてがHaskell

Deprecatad @deprecatad

軍師のツイート見て考えたんだけど、 IOなどの現実に効果を与えるような副作用が純粋と捉えられるような空間はないのかな。

Deprecatad @deprecatad

何を言っているのかわからないと思うけど僕もわからない。

Deprecatad @deprecatad

この世界はHaskellで出来ている？？？

Deprecatad @deprecatad

@kuzugunshi HaskellのIOも、RealWorldを引数に受け取って新しいRealWorldを返す…と考えると純粋な関数なんだよなぁ…。 やばい。

Deprecatad @deprecatad

@kuzugunshi HaskellのIOも、RealWorldを引数に受け取って新しいRealWorldを返す…と考えると純粋な関数なんだよなぁ…。 やばい。

Deprecatad @deprecatad

HaskellのIOのgetLineなどがRealWorldを引数として受け取り新しいRealWorldを返すのと 世界5分前誕生説を合わせると HaskellのIOは現実において純粋であって 全ての基軸はHaskellプログラムであることになる。

Deprecatad @deprecatad

多分。

Deprecatad @deprecatad

世界を跨ぐHaskellだ、すごい。

Deprecatad @deprecatad

世界Haskellが5分前に作った説。

屑軍師 @kuzugunshi

@aiya_000 捉え方を広くするか狭くするかという話ではないかと思う

Deprecatad @deprecatad

言ってて気づいた！！ StateやReaderを代表とするモナドって、do式の中で引数を文脈として暗黙的に処理するじゃん。 こういうの。

Deprecatad @deprecatad

f :: Reader Int Int f = do a <- ask return $ a + 10 x = runReader f 10 これでxに20が入る。

Deprecatad @deprecatad

このとき、関数fには引数が明示されていないのに、fは10と一緒に呼び出されている。 つまり10はfの暗黙的な文脈と言えると思うんだけど

Deprecatad @deprecatad

これってIOモナドも同じだったんだ。 つまり g :: IO String g = do a <- getLine print a return a y = g >>= return この時gを呼び出す際は何も引数に指定されていない…けれど

Deprecatad @deprecatad

本当はgにも引数が渡されていて、g内部で文脈として実行されている。 その引数こそがRealWorldだったんだよ！！

Deprecatad @deprecatad

GHCのIO型の定義を見た時に、気付けなかった。 1年越しくらいの気づきだ。

Deprecatad @deprecatad

(つまり、getLineは現実を引数として改変した現実を返す関数)

Deprecatad @deprecatad

もっと言うと、この考えでいくとgetLineも純粋な関数であって 純粋な関数はものからものに写すだけだと思うので IOは現実から新しい現実への橋。

Deprecatad @deprecatad

僕らはgetLineを実行する度に、新しい世界へと移動しているんだよ！！

Deprecatad @deprecatad

@kuzugunshi 僕はレイヤの問題だと考えてる。 現実世界ベースで考えるか、Haskellのプログラム内ベースで考えるか。 少なくともHaskellの中ではそうなってるんだよなあ…っていう感慨。

Deprecatad @deprecatad

「モナド則を理解したおかげで彼氏ができました！」 「モナド則を理解したおかげでダイエットに成功しました！」 「モナド則を理解したおかげでお金持ちになれました！」

Deprecatad @deprecatad

「モナド則を理解したおかげで彼氏ができました！」 「モナド則を理解したおかげでダイエットに成功しました！」 「モナド則を理解したおかげでお金持ちになれました！」

Deprecatad @deprecatad

「モナド則を理解したおかげで彼氏ができました！」 「モナド則を理解したおかげでダイエットに成功しました！」 「モナド則を理解したおかげでお金持ちになれました！」

Deprecatad @deprecatad

「モナド則を理解したおかげで彼氏ができました！」 「モナド則を理解したおかげでダイエットに成功しました！」 「モナド則を理解したおかげでお金持ちになれました！」