Type Theory With Erasure

1. Enunciato del Problema

Nei linguaggi di programmazione a tipi dipendenti (come Agda, Idris e Rocq), i tipi dipendono spesso da valori. Ciò crea un'ambiguità fondamentale: quali parti di un programma sono computazionalmente rilevanti a runtime e quali possono essere eliminate in sicurezza durante la compilazione?

• Approcci Attuali: Le soluzioni esistenti spesso si basano sulla Quantitative Type Theory (QTT), che utilizza un semianello quantitativo (es. $\{0 < \omega\}$) per tracciare l'uso delle variabili. Sebbene efficace, la QTT introduce complessità riguardo ai vincoli sub-strutturali e alla linearità. Altri approcci utilizzano "ghost sorts" o analisi euristica dell'intero programma, che possono essere fragili e imprevedibili per tipi dipendenti complessi.
• Il Divario: C'è la necessità di una formulazione strutturale, modulare e libera da riduzioni dell'eliminazione che si integri perfettamente con la metateoria standard della teoria dei tipi, supporti l'estrazione del codice e fornisca una solida fondazione semantica senza fare affidamento su semantica quantitativa complessa.

2. Metodologia

Gli autori propongono una versione strutturale della teoria dei tipi con eliminazione formulata come una Teoria Algebrica Generalizzata del Secondo Ordine (SOGAT).

• Distinzione Sintetica delle Fasi: Invece di utilizzare semianelli quantitativi, gli autori codificano l'eliminazione come una distinzione di fase utilizzando una proposizione sintetica, indicata come # (il marcatore di eliminazione).
  • Un contesto $\Gamma$ è considerato "eliminato" se contiene la proposizione $\#$ (cioè $\# \in \Gamma$).
  • Ciò crea una distinzione tra modalità runtime ($\omega$) e modalità eliminata ($0$).
  • Crucialmente, $\#$ è una proposizione senza valore di verità; non può essere costruita o scaricata arbitrariamente. Agisce come un marcatore che permette di costringere i termini tra le modalità.
