无限可能的序列可以终止吗？答案

【问题标题】：Can sequence over infinite maybes ever terminate?无限可能的序列可以终止吗？
【发布时间】：2018-01-10 23:15:15
【问题描述】：

也就是说，下面的可以优化成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 在无限列表中变得严格，但我看不出实际上是什么原因造成的。

还是这些不相关的问题？

附带问题：堆栈耗尽而不是堆重要吗？

【问题讨论】：

map Just [1..] 不等同于Just [1..]。结果是[Just 1, Just 2, ...]。
我认为 OP 是在询问 sequence 是否可以构造理论答案 Just [1..] 而无需检查其输入的无限多元素。
我觉得这里有两个单独的问题。也许考虑将seqOptional 部分作为一个单独的问题提出，并带有您描述的行为的 MCVE。我看不出改变前两种模式的顺序会如何改变任何东西，所以如果你有一个这样做的特定调用，请发布它。
“为什么改变前两种模式的顺序会使函数永远循环” - 我无法重现这种行为。请附上 MCVE。您无法将sequence (map Just [1..]) 优化为Just [1..]，因为前者是底部，而后者不是（这两个术语表示的值不同——第一个甚至没有值）。也许你的问题是，是否可以定义一个函数s 使得s = sequence 用于有限列表和s (map Just [1..]) = Just [1..] - 答案仍然是否定的，因为s 必须检查无限多的元素，然后终止（即废话）。

标签： haskell fold strictness

【解决方案1】：

即使可以，也不应该。正如@user2407038 的评论，根据Haskell 的denotational semantics，sequence (map Just [1..]) 表示与Just [1..] 不同的值。

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

⟂
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..]) = ⟂。如果您“优化”它以给出不同的答案，那么该优化将是不正确的。

【讨论】：

那么，我是否应该理解在 Haskell 语义中，将无限量的 1s 相乘是底部而不是 1？我可以在哪里阅读更多相关信息？
@sevo wikibook page on denotational semantics 是我开始的地方。

【解决方案2】：

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

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

【讨论】：