Can sequence over infinite maybes ever terminate?

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?

Solution

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.