IOモナド：数学的意味

Question

対GHC実装意味数学的な観点から、1つの入力を取り、型IO()の値を返す関数であり、ここで

ioFunction :: String -> IO() 
ioFunction str = do putStrLn str 
        putStrLn "2" 

、ioFunction検討します。私はそれが何も意味しないと推測します。つまり、数学的には、この関数は値を返し、それ以外は何も返しません。特に、何も印刷しません。

これは、ハスケルが命令的な副作用（この場合、この関数を実行すると、最初にstrを印刷し、次に "2"をその順に印刷する）のためにIOモナドを使用する方法は、純粋にGHC実装の詳細は、数学的（そしてある意味ではハスケル）の意味とは関係がありません。

EDIT：はこの質問をより明確にするために、私は例えば、ある依頼する何を意味するか、次の2つの機能の間のビューの数学的な点から任意の違いがあります：

ioFunction1 :: String -> IO() 
ioFunction1 str = do putStrLn str 
        putStrLn "2" 


ioFunction2 :: String -> IO() 
ioFunction2 str = do return() 

はそれ答えはいいえではないようです - 数学的観点から - 彼らはどちらも入力としてStringを受け取り、タイプIO()の値（たぶん同じ値）を返します。これは当てはまりませんか？

Answer 1

私はいつもそれが参考に簡略化され、「無条件言語のソースコード」IOモナドの実装を検討するために見つける：

data IO :: * -> * where 
    PutStr :: String -> IO() 
    GetLine :: IO String 
    IOPure :: a -> IO a 
    IOSeq :: IO a -> IO b -> IO b 
    ... 
    LaunchMissiles :: IO() 

その後ioFunctionは数学的な意味で適切な、賢明な機能は非常に明確である何：

ioFunction str = do putStrLn str 
        putStrLn "2" 
       = putStr (str++"\n") >> putStrLn "2\n" 
       = IOSeq (PutStr (str++"\n")) (PutStrLn "2\n") 

これは、命令型言語のソースコードを効果的に表すデータ構造です。 ioFunctionは、与えられた引数を結果構造体の特定の場所に配置するので、数学的には些細なことではありません。"()を返します。何も起こりませんがGHCの実装の詳細です"。

値はioFunction2のために実際に完全に異なっている：

ioFunction2 str = do return() 
       = return() 
       = IOPure() 

---

我々は、彼らがこの意味で異なっている知っていますか？

これは良い質問です。具体的には、プログラムを実行して、両方のプログラムを実行して、異なる効果が発生することを確認すると、must have been differentとなります。これはちょっと厄介なことですが、「何が起こるか観察する」というのは数学ではなく、物理学であり、科学的には厳密に同じ環境条件で2回実行する必要があります。

さらに悪いことに、純粋な値であっても数学的には同じであるとみなされても、異なる動作を観察することができます。print $ last [0..100000000]はすぐに副作用を引き起こしますが、 -printingコマンドは、実際には異なるテキスト出力を生成することができます）。

しかし、これらの問題は実際の状況では避けられません。したがって、ハスケルは、数学的厳密さが言語内から平等であるかどうかをチェックすることができるIO上の構造を特定していないことを意味するに過ぎない。ですから、ある意味ではかなりはputStrLn str >> putStrLn "2"はreturn()と同じではありません。

そして確かに彼らはかもしれませんは同じです。

data IO :: * -> * where 
    IONop :: IO() 
    IOHang :: IO a -> IO a 

単にノーオペレーション（及び無限ループへの入力）に任意の純粋な出力動作をマップする：従って、上記よりIOのも簡単なおもちゃの実装を行うことが考えられます。私たちはあなたがと結論づけることができることから、すなわち1 = 0、自然数の上に追加の公理を課してきたかのように、あなたは

ioFunction str = do putStrLn str 
        putStrLn "2" 
       = IONop >> IONop 
       = IONop 

と

ioFunction2 str = return() 
       = IONop 

を持っているでしょうこれは少しはありますすべて番号はゼロです。

明らかに、それはまったく役に立たない実装です。しかし、ハスケルのコードをサンドボックス環境で実行していて、何も悪いことが起こっていないことを完全に確かめたいのであれば、似たようなことが実際には理にかなっています。 http://tryhaskell.org/はこのようなことをします。ここ

Answer 2

、ioFunction、数学的な観点から、1つの入力を取り、型IO()の値を返す関数です。私はそれが何も意味しないと推測します。

はい。まったく。

だから、これはHaskellは（この場合：この機能を実行すると、まずそのためには、STR印刷した後、print "2"なること）が不可欠副作用のためIOモナドを使用する方法があることを意味しない、純粋にGHCの実装の詳細ですその言葉の数学的意味（そしてある意味ではハスケルの意味）とは何の関係もありません。

かなりです。数学的（セット理論）の観点からは、「同じ」は構造的に同一であることを意味します。私はIO()の値を構成するものがわからないので、その型の2つの値が同じかどうかについては何も言えません。実際に

、これは仕様によるものです。（私はIOを構成しているのか分からないという意味で）IO不透明させることにより、GHCはこれまでのタイプIO()の1つの値が等しいことを言うことができることから私を防ぎ別のIOでできることは、fmap、(<*>)、(>>=)、mplusなどの機能で公開されています。

Answer 3

簡単にするため、IOモナドの出力態様に注目しましょう。数学的に言えば、出力（ライター）モナドは、$ T（A）= U^* \ times A $である、$ U $を固定文字集合とすると、 $ U $を超える文字列の集合。 $ ioFunction：U^* \ times（）$、$ ioFunction（s）=（s ++ "\ n" ++ "2 \ n "、（））$。対照的に、$ ioFunction2（s）=（ ""、（））$。どんな実装もこの違いを尊重する必要があります。違いは主に数学的なものであり、実装の詳細ではありません。 （Hm、TeXのマークアップはマスオーバーフローでしか動作しないようです...）