我不确定这是否会有所帮助(如果它只会让更多人感到困惑,我会提前道歉),但是在 Mercury 中使 IO 具有引用透明性的方式是显式地将类型值传递io
给所有执行 IO 的代码,该代码也必须返回类型的新值io
。
输入io
代表代码被调用之前的“世界状态”。程序之外的整个世界;磁盘内容,屏幕上打印的内容,用户将要键入的内容,将从网络接收到的内容,一切。
输出io
代表代码被调用后的世界状态。io
输入和输出之间的差异io
包含该代码对世界所做的更改(加上理论上发生在外部的所有其他内容)。
Mercury 的模式系统确保 type 的值io
是唯一的;它们中只有一个,因此您不能将相同的io
值传递给两个不同的 IO 执行过程。您将一个传递io
给一个过程,使其对您无用,然后接收一个新的返回。
当然,现实世界的真实状态不会被编码为 type 的值io
;事实上引擎盖下io
是完全空的!根本没有信息传递!但io
价值观代表了世界的状态。
您可以将 IO monad 中的函数视为做同样的事情。它们采用一个额外的隐式世界状态参数,并返回一个额外的隐式世界状态值。IO monad 实现处理将这个额外的输出传递给下一个函数。这使得 IO monad 非常像 State monad;很容易看出get
,monad 是纯的,即使它似乎没有参数。
在这种理解中,main 在程序运行之前接收世界的初始状态,并在程序运行后通过线程处理程序中的所有 IO 代码将其转换为世界的状态。
而且由于您自己无法获得世界状态值,因此您无法在其他代码中间启动自己的小 IO 链。这就是确保纯洁性的原因,因为事实上,我们不可能有一个拥有自己状态的全新世界凭空出现。
所以getLine :: IO String
可以认为是类似的东西getLine :: World -> (World, String)
。它是纯粹的,因为它在所有不同的时间被调用并返回不同的字符串,它每次收到的字符串都不同。 World
无论您考虑作为 IO 操作的值,还是在函数之间传递的世界状态,或任何其他机制,所有这些构造都是具象性的。在幕后,所有的 IO 都是用不纯的代码实现的,因为这就是世界的运作方式;当您写入文件时,您已经更改了磁盘的状态。但我们可以在更高的抽象层次上表示这一点,让您以不同的方式思考它。
打个比方,您可以使用搜索树或哈希表或无数其他方式来实现地图。但是在实现了它之后,当您在推理使用映射的代码时,您不会考虑左右子树或桶和哈希,而是考虑作为映射的抽象。
如果我们能够以保持纯度和引用透明性的方式来表示IO,那么我们可以将任何需要引用透明性的推理应用到使用这种表示的代码中。这允许适用于此类代码的所有数学运算(其中大部分用于实现纯度强制语言的高级编译器),即使对于执行 IO 的程序也是如此。
关于您的第二个问题的快速附录。GHC 理论上可以将输入程序简化为输出。我不相信它会非常努力地这样做,因为这通常是无法确定的。想象一个程序不接受任何输入但生成一个无限列表,然后打印它的最后 3 个元素。理论上,任何不依赖于输入的程序都可以简化为输出,但为了做到这一点,编译器必须做一些相当于在编译时执行程序的事情。因此,要完全做到这一点,您必须对您的程序有时在编译时进入无限循环感到高兴。而且几乎每个程序都依赖于它的输入,因此即使尝试这样做也不会获得太多收益。
通过识别不依赖于任何输入的程序部分并用它们的结果替换它们,可以获得一些东西。这称为部分评估,是一个活跃的研究课题,但也非常困难,没有一刀切的解决方案。要做到这一点,您必须能够识别程序中不会将编译器送入无限循环以试图找出它们返回的区域,并且您必须决定是否删除一些需要花费一些时间的代码如果这意味着将它返回的数百兆数据结构嵌入到程序二进制文件中,那么运行时的秒数就足够了。而且您必须在不花费数小时编译中等复杂程序的情况下完成所有这些分析。