Perché il seq è cattivo?

Question

Haskell ha una funzione magica denominata seq, che accetta un argomento di qualsiasi tipo e lo riduce a Forma normale testa debole (WHNF).

Ho letto un paio di fonti [non che io ricordo chi fossero ora ...], che affermano che "polimorfica seq è male". In che modo sono "cattivi"?

Analogamente, esiste la funzione rnf, che riduce un argomento a Modulo normale (NF). Ma questo è un metodo di classe; non funziona per tipi arbitrari. Mi sembra "ovvio" che si possa modificare la specifica del linguaggio per fornire questo come una primitiva incorporata, simile a seq. Questo, presumibilmente, sarebbe "ancora più cattivo" rispetto al fatto di avere solo seq. In che modo è così?

Infine, qualcuno ha suggerito che dare seq, rnf, par e simili lo stesso tipo della funzione id, anziché la funzione const come è ora, sarebbe un miglioramento. Come mai?

Answer 1

Per quanto ne so una funzione polimorfica seq è un male perché indebolisce teoremi liberi o, in altre parole, alcune uguaglianze che sono validi senza seq non sono più validi con seq. Ad esempio, l'uguaglianza

map g (f xs) = f (map g xs) 

vale per tutte le funzioni g :: tau -> tau', tutti gli elenchi xs :: [tau] e tutte le funzioni polimorfiche f :: [a] -> [a]. Fondamentalmente, questa uguaglianza afferma che f può solo riordinare gli elementi della sua lista di argomenti o eliminare o duplicare elementi ma non può inventare nuovi elementi.

A dire il vero, può inventare elementi in quanto potrebbe "inserire" un errore di calcolo/run-time non terminante negli elenchi, in quanto il tipo di errore è polimorfico. Cioè, questa uguaglianza si rompe già in un linguaggio di programmazione come Haskell senza seq. Le seguenti definizioni di funzioni forniscono un contro esempio all'equazione. Fondamentalmente, sul lato sinistro g "nasconde" l'errore.

g _ = True 
f _ = [undefined] 

Al fine di risolvere l'equazione, g deve essere rigorosa, cioè, deve mappare un errore di un errore. In questo caso, l'uguaglianza regge di nuovo.

Se si aggiunge un operatore polimorfico seq, l'equazione si interrompe nuovamente, ad esempio, la seguente istanziazione è un esempio di contatore.

g True = True 
f (x:y:_) = [seq x y] 

Se consideriamo la lista xs = [False, True], abbiamo

map g (f [False, True]) = map g [True] = [True] 

ma, d'altra parte

f (map g [False, True]) = f [undefined, True] = [undefined] 

Cioè, è possibile utilizzare seq per rendere l'elemento di una certa la posizione dell'elenco dipende dalla definizione di un altro elemento nell'elenco. L'uguaglianza rimane valida se g è totale.Se sei interessato a teoremi gratuiti, consulta lo free theorem generator, che ti consente di specificare se stai considerando una lingua con errori o persino una lingua con seq. Sebbene ciò possa sembrare di minore rilevanza pratica, seq interrompe alcune trasformazioni utilizzate per migliorare l'efficienza dei programmi funzionali, ad esempio foldr/build in mancanza di fusione in presenza di seq. Se sei interessato a maggiori dettagli sui teoremi gratuiti in presenza di seq, dai un'occhiata a Free Theorems in the Presence of seq.

Per quanto ne so era noto che un polimorfo seq interrompe certe trasformazioni, quando è stato aggiunto alla lingua. Tuttavia, gli althernatives hanno anche degli svantaggi. Se si aggiunge una classe di tipo seq, potrebbe essere necessario aggiungere molti vincoli di classe tipo al programma, se si aggiunge uno seq da qualche parte in profondità. Inoltre, non era stata una scelta di omettere lo seq poiché era già noto che ci sono perdite di spazio che possono essere corrette usando seq.

Infine, potrei perdere qualcosa, ma non vedo come funzionerebbe un operatore seq di tipo a -> a. L'indizio di seq è che valuta un'espressione a capo della forma normale, se un'altra espressione viene valutata come una forma normale. Se seq ha il tipo a -> a non c'è modo di fare in modo che la valutazione di una espressione dipenda dalla valutazione di un'altra espressione.

Answer 2

Un altro controesempio viene fornito in this answer - le monade non riescono a soddisfare le leggi monad con seq e undefined. E dal momento che il undefined non può essere evitato in una lingua completa di Turing, quello da incolpare è seq.