Можно ли определить pseq в терминах seq?

Насколько я знаю, seq a b оценивает (форсирует) a и b перед возвратом b. Это не гарантирует, что a оценивается первым.

pseq a b сначала оценивает a, затем оценивает/возвращает b.

Теперь рассмотрим следующее:

xseq a b = (seq a id) b

Приложение-функция должно сначала оценить левый операнд (чтобы получить лямбда-форму), и оно не может слепо оценить правый операнд перед входом в функцию, потому что это нарушит нестрогую семантику Haskell.

Следовательно, (seq a id) b должен сначала оценить seq a id, что заставляет a и id (в каком-то неопределенном порядке (но оценка id ничего не делает)), затем возвращает id b (то есть b); поэтому xseq a b оценивает a перед b.

Является ли xseq допустимой реализацией pseq? Если нет, то что не так с приведенным выше аргументом (и возможно ли вообще определить pseq через seq)?


lazy-evaluation haskell strictness
person melpomene    schedule 11.02.2017    source источник
comment
Если компилятор решит встроить id в форму seq a (\x->x), то он также увидит, что \x -> x находится в WHNF, поэтому seq a (\x->x) можно "оптимизировать" до a. pseq фактически реализовано с точки зрения seq и lazy, которая является "глубоко волшебной" функцией идентификации, которую компилятор никогда не встраивает во время анализа строгости.   -  person user2407038    schedule 12.02.2017
comment
Магия, которую вы ищете, действительно находится в lazy.   -  person Alec    schedule 12.02.2017
comment
@user2407038 user2407038 Преобразование seq a (\x->x) в a является ошибкой типа. Даже если он встраивает id, ему все равно придется возвращать \x->x (и принудительно a). Это именно то, чего я хочу, не так ли?   -  person melpomene    schedule 12.02.2017
comment
@melpomene Извините, я имел в виду, что seq a (\x->x) b может стать seq a ((\x->x) b) - вообще seq a y o может стать seq a (y o), если y находится в WHNF. Выполнит ли когда-нибудь компилятор такую ​​оптимизацию, я не знаю, но определенно может. Я считаю, что с точки зрения «сырой операционной семантики» (т.е. делать вид, что компилятор вообще никогда не меняет ваш код) ваша функция правильная - она ​​просто ломается при наличии оптимизаций. (действительно, lazy денотационно равно id - так что ваше xseq денотационно равно pseq, и оба seq, только не операционно)   -  person user2407038    schedule 12.02.2017
comment
Вы, кажется, предполагаете, что f x должен сначала оценить f в WHNF, но это может быть не так. Если анализатор строгости окажется f строгим, я думаю, что среда выполнения может сначала оценить x как WHNF без изменения семантики. Я не уверен, действительно ли это происходит в оптимизаторе GHC.   -  person chi    schedule 12.02.2017
comment
Я вижу, что пять человек пока проголосовали за этот вопрос. Мне было бы интересно узнать, почему.   -  person melpomene    schedule 27.08.2018

Ответы (2)


arrow_upward
2
arrow_downward

Ответ, кажется, «нет, по крайней мере, не без дополнительной магии».

Проблема с

xseq a b = (seq a id) b

заключается в том, что компилятор может видеть, что результатом seq a id является id, что является строгим везде. Приложению функции разрешается сначала оценивать аргумент, если функция является строгой, потому что это не меняет семантику выражения. Поэтому оптимизирующий компилятор может сначала начать оценку b, потому что он знает, что в конечном итоге он ему понадобится.

person melpomene    schedule 24.01.2019
comment
Это прекрасный вопрос и ответ. - person Ignat Insarov; 12.10.2019

arrow_upward
0
arrow_downward

Можно ли определить pseq через seq?

В ГХК - да.

Как заметил Алек, вам также понадобится зеркальный дым lazy:

 -- for GHC 8.6.5
import Prelude(seq)
import GHC.Base(lazy)

infixr 0 `pseq`
pseq :: a -> b -> b
pseq x y = x `seq` lazy y

определение соответствует своему аналогу в источниках GHC; импорт очень разный.

Для других реализаций Haskell это может работать:

import Prelude(seq)

infixr 0 `pseq`
pseq :: a -> b -> b
pseq x y = x `seq` (case x of _ -> y)

возможно в сочетании, по крайней мере, с эквивалентом:

 -- for GHC 8.6.5
{-# NOINLINE pseq #-}

Я позволю Мельпомене решить, можно ли это считать зеркальным дымом...

person atravers    schedule 27.08.2020
comment
Любая реализация, -O0 которой не выполняет анализ строгости, должна позволить вам определить неэффективную версию lazy в своем собственном модуле. lazy :: a -> a; lazy x = x {-# NOINLINE lazy #-}. Пока модуль не показывает, что lazy на самом деле является строгим в своем аргументе, и не создает для него развертывание, вы должны быть в порядке. Специальное предложение GHC встраивает его в Core Prep, прямо в конце конвейера компиляции между ядрами. - person dfeuer; 27.08.2020