OCaml - Che cos'è un tipo non valido?

Question

Recentemente mi è stato dato il codice

List.fold_left (fun acc x -> raise x ; acc) 3 

sto completamente bene con questa applicazione parziale con un valore funzionale di> nell'elenco Tipo Exn -> int, e il fatto che produce un avvertimento non è sorprendente . Sto,> però, non certo quello che la metà della segnalazione significa:

Warning 21: this statement never returns (or has an unsound type.) 

non può effettivamente trovare alcun riferimento a questo avvertimento in cui non è il risultato di una dichiarazione di non-ritorno. Anche la pagina man per ocamlc menziona solo le istruzioni di non ritorno per questo avviso e warnings.ml si riferisce semplicemente a Notreturning_statement.

Ho familiarità con il concetto di solidità in relazione ai sistemi di tipi, ma l'idea che un tipo stesso sia intrinsecamente infondato mi sembra strano.

Quindi le mie domande sono:

Che cosa è esattamente un tipo alienato? Qual è la situazione in cui si presenterebbe un tipo non corretto quando OCaml emetterebbe solo un avvertimento piuttosto che fallire completamente?

Qualcuno ha postato questa domanda, e mentre stavo scrivendo una risposta, è stato cancellato. Credo che la domanda sia molto interessante e valga la pena di essere ripubblicata. Perche non si può avere qualcuno che è disposto ad aiutarvi :-(

Answer 1

Come Attenzione 21 è riportato

In primo luogo, pensiamo di funzioni che restituisce estranei 'a: Non voglio dire funzione come let id x = x qui dal momento che ha tipo 'a -> 'a e il ritorno tipo 'a riferisce agli ingressi. Cioe funzioni come raise : exn -> 'a e exit : int -> 'a.

Queste funzioni restituiscono estranei 'a sono considerati non ritorno. Poiché il tipo 'a (più precisamente forall 'a. 'a) non ha cittadino. L'unica cosa che possono fare le funzioni è terminare il programma (uscire o sollevare un'eccezione) o cadere in un ciclo infinito: let rec loop() = loop().

Avviso 21 è indicato quando il tipo di istruzione è 'a. (In realtà c'è un'altra condizione ma solo salto per semplicità). Ad esempio,

# loop(); print_string "end of the infinite loop";; 
Warning 21: this statement never returns (or has an unsound type.) 

Questo è lo scopo principale di avvertimento 21. Allora qual è la seconda metà?

"tipo Unsound"

Attenzione 21 può essere segnalato anche se l'istruzione rendimenti qualcosa in realtà. In questo caso, come suggerisce il messaggio di avviso, la dichiarazione ha un tipo non corretto.

Perché sbagliato? Poiché l'espressione restituisce un valore di tipo forall 'a. 'a, che non ha cittadinanza. Rompe le basi della teoria dei tipi da cui dipende OCaml.

In OCaml, ci sono diversi modi per scrivere un'espressione con un tipo tale infondata:

Uso di Obj.magic. E 'il sistema viti tipo, pertanto è possibile scrivere un'espressione di tipo 'a che restituisce:

(Obj.magic 1); print_string "2" 

Uso di external. Uguale Obj.magic si può dare tipo arbitrario per tutti i valori e le funzioni esterne:

external crazy : unit -> 'a = "%identity" 
let f() = crazy() (* val f : unit -> 'a *) 
let _ = f(); print_string "3" 

Per il sistema di tipo OCaml, è impossibile distinguere le espressioni non-ritorno e le espressioni con i tipi malsane. Questo è il motivo per cui non può escludere cose non vere come errori. Tracciare le definizioni per dire una dichiarazione ha un tipo non corretto o non è generalmente impossibile e costa molto anche quando possibile.