无限序列是否可能终止？

Question

换句话说，可以将以下内容优化为Just [1..]吗？

> sequence (map Just [1..])
*** Exception: stack overflow

data61/fp-course中还有一个更具体的示例，如果存在Empty值，则有望提前终止。

seqOptional ::
  List (Optional a)
  -> Optional (List a)
seqOptional =
    foldRight f (Full Nil)
      where
          f Empty _ = Empty
          f _ Empty = Empty
          f (Full a) (Full as) = Full (a :. as)

为什么前两个模式的顺序改变会使功能永远循环，好像Empty无法匹配？我模糊地理解，这样的定义会使f在无限列表中严格，但是我看不出是什么真正导致了这一点。

还是这些不相关的问题？

旁边的问题：堆栈耗尽而不是堆有关系吗？

Answer 1

即使可以，也不应该。就像@ user2407038的注释一样，根据Haskell的denotational semantics，sequence (map Just [1..])表示与Just [1..]不同的值。

Haskell函数是continuous，这是精确推理无限数据结构的关键工具。为了说明连续性的含义，假设我们有一个无限的值序列，这些值越来越多地被定义，例如：

⟂
1:⟂
1:2:⟂
1:2:3:⟂

现在，对它们每个应用一个函数，比方说tail：

tail ⟂             = ⟂
tail (1:⟂)         = ⟂
tail (1:2:⟂)       = 2:⟂
tail (1:2:3:⟂)     = 2:3:⟂
     ⋮                 ⋮
tail [1..]         = [2..]

对于一个连续的函数意味着，如果将函数应用于参数序列的limit，则将得到结果序列的limit，如最后的例子所示。行。

现在在部分定义的列表上对sequence的一些观察：

-- a ⟂ after a bunch of Justs makes the result ⟂
sequence (Just 1 : Just 2 : ⟂) = ⟂
-- a Nothing anywhere before the ⟂ ignores the ⟂ (early termination)
sequence (Just 1 : Nothing : ⟂) = Nothing

我们只需要第一个观察。我们现在可以问您一个问题：

sequence (map Just ⟂)       = sequence ⟂                     = ⟂
sequence (map Just (1:⟂))   = sequence (Just 1 : ⟂)          = ⟂
sequence (map Just (1:2:⟂)) = sequence (Just 1 : Just 2 : ⟂) = ⟂
          ⋮                                   ⋮                 ⋮
sequence (map Just [1..])                                    = ⟂

因此，连续性sequence (map Just [1..]) = ⟂。如果您对其进行“优化”以给出不同的答案，则该优化将是不正确的。

Answer 2

我无法回答您的第二个问题，但可以回答您的第一个问题。

理论上，编译器可以检测和优化这种情况，但是由于停止问题，它不可能检测到该模式的每个实例。它可以做的最好的事情就是一堆临时启发式方法，而且我认为，如果程序的终止取决于是否触发了特定的重写规则，将会更加令人困惑。