Haskell真的是一种纯函数式语言吗?考虑到unsafePerformIO?

46

Haskell通常被引用为纯函数式语言的典范。鉴于存在System.IO.Unsafe.unsafePerformIO,这该如何证明?

编辑:我原以为“纯函数式”意味着不可能将不纯的代码引入程序的函数式部分。


关于您的编辑:但仍然可以创建一个可以从命令式程序调用的功能库。最终,这取决于程序员决定有多少函数性存在。 - Robert Harvey
1
引入不纯净的代码并非不可能,只是这不是默认行为。该语言会花费大量精力来阻止它。然而,不纯净的代码有时非常有用,特别是在一个纯净接口的安全隐藏背后。 - Don Stewart
5
请参见 https://dev59.com/PnI-5IYBdhLWcg3wTWn4 和 https://dev59.com/gXE95IYBdhLWcg3wCJXk 。函数式编程中是否可能存在副作用,以及为什么在 Haskell 中将副作用建模为单子的问题。请注意不要改变原始意思或添加解释。 - Don Stewart
1
而且,https://dev59.com/xnA75IYBdhLWcg3wxcDV - Don Stewart
1
在一个问题中,unsafePerformIO被提到了三次,但没有明确的合理陈述表明这是否会使Haskell变得不纯。 - Stefan Schmidt
好的,我已经在标题中添加了unsafePerformIO。 - Stefan Schmidt
8个回答

119

我们称之为Haskell的语言

unsafePerformIOForeign Function Interface规范的一部分,而不是核心的Haskell 98规范。它可以用于执行本地副作用,以便在暴露纯函数接口时隐藏效果。也就是说,我们使用它来隐藏类型检查器无法为我们隐藏的效果(不像ST monad,后者通过静态保证隐藏效果)。

为了准确说明我们所称的“Haskell”具有多重语言特性,请参考下面的图像。每个环都对应一组特定的计算特性,按安全性排序,并且其面积与表现力相关(即如果您具备该特性,则可以编写的程序数量)。

已知的Haskell 98语言被指定为完全和部分函数,位于中间位置。只允许总函数的Agda(或 Epigram )甚至更不具有表现力,但更“纯”和更安全。虽然今天我们使用的Haskell包括FFI中的所有内容,其中包括unsafePerformIO。也就是说,您可以在现代Haskell中编写任何东西,但如果使用来自外部环的内容,则更难建立由内部环简化的安全和保障保证。

alt text

因此,Haskell程序通常不是完全由可透明引用代码构建的,但它仍然是唯一一种默认情况下是纯的中度常见语言


24
“Haskell本质上是纯函数式的”,但“GHC是Haskell的一个超集实现,包括非纯函数式的外部函数接口(Foreign Function Interface)”。 - yairchu
1
谢谢您提供这个有趣的图形! - Stefan Schmidt
1
我认为我更喜欢这个答案。 - Stefan Schmidt
1
在Haskell 2010中,unsafePerformIO出现在哪个规范中?是Haskell还是FFI? - alternative
@alternative 在语言报告中似乎没有出现。 - ThePiercingPrince
显示剩余2条评论

34
我认为"纯函数式"意味着不可能引入不纯的代码。实际上,unsafePerformIO并不是Haskell的一部分,就像垃圾回收器或运行时系统不是Haskell的一部分一样。系统中存在unsafePerformIO是为了让构建系统的人可以在非常有影响的硬件上创建纯函数式抽象。所有真正的语言都有漏洞,让系统构建者以比下降到C代码或汇编代码更有效的方式完成任务。
至于副作用和I/O如何通过IO单子适应Haskell的整体情况,我认为最容易思考Haskell的方法是它是一种描述有影响计算的纯语言。当所描述的计算是main时,运行时系统会忠实地执行这些影响。 unsafePerformIO是以不安全的方式获取效果的一种方式;其中“不安全”意味着“程序员必须保证安全性”——编译器没有检查任何内容。如果您是一个明智的程序员,并愿意承担重大的证明义务,您可以使用unsafePerformIO。但此时,您不再使用Haskell进行编程;您正在使用类似Haskell的不安全语言进行编程。

请访问以下网址以获取有关Haskell的更多信息:http://www.haskell.org/ghc/docs/6.12.2/html/libraries/在您看来,“Haskell的一部分”是什么意思? - Stefan Schmidt
3
已经在语言标准中定义的内容。仅仅因为某个东西是 GHC 的一部分,并不意味着它是 Haskell 语言的一部分,就像 GCC 中的任何内容都不是 C 语言的一部分一样。 - sepp2k
9
对于这样的问题,“Haskell”指的是“Haskell 2010”标准,或者可能是2003年由剑桥大学出版社发布的“Haskell 98”标准。在其他情况下,许多程序员使用“Haskell”一词来描述 GHC 当周实现的任何内容。 - Norman Ramsey

4

这种语言/实现是纯函数式的。它包括一些“逃生口”,如果你不想使用,可以不用。


