用 IO 理解 Haskell 中的纯函数

Question

给定一个 Haskell 值（根据Rein Heinrich 的comment 编辑）f：

f :: IO Int
f = ... -- ignoring its implementation

引用“使用 Idris 进行类型驱动开发”

纯函数的关键特性是相同的输入总是产生相同的结果。此属性称为引用透明度

f 和，即 Haskell 中的所有 IO ... 函数是纯的吗？在我看来，他们不是因为lookInDatabase :: IO DBThing，不会总是返回相同的值，因为：

• 在 t=0 时，数据库可能已关闭
• 在 t=1 时，DB 可能已启动，return MyDbThing 将导致

简而言之，f（和一般的IO ... 函数）是纯的吗？如果是，请纠正我的错误理解，因为我试图用我的 t=... 示例来反驳 f 的功能纯度。

Answer 1

IO 在概念上确实是一门独立的语言。它是 Haskell RTS（运行时系统）的语言。它在 Haskell 中作为（相对简单的）嵌入式 DSL 实现，其“脚本”类型为 IO a。

因此，返回 IO a 类型值的 Haskell 函数实际上并不是在运行时执行的函数——被执行的是 IO a 值本身。所以这些函数实际上是纯的，但它们的返回值代表非纯计算。

从语言设计的角度来看，IO 是一种非常优雅的 hack，它可以将非纯粹的丑陋完全隔离，同时将其紧密地集成到其纯粹的环境中，而无需使用特殊的外壳。换句话说，该设计并没有解决不纯 IO 引起的问题，但它做得很好，至少不影响代码的纯部分。

---

下一步是研究 FRP — 使用 FRP，您可以使包含 IO 的层更薄，并将更多的非纯逻辑移动到纯逻辑中。

您可能还想阅读 John Backus 关于函数编程、冯诺依曼架构的局限性等主题的著作。如果您对纯度和 IO 之间的关系感兴趣，Conal Elliott 也是 google 的名称。

---

附：另外值得注意的是，虽然 IO 严重依赖 monad 来解决惰性求值的一个方面，并且因为 monad 是一种非常好的构建嵌入式 DSL 的方式（其中 IO 只是一个示例），但 monad 比IO，所以尽量不要在同一个上下文中过多地考虑 IO 和 monad——它们是两个独立的东西，两者都可以在没有另一个的情况下存在。

Answer 2

首先，您正确地注意到 I/O 操作不是纯粹的。这不可能。但是，所有函数的纯度是 Haskell 的一大亮点，那么发生了什么？

不管你喜欢与否，一个函数应用于（也可能被错误地称为“返回一个”）IO Something 并带有一些参数将总是返回相同的 IO Something 和相同的论点。 IO monad 允许您在 monad 行为的容器内“隐藏”操作。当您拥有IO String 时，该函数/对象确实不包含String/[Char]，而是某种承诺，您将来会以某种方式获得String .因此，IO 包含在需要执行不纯 I/O 操作时做什么的信息。

毕竟，执行IO 操作的唯一方法是使用名称main，或者成为main 的依赖项。由于 monad 的灵活性，您可以“连接”IO 操作。像这样的程序……（注意：这段代码不是个好主意）

main = do
    input <- getLine
    putStrLn input

是...的合成糖

main =
    getLine >>= (\input -> putStrLn input)

这将表明main 是从标准输入读取的字符串打印到标准输出所产生的 I/O 操作，后跟换行符。你看到魔法了吗？ IO 只是一个包装器，表示在不纯的上下文中做什么，以产生一些给定的输出，但不是该操作的 result，因为这需要Haskell 语言承认不纯代码。

把它想象成一种收据。如果你有一个蛋糕的收据（阅读：IOmonad）（阅读：Something in IO Something），你知道如何做蛋糕，但你不能做蛋糕（因为你可以把它搞砸杰作）。相反，Master Chief（阅读：Haskell 运行时系统的最基本部分，负责应用main）为您完成肮脏的工作（阅读：做不纯/非法的事情），最重要的是，他赢了不要犯任何错误（阅读：破坏代码纯度）...除非烤箱当​​然坏了（阅读：System.IO.Error），但他知道如何清理它（阅读：代码将总是保持纯洁）。

这是IO 是不透明类型的原因之一。它的实现有些争议（直到您阅读 GHC 的源代码），最好由实现定义。

要快乐，因为你已经被纯洁照亮了。很多程序员甚至不知道 Haskell 的存在！

我希望这对你有所启发！

Answer 3

Haskell 在这里耍了个花招。 IO 既是纯的，也不是纯的，这取决于您如何看待它。

在“IO 是纯的”方面，您陷入了一个非常常见的错误，即认为函数返回 IO DBThing，因为它返回的是 DBThing。当有人声称 Stuff -> IO DBThing 类型的函数是纯函数时，他们不是说您可以提供相同的 Stuff 并始终得到相同的 DBThing；正如您正确指出的那样，这是不可能的，也不是很有用！他们节省的是，给定特定的Stuff，您将始终得到相同的IO DBThing。

实际上，您根本无法从IO DBThing 中得到DBThing，因此Haskell 不必担心数据库在不同时间包含不同的值（或不可用）。使用IO DBThing 所能做的就是将它与需要DBThing 的其他东西结合起来，并产生其他类型的IO thing；这种组合的结果是IO thing。

Haskell 在这里所做的是在纯 Haskell 值的操作与程序之外的世界中可能发生的变化之间建立对应关系。有些事情你可以用一些普通的纯值来做，这些事情对不纯的操作没有任何意义，比如改变数据库的状态。因此，使用 IO 值与外部世界之间的对应关系，Haskell 根本不会为您提供对 IO 值的任何操作，将对应于在现实中没有意义的事情世界。

