Il programma Haskell si interrompe con "loop" ma penso che non dovrebbe essere

Question

Ho questo codice Haskell che, una volta compilato con GHC ed eseguito, si interrompe con un loop rilevato.

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() 

Penso che non dovrebbe, e qui ci sono alcune modifiche. Ognuno di loro fa il loop va via:

• cambiamento data Foo-newtype Foo
• cambiamento (noOp <+> someOp) a (someOp <+> noOp)
• rimuovere la decostruzione @(Foo x)

Si tratta di un bug in GHC o è la mia mancanza di comprendere il processo di valutazione?

Answer 1

Non è un bug - hai appena trovato un difficile angolo della semantica del modello pigro. Mi permetta di presentare un caso più semplice:

> 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 

La differenza è che il primo let è equivalente a

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

mentre il secondo è

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

Il primo non sarà valutare l'undefined a meno a è richiesto (cosa che non succede).

Il secondo pattern match volontà contro entrambi i modelli Id a e Id b appena sia variabile è richiesto, costringendo sia undefined e Id 3 nel processo.

Si noti che, a causa di questo problema, i modelli ~(K1 (K2 x) (K3 y)), ~(K1 ~(K2 x) (K3 y)), ~(K1 (K2 x) ~(K3 y)) e ~(K1 ~(K2 x) ~(K3 y)) hanno diversi semantica.

per risolvere il tuo codice, provare

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

o

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

Answer 2

• corrispondenza di schema (_, _) esigenze WHNF di (f st, g st'). Facile.
• Corrispondenza modello (_, (_,_)) richieste WHNF di g st'. Ecco il problema, perché g è rigoroso, quindi è necessario prima anche st' in WHNF. Il runtime trova st' nel modello ((_,st'), (_,_)), quindi prima che possa effettivamente attraversare verso il basso in st' ha bisogno di WHNF entrambe le tuple. Perché g è rigoroso tuttavia, questo richiede prima st' ... e così via.

Se corrispondono il risultato di g con un motivo inconfutabile pigro

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

allora il problema va via, perché questo è valutato così:

• Pattern Match (_, _) esigenze WHNF di (f st, g st') . Facile.
• La corrispondenza di modello (_, ~(_,_)) non richiede altro per il momento.
• Corrispondenza modello ((_,st'), ~(_,_)) richieste WHNF di f st. Fortunatamente, possiamo adempiere a questo, perché st non dipende dal modello.
• Ora che abbiamo soddisfatto la corrispondenza del modello, il runtime può già procedere con lo in ((),st''). Solo a questo punto è forzato il modello irrefutabile ~(_,st''), ma questo non è più un problema perché st' è disponibile qui, quindi è solo una questione di calcolare il numero g una volta.

Le correzioni che hai provato tutto ammontano a fare g non rigorosa:

rimuovere la decostruzione @(Foo _)

Senza quella, g non ha davvero bisogno di guardare al suo argomento per costruire lo scheletro del risultato, ovvero la corrispondenza della tupla (_,st'') può quindi riuscire senza prima richiedere WHNF di st'.

cambiamento data Foo al newtype Foo

Questo ha l'effetto che il costruttore Foo non esiste effettivamente in fase di esecuzione, quindi non c'è nulla che lo schema st@(Foo _) costringerebbe.

cambiamento noOp <+> someOp a someOp <+> noOp

Come ho detto, il ciclo viene solo perché g è rigorosa. Se metti f nella sua posizione, che non è severa, allora non ci sono problemi.