Функция seq и строгость

Question

Я много размышлял об этом, но не смог ничего найти по этому поводу.

При использовании seq функция, как это тогда действительно работает? Везде просто объясняется, что seq a b оценивает a, отбрасывает результат и возвращает b,

Но что это на самом деле означает? Будет ли следующий результат в строгой оценке:

foo s t = seq q (bar q t) where
      q = s*t

Я имею в виду, что q строго оценены перед использованием в bar? И будет ли следующее эквивалентно:

foo s t = seq (s*t) (bar (s*t) t)

Я немного затрудняюсь разобраться в функциональности этой функции.

Answer 1

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

foo s t = seq q (bar q t) where
      q = s*t

q оценивается раньше bar q t оценивается. Если bar q t никогда не оценивается, q тоже не будет Так что если у вас есть

main = do
    let val = foo 10 20
    return ()

как val никогда не используется, оно не будет оцениваться. Так q не будет оцениваться либо. Если у вас есть

main = print (foo 10 20)

результат foo 10 20 оценивается (print), так в пределах fooq оценивается до результата bar,

Это также, почему это не работает:

myseq x = seq x x

Семантически это означает, что первый x будет оцениваться до второго x оценивается. Но если второе x никогда не оценивается, первый тоже не должен быть. Так seq x x в точности эквивалентно x,

Ваш второй пример может или не может быть то же самое. Здесь выражение s*t будет оцениваться раньше barвывод, но может не совпадать s*t в качестве первого параметра bar, Если компилятор выполняет общее удаление подвыражений, он может объединить два идентичных выражения. GHC может быть довольно консервативным в отношении того, где он проводит CSE, поэтому вы не можете полагаться на это. Если я определю bar q t = q*t он выполняет CSE и оценивает s*t перед использованием этого значения в баре. Это не может сделать это для более сложных выражений.

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

baz xs y = seq xs (map (*y) xs)

xs должен быть список, из-за map, когда seq оценивает его, он по существу преобразует код в

case xs of
  [] -> map (*y) xs
  (_:_) -> map (*y) xs

Это означает, что он определит, является ли список пустым или нет, а затем вернет второй аргумент. Обратите внимание, что ни одно из значений списка не оценивается. Так что вы можете сделать это:

Prelude> seq [undefined] 4
4

но не это

Prelude> seq undefined 5
*** Exception: Prelude.undefined

Какой бы тип данных вы не использовали seqПервый аргумент, оценка WHNF, зайдет достаточно далеко, чтобы выяснить конструктор, и не будет дальше. Если тип данных не имеет компонентов, которые помечены как строгие с шаблоном взрыва. Тогда все строгие поля также будут оцениваться в WHNF.

Редактировать: (спасибо Даниэлю Вагнеру за предложение в комментариях)

Для функций, seq будет вычислять выражение до тех пор, пока функция не будет иметь "лямбда-показ", что означает, что она готова к применению. Вот несколько примеров, которые могут продемонстрировать, что это значит:

-- ok, lambda is outermost
Prelude> seq (\x -> undefined) 'a'
'a'

-- not ok.  Because of the inner seq, `undefined` must be evaluated before
-- the lambda is showing
Prelude> seq (seq undefined (\x -> x)) 'b'
*** Exception: Prelude.undefined

Если вы думаете о лямбда-привязке как (встроенном) конструкторе данных, seq на функции прекрасно согласуется с использованием его на данных.

Кроме того, "лямбда-привязка" включает все типы определений функций, независимо от того, определены ли они лямбда-нотацией или как обычная функция.

В разделе " Противоречие " на странице seq HaskellWiki рассказывается о некоторых последствиях seq по отношению к функциям.

Answer 2

Вы можете думать о seq как:

seq a b = case a of
            _ -> b

Это оценит a к нормальной форме головы (WHNF), а затем продолжить оценку b,

Редактировать после комментария Августа: это case ... of является строгим, GHC Core, который всегда заставляет свои аргументы.