Haskell：处理死锁的自引用列表 [英] Haskell: Handling deadlocked self-referential lists

问题描述

是否有任何有用的理由说明为什么GHC允许永久阻止以下内容：

  list = 1：尾列表
  

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

1. 返回错误无限阻止列表


2. 返回 [1,1]

解释2：看来可能在进入生成器以获取元素 N 时，我们可以将生成器内的所有自引用限制在列表中，但以 N-1结尾（我们注意到在生成N 内的中读取N >并返回结束符-list）。这是一种简单的使用范围的死锁检测。

显然这对于​​上面的玩具例子并不有用，但它可能允许更有用/优雅的有限自我例如：

  primes = filter（\ x  - > none（（== 0））。 mod x）primes）[2 ..] 
  

请注意，任何更改只会影响列表生成器，目前导致无限块，因此它们看起来是向后兼容的语言变化。

忽略一段时间做出这种改变所需的GHC复杂性，这种行为是否会中断我缺少的任何现有语言行为？关于这种变化的优雅的任何其他想法？

另见另一个可以从下面受益的BFS示例。对我来说，这似乎比其他一些解决方案更具功能性/优雅性，因为我只需要定义一个bfsList 是，而不是如何生成它（即指定一个终止条件）：

  bfs ::（a  - > Bool） - > （a  - > [a]） - > [a]  - >也许
 bfs predf expandf xs = find pref bfsList 
 where bfsList = xs ++ concatMap expandf bfsList 
  

解决方案

以下是关于 list = 1：⊥的指示性透视。

首先，有一点背景。在Haskell中，值是通过defined部分排序的， （底部）比没有定义的更不明确。所以 $ b

• ⊥的定义不如 1：⊥


• 1：⊥不如 1：2：3：





但是这是部分订单，所以





• 1：⊥ not 定义不如 2：3：⊥ ，也没有更多的定义。
即使第二个列表更长，也是如此。





1：⊥只比从1开始的列表更少定义。我强烈建议阅读指定语义 Haskell。





现在回到您的问题。看看



  list = 1：尾列表
  

作为要解决的方程而不是函数声明。我们重写它：



  list =（（1 :)。tail）list 
  

通过这种方式查看，我们发现 list 是一个 / em>

  list = f list 
  

其中 f =（1 :)。尾。在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：⊥找到的那个比它们的全部定义都要少，它没有提供比等式所要求的更多的信息，那就是由语言指定。




Is there any useful reason why the GHC allows the following to block forever:

list = 1 : tail list

It seems with a bit of sophistication in the list iterator/generator we should be able to do something more useful:

1. Return error "Infinitely blocking list"
2. Return [1,1]

Explaining 2: it seems possible that when entering the generator to get element N, we could then make all self references inside the generator limited to the list but ending at N-1 (we notice the read N inside the scope generate N and return the end-of-list). It's a sort of simple deadlock detection using scopes.

Clearly this isn't that useful for the toy example above, but it may allow for more useful/elegant finite, self-referential list definitions, for example:

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

Note that either change should only affect list generators that would currently result in an infinite-block, so they seem backward compatible language changes.

Ignoring the GHC-complexity required to make such a change for a moment, would this behavior break any existing language behavior that I am missing? Any other thoughts on the "elegance" of this change?

Also see another BFS example that could benefit below. To me, this seems more functional/elegant than some other solutions, since I am only needing to define what a bfsList is, not how to generate it (i.e specifying a terminating condition):

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

解决方案

Here is a denotational perspective on how list = 1 : ⊥.

First, a little background. In Haskell, values are partially ordered by "definedness", where values inolving ⊥ ("bottom") are less-defined than ones without. So

• ⊥ is less defined than 1 : ⊥
• 1 : ⊥ is less defined than 1 : 2 : 3 : []

But it's a partial order, so

• 1 : ⊥ is not less defined than 2 : 3 : ⊥, nor is it more defined.

even though the second list is longer. 1 : ⊥ is only less defined than lists that start with 1. I highly recommend reading about denotational semantics of Haskell.

Now to your question. Look at

list = 1 : tail list

as an equation to be solved instead of a "function declaration". We rewrite it like this:

list = ((1 :) . tail) list

Viewing it this way, we see that list is a fixed point

list = f list

where f = (1 :) . tail. In Haskell semantics, recursive values are solved by finding the least fixed point according to the above ordering.

The way to find this is very simple. If you start with ⊥, and then apply the function over and over, and you will find an increasing chain of values. The point at which the chain stops changing will be the least fixed point (technically the it will be the limit of the chain, since it might not ever stop changing).

Starting with ⊥,

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

we see that ⊥ is not already a fixed point because we didn't get ⊥ out the other end. So let's try again with what we got out:

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

Oh look, it's a fixed point, we got the same thing out that we put in.

The important point here is that it's the least one. Your solution [1,1] = 1:1:[] is also a fixed point, so it solves the equation:

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

But of course, every list that starts with 1 is a solution, and it's unclear how we should choose between them. However, the one we found by recursion 1:⊥ is less defined than all of them, it delivers no more information than required by the equation, and that is the one that is specified by the language.

这篇关于Haskell：处理死锁的自引用列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！