list - Haskell:处理死锁的自引用列表

Question

GHC 允许以下内容永久阻塞是否有任何有用的理由:

list = 1 : tail list

似乎在列表迭代器/生成器中有一点复杂，我们应该能够做一些更有用的事情:

1. 返回错误“无限阻止列表”
2. 返回[1,1]

解释 2:似乎有可能当进入生成器获取元素 N 时，我们可以将生成器内的所有自引用限制为列表但以 N-1< 结尾(我们注意到范围 generate N 内的 read N 并返回列表结尾)。这是一种使用范围的简单死锁检测。

显然这对于​​上面的玩具示例没有多大用处，但它可能允许更有用/优雅的有限、自引用列表定义，例如:

primes = filter (\x -> none ((==0).mod x) primes) [2..]

请注意，任何一个更改都应该只影响当前会导致无限 block 的列表生成器，因此它们似乎是向后兼容的语言更改。

暂时忽略进行此类更改所需的 GHC 复杂性，此行为是否会破坏我缺少的任何现有语言行为？关于此更改的“优雅”还有其他想法吗？

另请参阅下面可能受益的另一个 BFS 示例。对我来说，这似乎比其他一些解决方案更实用/更优雅，因为我只需要定义 bfsList 是什么，而不是如何生成它(即指定终止条件):

bfs :: (a -> Bool) -> (a -> [a]) -> [a] -> Maybe a
bfs predf expandf xs = find predf bfsList
    where bfsList = xs ++ concatMap expandf bfsList

Answer 1

这里是关于如何 list = 1 : ⊥ 的指称视角。

首先，介绍一下背景。在 Haskell 中，值按“定义性”部分排序，其中包含 ⊥(“底部”)的值比没有定义的值更少定义。所以

• ⊥ 定义少于 1 : ⊥
• 1 : ⊥ 比 1 : 2 : 3 : []
定义更少

但这是偏序，所以

• 1 : ⊥ 不比 2 : 3 : ⊥ 定义更少，也没有更多定义。

即使第二个列表更长。 1 : ⊥ 仅比以 1 开头的列表定义更少。我强烈建议阅读 denotational semantics Haskell 的。

现在回答你的问题。看看

list = 1 : tail list

作为要求解的方程而不是“函数声明”。我们这样重写它:

list = ((1 :) . tail) list

这样看，我们看到 list 是一个不动点

list = f list

其中 f = (1 :) 。尾部。在 Haskell 语义中，递归值是通过根据上述顺序找到最小不动点来求解的。

找到这个的方法很简单。如果你从 ⊥ 开始，然后一遍又一遍地应用这个函数，你会发现一个递增的值(value)链。链条停止变化的点will be the least fixed point (从技术上讲，这将是链条的极限，因为它可能永远不会停止变化)。

以⊥开头，

f ⊥ = ((1 :) . tail) ⊥ = 1 : tail ⊥

我们看到 ⊥ 还不是一个不动点，因为我们没有从另一端得到 ⊥。所以让我们再试一次我们得到的东西:

f (1 : tail ⊥) = ((1 :) . tail) (1 : tail ⊥)
               = 1 : tail (1 : tail ⊥)
               = 1 : tail ⊥

哦，看，这是一个不动点，我们得到的和我们输入的一样。

这里的重点是它是最少的。您的解决方案 [1,1] = 1:1:[] 也是一个不动点，因此它求解方程:

f (1:1:[]) = ((1 :) . tail) (1:1:[]) 
           = 1 : tail (1:1:[])
           = 1:1:[]

当然，每个以 1 开头的列表都是一个解决方案，我们不清楚我们应该如何在它们之间进行选择。然而，我们通过递归 1:⊥ 找到的那个比所有的定义都少，它提供的信息不超过等式所需的信息，这就是语言指定的那个。