A Graded Modal Dependent Type Theory with Erasure, Formalized

1. Il Problema

Le lingue di programmazione tipate fortemente spesso necessitano di analisi statiche per determinare come le variabili vengono utilizzate (es. linearità, irrilevanza, cancellazione). Sebbene teorie come la Quantitative Type Theory (QTT) esistano, spesso mancano di formalizzazioni complete della loro meta-teoria, specialmente nel contesto dei tipi dipendenti con un universo e eliminazione grande (large elimination).

I problemi specifici affrontati includono:

• Gestione dell'Erasure (Cancellazione): Come garantire formalmente che le parti del codice marcate come "irrilevanti" per l'esecuzione (es. argomenti di funzione per la verifica) possano essere rimosse senza alterare il comportamento del programma.
• Programmi Aperti: La maggior parte delle prove di correttezza per l'eliminazione si limita a programmi chiusi. È necessario estendere queste garanzie a programmi aperti (con variabili libere), purché tali variabili siano anch'esse marcate come cancellabili e il contesto sia consistente.
• Complessità dei Tipi Dipendenti: Gestire la cancellazione in presenza di tipi dipendenti, dove i tipi stessi possono contenere termini che usano risorse, richiede un approccio più sofisticato rispetto ai sistemi a tipi semplici.
• Correttezza Formale: Evitare errori nella definizione delle regole di uso delle risorse (come dimostrato da fallimenti precedenti nella proprietà di sostituzione in lavori simili).

2. Metodologia

Gli autori hanno sviluppato una Teoria dei Tipi Modale Gradata (Graded Modal Dependent Type Theory) parametrizzata su una struttura di modalità (un semianello parzialmente ordinato).

• Struttura dei Gradi (Modalities): I gradi sono elementi di un semianello parzialmente ordinato che traccia l'uso delle variabili. Le operazioni includono somma (per l'uso congiunto), prodotto (per la scalatura) e incontro (meet, per l'uso alternativo).
• Separazione del Giudizio: Il sistema separa il giudizio di tipizzazione ($\Gamma \vdash t : A$) dal giudizio di assegnazione dei gradi ($\gamma \triangleright t$). Questo permette di tracciare l'uso delle risorse sia nei termini che nei tipi (sebbene non sia obbligatorio).
• Formalizzazione in Agda: L'intera teoria e le sue proprietà meta-teoriche sono state formalizzate in Agda. Questo garantisce la correttezza meccanica delle dimostrazioni.
• Relazione Logica (Logical Relation): Per provare la correttezza dell'estrazione (erasure), gli autori utilizzano una relazione logica di Kripke tra il linguaggio sorgente (tipato) e un linguaggio target non tipato (calcolo $\lambda$ non tipato).
  • Viene definita prima una relazione logica per i tipi ($\Gamma \models A$) basata sulla riducibilità.
  • Successivamente, una relazione logica per l'erasure ($t \rightsquigarrow v : A$) che collega i termini sorgente a quelli target.
• Gestione delle Match Cancellate: Il sistema distingue tra tipi $\Sigma$ forti (con proiezioni e $\eta$-uguaglianza) e deboli (con pattern matching). Viene studiato l'effetto di permettere o vietare il "matching su coppie cancellate" (erased matches) e le implicazioni sulla consistenza.

3. Contributi Chiave

1. Estensione della Struttura dei Gradi: Introduzione di una nuova funzione "nr" (natural recursor) per gestire l'assegnazione dei gradi nel ricorsore per i numeri naturali ($natrec$), risolvendo limitazioni delle precedenti definizioni basate su "star-semirings" che non supportavano bene la linearità.
2. Formalizzazione Completa della Meta-Teoria: Prima formalizzazione completa (in Agda) della meta-teoria di una teoria dei tipi dipendenti gradata con universo ed eliminazione grande. Questo include:
   • Proprietà di riduzione del soggetto (Subject Reduction).
   • Normalizzazione.
   • Decidibilità dell'uguaglianza definizionale.
   • Teorema di sostituzione per l'assegnazione dei gradi.
3. Prova di Correttezza dell'Erasure: Dimostrazione formale che l'estrazione di termini (rimozione di argomenti marcati con grado 0) preserva il valore dei programmi di tipo numero naturale. La prova vale sia per programmi chiusi che per programmi aperti in contesti consistenti.
4. Analisi dei "Match Cancellati": Studio approfondito delle conseguenze di permettere il pattern matching su coppie cancellate. Viene dimostrato che, sebbene possibile, ciò può violare la canonicità (un termine di tipo $N$ potrebbe non ridursi a un numerale) se non si impongono restrizioni sui contesti o si vietano certi match in posizioni non cancellate.
5. Estensioni Implementate:
   • Tipi Unitari deboli e forti.
   • Tipi $\Sigma$ gradata (per modellare record con campi cancellati).
   • Supporto per due semantiche di esecuzione nel linguaggio target: non-strict (call-by-name) e strict (call-by-value).

4. Risultati

• Correttezza dell'Estrazione: È stato provato che per una classe specifica di modalità (quelle con uno "zero ben comportato", come l'istituto di cancellazione), l'estrazione di termini è sound. Se un termine sorgente $t$ di tipo $N$ riduce a un numerale $n$, anche il termine estratto $t^\bullet$ riduce allo stesso numerale $n$.
• Gestione dei Programmi Aperti: La correttezza è stata estesa ai programmi aperti, purché tutte le variabili libere nel contesto siano marcate come cancellabili (grado 0) e il contesto sia consistente (nessuna prova di falsità disponibile).
• Decidibilità: La relazione di assegnazione dei gradi è decidibile e ammette un principio di "principialità" (esiste un contesto di uso più specifico per ogni termine ben formato).
• Impatto sulla Consistenza: È stato dimostrato che l'uso di assiomi consistenti in posizioni cancellate non compromette la correttezza dell'estrazione, mentre l'uso di assiomi inconsistenti in posizioni cancellate potrebbe portare a termini estratti non terminanti o errati (un problema noto in Rocq/Coq).

5. Significato

Questo lavoro rappresenta un passo fondamentale verso l'adozione pratica di sistemi di tipi quantitativi e modali nelle lingue di programmazione dipendenti moderne (come Agda e Idris).

• Rigorosità: Fornisce una base formale solida e verificata meccanicamente per le ottimizzazioni basate sull'eliminazione del codice (erasure), che sono cruciali per le prestazioni runtime.
• Flessibilità: La struttura parametrizzata su semianelli permette di modellare non solo la cancellazione, ma anche la linearità, i tipi affini e il flusso di informazioni (security levels).
• Sicurezza: Le prove di correttezza garantiscono che le ottimizzazioni aggressive (come la rimozione di interi blocchi di codice) non introducano bug o alterino la semantica dei programmi corretti.
• Impatto Futuro: La formalizzazione in Agda serve come punto di partenza per sviluppatori di compilatori e ricercatori per implementare verificatori di tipi certificati e migliorare le analisi statiche nelle lingue dipendenti.

In sintesi, il paper risolve il problema di come integrare in modo sicuro e formalmente verificato la gestione delle risorse (in particolare la cancellazione) all'interno di una teoria dei tipi dipendenti completa, fornendo prove meccaniche della correttezza delle trasformazioni di codice risultanti.