Слабая голова, нормальная форма и порядок оценки

Question

Я много читал о слабой голове и нормальной форме. Но мне все еще трудно представить себе логику порядка оценки Хаскелла

Общий пример, демонстрирующий, когда и как использовать, но я все еще не понимаю, как общий пример

foldl (+) 0 [1..5000000]

может привести к переполнению стека. В то время как другое определение сгиба с использованием seq не

foldl' _ a [] = a
foldl' f a (x:xs) = let a' = f a x in a' `seq` foldl' f a' xs
foldl' (+) 0 [0..5000000]

Из объяснений seq, которые я читал, авторы очень осторожны, чтобы прояснить следующее:

• Первый аргумент seq не гарантируется, что будет оцениваться перед вторым аргументом
• Первый аргумент seq будет оцениваться только для слабой головы нормальной формы
• Оценка первого аргумента seq произойдет только тогда, когда второй оценивается в WHNF

Итак, если вышеприведенное верно (так?), То почему foldl' не переполнен как foldl?

Когда мы уменьшаем один шаг, разве это не должно выглядеть так?

foldl' (+) 0 (1:xs) = let a' = (+) 0 1 in a' `seq` foldl' (+) a' xs

В приведенном выше, второй аргумент seq не находится в WHNF, так как есть функциональное приложение, которое нужно сделать. Гарантируем ли мы оценить первый аргумент seq здесь, прежде чем мы дойдем до WHNF второго аргумента?

Answer 1

• Первый аргумент seq не гарантируется, что будет оцениваться перед вторым аргументом

  Не гарантировано, но компилятор попытается и обычно делает это, если это предотвращает наращивание thunk. Сценарий, в котором это не так хорошо работает, - это параллелизм, следовательно, необходимость pseq - но для foldl' это не актуально.

• Первый аргумент seq будет оцениваться только для слабой головы нормальной формы

  Да, но для встроенных типов чисел WHNF = NF.

• Оценка первого аргумента seq произойдет только тогда, когда второй оценивается в WHNF

  Действительно, и это часто вызывает путаницу. Но in a' `seq` foldl' f a' xs означает, что если вы запросите какой-либо результат, это вызовет seq,

  Когда мы уменьшаем один шаг, разве это не должно выглядеть так? ... второй аргумент seq не в WHNF

  Именно это заставляет seq потому что оценить результат foldl' (+) 0 (1:xs) тебе нужно foldl' (+) a' xs быть WHNF, и seq гарантирует, что этого не произойдет раньше a' это WHNF.