Про seq

[deni_ok]

Как известно seq вычисляет свой первый аргумент до слабой заголовочной нормальной формы (WHNF). Не пользуясь GHCi, ответьте на вопрос, каково будет значение следующего выражения
Prelude> (\True y -> ()) False `seq` 5 Проверьте себя в GHCi. Какова будет полученная в первом аргументе seq WHNF?

UPD. А теперь вопрос на засыпку: каково будет значение

Comments

[kodt_rsdn]

Эээ, Boolean имеет вид *, а не *->*, как вообще может скомпилиться True y?

[kodt_rsdn]

А, тупанул. В скобках двуместная функция.
Если \P Q -> r истолковывается как \p -> \q -> patternmatching etc...,
то сзнф от частичного применения будет одноместной функцией с отложенным сопоставлением.
То есть, по сути, (\y -> (error "ничего не сопоставилось") :: ()).

[papa_lyosha]

(\True y -> ()) False само является WHNF, т.к. (\True y -> ()) требует двух обязательных аргументов в отличии от (\True -> \y -> ()).
Имено поэтому все патерны в одном патерн-матчинге должно иметь одинаковое количество аргументов.

[deni_ok]

То есть тут написано неправильное определение WHNF:
https://wiki.haskell.org/Weak_head_normal_form

[papa_lyosha]

Видимо да. Там написано, что (+) 2 - WHNF (это правда), но сказано, что это из-за того, что (+) это "build-in function". А это не так, даже если вы определите (+) сами, как \x y -> ..., то всё равно (+) 2 будет WHNF.

Другой дело, что возможно сам такой подход неправильный. Получается, что даже если мы знаем, что f::A->B, мы вчё равно не можем сказать, будет ли (f a) WHNF или нет, не зная как f была определена.

[deni_ok]

Почему не знаем. Знаем.

Prelude> let f = \True -> \y -> ()
Prelude> f False `seq` 5
5

Если мы используем lambda abstraction, то для трансляции используется

\ p1 ... pn -> e = \ x1 ... xn -> case (x1, ... , xn) of (p1, ... , pn) -> e
из раздела 3.3 Haskell Report. А если function binding, то

x = \ x1 ... xk -> case (x1, ... , xk) of (p11, ... , p1k) match1
...
(pn1, ... , pnk) matchn
из раздела 4.4.3.1.

[kurilka]

Интересно, что эту WHNF GHC тупо выкидывает (что логично т.к. мы её не используем):
qrilka@qdesktop ~ $ ghc -ddump-simpl seq.hs

[1 of 1] Compiling Main ( seq.hs, seq.o )

==================== Tidy Core ====================
Result size of Tidy Core = {terms: 7, types: 6, coercions: 0}

main :: IO ()
[GblId, Str=DmdType]
main = print @ Integer GHC.Show.$fShowInteger (__integer 5)

:Main.main :: IO ()
[GblId, Str=DmdType]
:Main.main = GHC.TopHandler.runMainIO @ () main

Linking seq ...
qrilka@qdesktop ~ $ cat seq.hs
main = print $ (\True y -> ()) False `seq` 5

Или есть вариант, когда такая конструкция будет иметь смысл в реальной жизни?

[deni_ok]

А вторую конструкцию, (\True -> \y -> ()) False `seq` 5?

[kurilka]

main :: IO ()
[GblId, Str=DmdType]
main =
print
@ Integer
GHC.Show.$fShowInteger
(case Control.Exception.Base.patError
@ (GHC.Prim.Any -> ()) "seq.hs:1:17-33|lambda"#
of wild_00 {
})

ну и -O0 на результат не влияет ни в том ни в другом случае

[kurilka]

а, хотя -O0 же по дефолту, так что странно былоб иное