Type Theory With Erasure

1. Probleemstelling

In afhankelijk getypeerde programmeertalen (zoals Agda, Idris en Rocq) hangen types vaak af van waarden. Dit creëert een fundamentele ambiguïteit: welke delen van een programma zijn computationeel relevant tijdens de uitvoering, en welke kunnen veilig worden verwijderd tijdens het compileren?

• Huidige Benaderingen: Bestaande oplossingen vertrouwen vaak op Quantitative Type Theory (QTT), die een kwantitatieve halfring (bijv. $\{0 < \omega\}$) gebruikt om variabelegebruik bij te houden. Hoewel effectief, introduceert QTT complexiteit met betrekking tot substructurele beperkingen en lineariteit. Andere benaderingen gebruiken "spooksoorten" of heuristische analyse van het hele programma, wat kwetsbaar en onvoorspelbaar kan zijn voor complexe afhankelijk getypeerde constructies.
• Het Gat: Er is behoefte aan een structurele, modulaire en reductievrije formulering van verwijdering die naadloos integreert met de standaard metatheorie van type-theorie, code-extractie ondersteunt en een duidelijke semantische basis biedt zonder te vertrouwen op complexe kwantitatieve semantiek.

2. Methodologie

De auteurs stellen een structurele versie van type-theorie met verwijdering voor, geformuleerd als een Second-Order Generalised Algebraic Theory (SOGAT).

• Synthetische Fasendistinctie: In plaats van kwantitatieve halfringen te gebruiken, coderen de auteurs verwijdering als een fasendistinctie met behulp van een synthetische propositie, aangeduid als # (het verwijderingsmarkeermiddel).
  • Een context $\Gamma$ wordt beschouwd als "verwijderd" als deze de propositie $\#$ bevat (d.w.z. $\# \in \Gamma$).
  • Dit creëert een onderscheid tussen uitvoeringsmodus ($\omega$) en verwijderde modus ($0$).
  • Cruciaal is dat $\#$ een propositie is zonder waarheidswaarde; deze kan niet willekeurig worden geconstrueerd of ontladen. Het fungeert als een marker die termen toestaat om tussen modi te worden gecoerceerd.
