Wo und warum sollte ich extra leere Muster verwenden?

Question

Zum Beispiel:

intersectBy : (a -> a -> Bool) -> List a -> List a -> List a 
intersectBy _ [] _  = [] 
intersectBy _ _ [] = [] 
intersectBy eq xs ys = [x | x <- xs, any (eq x) ys] 

Es gibt zusätzliche Muster für [] und scheinen, wie sie in Haskell verwendet werden Data.List aber welche Art von Optimierung ist das? Und wo ist der Unterschied zu Idris?

Ich frage, weil ich hörte, dass "es die Argumentation darüber schwieriger machen wird" und Person, die mich sagte, die keine Zeit hatte, es vollständig zu erklären.

Ich bezweifle, wenn ich es verstehe, "den Beweis" der Funktion zu reduzieren.

Kann mir jemand die Politik der zusätzlichen Muster hier von Positionen von Haskell und Idris erklären, damit ich in der Lage sein werde, den Unterschied zu verstehen und zu sehen.

Answer 1

semantisch zu sprechen, das Muster

intersectBy _ [] _  = [] 

sieht überflüssig, sogar von einer Performance-Sicht. Stattdessen in Haskell

intersectBy _ _ [] = [] 

ist nicht überflüssig, da sonst

intersectBy (==) [0..] [] 

würde auseinanderlaufen, da das Verständnis x <- [0..] alle Elemente, um zu versuchen versuchen würde.

Ich bin mir nicht sicher, dass ich diesen speziellen Fall mag, obwohl. Warum sollten wir keinen Sonderfall hinzufügen, der intersectBy (==) [0..] [2] abdeckt, so dass [2] zurückgegeben wird? Wenn es um Leistung geht, möchte ich in vielen Fällen einen O (n log n) -Ansatz durch Vorsortierung verwenden, auch wenn dies nicht für unendliche Listen funktioniert und Ord a erfordert.

Answer 2

@chi erklärt die _ _ [] Fall, aber _ [] _ dient einem Zweck auch: es gibt vor, wie intersectByhandles bottom. Mit der Definition wie folgt geschrieben:

λ. intersectBy undefined []  undefined 
[] 
λ. intersectBy (==) undefined [] 
*** Exception: Prelude.undefined 

Entfernen Sie das erste Muster und es wird:

λ. intersectBy undefined undefined [] 
[] 
λ. intersectBy (==)  []  undefined 
*** Exception: Prelude.undefined 

---

Ich bin nicht 100% sicher, aber ich glaube, es ist auch ein Performance-Vorteil zu nicht Bindung alles im ersten Muster. Das endgültige Muster ergibt das gleiche Ergebnis für xs == [] ohne Auswertung eq oder ys, aber AFAIK es immer noch allocates stack space für ihre Thunks.

Answer 3

Es ist nicht notwendig zu erraten, wann Sie die Geschichte durch git blame, GHC Trac und die Bibliotheken Mailingliste nachschlagen können.

Ursprünglich war die Definition nur die dritte Gleichung,

intersectBy eq xs ys = [x | x <- xs, any (eq x) ys] 

In https://github.com/ghc/ghc/commit/8e8128252ee5d91a73526479f01ace8ba2537667 die zweite Gleichung als Strikt/Performance-Verbesserung, und zugleich die erste Gleichung hinzugefügt wurde zugegeben, um das zu machen, neue Definition immer mindestens so definiert wie das Original. Ansonsten wäre intersectBy f [] _|__|_ wenn es vorher [] war.

Es scheint mir, dass diese aktuelle Definition jetzt maximal faul ist: Es ist so definiert wie möglich für alle Eingaben, außer dass man wählen muss, ob man zuerst die linke oder die rechte Liste auf Leerheit prüft. (Und, wie ich oben erwähnte, wird diese Wahl getroffen, um mit der historischen Definition übereinzustimmen.)

Answer 4

Dort ist ein großer Unterschied in Idris: Idris-Listen sind immer begrenzt! Darüber hinaus ist Idris eine meist strikte (call-by-value) Sprache und verwendet optional einen Totalitätsprüfer, so dass es ziemlich vernünftig anzunehmen ist, dass in den Argumentenlisten keine Bottoms versteckt sein werden. Die Bedeutung dieses Unterschieds besteht darin, dass die beiden Definitionen bei Idris wesentlich semantisch identischer sind als bei Haskell. Die Auswahl, die zu verwenden ist, kann basierend auf der Leichtigkeit des Nachweises von Eigenschaften der Funktion getroffen werden oder kann auf Einfachheit basieren.