有几种方法可以解释您是如何“纯粹”操纵现实世界的。一种是说IO 就像一个状态单子，只有被线程化的状态是你程序之外的整个世界；=（所以你的Stuff -> IO DBThing 函数确实有一个额外的隐藏参数来接收这个世界，实际上返回一个 DBThing 和另一个世界；它总是被不同的世界调用，这就是为什么即使使用相同的 Stuff 调用它也可以返回不同的 DBThing 值）。另一种解释是IO DBThing 值本身就是一个命令式程序；你的 Haskell 程序是一个完全不做 IO 的纯函数，它返回一个做 IO 的不纯程序，而 Haskell 运行时系统（不纯）执行它返回的程序。

但实际上，这些都只是比喻。关键是 IO 值只是有一个非常有限的界面，它不允许你做任何在现实世界中没有意义的事情。

请注意，monad 的概念实际上并没有出现。 Haskell 的 IO 系统真的不依赖于 monad。 Monad 只是一个方便的接口，它有足够的限制，如果你只使用通用的 monad 接口，你也不能打破 IO 限制（即使你不知道你的 monad 是实际上是 IO）。由于Monad 接口也足够有趣，可以编写很多有用的程序，IO 形成一个 monad 的事实允许大量对其他类型有用的代码在 IO 上通用地重用。

这是否意味着您实际上可以编写纯 IO 代码？并不真地。这是硬币的“当然 IO 不是纯粹的”一面。当您使用花哨的“将 IO 功能组合在一起”时，您仍然需要考虑您的程序一个接一个地（或并行地）执行步骤，影响并受外部条件和系统的影响；简而言之，您必须使用与用命令式语言编写 IO 代码完全相同的推理（仅使用比大多数类型系统更好的类型系统）。使 IO 变得纯粹并不能真正帮助您消除对代码的思考方式中的杂质。

那有什么意义呢？对于一个人来说，它为我们提供了一种编译器强制划分的可以执行 IO 的代码和不能执行 IO 的代码。如果类型上没有 IO 标记，则不涉及不纯 IO。 那在任何语言中都是有用的。编译器也知道这一点； Haskell 编译器可以对在大多数其他语言中无效的非 IO 代码进行优化，因为通常不可能知道给定的代码部分没有有副作用（除非你能看到完整的代码调用的所有内容的实现，可传递）。

另外，由于 IO 是纯粹的，代码分析工具（包括你的大脑）不必专门处理 IO 代码。如果您可以挑选出对与 IO 代码具有相同结构的纯代码有效的代码转换，则可以在 IO 代码上进行。编译器利用了这一点。 IO 代码必须使用的结构排除了许多转换（为了保持在与外界事物有合理对应关系的事物范围内），但它们也会被排除在外任何使用相同结构的纯代码； IO接口的精心构建使得“执行顺序依赖”看起来像普通的“数据依赖”，所以你可以直接使用数据依赖的规则来确定使用IO的规则。

Answer 4

简短回答：是的，f 是引用透明的。

无论何时查看它，它都等于相同的值。
但这并不意味着它总是绑定相同的值。

Answer 5

简而言之，f（和一般的IO ... 函数）是纯的吗？

所以你真正要问的是：

Haskell 中的 IO 定义是纯的吗？

你真的不会喜欢它。

深思。

It depends on what you mean by "pure".

来自Haskell 2010 report 的第 6.1.7 节（第 75 页）：

IO 类型用作与外部世界交互的操作（动作）的标记。 IO 类型是抽象的：没有构造函数对用户可见。 IO 是 Monad 和 Functor 类的一个实例。

关键是：

IO 类型是抽象

如果 Haskell 的 FFI 得到充分增强，IO 可以很简单：

data IO a  -- a tag type: no visible constructors

instance Monad IO where
    return = unitIO
    (>>=)  = bindIO

foreign import unsafe unitIO :: a -> IO a
foreign import unsafe bindIO :: IO a -> (a -> IO b) -> IO b
                        ⋮

没有任何 Haskell 定义：所有与 I/O 相关的活动都是通过调用外部代码来执行的，通常使用与 Haskell 实现相同的语言编写。这种方法的一种变体 is used in Agda:

4 编译 Agda 程序

本节讨论让 Agda 程序交互的主题 与现实世界。类型检查 Agda 程序需要评估 任意项，只要所有项都是纯项并规范化，这是 不是问题，但是当我们引入副作用时会发生什么？清楚地， 我们不希望在编译时发生副作用。另一个问题是 语言应该为构建副作用提供什么原语 程式。在 Agda 中，这些问题通过允许任意 Haskell 函数作为公理导入。在编译时，这些导入 函数没有归约行为，只有在运行时才是 Haskell 函数已执行。

^{（强调。）}

通过将 I/O 问题移到 Haskell 或 Agda 之外，“纯度”问题现在由其他语言（或多种语言！）来解决。

鉴于这些情况，IO 没有“标准定义”，因此没有通用方法来确定该类型的此类属性，更不用说它的任何表达式。我们甚至无法提供一个简单的证据来证明IO 是一元的（即它满足monad laws），因为return 和(>>=) 只是不能在标准Haskell 2010 中定义。 p>

要了解这如何影响各种IO 相关属性的确定，请参阅：

• Semantics of fixIO，作者：Levent Erkok、John Launchbury 和 Andrew Moran。

• Tackling the Awkward Squad: … 由 Simon Peyton Jones 撰写（从第 20 页的第 3.2 节开始）。

因此，当您下次听到或读到 Haskell 是“引用透明”或“纯函数式”时，您现在知道（至少对于 I/O）它们只是推测 - 没有实际标准定义意味着没有办法证明或反驳它们。

（如果您现在想知道 Haskell 是如何进入这种状态的，我会提供更多详细信息 here。）