为什么副作用在哈斯克尔被模拟为单子？

有没有人能提供一些建议，解释一下为什么哈斯克尔的不纯计算被模拟为单子(monads) ？

我的意思是单子只是一个接口与4个操作，那么是什么原因建模副作用在它？

21925 次浏览
小开

有没有人能提供一些建议，解释为什么哈斯克尔的非纯计算被建模为单子？

因为 Haskell 是 纯洁。您需要一个数学概念来区分 类型级别上的 不纯粹的计算和 纯洁的人，并分别建模 程序流。

这意味着您最终必须使用某种类型的 IO a来建模非纯计算。然后你需要知道 结合的这些计算方法，其中 按顺序应用(>>=)和 提升一个值(return)是最明显和最基本的。

通过这两个，您已经定义了 monad (甚至没有考虑它) ;)

此外，单子提供了 非常普遍和强大的抽象概念，所以很多种控制流可以方便地推广到单子函数中，如 sequence、 liftM或者特殊的语法，使得不纯不是这样的特例。

有关更多信息，请参见 函数式编程中的单子和 唯一性类型(我所知道的唯一选择)。

小开

AFAIK，原因是能够包括在类型系统的副作用检查。如果你想知道更多，听听这些 SE-Radio节目: 第108集: 函数式编程和 Haskell 西蒙·佩顿·琼斯 第72集: Erik Meijer on LINQ

小开
最佳答案

假设一个函数有副作用。如果我们把它产生的所有效果作为输入和输出参数，那么这个函数对于外部世界是纯粹的。

因此，对于一个不纯函数

f' :: Int -> Int

我们把现实世界也考虑在内

f :: Int -> RealWorld -> (Int, RealWorld)
-- input some states of the whole world,
-- modify the whole world because of the side effects,
-- then return the new world.

那么 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 -- results in ((), world3)

我们在这里看到一个模式，函数是这样调用的:

...
(<result-of-f>, worldY) = f               worldX
(<result-of-g>, worldZ) = g <result-of-f> worldY
...

因此，我们可以定义一个操作符 ~~~来绑定它们:

(~~~) :: (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))

我们一直在研究单子

现在让我们看看我们做了什么:

  1. 我们定义了一个运算符 (~~~) :: IO b -> (b -> IO c) -> IO c，它将两个不纯函数链接在一起
  2. 我们定义了一个函数 impurify :: a -> IO a，它将一个纯值转换为不纯值。

现在我们做 (>>=) = (~~~)和 return = impurify的识别，看到了吗? 我们得到了一个单子。

技术说明

为了确保它真的是一个单子，还有一些公理需要检验:

  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

    作为锻炼。

小开

据我所知，一个叫做 Eugenio Moggi的人首先注意到了一个之前被称为“ monad”的晦涩的数学结构，它可以被用来在计算机语言中建模副作用，从而使用 Lambda 演算来指定它们的语义。当 Haskell 被开发出来的时候，有各种各样的方法来模拟不纯计算(更多细节见西蒙·佩顿·琼斯的 “毛衬衫”纸) ，但是当 Phil Wadler 介绍 monads 的时候，很快就明白了这就是答案。剩下的就是历史了。

小开

这实际上是一种非常简洁的用函数的方式来思考 I/O 的方法。

在大多数编程语言中，都要执行输入/输出操作。在哈斯克尔，想象一下，不是为操作编写代码，而是为了生成您想要执行的操作的列表。

Monads 就是这样的语法。

如果你想知道为什么单子与其他东西相反，我想答案是它们是人们在制作 Haskell 时能想到的最好的表示 I/O 的函数式方法。

小开

有没有人能提供一些建议，解释为什么哈斯克尔的非纯计算被建模为单子？

这个问题包含了一个普遍的误解。 杂质和单子是独立的概念。 杂质是由 Monad 模拟的 没有。 相反，有一些数据类型，如 IO，表示命令式计算。 对于其中的一些类型，它们的接口的一小部分对应于称为“ Monad”的接口模式。 此外，对于 IO没有已知的纯粹/功能/外延解释(考虑到 IO的 “罪恶之箱”目的，不太可能有这样的解释) ，尽管有关 World -> (a, World)是 IO a的意义的常见故事。 这个故事不能真实地描述 IO，因为 IO支持并发性和非确定性。 当确定性计算允许中间计算与世界交互时，这个故事甚至不起作用。

有关详细说明，请参阅 这个答案。

编辑 : 重读这个问题，我不认为我的答案是正确的。 正如问题所说，命令式计算模型往往是单子模型。 询问者可能并不真正认为单子性以任何方式支持命令式计算的建模。

小开

