Warum ist seq schlecht?

Question

Haskell hat eine magische Funktion namens seq, die ein Argument von jedem Typ nimmt und reduziert es auf Schwachkopf Normalform (WHNF).

ich ein paar Quellen gelesen habe [nicht, dass ich mich erinnern kann, wer sie jetzt waren ...], die behaupten, dass „polymorphe seq schlecht ist“. Auf welche Weise sind sie "schlecht"?

Ebenso gibt es die rnf Funktion, die ein Argument auf Normalform (NF) reduziert. Aber dieser ist eine Klassenmethode; Es funktioniert nicht für beliebige Typen. Es scheint mir "offensichtlich" zu sein, dass man die Sprachspezifikation ändern könnte, um dies als ein eingebautes Primitiv zu liefern, ähnlich wie seq. Dies wäre vermutlich "noch schlimmer" als nur seq zu haben. In welcher Weise ist das so? Schließlich

, schlug jemand, dass seq geben, rnf, par und den gleichen Typ wie die id Funktion similars, anstatt die const Funktion, wie es jetzt ist, wäre eine Verbesserung. Wie das?

Answer 1

Soweit ich weiß, eine polymorphe seq Funktion schlecht ist, weil es frei Sätze oder, mit anderen Worten schwächt, einige Gleichheiten, die ohne seq gültig sind nicht mehr gültig ist mit seq. Zum Beispiel der Gleichheit

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

gilt für alle Funktionen g :: tau -> tau', alle Listen xs :: [tau] und alle polymorphen Funktionen f :: [a] -> [a]. Grundsätzlich besagt diese Gleichheit, dass f nur die Elemente seiner Argumentliste neu anordnen oder Elemente löschen oder duplizieren kann, aber keine neuen Elemente erfinden kann.

Um ehrlich zu sein, kann es Elemente erfinden, da es einen nicht terminierenden Berechnungs-/Laufzeitfehler in die Listen "einfügen" könnte, da der Typ eines Fehlers polymorph ist. Das heißt, diese Gleichheit bricht bereits in einer Programmiersprache wie Haskell ohne seq. Die folgenden Funktionsdefinitionen bieten ein Gegenbeispiel für die Gleichung. Grundsätzlich "verbirgt" auf der linken Seite der Fehler g.

g _ = True 
f _ = [undefined] 

Um die Gleichung zu beheben, hat g streng sein, das heißt, es hat einen Fehler zu einem Fehler kartieren. In diesem Fall gilt die Gleichheit wieder.

Wenn Sie einen polymorphen seq-Operator hinzufügen, wird die Gleichung erneut unterbrochen. Die folgende Instanziierung ist beispielsweise ein Gegenbeispiel.

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

Wenn wir die Liste xs = [False, True] betrachten, haben wir

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

aber auf der anderen Seite

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

Das heißt, Sie seq verwenden können, um das Element eines bestimmten zu machen Die Position der Liste hängt von der Definition eines anderen Elements in der Liste ab. Die Gleichheit gilt wieder, wenn g insgesamt ist.Wenn Sie an freien Theoremen interessiert sind, lesen Sie die free theorem generator, mit der Sie angeben können, ob Sie eine Sprache mit Fehlern oder sogar eine Sprache mit seq betrachten. Obwohl dies von geringerer praktischer Relevanz zu sein scheint, bricht seq einige Transformationen, die verwendet werden, um die Ausführung von Funktionsprogrammen zu verbessern, zum Beispiel foldr/build Fusion scheitert in Gegenwart von seq. Wenn Sie sich näher mit den freien Theoremen in Gegenwart von seq beschäftigen, werfen Sie einen Blick in Free Theorems in the Presence of seq.

Soweit ich weiß, war bekannt, dass eine polymorphe seq bestimmte Transformationen bricht, wenn es der Sprache hinzugefügt wurde. Die Altherkömmlinge haben jedoch auch Nachteile. Wenn Sie eine Typklasse basierend auf seq hinzufügen, müssen Sie Ihrem Programm möglicherweise eine Menge Klassenbeschränkungen hinzufügen, wenn Sie irgendwo tief unten eine seq hinzufügen. Darüber hinaus war es keine Wahl, seq wegzulassen, da bereits bekannt war, dass es Platzlecks gibt, die unter Verwendung von seq behoben werden können.

Schließlich könnte ich etwas verpassen, aber ich sehe nicht, wie ein seq Operator des Typs a -> a würde funktionieren. Der Schlüssel von seq ist, dass es einen Ausdruck evaluiert, um normale Form zu führen, wenn ein anderer Ausdruck ausgewertet wird, um normale Form zu führen. Wenn seq den Typ a -> a hat, gibt es keine Möglichkeit, die Auswertung eines Ausdrucks von der Auswertung eines anderen Ausdrucks abhängig zu machen.

Answer 2

Ein weiteres Gegenbeispiel ist in this answer gegeben - Monaden nicht Monade Gesetze mit seq und undefined zu befriedigen. Und da undefined in einer Turing-vollständigen Sprache nicht vermieden werden kann, ist derjenige schuld, seq.