Program Haskell przerywa z "pętlą", ale myślę, że nie powinien

Question

Mam ten kod Haskella, który po skompilowaniu z GHC i uruchomi, przerwie z wykrytą pętlą.

data Foo = Foo() 
deriving (Eq,Show) 

type Foop = Foo -> ((),Foo) 

noOp :: Foop 
noOp st = ((),st) 

someOp :: Foop 
someOp st@(Foo x) = ((),st) 

(<+>) :: Foop -> Foop -> Foop 
(<+>) f g st = let ((_,st'),(_,st'')) = ((f st),(g st')) in ((),st'') 

main = print $ (noOp <+> someOp) $ Foo() 

Myślę, że nie powinno, a tutaj są pewne modyfikacje. Każdy z nich sprawia, że ​​pętla odejść:

• zmiana data Foo do newtype Foo
• zmiana (noOp <+> someOp) do (someOp <+> noOp)
• usunąć dekonstrukcja @(Foo x)

Jest to błąd w GHC czy jest to mój brak zrozumienia procesu oceny?

Answer 1

To nie jest błąd - właśnie znalazłeś podstępny kąt leniwego semantyki wzoru. Pozwól mi przedstawić prostszy przypadek:

> data Id a = Id a 
> let Id a = undefined ; Id b = Id 3 in b 
3 
> let (Id a, Id b) = (undefined, Id 3) in b 
*** Exception: Prelude.undefined 

Różnica polega na tym, że pierwszy let jest równoważna

case undefined of 
    ~(Id a) -> case Id 3 of 
       ~(Id b) -> b 

natomiast druga jest

case (undefined, Id 3) of 
    ~(Id a, Id b) -> b 

Pierwszy nie oceni undefined chyba a jest wymagany (co nie ma miejsca).

Drugi mecz wzór przeciwko obu wzorów Id a i Id b jak najszybciej albo zmienna jest wymagane, zmuszając zarówno undefined i Id 3 w procesie.

zauważyć, że z powodu tego problemu, wzory ~(K1 (K2 x) (K3 y)), ~(K1 ~(K2 x) (K3 y)), ~(K1 (K2 x) ~(K3 y)) i ~(K1 ~(K2 x) ~(K3 y)) mają różne semantykę.

Aby rozwiązać swój kod, spróbuj

let (~(_,st'),~(_,st'')) = ((f st),(g st')) in ((),st'') 

lub

let (_,st') = f st ; (_,st'') = g st' in ((),st'') 

Answer 2

• Wzór mecz (_, _) wymagania WHNF z (f st, g st'). Łatwo.
• Wzór dopasowania (_, (_,_)) wymaga WHNF z g st'. Tutaj jest problem, ponieważ g jest ścisły, dlatego też najpierw potrzebuje st' w WHNF. Środowisko wykonawcze znajduje st' we wzorze ((_,st'), (_,_)), więc zanim faktycznie może przejść do st', potrzebuje WHNF obu krotek. Ponieważ jednak g jest ścisły, wymaga to najpierw st' ... i tak dalej.

Jeśli dopasować wynik g z leniwym niepodważalny wzór

(<+>) f g st = let ((_,st'), ~(_,st'')) = (f st, g st') in ((),st'') 

wtedy problem zniknie, bo to jest oceniane w następujący sposób:

• Wzór meczu (_, _) wymaganiom WHNF z (f st, g st') . Łatwo.
• Wzór zapałki (_, ~(_,_)) nie wymaga już nic więcej.
• Wzór dopasowania ((_,st'), ~(_,_)) Żądanie WHNF z f st. Na szczęście możemy to spełnić, ponieważ st nie zależy od wzoru.
• Teraz, gdy dopasowaliśmy wzorzec, środowisko wykonawcze może już działać z in ((),st''). Tylko w tym momencie wymuszony jest wymuszony wzorzec, ale teraz to już nie jest problem, ponieważ st' jest dostępny tutaj, więc jest to tylko kwestia jednokrotnego obliczenia g.

Poprawki wypróbowałeś wszystkie kwoty do podejmowania g niż surowe:

usunąć dekonstrukcji @(Foo _)

Bez tego g naprawdę nie trzeba spojrzeć na jej Argument dotyczący zbudowania szkieletu wyniku, tj. meczu krotki (_,st''), może następnie odnieść sukces bez wcześniejszego wymagania WHNF wynoszącego st'.

zmiana data Foo do newtype Foo

Ma to ten skutek, że konstruktor Foo faktycznie nie istnieje w czasie wykonywania, więc nie ma nic, co zmusiłoby wzór st@(Foo _).

zmiana noOp <+> someOp do someOp <+> noOp

Jak powiedziałem, pętla chodzi tylko o ponieważ g jest surowe. Jeśli umieścisz f w swojej pozycji, co nie jest ścisłe, nie ma problemu.