上面有非常好的具有理论背景的详细答案。但是我想谈谈我对 IO 单体的看法。我不是经验丰富的哈斯克尔程序员，所以可能是相当幼稚，甚至错误的。但我帮助我处理 IO 单子在一定程度上(注意，它不涉及其他单子)。

首先我想说，“真实世界”的例子对我来说不太清楚，因为我们不能访问它(真实世界)以前的状态。也许它根本不涉及单子计算，但是它在参照透明度(计算机科学)的意义上是需要的，这通常在 haskell 代码中出现。

所以我们希望我们的语言(haskell)是纯粹的。但是我们需要输入/输出操作，因为没有它们，我们的程序就没有用处。这些行动本质上不可能是纯粹的。所以处理这个问题的唯一方法就是把不纯操作和其他代码分开。

Monad 来了。实际上，我不确定是否存在具有类似所需属性的其他构造，但关键是 monad 具有这些属性，因此它可以被使用(并且被成功地使用)。主要的特点是我们不能逃避它。单子接口没有操作去除我们的值周围的单子。其他(非 IO)单子提供这样的操作并允许模式匹配(例如“也许”) ，但这些操作不在单子接口中。另一个必需的属性是链式操作的能力。

如果从类型系统的角度考虑我们需要什么，我们就会发现这样一个事实: 我们需要带有构造函数的类型，构造函数可以包装任何值。构造函数必须是私有的，因为我们禁止从它逃逸(即模式匹配)。但是我们需要函数来给这个构造函数赋值(这里需要考虑 return)。我们需要连锁经营的方法。如果我们考虑一段时间，我们就会发现这样一个事实: 链接操作必须像 > > = has 那样具有类型。所以，我们得到了一些非常类似于单子的东西。我认为，如果我们现在用这个结构分析可能的矛盾情况，我们将得到单子公理。

注意，已开发的结构与杂质没有任何共同之处。它只有一些属性，我们希望这些属性能够处理不纯操作，即无转义、链接和进入的方法。

现在，这个选定的单子 IO 中的语言预定义了一些不纯操作集。我们可以组合这些操作来创建新的非纯操作。所有这些操作都必须在其类型中包含 IO。但是请注意，某些函数类型中 IO 的存在并不会使这个函数变得不纯粹。但是据我所知，在类型中使用 IO 编写纯函数是不明智的，因为最初我们的想法是分离纯函数和不纯函数。

最后，我想说的是，单子不会把不纯操作变成纯操作。它只能有效地分离它们。(我重复，这只是我的理解)

小开

如您所说，Monad是一个非常简单的结构。答案的一半是: Monad是最简单的结构，我们可以给副作用函数，并能够使用它们。有了 Monad，我们可以做两件事: 我们可以把一个纯值看作一个副作用值(return) ，我们可以把一个副作用函数应用到一个副作用值上，得到一个新的副作用值(>>=)。失去做这两件事情的能力将是致命的，所以我们的副作用类型需要是“至少”Monad，结果是 Monad足以实现我们到目前为止所需要的所有东西。

另一半是: 我们能给出的“可能的副作用”的最详细的结构是什么？我们当然可以把所有可能的副作用的空间看作一个集合(唯一需要的操作是成员资格)。我们可以通过一个接一个的做这两个副作用，这将导致一个不同的副作用(或者可能相同的一个-如果第一个是“关机计算机”和第二个是“写文件”，那么这些组成的结果只是“关机计算机”)。

好吧，关于这次行动我们能说些什么呢？它是联合的，也就是说，如果我们结合了三个副作用，结合的顺序并不重要。如果我们这样做(写文件，然后读套接字) ，然后关机，这是相同的做写文件，然后(读套接字，然后关机计算机)。但它不是可交换的: (“写文件”然后“删除文件”)是一个不同的副作用从(“删除文件”然后“写文件”)。我们有一个共同点: 特殊的副作用“没有副作用”的工程(“没有副作用”，然后“删除文件”是相同的副作用，只是“删除文件”)在这一点上，任何数学家正在思考“组!”但是组有反转，而且通常没有办法反转副作用; “删除文件”是不可逆的。所以我们剩下的结构是幺半群，这意味着我们的副作用函数应该是单子。

还有更复杂的结构吗？当然！我们可以将可能的副作用分为基于文件系统的效果、基于网络的效果等等，并且我们可以提出更详细的合成规则来保留这些细节。但是这又可以归结为: Monad非常简单，但是它足够强大，可以表达我们所关心的大部分属性。(特别是，结合性和其他公理让我们可以在小块中测试我们的应用程序，并确信组合应用程序的副作用将与小块副作用的组合相同)。


提交答案