Dove e perché dovrei usare schemi extra vuoti?

Question

Per esempio:

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

Ci sono modelli aggiuntivi per [] e sembra come essi sono utilizzati in Haskell Data.List ma che tipo di ottimizzazione è quello? E dove sta la differenza con Idris qui?

Chiedo perché ho sentito che "renderà il ragionamento più difficile" e la persona che mi ha detto che non ha avuto il tempo di spiegarlo pienamente.

Dubito che riesca a capirlo facendo "ridurre la prova" della funzione.

maggio qualcuno mi spieghi la politica di schemi extra qui da posizioni di Haskell e Idris così sarò in grado di capire e vedere la differenza.

Answer 1

parlare semanticamente, il modello

intersectBy _ [] _  = [] 

sembra ridondante, anche da un punto di vista delle prestazioni. Invece, in Haskell

intersectBy _ _ [] = [] 

non è ridondante poiché altrimenti

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

sarebbe divergere, in quanto la comprensione avrebbe cercato di provare tutti gli elementi x <- [0..].

Non sono sicuro che mi piaccia questo caso speciale, però. Perché non dovremmo aggiungere un caso speciale che copre intersectBy (==) [0..] [2] in modo che restituisca [2]? Inoltre, se la prestazione è la preoccupazione, in molti casi mi piacerebbe utilizzare un approccio O (n log n) attraverso il pre-ordinamento, anche se questo non funziona su liste infinite e richiede Ord a.

Answer 2

@chi spiega il caso _ _ [], ma lo _ [] _ ha anche uno scopo: stabilisce come intersectByhandles bottom. Con la definizione come scritto:

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

Rimuovere il primo modello e diventa:

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

---

Io non sono sicuro al 100% di questo, ma credo che ci sia anche un miglioramento delle prestazioni non vincolante nulla nel primo schema. Il modello finale restituirà lo stesso risultato per xs == [] senza con valutazione eq o ys, ma AFAIK è ancora allocates stack space per i loro thunk.

Answer 3

Non è necessario indovinare quando è possibile cercare la cronologia tramite git blame, GHC Trac e la mailing list delle librerie.

Originariamente la definizione era solo la terza equazione,

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

Nella https://github.com/ghc/ghc/commit/8e8128252ee5d91a73526479f01ace8ba2537667 seconda equazione è stata aggiunta come un miglioramento severità/prestazioni, e allo stesso tempo, la prima equazione è stato aggiunto in modo da rendere la nuova definizione sempre almeno definita come l'originale. Altrimenti, intersectBy f [] _|_ sarebbe _|_ quando era [] prima.

Mi sembra che questa definizione attuale sia al momento estremamente pigra: è il più possibile definita per qualsiasi input, tranne che bisogna scegliere se controllare prima la lista di sinistra o di destra per il vuoto. (E, come ho detto sopra, questa scelta è fatta per essere coerente con la definizione storica.)

Answer 4

Lì è una grande differenza in Idris: le liste di Idris sono sempre finite! Inoltre, Idris è un linguaggio perlopiù rigoroso (call-by-value) e utilizza facoltativamente un correttore di totalità, quindi è abbastanza ragionevole presumere che non ci sarà alcun fondo nascosto negli elenchi degli argomenti. Il significato di questa differenza è che le due definizioni sono molto più semanticamente identiche in Idris che in Haskell. La scelta di quale usare può essere fatta sulla base della facilità di dimostrare le proprietà della funzione, o può essere basata sulla semplicità.