Questo modello sembra esaustivo, ma sto ancora ricevendo avvisi

Question

sto imparando SML, e scrisse la seguente semplice funzione:

(* Return a list with every other element of the input list *) 
fun everyOther [] = [] 
    | everyOther [x] = [x] 
    | everyOther x = let 
     val head::head2::tail = x 
    in 
     head::everyOther(tail) 
    end; 

che sta generando il seguente avviso:

! Toplevel input: 
! val head::head2::tail = x 
!  ^^^^^^^^^^^^^^^^^ 
! Warning: pattern matching is not exhaustive 

I crediamo che la funzione non possa mai fallire, dal momento che val head::head2::tail funzionerà sempre per liste con due o più elementi e il caso di un elemento e zero elementi è coperto. Per quanto posso dire, questa funzione funziona come previsto. Penso che il problema potrebbe essere legato all'uso di [] ma davvero non lo so.

La mia domanda è in realtà tre volte:

1. Perché SML pensare che questo non è esaustivo (come sto interpretando male questo)?
2. C'è un caso in cui questa funzione avrà esito negativo?
3. Sto facendo qualcosa di stupido scrivendo la funzione in questo modo?

Answer 1

1. SML ti dà questo avvertimento perché non sa che x ha almeno due elementi. Tutto ciò che sa è che x è una lista, non ricorda il fatto che x non doveva corrispondere ai primi due modelli, per entrare nel terzo caso.

2. No, il codice non può fallire.

3. Non vi è alcun motivo per eseguire la corrispondenza del modello nella let-statement. Si può semplicemente mettere il modello al fun dichiarazione, che si tradurrà in meno codice e rimuovere l'avviso:

   fun everyOther [] = [] 
       | everyOther [x] = [x] 
       | everyOther (head::head2::tail) = head :: everyOther tail;