2

我认为unsafePerformIO并不意味着Haskell变得不纯。您可以从不纯的函数创建纯(引用透明)函数。

考虑跳表。为了使其正常工作,它需要访问RNG(一个不纯的函数),但这并不使数据结构变得不纯。如果您添加一个项目,然后将其转换为列表,则给定您添加的项目,每次都会返回相同的列表。

因此,我认为应该将unsafePerformIO视为promisePureIO。这是一种函数,意味着具有副作用并因此被类型系统标记为不纯的函数可以通过类型系统被确认为引用透明。

我知道为了实现这一点,您必须对纯的定义进行略微放宽。即纯函数是引用透明的,从不因副作用(如打印)而被调用。


1

安全的Haskell是GHC的最新扩展,为这个问题提供了一个新的答案。unsafePerformIO是GHC Haskell的一部分,但不是安全方言的一部分。

unsafePerformIO只应用于构建引用透明函数,例如记忆化。在这些情况下,包的作者将其标记为“可信任”。安全模块只能导入安全和可信任的模块;它不能导入不安全的模块。

更多信息:GHC手册, 安全的Haskell论文


1

不幸的是,编程语言必须处理一些现实世界的工作,这意味着需要与外部环境进行交互。

好消息是,您可以(并且应该)将这种“过时”的代码的使用限制在程序中少数特定、有良好文档记录的部分。


1
不幸?我会说“幸运” :) 我们不再“不惜一切代价避免成功”。 - Artyom

1

我有一种感觉,我将因为我即将说的话而变得非常不受欢迎,但我觉得我必须回应这里提出的(在我看来是误导性的)信息。

虽然unsafePerformIO确实作为FFI附录的一部分被正式添加到语言中,但其原因主要是历史性的而不是逻辑性的。它在Haskell拥有FFI之前就已经非正式存在并广泛使用。它从未正式成为Haskell主要标准的一部分,因为正如你所观察到的那样,它只是太过尴尬了。我想希望是它在未来某个时候会消失。好吧,我认为这不会发生,也不会消失。

FFI附录的开发为unsafePerformIO提供了一个方便的借口,使其能够被悄悄地加入到官方语言标准中。与添加调用外部(即C)代码的能力相比(在这种情况下,无法静态确保纯度和类型安全),它可能看起来并不那么糟糕。出于政治原因,将它放在这里也非常方便。它培养了这样一个神话:如果没有所有那些肮脏的“设计不良”的C、操作系统或硬件等等,Haskell就会是纯的。当然,unsafePerformIO经常与FFI相关的代码一起使用,但这样做的原因通常更多地与FFI和Haskell本身的设计不良有关,而不是与Haskell试图接口的任何外部事物的设计不良有关。
正如Norman Ramsey所说,官方立场是可以使用unsafePerformIO,前提是使用者满足某些证明义务(主要是这样做不会使重要的编译器转换(如内联和公共子表达式消除)失效)。到目前为止,一切都很好,或者人们可能会这么想。真正的问题在于,这些证明义务无法被满足,而这可能是unsafePerformIO最常见的用例之一,根据我的估计,在野外所有unsafePerformIO中占比超过50%。我指的是可怕的习语“unsafePerformIO hack”,在内联和cse存在的情况下,它是可以证明(事实上显然)完全不安全的。

我实在没有时间、空间或倾向去深入讲解什么是“unsafePerformIO hack”以及为什么真正的IO库需要它,但底线是,那些致力于Haskell IO基础架构的人通常“进退两难”。他们可以提供天生安全的API,但无法在Haskell中进行安全实现,或者他们可以提供固有不安全的API,但可以安全地实现。但他们很少能同时在API设计实现中提供安全性。鉴于“unsafePerformIO hack”在现实世界代码(包括Haskell标准库)中出现的令人沮丧的频率,似乎大多数人选择前者作为两种恶中较轻的一种,并希望编译器不会在内联、CSE或任何其他转换中搞砸事情。

我真希望这一切不是这样。不幸的是,它就是这样。


3
我本想为你的回答点赞,但我认为解释“unsafePerformIO hack”的含义以及为什么在实际IO库中需要它才能使你的回答更有帮助。你的大部分回答只是泛泛而谈。 - Wei Hu
我猜“unsafePerformIO hack”是指http://www.haskell.org/haskellwiki/Top_level_mutable_state中描述的那个。 - hvr

0
Haskell通常被引用作为纯函数式语言的示例。鉴于System.IO.Unsafe.unsafePerformIO的存在,如何证明这一点?编辑:我认为“纯函数式”意味着不可能在程序的函数式部分引入不纯的代码。
IO单子实际上是在Haskell中定义的,您可以在这里看到其定义。此单子的存在不是为了处理不纯性,而是为了处理副作用。无论如何,您实际上可以模式匹配来退出IO单子,因此unsafePerformIO的存在对您不应该造成困扰。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接