IO Monads:GHC实现意义与数学意义

Question

考虑

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

这里,ioFunction从数学的角度来看,是一个函数,它接受一个输入并返回一个类型的值IO ().我认为这意味着什么.也就是说,从数学的角度来看,这个函数返回一个值,而不是别的; 特别是,它不会打印任何东西.

这是否意味着Haskell使用IO monad进行命令性副作用的方式(在这种情况下:运行此函数将首先打印str,然后按顺序打印"2")纯粹是GHC实现细节,没有任何内容做数学(在某种意义上甚至是Haskell)这个术语的含义？

编辑:为了使这个问题更清楚,我的意思是,例如,以下两个函数之间的数学观点有什么不同:

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


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

似乎答案是否定的,因为 - 从数学的角度来看 - 它们都作为输入a String并返回类型的值(可能是相同的值)IO ().这不是这种情况吗？

Answer 1

这里,ioFunction从数学的角度来看,是一个函数,它接受一个输入并返回一个类型的值IO ().我认为这意味着什么.

是.究竟.

这是否意味着Haskell使用IOmonad进行命令性副作用的方式(在这种情况下:运行此函数将首先打印str然后按此print "2"顺序)纯粹是一个与数学无关的GHC实现细节(在某种意义上甚至是Haskell)这个术语的含义？

不完全的.从数学(集合论)的角度来看,我认为"相同"意味着结构相同.由于我不知道是什么构成了一个值IO (),我不能说这个类型的两个值是否相同.

事实上,这是设计的:通过制作IO不透明(在某种意义上我不知道是什么构成IO),GHC阻止我永远不能说一个类型的IO ()值等于另一个.唯一的东西,我可以做的IO是通过类似的功能暴露fmap,(<*>),(>>=),mplus,等.