为什么在Haskell中将副作用建模为monad？
在Haskell中，为什么将副作用建模为monad？
根据Eugenio Moggi的观察，先前被称为“monad”的数学结构可以用于模拟计算机语言中的副作用，从而使用Lambda演算来指定它们的语义。在Haskell开发过程中，有多种方法可以对非纯计算进行建模（有关更多详细信息，请参见Simon Peyton Jones的“毛衣”论文），但当Phil Wadler引入monads时，很快就明显这是解决方案。剩下的就是历史。
然而，monad可以用于模拟解释已经是众所周知的事情很久了（至少从《Topoi: A Categorical Analysis of Logic》以来）。另一方面，在强类型的函数式语言出现之前，无法清晰地表达monad的类型，然后Moggi将两者结合在一起。
为什么Haskell中的副作用被建模为Monad？
在Haskell中，副作用表示为Monad的原因是因为一些数据类型（如IO）用于表示命令式计算。这些数据类型的接口中的一小部分对应于被称为“Monad”的接口模式。然而，没有已知的关于IO的纯净/函数/指示性解释（考虑到IO的“罪箱”目的，可能不会有一个），尽管通常有一个关于IO的故事，即“World -> (a, World)”是IO a的含义。这个故事无法真实地描述IO，因为IO支持并发和非确定性。这个故事甚至在允许在计算过程中与世界进行中间交互的确定性计算中也不起作用。
模型化命令式计算通常会变成monad，这正如问题所说。但是，问答者可能并没有真正假设monad本质上以任何方式使命令式计算的建模成为可能。而RealWorld是“非常神奇的”。它是一个代表运行时系统正在进行的操作的标记，它并不真正意味着任何关于真实世界的事情。你甚至不能轻易地产生一个新的RealWorld来创建一个“线程”，而不进行额外的诡计。简单的方法只会创建一个阻塞的操作，对于它何时运行存在很多模糊性。
此外，我认为monad本质上具有命令式性质。如果函子表示嵌入其中的一些值的结构，那么monad实例意味着你可以基于这些值构建和展开新的层次。因此，无论你为函子的单个层次分配什么含义，monad意味着你可以创建无限数量的层次，并且具有从一个层次到下一个层次的严格的因果关系。具体的实例可能没有固有的命令式结构，但是Monad整体上确实是如此。通过“Monad整体上”，我大致指的是forall m. Monad m => ...，即在任意实例上工作。你可以通过任意monad做的事情几乎与IO可以做的事情完全相同：接收不透明的原语（作为函数参数或从库中），使用return构造无操作，或使用(>>=)以不可逆的方式转换值。在任意monad中编程的本质是生成一系列不可撤销的操作：“做X，然后做Y，然后……”。听起来相当命令式！
不，你仍然没有理解我的观点。当然，你不会将这种思维方式应用于任何特定类型，因为它们具有清晰，有意义的结构。当我说“任意monad”时，我意思是“你不能选择哪一个”；这里的观点是从量化器内部的角度来看的，所以将m视为存在性可能更有帮助。此外，我的“解释”是对定律的“重新表述”；“做X”语句的列表恰好是通过(>>=)创建的未知结构的自由幺半群；而monad定律只是对于自函子组合的幺半群定律。
总之，所有monad一起描述的最大下界是一个盲目的，毫无意义的向前推进。IO是一个特殊的情况，因为它几乎没有提供比这个最小要求更多的功能。在特定情况下，类型可能会显示更多的结构，从而具有实际含义；但是，monad的基本属性（基于定律）与IO一样不适合明确的指示。在不导出构造函数，详尽列举原始操作或类似的情况下，情况是无望的。
为什么在Haskell中将副作用建模为monad？
假设一个函数具有副作用。如果我们将它产生的所有效果作为输入和输出参数，那么该函数对外部世界来说是纯的。
所以，对于一个不纯的函数
f' :: Int -> Int
我们需要考虑RealWorld
f :: Int -> RealWorld -> (Int, RealWorld)
-- 输入整个世界的某些状态，
-- 由于副作用而修改整个世界，
-- 然后返回新的世界。
然后f又变得纯洁了。我们定义了一个带参数的数据类型type IO a = RealWorld -> (a, RealWorld)，这样我们就不需要多次输入RealWorld了，可以直接写
f :: Int -> IO Int
对程序员来说，直接处理RealWorld太危险了，特别是如果程序员拿到了RealWorld类型的值，他们可能会尝试复制它，这基本上是不可能的。（比如试图复制整个文件系统。那你会把它放在哪里？）因此，我们的IO定义了整个世界的状态。
“不纯”函数的组合
如果我们不能将这些不纯函数链接在一起，那么这些不纯函数就没有用处。考虑以下函数：
getLine :: IO String ~ RealWorld -> (String, RealWorld)
getContents :: String -> IO String ~ String -> RealWorld -> (String, RealWorld)
putStrLn :: String -> IO () ~ String -> RealWorld -> ((), RealWorld)
我们想要从控制台获取一个文件名，然后读取该文件，并将文件内容打印到控制台。如果我们能够访问真实的世界状态，我们该如何做呢？
printFile :: RealWorld -> ((), RealWorld)
printFile world0 = let (filename, world1) = getLine world0
(contents, world2) = (getContents filename) world1
in (putStrLn contents) world2 -- 结果为((), world3)
我们在这里看到了一个模式。函数的调用方式如下：
...
(
(
...
所以我们可以定义一个操作符~~~来绑定它们：
(~~~) :: (IO b) -> (b -> IO c) -> IO c
(~~~) :: (RealWorld -> (b, RealWorld))
-> (b -> RealWorld -> (c, RealWorld))
-> (RealWorld -> (c, RealWorld))
(f ~~~ g) worldX = let (resF, worldY) = f worldX
in g resF worldY
然后我们就可以简单地写
printFile = getLine ~~~ getContents ~~~ putStrLn
而不用触及真实的世界。
“不纯化”
现在假设我们还想将文件内容变为大写。大写化是一个纯函数
upperCase :: String -> String
但是要将它变成真实世界，它必须返回一个IO String。很容易提升这样的函数：
impureUpperCase :: String -> RealWorld -> (String, RealWorld)
impureUpperCase str world = (upperCase str, world)
这可以被泛化：
impurify :: a -> IO a
impurify :: a -> RealWorld -> (a, RealWorld)
impurify a world = (a, world)
所以impureUpperCase = impurify . upperCase，我们可以写
printUpperCaseFile =
getLine ~~~ getContents ~~~ (impurify . upperCase) ~~~ putStrLn
（注意：通常我们会写getLine ~~~ getContents ~~~ (putStrLn . upperCase)）
我们一直在使用monad
现在让我们看看我们做了什么：
1. 我们定义了操作符(~~~) :: IO b -> (b -> IO c) -> IO c，将两个不纯函数链接在一起
2. 我们定义了一个函数impurify :: a -> IO a，将纯值转换为不纯。
现在我们将等号定义为(>>=) = (~~~)和return = impurify，看到了吗？我们得到了一个monad。
技术说明
为了确保它确实是一个monad，还有一些公理需要检查：
1. return a >>= f = f a
impurify a = (\world -> (a, world))
(impurify a ~~~ f) worldX = let (resF, worldY) = (\world -> (a, world )) worldX
in f resF worldY
= let (resF, worldY) = (a, worldX)
in f resF worldY
= f a worldX
2. f >>= return = f
(f ~~~ impurify) worldX = let (resF, worldY) = f worldX
in impurify resF worldY
= let (resF, worldY) = f worldX
in (resF, worldY)
= f worldX
3. f >>= (\x -> g x >>= h) = (f >>= g) >>= h
留作练习。
这个解释不能真正适用于Haskell的IO，因为后者支持交互、并发和非确定性。请参阅我对这个问题的回答，了解更多指示。
非常好的总结。通过这个和范畴论的基础知识，我觉得离真正的可能性有点近了...虽然还是太远了:) 谢谢。
GHC实际上是通过这种方式实现IO的，但是RealWorld并不真正表示真实世界，它只是一个令牌，用于保持操作的顺序（这种“魔法”是GHC Haskell的唯一的独特类型）。
据我了解，GHC通过这种表示和非标准的编译器魔法（类似于Ken Thompson的著名C编译器病毒）来实现IO。对于其他类型，真相在源代码中，以及通常的Haskell语义。
我的评论是因为我阅读了GHC源代码的相关部分。
我认为证明（2）f >>= return = f 中有一个错误。我认为应该是下面这样：(f ~~~ impurify) worldX = let (resF, worldY) = f worldX in impurify resF worldY = let (resF, worldY) = f worldX in (resF, worldY) = f worldX
我认为你是对的，它不应该应用于a，而是应该应用于worldX。我会再检查一下，并进行编辑。真棒的发现！:) 如果在“SO应该是这样的”中，你会因为这个修复获得巨大的声望奖励！
谢谢！还要感谢你的编辑！事实上，我几个月前就进行了编辑，但是编辑被拒绝了。所以我在获得“随处评论”特权后，才进行了评论，这需要超过50的声望:)