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

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

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

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

Answer 2

即使可以，也不应该。正如@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..]) = ⟂。如果你 "optimized" 它给出不同的答案，那么优化是不正确的。

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

Can sequence over infinite maybes ever terminate?

haskell

fold

strictness