18

Haskell 语言在引用透明度方面提供的确切承诺/保证是什么？至少 Haskell 报告没有提到这个概念。

考虑表达式

(7^7^7`mod`5`mod`2)

我想知道这个表达式是否为 1。为了我的安全，我会执行两次：

( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )

现在提供(True,False)GHCi 7.4.1。

显然，这个表达式现在在引用上是不透明的。我如何判断一个程序是否会受到这种行为的影响？我可以将整个程序淹没，::但这并不能使它变得非常可读。我想念的还有其他类别的 Haskell 程序吗？那是在完全注释和未注释之间？

（除了我在 SO 上发现的唯一有点相关的问题之外，这上面肯定还有其他问题）

4

7 回答 7

20

对于“兼容”的任何合理定义，我认为无法保证评估多态类型表达式（例如5不同类型）会产生“兼容”结果。

GHCi 会话：

> class C a where num :: a
> instance C Int    where num = 0
> instance C Double where num = 1
> num + length []  -- length returns an Int
0
> num + 0          -- GHCi defaults to Double for some reason
1.0

这看起来因为它打破了引用透明度，length []并且0应该是平等的，但在引擎盖下它num被用于不同的类型。

还，

> "" == []
True
> [] == [1]
False
> "" == [1]
*** Type error

False在最后一行中可以预料到的地方。

所以，我认为只有在指定确切的类型来解决多态性时，引用透明度才成立。一个显式的类型参数应用程序 à la System F 可以始终用其定义替换变量而不改变语义：据我了解，GHC 在优化期间内部正是这样做的，以确保语义不受影响。事实上，GHC Core 有明确的类型参数，可以传递。

于 2014-11-19T15:59:22.687 回答
18

问题是重载，这确实有点违反引用透明度。你不知道(+)Haskell 中类似的东西是做什么的；这取决于类型。

当 Haskell 程序中的数值类型不受约束时，编译器使用类型默认值来选择一些合适的类型。这是为了方便，通常不会导致任何意外。但在这种情况下，它确实导致了一个惊喜。在 ghc 中，您可以使用-fwarn-type-defaults来查看编译器何时使用默认设置为您选择类型。您还可以将该行添加default ()到您的模块中以停止所有默认设置。

于 2014-11-19T19:00:55.133 回答
15

我想到了一些可能有助于澄清事情的事情......

表达式mod (7^7^7) 5具有类型Integral a，因此有两种常用方法将其转换为Int:

  1. 使用操作和类型执行所有算术运算Integer，然后将结果转换为Int.
  2. 使用操作执行所有算术Int运算。

如果在Int上下文中使用表达式，Haskell 将执行方法 #2。如果你想强制 Haskell 使用#1，你必须写：

fromInteger (mod (7^7^7) 5)

这将确保所有算术运算都将使用Integer操作和类型来执行。

当您在 ghci REPL 中输入表达式时，默认规则将表达式键入为Integer，因此使用方法 #1。当您将表达式与!!运算符一起使用时，它被键入为 an Int，因此它是通过方法 #2 计算的。

我原来的答案：

在 Haskell 中，表达式的求值

(7^7^7`mod`5`mod`2)

完全取决于使用哪个Integral实例，这是每个 Haskell 程序员都学会接受的。

每个程序员（在任何语言中）都必须注意的第二件事是，数字运算容易上溢、下溢、精度损失等，因此算术定律可能并不总是成立。例如，x+1 > x并不总是正确的；实数的加法和倍数并不总是关联的；分配规律并不总是成立；等等当你创建一个溢出表达式时，你进入了未定义行为的领域。

此外，在这种特殊情况下，还有更好的方法来评估这个表达式，这可以保留我们对结果应该是什么的更多期望。特别是，如果您想高效准确地计算 a^b mod c，您应该使用“power mod”算法。

更新：运行以下程序以查看Integral实例的选择如何影响表达式的计算结果：

import Data.Int
import Data.Word
import Data.LargeWord -- cabal install largeword

expr :: Integral a => a
expr = (7^e `mod` 5)
  where e = 823543 :: Int

main :: IO ()
main = do
  putStrLn $ "as an Integer: " ++ show (expr :: Integer)
  putStrLn $ "as an Int64:   " ++ show (expr :: Int64)
  putStrLn $ "as an Int:     " ++ show (expr :: Int)
  putStrLn $ "as an Int32:   " ++ show (expr :: Int32)
  putStrLn $ "as an Int16:   " ++ show (expr :: Int16)
  putStrLn $ "as a Word8:    " ++ show (expr :: Word8)
  putStrLn $ "as a Word16:   " ++ show (expr :: Word16)
  putStrLn $ "as a Word32:   " ++ show (expr :: Word32)
  putStrLn $ "as a Word128:  " ++ show (expr :: Word128)
  putStrLn $ "as a Word192:  " ++ show (expr :: Word192)
  putStrLn $ "as a Word224:  " ++ show (expr :: Word224)
  putStrLn $ "as a Word256:  " ++ show (expr :: Word256)