• Meccanismo di Costrizione: La teoria introduce due costrizioni:
  • Eliminazione ($\#$): Se un termine $a$ è di tipo $A$ in un contesto esteso da $\#$, può essere costretto in un termine eliminato ($\# a : 0: A$).
  • Sollevamento (\$): Se un termine $a$ è eliminato, può essere sollevato a un termine runtime sotto l'assunzione di $\#$ (\ a : \omega: A$).
  • Questi sono inversi reciproci fino all'uguaglianza definizionale, garantendo che i termini eliminati non dipendano da dati runtime.
• Formulazione Modulare SOGAT: La teoria è definita come una SOGAT che estende la Teoria dei Tipi di Martin-Löf (MLTT). Ciò permette agli autori di sfruttare la metateoria esistente per le SOGAT, inclusa la semantica funtoriale e la costruzione di modelli tramite Categorie con Famiglie (CwF).

3. Contributi Chiave

A. Formulazione Teorica

• Definizione SOGAT: Il paper definisce TT0 (Type Theory with Erasure) come una SOGAT. Include tipi ($Ty$), termini ($Tm$) indicizzati dalle modalità $\{0, \omega\}$ e il marcatore di eliminazione ($\#$).
• Frammento Eliminato Derivato: Un contributo significativo è che la teoria non ha bisogno di definire esplicitamente versioni eliminate di ogni costruttore di termini (es. $\Pi_0, \Sigma_0$). A causa dell'isomorfismo tra contesti con e senza $\#$, l'intero frammento eliminato è derivato automaticamente dal frammento runtime.
• Tipi Induttivi: Il framework supporta tipi induttivi in cui argomenti specifici (come gli indici) possono essere contrassegnati come eliminati. Gestisce tipi induttivi "esotici" in cui gli stessi costruttori potrebbero esistere solo in modalità eliminata.

B. Modelli Semantici

• Modello Fam(Set): Gli autori costruiscono un modello standard nella categoria delle famiglie di insiemi ($Fam(Set)$).
  • In questo modello, un oggetto è una coppia $(X_0, X_1)$ dove $X_0$ rappresenta dati eliminati e $X_1$ rappresenta dati runtime.
  • Il marcatore di eliminazione $\#$ è interpretato come una "piccola proposizione" (un oggetto $\phi$ tale che l'elevazione a potenza per $\phi$ isola il componente base).
  • Questo modello si generalizza a qualsiasi topos di Grothendieck equipaggiato con una piccola proposizione.
• Universi Schiacciati: Per gestire gli universi nel contesto eliminato, gli autori introducono "universi schiacciati" ($\sqrt{\phi}U$). Questi sono oggetti $\phi$-modali che mantengono la struttura degli universi standard ma soddisfano la condizione che le loro fibre siano contraibili, permettendo loro di esistere in contesti eliminati senza trasportare dati runtime.

C. Estrazione del Codice e Correttezza

• Estrazione nel Calcolo Lambda Non Tipato: Gli autori costruiscono un modello che estrae programmi TT0 nel calcolo lambda non tipato.
  • I termini runtime mappano a termini lambda.
  • I termini eliminati mappano all'oggetto terminale (effettivamente scomparendo).
  • I contesti con variabili eliminate sono isomorfi ai contesti senza di esse.
• Gluing e Relazioni Logiche: Per dimostrare la correttezza, utilizzano il gluing per costruire una relazione logica tra il modello di estrazione del codice e il modello standard insiemistico.
  • Teorema 27 (Non-interferenza): Dimostra che ogni funzione eliminata è costante a runtime. Se una funzione prende un argomento eliminato, il suo output non può dipendere da quell'argomento a runtime.
  • Teorema 25 e 26: Dimostrano la canonicità e che il codice estratto traccia l'interpretazione semantica.

D. Implementazione

• Elaboratore: È stato implementato un elaboratore giocattolo in Agda. Prende un linguaggio di alto livello (simile a Idris/Agda con annotazioni 0 e @0) e lo elabora nella SOGAT core.
• Unificazione di Pattern: Gli autori dimostrano che, poiché il core è strutturale, gli algoritmi standard di unificazione di pattern possono essere riutilizzati senza bisogno di controlli quantitativi complessi o meccanismi di generalizzazione speciali per le metavariable eliminate, risolvendo problemi riscontrati nelle attuali implementazioni di Agda e Idris.

4. Risultati

• Conservatività: La teoria è dimostrata essere conservativa rispetto alla MLTT. Aggiungere l'eliminazione non aumenta il potere dimostrativo della teoria dei tipi; qualsiasi teorema dimostrabile in TT0 è dimostrabile nella MLTT standard.
• Indipendenza: I dati eliminati sono dimostrati essere indipendenti dai dati runtime. Un termine eliminato in un contesto $\Gamma$ corrisponde in modo unico a un termine eliminato nel contesto "azzerato" $0\Gamma$ (dove tutte le modalità sono imposte a 0).
• Correttezza dell'Estrazione: La prova di gluing conferma che il processo di estrazione preserva il comportamento computazionale ed elimina correttamente i dati irrilevanti, garantendo che il codice generato sia sicuro ed efficiente.

5. Significato

• Chiarezza Strutturale: Spostandosi dai semianelli quantitativi a una distinzione sintetica delle fasi, il paper fornisce una fondazione più pulita e modulare per l'eliminazione. Separa il concetto di eliminazione dal meccanismo di tracciamento delle risorse.
• Guida all'Implementazione: L'approccio strutturale semplifica l'implementazione di type checker ed elaboratori. Rimuove la necessità di controlli quantitativi ad hoc durante l'unificazione, potenzialmente risolvendo bug in sistemi esistenti come Idris 2 e Agda.
• Fondazione Semantica: L'uso di topos di Grothendieck e piccole proposizioni collega l'eliminazione alla logica categoriale più ampia, permettendo l'uso della Computabilità Sintetica di Tait per prove metateoriche.
• Estensioni Future: Il framework è progettato per essere estensibile, supportando potenziali lavori futuri sui tipi runtime, distinzioni di fase multiple (per staging/metaprogrammazione) e integrazione con la Cubical Type Theory.

In sintesi, questo paper presenta un approccio rigoroso, strutturale e semanticamente fondato alla teoria dei tipi con eliminazione, offrendo sia garanzie teoriche (conservatività, non-interferenza) che benefici pratici per l'implementazione dei compilatori e l'estrazione del codice.