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

Мне было очень интересно об этом, но я ничего не смог найти.

При использовании функции 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)

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

Ответ 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), поэтому внутри foo q оценивается до результата 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 для функций полностью согласуются с использованием данных на данных.

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

В разделе Противоречия на странице Sequice HaskellWiki есть немного о некоторых последствиях seq относительно функций.

Ответ 2

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

seq a b = case a of
            _ -> b

Это будет оценивать a в форме head-normal (WHNF), а затем продолжить с оценкой b.

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