Can sequence over infinite maybes ever terminate?

Question

In other words, can the following be optimized to Just [1..]?

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

There is also a more specific example in data61/fp-course where early termination is expected iff an Empty value is present.

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)

Why does changing order of the first two patterns make function loop forever as if Empty cannot be ever matched? I vaguely understand that such definition would make f strict in the infinite list, but I don't see what is actually causing this.

Or are these unrelated problems?

Side question: does it matter that stack is exhausted and not heap?

Answer 1

Even if it could, it shouldn't. As in @user2407038's comment, according to Haskell's denotational semantics, sequence (map Just [1..]) denotes a different value than Just [1..].

Haskell functions are continuous, which is the key tool for reasoning precisely about infinite data structures. To illustrate what continuity means, suppose we have an infinite sequence of values which are increasingly defined, for example:

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

Now, apply a function to each of them, let's say tail:

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

What it means for a function to be continuous is that if you apply the function to the limit of the sequence of arguments, you get the limit of the sequence of results, as illustrated in the final line.

Now some observations about sequence on partially defined lists:

-- 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

We only need the first observation. We can now ask your question:

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..])                                    = ⟂

So by continuity, sequence (map Just [1..]) = ⟂. If you "optimized" it to give a different answer, that optimization would be incorrect.

Answer 2

I cannot answer your second question, but can answer your first one.

In theory the compiler can detect and optimize cases like this, but due to the Halting Problem it's impossible for it to detect every instance of this pattern. The best it can do is a bunch of ad-hoc heuristics, and I think it would be more confusing if the termination of your program depended on whether a particular rewrite rule fired or not.