Un tipo di fondo è un costrutto che appare principalmente nella teoria dei tipi matematici. Viene anche chiamato il tipo vuoto. È un tipo che non ha valori, ma è un sottotipo di tutti i tipi.
Se il tipo di ritorno di una funzione è il tipo in basso, significa che non ritorna. Periodo. Forse circola per sempre, o forse lancia un'eccezione.
Che senso ha avere questo strano tipo in un linguaggio di programmazione? Non è così comune, ma è presente in alcuni, come Scala e Lisp.
Prenderò un semplice esempio: C ++ vs Rust.
Ecco una funzione utilizzata per generare un'eccezione in C ++ 11:
[[noreturn]] void ThrowException(char const* message,
char const* file,
int line,
char const* function);
Ed ecco l'equivalente in Rust:
fn formatted_panic(message: &str, file: &str, line: isize, function: &str) -> !;
Su una questione puramente sintattica, il costrutto di Rust è più ragionevole. Si noti che il costrutto C ++ specifica un tipo di ritorno anche se specifica anche che non verrà restituito. È un po 'strano.
Su una nota standard, la sintassi C ++ appariva solo con C ++ 11 (era attaccata sopra), ma vari compilatori avevano fornito varie estensioni per un po ', così che gli strumenti di analisi di terze parti dovevano essere programmati per riconoscere i vari modi in cui questo attributo potrebbe essere scritto. Averlo standardizzato è ovviamente chiaramente superiore.
Ora, per quanto riguarda il vantaggio?
Il fatto che una funzione non ritorni può essere utile per:
La risposta di Karl è buona. Ecco un altro uso che non penso sia stato menzionato da nessun altro. Il tipo di
if E then A else B
dovrebbe essere un tipo che include tutti i valori nel tipo di A e tutti i valori nel tipo di B . Se il tipo di B è Nothing , il tipo dell'espressione if può essere il tipo di A . Definirò spesso una routine
def unreachable( s:String ) : Nothing = throw new AssertionError("Unreachable "+s)
per dire che il codice non dovrebbe essere raggiunto. Poiché il suo tipo è Nothing , unreachable(s) può ora essere utilizzato in qualsiasi if o (più spesso) switch senza influenzare il tipo di risultato. Ad esempio
val colour : Colour := switch state of
BLACK_TO_MOVE: BLACK
WHITE_TO_MOVE: WHITE
default: unreachable("Bad state")
Scala ha un tale tipo di Nothing.
Un altro caso d'uso per Nothing (come menzionato nella risposta di Karl) è List [Nothing] è il tipo di liste di cui ognuno dei membri ha tipo Nothing. Quindi può essere il tipo della lista vuota.
La proprietà chiave di Nothing che fa funzionare questi casi d'uso è non che non ha valori (anche se in Scala, ad esempio, non ha valori), è che è un sottotipo di ogni altro tipo.
Supponiamo che tu abbia una lingua in cui ogni tipo contiene lo stesso valore: chiamiamolo () . In tale linguaggio il tipo di unità, che ha () come unico valore, potrebbe essere un sottotipo di ogni tipo. Questo non lo rende un tipo di fondo nel senso che significava l'OP; l'OP era chiaro che un tipo di fondo non contiene valori. Tuttavia, poiché si tratta di un tipo che è un sottotipo di ogni tipo, può avere lo stesso ruolo di un tipo in fondo.
Haskell fa le cose in modo un po 'diverso. In Haskell un'espressione che non produce mai un valore può avere il tipo forall a.a . Un'istanza di questo tipo di schema si unificherà con qualsiasi altro tipo, quindi agisce effettivamente come un tipo di fondo, anche se Haskell (standard) non ha la nozione di sottotipizzazione. Ad esempio la funzione error del preludio standard ha lo schema di tipo forall a. [Char] -> a . Quindi puoi scrivere
if E then A else error ""
e il tipo dell'espressione sarà uguale al tipo di A , per qualsiasi espressione A .
L'elenco vuoto in Haskell ha lo schema dei tipi forall a. [a] . Se A è un'espressione il cui tipo è un tipo di lista, quindi
if E then A else []
è un'espressione con lo stesso tipo di A . Il tipo di [] è uguale al tipo [error ""] , che indica che l'elenco vuoto non è l'unico valore del suo tipo.
Maybe it loops forever, or maybe it throws an exception.
Sembra un tipo utile da avere in quelle situazioni, per quanto raro possa essere.
Inoltre, anche se Nothing (il nome di Scala per il tipo in basso) non può avere valori, List[Nothing] non ha quella restrizione, che lo rende utile come il tipo di una lista vuota. La maggior parte delle lingue aggira il problema creando una lista vuota di stringhe di un tipo diverso rispetto a una lista vuota di numeri interi, il che ha senso, ma rende una lista vuota più prolissa da scrivere, che è un grosso svantaggio in un linguaggio orientato alle liste.
I tipi formano un monoid in due modi, insieme creando un semiring . Questo è ciò che viene chiamato tipi di dati algebrici . Per i tipi finiti, questo semiring si riferisce direttamente al semiring dei numeri naturali (compreso lo zero), il che significa che contate quanti valori possibili ha il tipo (esclusi i "valori non terminanti").
Vacuous ) ha valori zero † . () . (Bool, Bool) ha quattro possibili valori, ovvero (False,False) , (False,True) , (True,False) e (True,True) . ((), False) e ((), True) sono gli unici valori di tipo ((), Bool) , quindi questo tipo è isomorfo a Bool stesso. A e B ha fondamentalmente tutti i valori di A , più tutti i valori di B , quindi tipo di somma . Ad esempio, Either () Bool ha tre valori, li chiamerò Left () , Right False e Right True . Either Vacuous A ha solo valori della forma Right a , perché Left ... non ha senso ( Vacuous non ha valori). La cosa interessante di questi monoidi è che, quando presenti funzioni nella tua lingua, categoria di questi tipi con le funzioni di morfismo è una categoria monoidale . Tra le altre cose, questo ti permette di definire i funtori applicativi e le monadi , che risultano essere un'astrazione eccellente per calcoli generali (possibilmente coinvolgenti effetti collaterali ecc.) in termini altrimenti puramente funzionali.
Ora, in realtà puoi andare molto lontano preoccupandoti solo di un lato del problema (la composizione monoid), quindi non hai davvero bisogno del tipo di fondo in modo esplicito. Ad esempio, anche Haskell ha fatto per molto tempo non avere un tipo di fondo standard. Ora lo è, si chiama Void .
Ma se consideri l'immagine completa, come categoria chiusa bicartesiana , il sistema di tipi è in realtà equivalente all'intero lambda calcolo, quindi fondamentalmente si ha la perfetta astrazione su tutto il possibile in un linguaggio completo di Turing. Ottimo per le lingue specifiche del dominio incorporato, ad esempio c'è un progetto sulla codifica diretta dei circuiti elettronici in questo modo .
Naturalmente, si può ben dire che questa è tutta la assurdità generale di tutti i teorici. Non devi assolutamente conoscere la teoria delle categorie per essere un buon programmatore, ma quando lo fai, ti dà modi potenti e ridicolmente generali per ragionare sul codice e per creare invarianti.
† mb21 mi ricorda di notare che questo non deve essere confuso con valori di fondo . Nei linguaggi pigri come Haskell, il tipo ogni contiene un "valore" inferiore, denotato ⊥ . Questa non è una cosa concreta che potresti mai passare esplicitamente in giro, invece è ciò che viene "restituito", ad esempio quando una funzione scorre per sempre. Anche il tipo Void di Haskell "contiene" il valore inferiore, quindi il nome. In questa luce, il tipo di fondo di Haskell ha davvero un valore e il suo tipo di unità ha due valori, ma nella discussione sulla teoria delle categorie questo è generalmente ignorato.
È utile per l'analisi statica documentare il fatto che un particolare percorso di codice non è raggiungibile. Ad esempio se scrivi quanto segue in C #:
int F(int arg) {
if (arg != 0)
return arg + 1; //some computation
else
Assert(false); //this throws but the compiler does not know that
}
void Assert(bool cond) { if (!cond) throw ...; }
Il compilatore si lamenterà che F non restituisce nulla in almeno un percorso di codice. Se Assert doveva essere contrassegnato come non-return, il compilatore non avrebbe bisogno di avvertire.
In alcune lingue, null ha il tipo di fondo, dal momento che il sottotipo di tutti i tipi definisce bene a quali linguaggi usare null (nonostante la lieve contraddizione di avere null essere sia se stesso sia una funzione che restituisce sé stesso, evitando il argomenti comuni sul perché bot dovrebbe essere disabitato).
Può anche essere usato come un catch-all nei tipi di funzione ( any -> bot ) per gestire la spedizione andata storta.
E alcune lingue ti consentono di risolvere effettivamente bot come un errore, che può essere utilizzato per fornire errori del compilatore personalizzati.
Sì, questo è un tipo abbastanza utile; mentre il suo ruolo sarebbe per lo più interno al sistema di tipi, ci sono alcune occasioni in cui il tipo di fondo appare in modo aperto.
Considera un linguaggio tipizzato staticamente in cui i condizionali sono espressioni (quindi la costruzione if-then-else funge anche da operatore ternario di C e amici, e potrebbe esserci un'affermazione di un caso multidirezionale simile). Il linguaggio di programmazione funzionale ha questo, ma succede anche in alcune lingue imperative (sin da quando ALGOL 60). Quindi tutte le espressioni derivate devono alla fine produrre il tipo di tutta l'espressione condizionale. Si potrebbe semplicemente richiedere che i loro tipi siano uguali (e penso che questo sia il caso per l'operatore ternario in C) ma questo è eccessivamente restrittivo specialmente quando il condizionale può anche essere usato come dichiarazione condizionale (non restituendo alcun valore utile). In generale si vuole che ogni espressione di ramo sia (implicitamente) convertibile in un tipo comune che sarà il tipo di espressione completa (eventualmente con restrizioni più o meno complicate per consentire di trovare efficacemente quel tipo comune dal compilatore, C ++, ma non entrerò in questi dettagli qui.
Esistono due tipi di situazioni in cui un tipo generale di conversione consente la necessaria flessibilità di tali espressioni condizionali. Uno è già menzionato, dove il tipo di risultato è il tipo di unità void ; questo è naturalmente un super-tipo di tutti gli altri tipi, e consentendo a qualsiasi tipo di essere (banalmente) convertito in esso rende possibile usare l'espressione condizionale come istruzione condizionale. L'altro riguarda casi in cui l'espressione restituisce un valore utile, ma uno o più rami non sono in grado di produrne uno. Solitamente generano un'eccezione o implicano un salto e richiedendo loro di (anche) produrre un valore del tipo dell'intera espressione (da un punto irraggiungibile) sarebbe inutile. È questo tipo di situazione che può essere gestita con grazia dando clausole, salti e chiamate che generano eccezioni, con un tale effetto, il tipo in basso, l'unico tipo che può essere (banalmente) convertito in qualsiasi altro tipo.
Suggerirei di scrivere un tipo di fondo come * per suggerire la sua convertibilità in un tipo arbitrario. Può servire ad altri scopi utili internamente, ad esempio quando si tenta di dedurre un tipo di risultato per una funzione ricorsiva che non ne dichiara alcuna, il tipo di inferenza potrebbe assegnare il tipo * a qualsiasi chiamata ricorsiva per evitare una situazione di uovo e gallina ; il tipo effettivo sarà determinato da rami non ricorsivi e quelli ricorsivi saranno convertiti nel tipo comune di quelli non ricorsivi. Se ci sono no rami non ricorsivi, il tipo rimarrà * , e indica correttamente che la funzione non ha modo di tornare dalla ricorsione. A parte questo e come risultato il tipo di funzioni di lancio di eccezioni, si può usare * come tipo di componente di sequenze di lunghezza 0, ad esempio della lista vuota; di nuovo se mai un elemento viene selezionato da un'espressione di tipo [*] (necessariamente lista vuota), quindi il tipo risultante * indicherà correttamente che questo non può mai tornare senza errori.
Leggi altre domande sui tag programming-languages type-systems