Про seq

Oct. 1st, 2015 12:29 am
deniok: (typed lambda)
[personal profile] deniok
Как известно seq вычисляет свой первый аргумент до слабой заголовочной нормальной формы (WHNF). Не пользуясь GHCi, ответьте на вопрос, каково будет значение следующего выражения
Prelude> (\True y -> ()) False `seq` 5
Проверьте себя в GHCi. Какова будет полученная в первом аргументе seq WHNF?

UPD. А теперь вопрос на засыпку: каково будет значение следующего выражения
Prelude> (\True -> \y -> ()) False `seq` 5
Считаете ли вы это правильным?

Date: 2015-09-30 09:51 pm (UTC)
From: [identity profile] kodt-rsdn.livejournal.com
Эээ, Boolean имеет вид *, а не *->*, как вообще может скомпилиться True y?

Date: 2015-09-30 10:04 pm (UTC)
From: [identity profile] kodt-rsdn.livejournal.com
А, тупанул. В скобках двуместная функция.
Если \P Q -> r истолковывается как \p -> \q -> patternmatching etc...,
то сзнф от частичного применения будет одноместной функцией с отложенным сопоставлением.
То есть, по сути, (\y -> (error "ничего не сопоставилось") :: ()).

Date: 2015-09-30 10:09 pm (UTC)
From: [identity profile] papa-lyosha.livejournal.com
(\True y -> ()) False само является WHNF, т.к. (\True y -> ()) требует двух обязательных аргументов в отличии от (\True -> \y -> ()).
Имено поэтому все патерны в одном патерн-матчинге должно иметь одинаковое количество аргументов.

Date: 2015-09-30 10:26 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
То есть тут написано неправильное определение WHNF:
https://wiki.haskell.org/Weak_head_normal_form

Date: 2015-10-01 12:08 am (UTC)
From: [identity profile] papa-lyosha.livejournal.com
Видимо да. Там написано, что (+) 2 - WHNF (это правда), но сказано, что это из-за того, что (+) это "build-in function". А это не так, даже если вы определите (+) сами, как \x y -> ..., то всё равно (+) 2 будет WHNF.

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

Date: 2015-10-01 08:18 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Почему не знаем. Знаем.
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.

Date: 2015-10-01 09:56 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Предыдущий мой комментарий был, конечно, дурацки устроен. Это просто некоторая справка, я не разобрался какой подход вы считаете неправильным.

Date: 2015-10-02 05:13 pm (UTC)
From: [identity profile] lomeo.livejournal.com
А это как трактовать?

If a lambda abstraction is applied to "too few arguments", then evaluating the application just means substituting arguments for some of the lambda abstraction's variables, which always halts with the result a now unapplied lambda abstraction.

Какой именно unapplied?
(\True y -> ()) False = (\True -> \y -> ()) False или (\y -> (\True y -> ()) False y)?

Судя по запуску в GHCi второе. Как-то мутно всё.

Date: 2015-10-02 05:35 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Не, я выше писал, лямбда с паттернами транслируется по правилу
\ p1 ... pn -> e = \ x1 ... xn -> case (x1, ... , xn) of (p1, ... , pn) -> e
то есть
(\True y -> ()) False 
  ~> (\x1 x2 -> case (x1,x2) of (True,y) -> ()) False 
  ~> \x2 -> case (False,x2) of (True,y) -> ()
Ну может переменная y и не переименовывается, но это уж точно неважно.

Date: 2015-10-02 08:04 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Но тогда
(\True -> \y -> ()) False
-> (\x1 -> case (x1) of (True) -> (\x2 -> ())) False
-> case (False) of (True) -> (\x2 -> ())
-> error

WHNF у case будет его применение, чтобы под определение попало?

Но тогда не built-in функция будет (\y -> f x y) что ли? Что такое f x вообще (частичное применение)? Это лямбда?

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


WTF?

Date: 2015-10-02 08:29 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
1. Ну так да, именно так и ведет себя:
GHCi> (\True -> \y -> ()) False `seq` 42
*** Exception: :21:2-18: Non-exhaustive patterns in lambda
2. Я выше писал трансляцию function binding из haskell report. Любая определенная пользователем именованная функция семантически эквивалентна (ну то есть, проще говоря, превращается при трансляции в core в)
x = \ x1 ... xk -> case (x1, ... , xk) of (p11, ... , p1k) match1
                                          ...
                                          (pn1, ... , pnk) matchn

Date: 2015-10-02 08:37 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
То есть для меня открытие последних суток в том, что \x -> \y -> body и \x y -> body это в Хаскеле достаточно отличающиеся вещи: первое - неименованная функция арности 1 (несмотря на тип), а второе - арности 2.

Date: 2015-10-02 09:56 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Ну да. Странно.

Date: 2015-10-02 11:22 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
С другой стороны я и раньше знал, что они не идентичны: \b -> \b -> b - допустимое выражение, а \b b -> b - нет. Каждая отдельная лямбда монтирует свою область видимости для связываемой переменной, а двойная - общую для двух переменных.

Date: 2015-10-03 06:53 am (UTC)
From: [identity profile] lomeo.livejournal.com
Это совсем другое, не считается. Я думал, что с точностью до переименований они одинаковые. И, главное, семантически действительно одинаковы, если паттерна нет.

Date: 2015-10-02 05:46 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
И функции так же транслируются. То есть можно считать все функции - примитивные лямбды заданной арности, а сопоставление с образцом откладывается до момента полной аппликации.

Date: 2015-10-03 11:35 am (UTC)
From: [identity profile] kurilka.livejournal.com
Интересно, что эту 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

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

Date: 2015-10-03 01:35 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
А вторую конструкцию, (\True -> \y -> ()) False `seq` 5?

Date: 2015-10-03 02:29 pm (UTC)
From: [identity profile] kurilka.livejournal.com
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 на результат не влияет ни в том ни в другом случае

Date: 2015-10-03 02:30 pm (UTC)
From: [identity profile] kurilka.livejournal.com
а, хотя -O0 же по дефолту, так что странно былоб иное

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 22nd, 2017 10:27 pm
Powered by Dreamwidth Studios