Perché init è una funzione parziale?

Question

secondo la Haskell 2010 report, init è definito come il seguente:

init    :: [a] -> [a] 
init [x]   = [] 
init (x:xs)  = x : init xs 
init []   = error "Prelude.init: empty list" 

base-4.4.1.0 la definisce in modo simile. A me, sembra che sarebbe perfettamente accettabile e intuitivo da avere:

init [] = [] 

wich farebbe init una funzione totale. Dal momento che questa definizione è entrata nel rapporto di haskell 2010, suppongo che ci siano degli argomenti a riguardo. È così o è definito in questo modo a causa della tradizione e della retrocompatibilità?

Answer 1

Lo stesso motivo tail [] non è []; rompe gli invarianti che definiscono queste funzioni. Possiamo definire head e tail dicendo che se head e tail sono definiti per un valore xs, quindi xs ≡ head xs : tail xs.

Come ha sottolineato Niklas, l'invariante che vogliamo definire init e last è xs ≡ init xs ++ [last xs]. È vero che last non è definito anche negli elenchi vuoti, ma perché è necessario definire last se non è possibile specificare init? Proprio come sarebbe sbagliato se uno di head o tail fosse definito su un input mentre l'altro non lo era, init e last sono due lati della stessa moneta, suddividendo un elenco in due valori che insieme equivalgono all'originale.

Per una visione più "pratico" (pur essendo in grado di ragionare sui programmi in termini di invarianti utili circa le operazioni che usiamo ha molto beneficio pratico!), Un algoritmo che utilizza init probabilmente non comportarsi correttamente su un lista vuota, e se init funzionasse in questo modo, avrebbe funzionato per nascondere gli errori prodotti. È meglio per init essere prudenti sui suoi input in modo che si debba prendere in considerazione i casi limite come la lista vuota quando viene usata, specialmente quando non è del tutto chiaro che il valore proposto per il ritorno in questi casi è ragionevole.

Ecco un previous Stack Overflow question su head e tail, tra cui il motivo tail [] non significa solo tornare []; le risposte dovrebbero aiutare a spiegare perché questi invarianti sono così importanti.

Answer 2

Sarebbe terribile avere init [] = [], in particolare si potrebbero rompere invarianti importanti come xs == init xs ++ [last xs] e length xs == 1 + length (init xs) e quindi nascondere gli errori.

Answer 3

Perché trovo la domanda interessante, ho deciso di scrivere i miei pensieri sul tema:

Logical

dire che definiamo init xs come "la lista, che, se si mette last xs sul suo end, è uguale a xs. Questo è equivalente a: init xs è l'elenco senza il suo ultimo elemento. Per xs == [], non esiste alcun ultimo elemento, pertanto init [] deve essere indefinito.

Si potrebbe aggiungere un caso speciale per questo, come in "se xs è la lista vuota, quindi init xs è la lista vuota, altrimenti init xs è la lista, che, se si mette last xs sulla sua fine, è pari a xs ". Nota come questo è molto più prolisso e meno pulito. Introduciamo ulteriore complessità, ma per cosa?

intuitiva

init [1,2,3,4] == [1,2,3] 
init [1,2,3] == [1,2] 
init [1,2]  == [1] 
init [1]  == [] 
init []  == ?? 

Si noti come la lunghezza delle liste sul lato destro delle equazioni diminuisce insieme alla lunghezza del lato sinistro. Per me, questa serie non può essere proseguita in modo ragionevole, perché l'elenco sul lato destro dovrebbe avere una dimensione negativa!

pratiche

Come altri hanno sottolineato, definente un trattamento per init o tail per la lista vuota come argomento caso particolare, può introdurre errori difficili da luogo a situazioni in cui funzioni possono avere alcuna ragionevole risultato per la lista vuota, ma ancora non produce un'eccezione!

Inoltre, non riesco a pensare ad alcun algoritmo in cui sarebbe effettivamente vantaggioso avere init [] valutare su [], quindi perché introdurre questa complessità aggiuntiva? La programmazione riguarda la semplicità e soprattutto Haskell è tutto basato sulla purezza, non sei d'accordo?

Answer 4

Il vero problema qui è che init, come definito, non può funzionare; è una funzione intrinsecamente parziale, proprio come head e tail. Non sono entusiasta di quante funzioni volutamente parziali esistono nelle librerie standard, ma questa è un'altra questione.

Dal init come dato non può essere recuperato, abbiamo due opzioni:

• prendere l'interpretazione che si tratta di un filtro sulla lista data, mantenendo tutti gli elementi che non sono l'ultimo elemento, e abbandonando le invarianti rispetto a length e last. Questo può essere scritto come reverse . drop 1 . reverse, il che suggerisce un'ovvia generalizzazione. Potremmo anche introdurre una controparte simile a take se lo si desidera.

• Riconoscere che init definisce una funzione parziale e assegnargli il tipo corretto, [a] -> Maybe [a]. L'errore può quindi essere correttamente sostituito con Nothing.

Answer 5

È tradizionale. A quel tempo, hanno fatto una scelta arbitraria, e ora le persone ci sono abituate.

Hanno fatto init simile a last, in modo che entrambi falliscono su liste vuote. (tail e head sono un'altra coppia come quella.)

Ma loro avrebbero potuto scegliere il contrario, come suggerisci. Il preludio potrebbe facilmente contenere una funzione tail' = drop 1, così come una corrispondente funzione init', che consente liste vuote.Non penso che questo sarebbe un problema - non sono convinto da tutte le chiacchiere su invarianti e teoremi liberi. Significherebbe solo che init' era un po 'dissimile dal suo compagno last; È tutto.

(last e head sono un'altra storia: La loro firma è [a] -> a, quindi devono restituire un elemento, e non possono fare uno dal nulla, invece, il tipo di init e tail è naturalmente [a] -> [a]. , che significa che possono produrre e producono liste vuote.)