Ci sono alternative ai tipi per l'analisi statica?

I sistemi di tipo statico sono una sorta di analisi statica, ma ci sono molte analisi statiche che non sono generalmente codificate nei sistemi di tipi. Ad esempio:

• La verifica del modello è una tecnica di analisi e verifica per i sistemi concorrenti che ti consente di dimostrare che il tuo programma è ben educato in tutti i possibili intrecci di thread.

• Analisi del flusso di dati raccoglie informazioni sui possibili valori delle variabili, che possono determinare se alcuni calcoli sono ridondanti o se alcuni errori non vengono considerati.

• L'interpretazione astratta modella in modo conservativo gli effetti di un programma, solitamente in modo tale che l'analisi sia garantita per i controllori del tipo di terminazione che possono essere implementati in modo simile agli interpreti astratti.

• Logica di separazione è una logica di programma (utilizzata ad esempio nell'analizzatore Infer ) che può essere usato per ragionare sugli stati del programma e identificare problemi come dereferenze del puntatore nullo, stati non validi e perdite di risorse.

• La programmazione basata su contratto è un mezzo per specificare le condizioni preliminari, le postcondizioni, gli effetti collaterali e gli invarianti. Ada ha il supporto nativo per i contratti e può verificare alcuni di essi staticamente.

L'ottimizzazione dei compilatori esegue molte piccole analisi per creare strutture di dati intermedie da utilizzare durante l'ottimizzazione, come SSA, stime dei costi di inlining, informazioni sull'associazione delle istruzioni e così via.

Un altro esempio di analisi statica non dichiarativa si trova nel typececker Hack , in cui i normali costrutti del flusso di controllo possono perfezionare il tipo di una variabile :

$x = get_value();
if ($x !== null) {
    $x->method();    // Typechecks because $x is known to be non-null.
} else {
    $x->method();    // Does not typecheck.
}

E parlando di "raffinazione", di nuovo nella terra dei sistemi di tipi, tipi di perfezionamento ( come usato nei LiquidHaskell ) tipi di coppia con predicati che sono garantiti per le istanze del Tipo "raffinato". E i tipi dipendenti vanno ulteriormente oltre, consentendo ai tipi di dipendere dai valori. Il "ciao mondo" della tipizzazione dipendente è solitamente la funzione di concatenazione degli array:

(++) : (a : Type) -> (m n : Nat) -> Vec a m -> Vec a n -> Vec a (m + n)

Qui, ++ prende due operandi di tipo Vec a m e Vec a n , essendo vettori con tipo di elemento a e lunghezze m e n rispettivamente, che sono numeri naturali ( Nat ). Restituisce un vettore con lo stesso tipo di elemento la cui lunghezza è m + n . E questa funzione dimostra questo vincolo in modo astratto, senza conoscere i valori specifici di m e n , quindi le lunghezze dei vettori potrebbero essere dinamiche.

@ La risposta di JonPurdy è migliore, ma mi piacerebbe aggiungere qualche altro esempio:

Ovvio:

• controllo della sintassi

• linting

Non ovvia:

• Rust consente al programmatore di specificare se i "binding" sono modificabili , e applica questi vincoli.

• Questa è una sorta di correlazione: alcune lingue consentono di eseguire codice in fase di compilazione, il che significa che molte cose che altrimenti sarebbero errori di runtime possono essere catturate in fase di compilazione. Alcuni esempi sono le macro e le procedure di linguaggio Nim contrassegnate con compileTime pragma .

• Logica la programmazione sta fondamentalmente costruendo un programma fornendo delle asserzioni.

Tipizzazione semi-statica:

• Il flusso di Facebook consente un ibrido tra digitazione dinamica e statica. L'idea è che anche il codice dinamico sia digitato implicitamente. Flow ti consente di eseguire un server che controlla il codice mentre viene eseguito per rilevare possibili errori di tipo, anche se non annoti le tue funzioni.

L'analisi del tipo non significa molto.

Agda è noto per avere un sistema di tipo completo di Turing, molto diverso (e molto più difficile per calcolare) rispetto ai linguaggi ML (ad es. Ocaml ).