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

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 的指称语义，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..]

这意味着什么的是连续的功能是，如果你应用功能的极限参数的顺序，你会得到限制的结果序列，如在最后一行所示。

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