递归定义的 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>

我需要一些帮助来理解这里发生的事情。可以使用等式推理来理解发生了什么吗？数组内部表示是否相关？

我的困惑在于为什么第二个数组元素的严格性很重要，如果前者已经很容易在 cons 中使用。我还注意到，使用数组维度

(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

虽然列表的表示是链表，它允许尾部未定义，但数组占用连续的内存块，因此需要定义其整个脊柱。

看到这种区别的一种方法是如下等式：

listArray (0,1) (a : b : t) = array (0, 1) [(0, a), (1, b)]
listArray (0,1) (a : _|_) = _|_

其中

array (0,1) [(0, a), (1, b)]

表示分别在索引

a

和

b

处包含两个元素

0

和

1

的数组，并且

_|_

是未定义的值。 请特别注意，在第一个等式中，如果

a

、

b

或

t

是

_|_

，则数组仍然定义。 （将

array

视为

Array

类型的构造函数；它是一个原始数据，不能表示为用户定义的数据类型。）

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

为了证明一个值 (

goodArray

) 确实被定义了（即，大于

_|_

），展开它的定义就足够了，直到我们到达构造函数形式（在这种情况下，

array

）。这保证了

goodArray = _|_

不是方程的解。

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

            -- unfold go
goodArray = listArray (0, 1) (0 : go ((goodArray ! 0) + 1))
            -- unfold go again
          = listArray (0, 1) (0 : (goodArray ! 0) + 1 : go (...))
            -- by the listArray equation above
          = array (0,1) [(0, 0), (1, (goodArray ! 0) + 1)]

因此

goodArray

被定义：它至少是一个

array

，这允许索引成功以进一步简化该表达式。

在第二个版本

badArray

中，

go

是严格的，不同之处在于

go

的第二次展开是不允许的，直到我们知道它的参数被定义。

实际上，严格性注释为

go

生成了以下方程式，在第二个方程式中有一个附加条件：

go _|_ = _|_
go x = x : go ((badArray ! x) + 1)      if x is not _|_

直觉上，在应用

go

的定义展开

go ((badArray ! x) + 1)

之前，您必须将其参数计算为实际整数，显然您最终陷入无限循环。

这可能足以让你自己相信

badArray

是未定义的，但是“它永远持续下去”是一个很难正确的论证。下面是一个更有限的证明技术。

证明一个值（

badArray

）是未定义的就是证明

_|_

是其定义方程的解，换句话说，证明

badArray = _|_

确实满足以下系统：

badArray = listArray (0,1) (go 0)
go _|_ = _|_
go x = x : go ((badArray ! x) + 1)      if x is not _|_

检查

_|_

确实是一个解决方案， 将

badArray

替换为

_|_

并简化：

_|_ = listArray (0,1) (go 0)
    = listArray (0,1) (0 : go ((_|_ ! 0) + 1))  -- (!) is strict
    = listArray (0,1) (0 : go (_|_ + 1))        -- (+) is strict
    = listArray (0,1) (0 : go _|_)              -- go is strict
    = listArray (0,1) (0 : _|_)                 -- listArray needs as many elements from the list as the range (0,1) requires
    = _|_