7

putStrLn当使用任何参数调用时,将始终返回 type 的值IO ()。我同意这是纯粹的,我可以处理。但它是参照透明的吗?我认为是这样,因为对于任何给定的输入,您都可以将函数调用替换为IO ()将在标准输出中抛出正确字符串的函数调用。

所以我很酷putStrLn,但是getLine当不带参数调用时可以返回任意数量的东西,只要它们是 type IO String。这既不是纯粹的,也不是参照透明的,对吧?

愚蠢的迂腐问题,它可能不会改变我编写代码的方式,但我真的想一劳永逸地解决这个问题。(我知道 IO monad 会正确排序,这不是我的问题)

这对我提出了另一个问题。编译器是否足够聪明,可以识别不需要输入的程序?例如说我编译

main = putStrLn . show $ map (+1) [1..10]

GHC 是否足够聪明,可以将该程序简化为IO ()导致 [2,3,4,5,6,7,8,9,10,11] 被打印出来的程序?还是它仍然可以解决并在运行时评估/执行所有内容?对于不需要输入的任意程序也是如此。GHC 是否采用了整个程序是引用透明的并且可以简单地用它的值替换的事实?

4

6 回答 6

7

是的,这些单子函数是纯粹的引用透明的,因为替换规则仍然适用于它们。

在 Haskell 中,以下两个程序是等价的

main = (puStrLn "17" >> puStrLn "17")
main = let x = putStrLn "17" in (x >> x)

在“正常”语言中,第二个示例只会打印一次,作为评估的副作用x。当您意识到类型的值IO()实际上不是副作用计算,而是实际上是对此类计算的描述时,这两个程序实际上相同的方式变得更加清晰,您可以将其用作构建块来构建更大的计算.

于 2011-12-05T14:17:29.750 回答
7

我认为这里有两个问题。

  1. IO 引用透明吗
  2. GHC 会在编译时减少任意表达式吗

查看 IO 的类型,您可以想象它通过依赖RealWorld没有数据构造函数的神秘值来模拟引用透明性,并使每个语句都依赖于最后一个语句(在单线程世界中)。在 an 的情况下IO String,这是一个围绕RealWorld -> (RealWorld, String)... 的新类型包装器,它是一个函数,而不是一个值。IO在没有实例的情况下使用Monad会使这一点特别而痛苦地显而易见。

Prelude GHC.Types> :info IO
newtype IO a
  = IO (GHC.Prim.State# GHC.Prim.RealWorld
        -> (# GHC.Prim.State# GHC.Prim.RealWorld, a #))

至于 GHC 的优化,在这种情况下,它不会在编译时将列表缩减为字符串。GHC 7.2.1 生成的优化代码延迟生成一个列表,映射 (+1) 结果,将列表转换为字符串,最后将其打印到控制台。几乎与您的示例中的内容完全相同。

于 2011-12-05T08:47:33.847 回答
6

getLine :: IO String是纯净的;它的值是从标准输入读取并返回*字符串的 IO 操作。getLine总是等于这个值。

*我在这里使用“returns”这个词是因为没有更好的词。

维基百科将引用透明度定义为:

如果一个表达式可以用它的值替换而不改变程序的行为(换句话说,产生一个在相同输入上具有相同效果和输出的程序),则称该表达式是引用透明的。

所以 getLine 也是参照透明的。尽管出于“用其价值替换表达式”的目的,我想不出一种以其他方式表达其“价值”的好方法。

putStrLn此外,对于诸如“使用任何参数调用时将始终返回”之类的语句,应该小心一点IO ()IO ()是一个类型,而不是一个值。对于每个s :: String,putStrLn s都是 type 的值IO (),是的。但是这个值是多少,当然取决于s

(此外,如果你排除这些unsafe东西,一切都是纯粹的和参照透明的,尤其如此getLine。)

于 2011-12-05T09:14:16.020 回答
4

让我只回答问题的第二部分(我已经回答了之前问题的第一部分)。只要不改变程序的语义,编译器就可以自由地对表达式做任何事情。因此,您必须询问有关特定编译器的问题才能使其有意义。ghc吗?不,不是当前版本。有没有可以做的编译器?就在这里。

于 2011-12-05T12:46:59.577 回答
3

我不确定这是否会有所帮助(如果它只会让更多人感到困惑,我会提前道歉),但是在 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 个元素。理论上,任何不依赖于输入的程序都可以简化为输出,但为了做到这一点,编译器必须做一些相当于在编译时执行程序的事情。因此,要完全做到这一点,您必须对您的程序有时在编译时进入无限循环感到高兴。而且几乎每个程序依赖于它的输入,因此即使尝试这样做也不会获得太多收益。

通过识别不依赖于任何输入的程序部分并用它们的结果替换它们,可以获得一些东西。这称为部分评估,是一个活跃的研究课题,但也非常困难,没有一刀切的解决方案。要做到这一点,您必须能够识别程序中不会将编译器送入无限循环以试图找出它们返回的区域,并且您必须决定是否删除一些需要花费一些时间的代码如果这意味着将它返回的数百兆数据结构嵌入到程序二进制文件中,那么运行时的秒数就足够了。而且您必须在不花费数小时编译中等复杂程序的情况下完成所有这些分析。

于 2011-12-06T00:00:22.357 回答
2

关于问题的第二部分。有一种叫做超级编译的东西,希望能得到类似的东西。这仍然是一个研究领域。

于 2011-12-05T09:50:52.553 回答