递归定义的 Haskell Data.Array 和严格性的直觉是什么？

Question

考虑这个 Haskell 程序

module RecursiveArray where

import Data.Array ( (!), listArray, Array )

goodArray :: Array Int Int
goodArray = listArray (0, 1) (go 0)
  where
    go x = x : go ((goodArray ! x) + 1)

badArray :: Array Int Int
badArray = listArray (0, 1) (go 0)
  where
    go !x = x : go ((badArray ! x) + 1)

main = do
  print goodArray
  print badArray

哪个将打印

> runghc "RecursiveArray.hs"
array (0,1) [(0,0),(1,0)]
array <program stalls here>

我需要一些帮助来理解这里发生的事情。人们可以使用等式推理来理解正在发生的事情吗？数组内部表示相关吗？

我的困惑在于为什么第二个数组元素的严格性很重要，如果前者已经在缺点中很容易获得。我还注意到，使用数组维度(0, 0)而不是(0, 1)数组会使数组突然定义。

---

我尝试做一些等式推理但失败了，我得到了这个类似的程序：

module RecursiveArray where

import Data.Array ( (!), listArray, Array )

goodArray :: Array Int Int
goodArray = listArray (0, 1) [0, x]
    where x = goodArray ! 0

badArray :: Array Int Int
badArray = listArray (0, 1) [0, x]
    where !x = badArray ! 0

main = do
  print goodArray
  print badArray

但我看到的不一样，因为现在将数组范围设置为(0, 0)仍会导致数组未定义。

Answer 1

列表的表示形式是链表，允许未定义尾部，而数组占用连续的内存块，因此需要定义其整个主干。

\n

查看这种区别的一种方法是使用以下等式：

\n

listArray (0,1) (a : b : t) = array (0, 1) [(0, a), (1, b)]\nlistArray (0,1) (a : \xe2\x8a\xa5) = \xe2\x8a\xa5\n

\n

其中表示包含两个元素和 的array (0,1) [(0, a), (1, b)]数组，分别位于索引和处，并且是未定义值。\n特别注意，在第一个方程中，如果、或是 ，则数组仍然是定义的。（将其视为该类型的构造函数；它是无法表示为用户定义的数据类型的原语。）ab01\xe2\x8a\xa5abt\xe2\x8a\xa5arrayArray

\n

Haskell 程序是一个方程组，其未知的是所有函数和值，程序的含义是该方程组相对于定义顺序的最小解（保证存在解，并且存在解）是至少一个）。

\n

为了表明值 ( goodArray) 确实已定义（即，大于\xe2\x8a\xa5），只需展开其定义，直到我们到达构造函数形式（在本例中为array）。这保证了这goodArray = \xe2\x8a\xa5不是方程的解。

\n

goodArray :: Array Int Int\ngoodArray = listArray (0, 1) (go 0)\n  where\n    go x = x : go ((goodArray ! x) + 1)\n\n            -- unfold go\ngoodArray = listArray (0, 1) (0 : go ((goodArray ! 0) + 1))\n            -- unfold go again\n          = listArray (0, 1) (0 : (goodArray ! 0) + 1 : go (...))\n            -- by the listArray equation above\n          = array (0,1) [(0, 0), (1, (goodArray ! 0) + 1)]\n

\n

因此goodArray定义为：它至少是一个array, 并且允许索引成功以进一步简化该表达式。

\n

在第二个版本中，badArray，其中go是 strict ，不同之处在于，go在我们知道其参数已定义之前，不允许进行第二次展开。

\n

事实上，严格性注释为 生成以下方程go，第二个方程有一个附带条件：

\n

go \xe2\x8a\xa5 = \xe2\x8a\xa5\ngo x = x : go ((badArray ! x) + 1)      if x is not \xe2\x8a\xa5\n

\n

直观上，在应用goto Expand的定义之前go ((badArray ! x) + 1)，您必须将其参数计算为实际整数，显然您最终会陷入无限循环。

\n

这可能足以让你自己相信这badArray是未定义的，但“它会永远持续下去”是一个很难正确理解的论点。更有限的证明技术如下。

\n

证明一个值 ( badArray) 是未定义的，就是证明它\xe2\x8a\xa5是其定义方程的解，换句话说，证明它badArray = \xe2\x8a\xa5确实满足以下系统：

\n

badArray = listArray (0,1) (go 0)\ngo \xe2\x8a\xa5 = \xe2\x8a\xa5\ngo x = x : go ((badArray ! x) + 1)      if x is not \xe2\x8a\xa5\n

\n

要检查这\xe2\x8a\xa5确实是一个解决方案，\n请替换badArray为\xe2\x8a\xa5并简化：

\n

\xe2\x8a\xa5 = listArray (0,1) (go 0)\n  = listArray (0,1) (0 : go ((\xe2\x8a\xa5 ! 0) + 1))  -- (!) is strict\n  = listArray (0,1) (0 : go (\xe2\x8a\xa5 + 1))        -- (+) is strict\n  = listArray (0,1) (0 : go \xe2\x8a\xa5)              -- go is strict\n  = listArray (0,1) (0 : \xe2\x8a\xa5)                 -- listArray needs as many elements from the list as the range (0,1) requires\n  = \xe2\x8a\xa5\n

\n