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

3

GHC为什么允许以下代码永远阻塞?是否有什么有用的原因:

list = 1 : tail list

似乎通过对列表迭代器/生成器的一些复杂操作,我们应该能够做些更有用的事情:
  1. 返回错误 "无限阻塞列表"
  2. 返回 [1,1]
解释第二条:当进入生成器以获取元素 N 时,我们似乎可以使生成器内部所有自引用都限制在列表内,但结束于 N-1 (我们注意到 read N 在作用域 generate N 内部,并返回列表结尾)。这是一种使用作用域进行简单死锁检测的方法。
显然,对于上面的玩具示例来说,这并没有什么用处,但它可能允许更有用/优雅的有限自引用列表定义,例如:
primes = filter (\x -> none ((==0).mod x) primes) [2..]

请注意,任何变更都只应影响当前会导致无限阻塞的列表生成器,因此它们似乎是向后兼容的语言变更。
暂时忽略实现这种改变需要的GHC复杂性,这种行为是否会破坏我所忽略的任何现有语言行为?对于这种变化的“优雅程度”,还有其他想法吗?
另请见下面可能受益的另一个BFS示例。对我而言,这似乎比其他一些解决方案更具有功能性/优雅性,因为我只需定义bfsList是什么,而不是指定终止条件(即如何生成它)。
bfs :: (a -> Bool) -> (a -> [a]) -> [a] -> Maybe a
bfs predf expandf xs = find predf bfsList
    where bfsList = xs ++ concatMap expandf bfsList

6
虽然在这个特定案例中可能很简单,但一般情况下您正在要求编译器解决停机问题。但无论如何,为什么编译器不能根据代码描述表示列表呢?在该示例中返回 [1,1] 是完全无意义的,因为例如 [1,32132132] 同样有效。 - AJF
4
给定list = 1: tail list,即list = 1:t,其中t = tail list,那么t是什么?它是t = tail list = tail (1: t) = t。即使从方程推导中得出t = t对于任何值的t都是显然有效的,但这实际上并没有说明t的任何特定值,因此没有理由给它任何特定的值。尝试打印list可能会导致[1,***错误:检测到黑洞***[1,并陷入无限循环。将列表关闭为[1]意味着t = [],这也是不合理的(因此,从方程推导的角度来看,这是错误的)。 - Will Ness
2
“list = 1 : tail list” 在 Haskell 中不会阻塞任何东西,也不会在 GHC Haskell 中阻塞。这是一个完全有效的值定义,具有良好定义的操作,这些操作适用且实用。 - Justin L.
1
解决递归方程意味着在某个域中找到一个合适函数的最小不动点。这里的最小表示“最少定义”:任何比这更多定义的都涉及从空气中创造价值。例如,解决 let (a,b,c,d) = (b,1,d,c) 必须选择 a=b=1,但有无限多种选择 c,d。由于我们无法一般地解决停机问题,唯一明智的选择是 c=d=bottom,其中 bottom 是非终止/无限递归/无限循环。 - chi
2个回答

5

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

首先,先了解一下背景。在Haskell中,值按“确定性”部分排序,其中包含 ⊥(“底部”)的值比没有 ⊥ 的值更少确定。所以:

  • 不如 1 : ⊥ 确定
  • 1 : ⊥ 不如 1 : 2 : 3 : [] 确定

但这只是一个部分排序,因此:

  • 1 : ⊥2 : 3 : ⊥ 相比,不确定度也不高或低。

即使第二个列表更长。 1 : ⊥ 只不确定度低于以1开头的列表。我强烈建议了解Haskell的指称语义

现在来回答你的问题。看看:

list = 1 : tail list

作为方程式而不是“函数声明”的解决方案。我们将其重写为:

list = ((1 :) . tail) list

以这种方式查看,我们可以看到list是一个不动点
list = f list

其中f = (1 :) . tail。在Haskell语义中,递归值是通过根据上述排序找到最小不动点来解决的。

找到最小不动点的方法非常简单。如果您从⊥开始,然后一遍又一遍地应用该函数,您将找到一个逐渐增长的值链。链停止变化的点将是最小不动点(严格来说,它将是链的极限,因为它可能永远不会停止变化)。

从⊥开始:

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:⊥比它们所有的都要少定义,它提供的信息不超过方程所需的信息,这就是语言指定的那个。


2

尽管在GHCi下,list会无限循环,但使用GHC编译的二进制文件能够检测到循环并报错。如果你进行编译和运行,即:

list = 1 : tail list
main = print list

如果出现以下错误信息,则表示程序已经终止:

Loop: <<loop>>

它对您的primes示例执行相同的操作。

正如其他人所指出的,GHC无法检测所有可能的循环。如果可以,那么它将解决停机问题,这可能会使Haskell更受欢迎。

它返回错误(或“卡住”)而不是返回[1,1]的原因是因为表达式:

list = 1 : tail list

Haskell语言中定义了底值语义,它赋予表达式一个值,这个值是“bottom”(或“error”或符号_|_),就像head [1,2,3]的值一样是1

(严格来说,list的值是1 : _|_,几乎等于底值。这是@Justin Li在评论中谈到的问题。我在下面尝试解释了为什么它有这个值。)

虽然您可能看不出一个返回底值的程序或表达式的用途,也看不出在基础上分配非底值语义的危害,但Haskell社区的大多数人(语言设计者、编译器开发者和经验丰富的用户)会不同意您的看法,因此不要期望与他们取得太多进展。

至于您提出的具体新语义,它们不清楚。为什么list的值不等于[1]?我认为当我输入“生成器”以获取元素n=1(从零开始索引,因此第二个元素)并评估tail list时,结束于元素n-1=0的list[1],它的尾巴等于[],所以我应该得到以下结果,对吧?

list = 1 : tail list
     = 1 : tail [1]   -- use list-so-far
     = 1 : []
     = [1]

为什么值(几乎)是底部

根据标准 Haskell 的语义(但请参见末尾的注释),这就是为什么 list 的值(几乎)是底部的原因。

作为参考,tail 的定义实际上是:

tail l = case l of _:xs -> xs
                   [] -> error "ack, you dummy!"

让我们尝试使用Haskell语义“完全”评估list

-- evaluating `list` using definition of `list`
list = 1 : tail list

-- evaluating `tail list` using definition of `tail`
list = 1 : case list of _:xs -> xs
                        ...
-- evaluating case construct requires matching `list` to
-- a pattern, this requires evaluation of `list` using its defn
list = 1 : case (1 : tail list) of _:xs -> xs
                                   ...
-- case pattern match succeeds
list = 1 : let xs = tail list in xs    -- just to be clear
     = 1 : tail list

-- awesome, now all we need to do is evaluate:
list = 1 : tail list
-- ummm, Houston, we have a problem

最后的无限循环是导致该表达式被称为“几乎底部”的原因。

注意:实际上有几种不同的Haskell语义,不同的计算Haskell表达式值的方法。黄金标准是@luqui答案中描述的指示性语义。我上面使用的语义,最多可以被视为Haskell报告中描述的一种“非正式语义”,但足以得到正确的答案。


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