Dependent Multiplicities in Dependent Linear Type Theory

Enunciato del Problema
Le teorie dei tipi quantitative esistenti, come la Teoria dei Tipi Quantitativa (QTT) e la Teoria dei Tipi Modali Gradata, permettono annotazioni delle risorse in cui le variabili hanno molteplicità che specificano quante volte vengono utilizzate. Tuttavia, questi sistemi si basano tipicamente su molteplicità statiche tratte da un'algebra delle risorse fissa (ad esempio, numeri naturali o semianelli). Questa natura statica crea limitazioni significative quando si affronta la logica dei programmi che non rappresenta direttamente le risorse ma le organizza, come il diramamento (condizionali) e la ricorsione.

Nei sistemi attuali, una condizione booleana utilizzata per selezionare tra due rami richiede che entrambi i rami consumino risorse identiche, il che è spesso poco pratico poiché rami diversi eseguono tipicamente operazioni diverse. Analogamente, nelle funzioni di ordine superiore o nei tipi induttivi (come gli alberi binari), il numero di volte in cui una funzione viene applicata o una risorsa consumata dipende spesso da valori noti solo a runtime (ad esempio, il numero di foglie in un albero). I precedenti tentativi di combinare la Teoria dei Tipi Dipendenti (DTT) con la logica lineare hanno faticato con la questione se i tipi dipendenti dai termini costituiscano un "utilizzo" di tali termini. Sebbene McBride e Atkey abbiano sostenuto che i tipi sono per la contemplazione e non per il calcolo (consentendo la dipendenza da variabili lineari), la loro QTT risultante continua a limitare le molteplicità a elementi statici, fallendo nel catturare l'uso dinamico delle risorse intrinseco ai programmi ricorsivi e al diramamento dipendente dai dati.

Metodologia
Il documento propone una nuova teoria dei tipi lineare dipendente che incorpora la logica lineare direttamente in una Teoria dei Tipi Dipendenti intuizionistica standard (la "teoria ospite"). L'innovazione fondamentale è il trattamento delle molteplicità non come elementi algebrici statici, ma come termini all'interno della teoria ospite stessa.

1. Due Relazioni di Conseguenza: Il sistema distingue tra due giudizi:
   • $\vdash$: La DTT intuizionistica standard (teoria ospite), utilizzata per definire tipi, termini e dipendenze.
   • $\Vdash$: Un calcolo consapevole delle risorse in cui i termini sono derivati da "forniture" (contesti lineari).
2. Forniture come Tipi Intuizionistici: A differenza dei contesti lineari tradizionali, le forniture in questo sistema sono termini della teoria ospite. Ciò permette alla teoria ospite di calcolare con le annotazioni delle risorse. Nello specifico, il sistema utilizza i numeri naturali della teoria ospite per definire una "moltiplicazione" delle forniture ($\Delta \hat{m}$), dove $m$ è un termine di tipo $\mathbb{N}$. Questa operazione permette di duplicare una fornitura $m$ volte, dove $m$ può dipendere da altre variabili nel contesto.
3. Molteplicità Dinamiche: Consentendo alla molteplicità $m$ di essere un termine aperto della teoria ospite, il sistema supporta annotazioni delle risorse dinamiche. Ad esempio, una funzione che mappa su un albero può specificare che una funzione $f$ è utilizzata esattamente leafs(t) volte, dove leafs(t) è calcolato dalla struttura dell'albero di input $t$.
4. Formatori di Tipi: Il documento definisce versioni lineari dei formatori di tipi standard della DTT (funzioni, coppie, booleani e tipi W) annotate con queste molteplicità dinamiche. Crucialmente, le regole di eliminazione per i booleani e i tipi W permettono alle risorse di essere distribuite diversamente tra i rami o i costruttori in base ai valori a runtime.
5. Semantica: La semantica è caratterizzata come "Categorie Lineari con Famiglie" (lCwF), che sono Categorie con Famiglie (CwF) indicizzate in categorie monoidali simmetriche. Questa struttura generalizza le CwF Quantitative utilizzate per la QTT.

Contributi Chiave

• Sintassi con Molteplicità Dipendenti: Il documento presenta una sintassi in cui le molteplicità delle variabili sono termini della teoria ospite, abilitando la tipizzazione precisa di programmi che coinvolgono diramamento e ricorsione che precedentemente non erano tipabili nei sistemi lineari.
• Tipi W Lineari: Un trattamento rigoroso dei tipi induttivi (in particolare i tipi W con posizioni finite) in un contesto lineare. Il sistema fornisce regole di introduzione ed eliminazione che tengono correttamente conto dell'uso dinamico delle risorse delle strutture ricorsive.
• Caratterizzazione Semantica: Gli autori definiscono le lCwF come modello semantico per la teoria, mostrando come i modelli DTT standard e i modelli di logica lineare si combinino. Dimostrano che questo modello giustifica le regole intricate per i tipi W lineari e generalizza i modelli esistenti per la QTT.
• Realizzabilità ed Erasure: Viene costruito un modello di realizzabilità (basato su algebre BCI) per mostrare che il frammento intuizionistico ($\vdash$) può essere cancellato per il calcolo, lasciando solo il frammento lineare ($\Vdash$) per l'esecuzione, simile ai frammenti 0 e 1 della QTT.
• Implementazione: La teoria è implementata in Agda. L'implementazione utilizza l'interpretazione semantica (mappando giudizi lineari a termini intuizionistici equipaggiati con testimoni di fornitura) per creare un type checker rigoroso, sebbene non ancora pratico.

Risultati

• Espressività: Il sistema tipizza con successo programmi che richiedono il conteggio dinamico delle risorse, come una funzione map per alberi binari in cui l'uso della funzione di mappatura è proporzionale al numero di foglie.
• Completezza: Il documento dimostra un risultato di completezza per i "termini chiaramente lineari" (termini intuizionistici che non scartano o duplicano valori tramite specifici eliminatori), mostrando che possono essere tipizzati con precisione nel sistema lineare.
• Recupero della Logica Intuizionistica: Introducendo un comonade esponenziale lineare ("!"), il sistema può recuperare la logica intuizionistica completa all'interno del frammento lineare, permettendo l'uso illimitato delle risorse dove necessario.
• Compromesso sulla Decidibilità: Gli autori riconoscono che il type-checking è indecidibile nel caso generale perché richiede il confronto di termini aperti di numeri naturali (ad esempio, verificare se $\Delta \hat{m}$ è uguale a $\Delta \hat{n}$). Tuttavia, notano che l'uguaglianza proposizionale nella teoria ospite può essere utilizzata per convincere il type checker dell'equivalenza delle risorse.

Significato
Il documento afferma di fornire una versione più espressiva della Teoria dei Tipi Quantitativa passando da algebre delle risorse statiche a molteplicità dinamiche e calcolabili derivate dalla teoria ospite. Incorporando la logica lineare nella DTT invece di trattarle come logiche separate, il sistema evita la dicotomia restrittiva tra variabili intuizionistiche e lineari trovata nei lavori precedenti. Ciò permette un "trattamento consapevole delle risorse e rigoroso" di una vasta classe di tipi induttivi e funzioni di ordine superiore. Il lavoro dimostra che i linguaggi esistenti con tipi dipendenti possono essere estesi con questo sistema, offrendo una via verso una gestione delle risorse più precisa nella programmazione funzionale senza sacrificare l'espressività dei tipi dipendenti. Gli autori posizionano il loro lavoro come una generalizzazione della QTT che risolve le limitazioni delle molteplicità statiche nella gestione dell'uso delle risorse dipendente dal runtime.