IO單子：GHC實施含義與數學含義

Question

考慮

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

這裏，ioFunction，從數學的角度來看，是一個函數，它有一個輸入，並返回IO()類型的值。我認爲這沒有別的意思。也就是說，從數學的角度來看，這個函數返回一個值，沒有別的東西;特別是它不打印任何東西。因此，這是否意味着Haskell使用IO monad來實現命令式副作用（在這種情況下：運行此功能將首先打印str，然後按此順序打印「2」）的方式是純粹的GHC爲實現細節與數學（在某種意義上甚至是哈斯克爾）這個術語的含義沒有關係？

編輯：爲了使這個問題更清楚，我的意思是要問的是，例如什麼，有沒有從視圖以下兩種功能之間的數學的角度有什麼區別：

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。這當然有點尷尬 - 「觀察發生的事情」不是數學，而是物理學，觀察科學上要求在相同的環境條件下執行兩次。

糟糕的是，即便如此，一般認爲是數學上可以觀察到不同的行爲相同的純值：print 100000000將立即引起副作用，而print $ last [0..100000000]需要顯著暫停（其中，如果按照其與時間打印命令，實際上可以產生不同的文本輸出）。

但是這些問題在現實世界中是不可避免的。因此，Haskell's沒有指定IO上的任何結構，只有通過語言內部的數學嚴格性來檢查其是否相等，纔有意義。所以，在某種意義上你真的不能知道putStrLn str >> putStrLn "2"是不一樣的return()。

其實他們可能是一樣的。可以設想使一個甚至更簡單的玩具實施IO比從而上述：

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

和簡單地任何純輸出操作映射到無操作（和任何輸入到一個無限循環）。然後，你將有

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

和

ioFunction2 str = return() 
       = IONop 

這一點，就好像我們已經強加於自然數的附加公理，即1 = 0。從這你就可以得出結論：每號碼爲零。

顯然，這將是一個完全無用的實現。但是，如果您在沙箱環境中運行Haskell代碼，並且希望完全確定沒有發生任何錯誤，那麼類似的東西實際上可能有意義。 http://tryhaskell.org/做這樣的事情。

Answer 2

這裏，ioFunction從數學的角度來看是一個函數，它接受一個輸入並返回一個IO()類型的值。我認爲這沒有別的意思。

是的。究竟。

那麼，這是否意味着這樣Haskell使用的IO單子命令式的副作用（在這種情況下：運行此功能將首先打印海峽，然後print "2"，順序）是純粹的GHC實現細節這與該術語的數學意義（甚至是Haskell）無關？

不完全。從數學（集合論）的角度來看，我認爲「相同」意味着結構相同。由於我不知道什麼構成了IO()的值，所以我不能說這種類型的兩個值是否相同。

其實，這是由設計：通過使IO不透明（在這個意義上，我不知道是什麼構成了IO），GHC阻止我以往任何時候都能夠說，IO()類型的一個值等於另一個。通過fmap,(<*>),(>>=),mplus等功能，我可以處理的唯一事情是IO。

Answer 3

爲了簡單起見，讓我們專注於IO monad的輸出方面。從數學上講，輸出（作家）monad是由內部管理員$ T $給出的，其中$ U（A）= U^* \ times A $，其中$ U $是一組固定的字符，$ U^* $是$ U $以上的字符串集合。然後$ ioFunction：U^* \到T（）$，即$ ioFunction：U^* \到U^* \ times（）$和$ ioFunction（s）=（s ++「\ n」++「2 \ N」，（））$。相比之下，$ ioFunction2（s）=（「」，（））$。任何實施必須尊重這種差異。差異主要是數學上的差異，而不是實施細節。 （嗯，TeX標記似乎只能在mathoverflow中運行...）