183

谁能给出一些关于为什么 Haskell 中的不纯计算被建模为 monad 的指示?

我的意思是 monad 只是一个具有 4 个操作的接口,那么在其中建模副作用的原因是什么?

4

8 回答 8

301

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

因此,对于不纯函数

f' :: Int -> Int

我们将 RealWorld 添加到考虑中

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)

我们一直在使用 monad

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

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

现在我们进行识别(>>=) = (~~~)return = impurify,看看?我们有一个单子。


技术说明

为了确保它真的是一个 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

    留作练习。

于 2010-03-21T21:44:05.703 回答
44

谁能给出一些关于为什么 Haskell 中的不纯计算被建模为 monad 的指示?

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

有关更多解释,请参阅此答案

编辑:在重新阅读问题时,我认为我的答案不太正确。正如问题所说,命令式计算的模型通常是单子。提问者可能不会真正假设 monadness 以任何方式支持命令式计算的建模。

于 2011-08-16T00:08:54.950 回答
13

据我了解,一个叫Eugenio Moggi的人首先注意到一个以前晦涩难懂的数学结构,称为“monad”,可用于对计算机语言中的副作用进行建模,从而使用 Lambda 演算来指定它们的语义。在开发 Haskell 时,有多种方法可以对不纯的计算进行建模(有关更多详细信息,请参见 Simon Peyton Jones 的“hair shirt”论文),但是当 Phil Wadler 引入 monad 时,很快就很明显这就是答案。剩下的就是历史。

于 2010-03-22T07:54:22.430 回答
8

谁能给出一些关于为什么 Haskell 中的不纯计算被建模为 monad 的指示?

好吧,因为 Haskell 是的。您需要一个数学概念来区分类型级别的非纯计算纯计算,并分别对程序流进行建模。

这意味着您最终将不得不使用某种类型IO a来模拟非纯计算。然后,您需要知道组合这些计算的方法,其中按顺序应用( >>=) 和提升值( return) 是最明显和最基本的。

有了这两个,你已经定义了一个 monad(甚至没有想到它);)

此外,monad 提供了非常通用和强大的抽象,因此可以方便地将多种控制流概括为 monadic 函数sequenceliftM或特殊语法,使不纯不是这样的特殊情况。

有关更多信息,请参阅函数式编程唯一性类型(我知道的唯一替代方法)中的 monad。

于 2010-03-21T21:18:37.237 回答
7

正如你所说,Monad是一个非常简单的结构。一半的答案是:Monad这是我们可能赋予副作用函数并能够使用它们的最简单的结构。有了Monad我们可以做两件事:我们可以将纯值视为副作用值(return),我们可以将副作用函数应用于副作用值以获得新的副作用值(>>=)。失去做这些事情的能力将是严重的,所以我们的副作用类型需要是“至少” Monad,事实证明Monad它足以实现我们到目前为止所需要的一切。

另一半是:对于“可能的副作用”,我们可以给出的最详细的结构是什么?我们当然可以将所有可能的副作用的空间视为一个集合(唯一需要的操作是成员资格)。我们可以通过一个接一个地执行它们来组合两种副作用,这会产生不同的副作用(或者可能是相同的副作用 - 如果第一个是“关闭计算机”,第二个是“写入文件”,那么结果组成这些只是“关闭计算机”)。

好的,那么我们能对这个操作说些什么呢?它是关联的;也就是说,如果我们结合三个副作用,那么我们按照哪个顺序进行结合并不重要。如果我们这样做(写入文件然后读取套接字)然后关闭计算机,这与执行写入文件然后(读取套接字然后关闭)相同计算机)。但它不是可交换的:("write file" then "delete file") 与 ("delete file" then "write file") 的副作用不同。我们有一个身份:特殊副作用“无副作用”有效(“无副作用”然后“删除文件”与“删除文件”的副作用相同)此时任何数学家都在思考“组!” 但是群体有反面,一般来说没有办法逆转副作用。“删除文件” 是不可逆的。所以我们留下的结构是一个幺半群,这意味着我们的副作用函数应该是单子。

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

于 2014-09-30T01:08:46.107 回答
4

它实际上是一种以功能方式考虑 I/O 的非常简洁的方式。

在大多数编程语言中,您执行输入/输出操作。在 Haskell 中,想象编写代码不是为了执行操作,而是生成您想要执行的操作的列表。

Monads 正是这样的语法。

如果您想知道为什么 monad 与其他东西相反,我想答案是它们是人们在制作 Haskell 时可以想到的表示 I/O 的最佳功能方式。

于 2010-03-22T14:44:03.907 回答
3

AFAIK,原因是能够在类型系统中包含副作用检查。如果您想了解更多信息,请收听SE-Radio剧集:第 108 集:Simon Peyton Jones 谈函数式编程和 Haskell 第 72 集:Erik Meijer 谈 LINQ

于 2010-03-21T21:18:56.083 回答
2

Above there are very good detailed answers with theoretical background. But I want to give my view on IO monad. I am not experienced haskell programmer, so May be it is quite naive or even wrong. But i helped me to deal with IO monad to some extent (note, that it do not relates to other monads).

First I want to say, that example with "real world" is not too clear for me as we cannot access its (real world) previous states. May be it do not relates to monad computations at all but it is desired in the sense of referential transparency, which is generally presents in haskell code.

So we want our language (haskell) to be pure. But we need input/output operations as without them our program cannot be useful. And those operations cannot be pure by their nature. So the only way to deal with this we have to separate impure operations from the rest of code.

Here monad comes. Actually, I am not sure, that there cannot exist other construct with similar needed properties, but the point is that monad have these properties, so it can be used (and it is used successfully). The main property is that we cannot escape from it. Monad interface do not have operations to get rid of the monad around our value. Other (not IO) monads provide such operations and allow pattern matching (e.g. Maybe), but those operations are not in monad interface. Another required property is ability to chain operations.

If we think about what we need in terms of type system, we come to the fact that we need type with constructor, which can be wrapped around any vale. Constructor must be private, as we prohibit escaping from it(i.e. pattern matching). But we need function to put value into this constructor (here return comes to mind). And we need the way to chain operations. If we think about it for some time, we will come to the fact, that chaining operation must have type as >>= has. So, we come to something very similar to monad. I think, if we now analyze possible contradictory situations with this construct, we will come to monad axioms.

Note, that developed construct do not have anything in common with impurity. It only have properties, which we wished to have to be able to deal with impure operations, namely, no-escaping, chaining, and a way to get in.

Now some set of impure operations is predefined by the language within this selected monad IO. We can combine those operations to create new unpure operations. And all those operations will have to have IO in their type. Note however, that presence of IO in type of some function do not make this function impure. But as I understand, it is bad idea to write pure functions with IO in their type, as it was initially our idea to separate pure and impure functions.

Finally, I want to say, that monad do not turn impure operations into pure ones. It only allows to separate them effectively. (I repeat, that it is only my understanding)

于 2012-01-06T20:12:08.070 回答