In che modo un linguaggio di programmazione tipizzato in modo affidabile fa fronte alla mutabilità?

Risposta pubblicata da gelisam sul dependent_types subreddit

Ci sono due aspetti nella tua domanda.

1. Il tipo di una variabile cambia man mano che viene mutato
2. Tipo ambiguo dopo un blocco condizionale

Un'assegnazione che cambia il tipo della variabile assegnata è chiamata "aggiornamento strong". Se vuoi davvero che la tua lingua li supporti, tieni presente che rintracciare tali cambiamenti di tipo renderà il tuo tipo di sistema molto più complicato, perché i tuoi giudizi di tipo dovranno tenere traccia delle regioni di codice all'interno delle quali le tue ipotesi e conclusioni sono valide. p>

Uno di questi tipi di sistema è descritto nel documento di Stefan Monnier Stato di tracciamento statico con regioni tipizzate . È passato un po 'di tempo da quando ho imparato a conoscere questo, ma il documento sembra descrivere un linguaggio che ha delle affermazioni per un strong aggiornamento, eppure supporta tipi di dipendenza molto potenti, vale a dire il calcolo delle costruzioni induttive.

Dato il tipo di linguaggio che stai tentando di implementare, tuttavia, probabilmente non puoi permettertelo di aumentare il tuo budget di complessità. Quindi, ecco una soluzione molto più semplice: usa assegnazioni ordinarie invece di aggiornamenti forti!

Penso di capire perché pensi di aver bisogno di aggiornamenti forti, ma probabilmente no. Considera il seguente frammento di codice Java:

Parent p = new Child1();
p = new Child2();
if (condition) {
  p = new Child3();
}

Il tipo di runtime di p cambia ad ogni assegnazione, ma poiché Java non ha aggiornamenti importanti, il tipo in fase di compilazione di p rimane Parent. Esiste un compromesso nella scelta di p : un tipo come Child1 sarebbe stato più preciso e avrebbe permesso di chiamare più metodi su p , ma consentirebbe solo a futuri incarichi di sostituire p con un altro valore di tipo Child1 o una sua sottoclasse. Il tipo Parent consente assegnazioni più flessibili, ma limita i metodi disponibili a quelli di Parent .

Allo stesso modo, quando scegli un tipo per una variabile mutabile xs nel tuo linguaggio tipizzato, gli utenti potrebbero dover scegliere tra un tipo preciso come ist<int,3> e un tipo impreciso come Σ n:Nat. List<int, n> , cioè, una coppia dipendente che indica che la parte int di List<int,n> è fissa ma la parte n può essere modificata da mutazioni.

Con il primo tipo, sarebbero disponibili alcuni metodi, come quelli che richiedono che l'elenco sia non vuoto, ad esempio, mentre altri metodi non sarebbero disponibili, cioè quelli che modificano la lunghezza della lista. Con quest'ultimo tipo, si possono chiamare solo i metodi che funzionano indipendentemente dal n corrente, ma questa volta sarebbe legale cambiare la lunghezza della lista. In particolare, sarebbe legale cambiare la lunghezza della lista all'interno di un blocco condizionale, perché il codice dopo il blocco non è già in grado di chiamare metodi che si aspettano una determinata lunghezza.

Quello che sto cercando di dire è che l'aggiunta di mutabilità a una lingua con tipi dipendenti non porta necessariamente ad aggiungere anche forti aggiornamenti e che una lingua con le prime due funzionalità ma non la terza sarebbe più semplice e familiare di una lingua con aggiornamenti forti.

Come delnan ha detto nei commenti , questo ha poco a che fare con la mutabilità. Vediamo come si potrebbe digitare il loro esempio.

let xs = [3,2,1] in (if random_bool then 4:xs else xs)

In un linguaggio tipizzato, if-then-else è un caso speciale di elimBool , l'eliminatore per le espressioni con valore booleano il cui tipo è:

elimBool :: (P : Bool -> Type) (t : P true) (f : P false) (b : Bool) -> P b

Infatti: se prendiamo P una costante, recuperiamo il principio di battitura per if-then-else permutazione del modulo degli argomenti.

Ora, in questo caso non abbiamo un'espressione di if-then-else dato che i due rami non hanno lo stesso tipo. Abbiamo uno elimBool in piena regola. E può essere digitato nel seguente modo:

Inizia definendo il predicato appropriato Pred che descrive il tipo di espressione:

Pred :: Bool -> Type
Pred b = elimBool (\ _ -> Type) List<int, 4> List<int, 3> b

o, in modo equivalente dato che il predicato di Pred è costante, possiamo usare un'espressione if-then-else :

Pred :: Bool -> Type
Pred b = if b then List<int, 4> else List<int, 3> b

In altre parole, il predicato ispeziona il suo argomento e dice che si aspetta un elenco di lunghezza 4 o di lunghezza 3 a seconda che l'argomento sia vero o falso.

L'espressione stessa può quindi essere scritta:

Exp :: Pred random_bool
Exp = elimBool Pred (4 : xs) xs random_bool

Infatti, secondo il tipo di elimBool il primo ramo 4 : xs deve avere tipo Pred true che è precisamente List<int, 4> mentre il secondo ha tipo Pred false che è uguale a List<int, 3> .