• Coerciemechanisme: De theorie introduceert twee coercies:
  • Verwijdering ($\#$): Als een term $a$ van type $A$ is in een context die is uitgebreid met $\#$, kan deze worden gecoerceerd tot een verwijderde term ($\# a : 0: A$).
  • Opheffing (\$): Als een term $a$ is verwijderd, kan deze worden opgeheven tot een uitvoeringsterm onder de aanname van $\#$ (\ a : \omega: A$).
  • Deze zijn wederzijdse inverse tot op definitorische gelijkheid, wat garandeert dat verwijderde termen niet afhankelijk zijn van uitvoeringsdata.
• Modulaire SOGAT-Formulering: De theorie is gedefinieerd als een SOGAT die Martin-Löf Type Theory (MLTT) uitbreidt. Dit stelt de auteurs in staat om bestaande metatheorie voor SOGATs te benutten, inclusief functoriële semantiek en modelconstructie via Categories with Families (CwFs).

3. Belangrijkste Bijdragen

A. Theoretische Formulering

• SOGAT-definitie: Het artikel definieert TT0 (Type Theory with Erasure) als een SOGAT. Het bevat types ($Ty$), termen ($Tm$) geïndexeerd door modi $\{0, \omega\}$, en het verwijderingsmarkeermiddel ($\#$).
• Afgeleid Verwijderd Fragment: Een aanzienlijke bijdrage is dat de theorie niet expliciet verwijderde versies van elke termvormer hoeft te definiëren (bijv. $\Pi_0, \Sigma_0$). Vanwege de isomorfie tussen contexten met en zonder $\#$, wordt het volledige verwijderde fragment automatisch afgeleid uit het uitvoeringsfragment.
• Inductieve Types: Het raamwerk ondersteunt inductieve types waarbij specifieke argumenten (zoals indices) kunnen worden gemarkeerd als verwijderd. Het behandelt "exotische" inductieve types waarbij constructoren zelf mogelijk alleen in verwijderde modus bestaan.

B. Semantische Modellen

• Fam(Set)-model: De auteurs construeren een standaardmodel in de categorie van familie van verzamelingen ($Fam(Set)$).
  • In dit model is een object een paar $(X_0, X_1)$ waarbij $X_0$ verwijderde data voorstelt en $X_1$ uitvoeringsdata.
  • Het verwijderingsmarkeermiddel $\#$ wordt geïnterpreteerd als een "kleine propositie" (een object $\phi$ zodat exponentiatie door $\phi$ het basiscomponent isoleert).
  • Dit model generaliseert naar elke Grothendieck-topos uitgerust met een kleine propositie.
• Geknepen Universa: Om universa in de verwijderde context te hanteren, introduceren de auteurs "geknepte universa" ($\sqrt{\phi}U$). Dit zijn $\phi$-modale objecten die de structuur van standaard universa behouden, maar voldoen aan de voorwaarde dat hun vezels contractibel zijn, waardoor ze kunnen bestaan in verwijderde contexten zonder uitvoeringsdata te dragen.

C. Code-extractie en Correctheid

• Extractie naar Ongetypeerde Lambda-calculus: De auteurs construeren een model dat TT0-programma's extrahert naar ongetypeerde lambda-calculus.
  • Uitvoeringstermen worden afgebeeld op lambdatermen.
  • Verwijderde termen worden afgebeeld op het terminale object (effectief verdwijnend).
  • Contexten met verwijderde variabelen zijn isomorf aan contexten zonder deze variabelen.
• Lijmen en Logische Relaties: Om correctheid te bewijzen, gebruiken ze lijmen om een logische relatie te construeren tussen het code-extractiemodel en het standaard verzamelingstheoretische model.
  • Stelling 27 (Niet-interferentie): Bewijst dat elke verwijderde functie constant is tijdens de uitvoering. Als een functie een verwijderd argument neemt, kan de uitvoer niet afhankelijk zijn van dat argument tijdens de uitvoering.
  • Stelling 25 & 26: Bewijzen canoniciteit en dat geëxtraheerde code de semantische interpretatie volgt.

D. Implementatie

• Elaborator: Een toy-elaborator is geïmplementeerd in Agda. Deze neemt een hoog-niveau taal (vergelijkbaar met Idris/Agda met 0 en @0 annotaties) en elaboratieert deze naar de kern-SOGAT.
• Patroonunificatie: De auteurs demonstreren dat, omdat de kern structureel is, standaard patroonunificatie-algoritmen kunnen worden hergebruikt zonder complexe kwantiteitscontroles of speciale generalisatiemechanismen voor verwijderde metavariables nodig te hebben. Dit lost problemen op die worden aangetroffen in huidige implementaties van Agda en Idris.

4. Resultaten

• Conservativiteit: De theorie is bewezen conservatief over MLTT te zijn. Het toevoegen van verwijdering verhoogt niet de bewijskracht van de type-theorie; elke stelling die in TT0 bewijsbaar is, is bewijsbaar in standaard MLTT.
• Onafhankelijkheid: Verwijderde data is bewezen onafhankelijk te zijn van uitvoeringsdata. Een verwijderde term in een context $\Gamma$ komt uniek overeen met een verwijderde term in de "gezeroede" context $0\Gamma$ (waar alle modi op 0 zijn ingesteld).
• Correctheid van Extractie: Het lijm-bewijs bevestigt dat het extractieproces computationeel gedrag behoudt en irrelevante data correct verwijdert, waardoor gegarandeerd wordt dat de gegenereerde code veilig en efficiënt is.

5. Betekenis

• Structurele Duidelijkheid: Door weg te bewegen van kwantitatieve halfringen naar een synthetische fasendistinctie, biedt het artikel een schonere, meer modulaire basis voor verwijdering. Het scheidt het concept van verwijdering van het mechanisme van resource-tracking.
• Implementatiegids: De structurele benadering vereenvoudigt de implementatie van typecheckers en elaborators. Het verwijdert de noodzaak voor ad-hoc kwantiteitscontroles tijdens unificatie, wat potentieel bugs in bestaande systemen zoals Idris 2 en Agda kan oplossen.
• Semantische Basis: Het gebruik van Grothendieck-toposen en kleine proposities verbindt verwijdering met bredere categorische logica, waardoor het gebruik van Synthetic Tait Computability voor metatheoretische bewijzen mogelijk wordt.
• Toekomstige Uitbreidingen: Het raamwerk is ontworpen om uitbreidbaar te zijn, met ondersteuning voor potentiële toekomstig werk aan runtime-types, meerdere fasendistincties (voor staging/metaprogrammering), en integratie met Cubical Type Theory.

Kortom, dit artikel presenteert een rigoureuze, structurele en semantisch onderbouwde aanpak van type-theorie met verwijdering, die zowel theoretische garanties (conservativiteit, niet-interferentie) als praktische voordelen biedt voor compiler-implementatie en code-extractie.