和输出（使用 GHC 7.8.3（64 位）编译：

as an Integer: 3
as an Int64:   2
as an Int:     2
as an Int32:   3
as an Int16:   3
as a Word8:    4
as a Word16:   3
as a Word32:   3
as a Word128:  4
as a Word192:  0
as a Word224:  2
as a Word256:  1
于 2014-11-19T15:48:02.700 回答
7

Haskell 语言在引用透明度方面提供的确切承诺/保证是什么？至少 Haskell 报告没有提到这个概念。

Haskell 不提供准确的承诺或保证。存在许多类似unsafePerformIO或traceShow不具有引用透明性的功能。然而，名为Safe Haskell的扩展提供了以下承诺：

引用透明性——安全语言中的函数是确定性的，评估它们不会产生任何副作用。IO monad 中的函数仍然被允许并且像往常一样运行。但是，根据其类型，任何纯函数都可以保证确实是纯函数。此属性允许安全语言的用户信任这些类型。例如，这意味着 unsafePerformIO :: IO a -> a 函数在安全语言中是不允许的。

Haskell 在此之外提供了一个非正式的承诺：Prelude 和基础库往往没有副作用，而 Haskell 程序员倾向于将带有副作用的东西标记为此类。

显然，这个表达式现在在引用上是不透明的。我如何判断一个程序是否会受到这种行为的影响？我可以用 :: 来淹没程序，但这并不能使它变得非常可读。我想念的还有其他类别的 Haskell 程序吗？那是在完全注释和未注释之间？

正如其他人所说，问题来自这种行为：

Prelude> ( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(True,False)
Prelude> 7^7^7`mod`5`mod`2 :: Integer
1
Prelude> 7^7^7`mod`5`mod`2 :: Int
0

发生这种情况是因为7^7^7一个巨大的数字（大约 700,000 个十进制数字）很容易溢出 64 位Int类型，但问题在 32 位系统上无法重现：

Prelude> :m + Data.Int
Prelude Data.Int> 7^7^7 :: Int64
-3568518334133427593
Prelude Data.Int> 7^7^7 :: Int32
1602364023
Prelude Data.Int> 7^7^7 :: Int16
8823

如果使用rem (7^7^7) 5Int64 的余数将被报告为-3但是因为 -3 相当于 +2 模 5，所以mod报告 +2。

由于类Integer的默认规则，答案在左侧使用Integral；由于. Int_ (!!) :: [a] -> Int -> a如果您使用适当的索引运算符来Integral a代替获得一致的东西：

Prelude> :m + Data.List
Prelude Data.List> ((7^7^7`mod`5`mod`2) == 1, genericIndex [False,True] (7^7^7`mod`5`mod`2))
(True,True)

这里的问题不在于引用透明性，因为我们调用的函数^实际上是两个不同的函数（因为它们具有不同的类型）。让你感到困惑的是类型类，它是Haskell中约束歧义的一种实现；您已经发现这种歧义（与不受约束的歧义不同——即参数类型）会产生违反直觉的结果。这不应该太令人惊讶，但有时肯定有点奇怪。

于 2014-11-19T19:25:29.497 回答
5

已选择另一种类型，因为!!需要Int. 完整的计算现在使用Int而不是Integer.

λ> ( (7^7^7`mod`5`mod`2 :: Int)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(False,False)
于 2014-11-19T15:32:59.743 回答
4

您认为这与参照透明性有什么关系？您对7, ^, mod, 5,2和==的使用是这些变量对字典的应用，是的，但我不明白为什么您认为这一事实使 Haskell 引用不透明。毕竟，通常将相同的函数应用于不同的参数会产生不同的结果！

引用透明度与这个表达式有关：

let x :: Int = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)

x这里是单个值，并且应该始终具有相同的单个值。

相比之下，如果你说：

let x :: forall a. Num a => a; x = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)

（或使用等效的表达式 inline）现在是一个函数，并且可以根据您提供给它x的参数返回不同的值。Num你不妨抱怨let f = (+1) in map f [1, 2, 3]is [2, 3, 4]，但是let f = (+3) in map f [1, 2, 3]is[4, 5, 6]然后说“Haskellmap f [1, 2, 3]根据上下文给出不同的值，所以它在引用上是不透明的”！

于 2014-11-19T16:18:17.730 回答
2

可能另一个类型推断和引用透明相关的事情是“可怕的”单态限制（准确地说，它的缺失）。直接报价：

一个例子，来自“A History of Haskell”：
考虑 genericLength 函数，来自Data.List

genericLength :: Num a => [b] -> a

并考虑函数：

f xs = (len, len) where len = genericLength xs

len有类型Num a => a，并且没有单态限制，它可以被计算两次。

请注意，在这种情况下，两个表达式的类型是相同的。结果也是如此，但替换并不总是可能的。

于 2014-11-28T13:19:31.743 回答