Measuring data types

Technische Samenvatting: Het Meten van Datatypen

Probleemstelling
Functionele programmeertalen (bijv. Haskell, Agda, Coq) leunen zwaar op inductieve datatypen, die categorisch gerechtvaardigd zijn als initiële algebra's van endofunctoren, specifiek polynomiale endofunctoren bekend als W-typen. Hoewel de categorische semantiek van deze typen goed begrepen is als initiële algebra's, identificeert het artikel een gat in de wiskundige structuur daaromheen. Specifiek behandelt het standaard categorische kader tussen algebra's slechts hom-sets van totale homomorfismen. Dit faalt om "partiële" of "benaderende" structurele relaties tussen datatypen te vatten, die cruciaal zijn voor het begrijpen van hoe morfismen interageren met inductieve structuren op een gegradeerde of gelaagde wijze. De auteurs zoeken naar de structuur waarin W-typen zijn ingebed door een analogie te trekken met Sweedlers klassieke theorie van meetende coalgebra's, waarbij algebra's over een veld verrijkt zijn in coalgebra's.

Methodologie
Het artikel maakt gebruik van een synthese van twee afzonderlijke categorische theorieën:

1. Sweedlers Meetende Coalgebra's: De auteurs herzien de klassieke theorie waarbij $k$-algebra's verrijkt zijn in $k$-coalgebra's. In deze setting is het hom-object tussen twee algebra's niet een verzameling homomorfismen, maar een coalgebra van "partiële homomorfismen" (of measurings). Deze measurings maken morfismen mogelijk die "bijna" homomorfismen zijn, waarbij de coalgebra-structuur codeert "hoe dicht" een morfisme bij een totaal homomorfisme ligt.
2. W-Typen en Inductieve Datatypen: Het artikel herzien de categorische semantiek van inductieve typen als initiële algebra's van endofunctoren (specifiek polynomiale endofunctoren).

De kernmethodologie behelst het generaliseren van Sweedlers theorie van de context van algebra's over een veld naar algebra's van een willekeurige endofunctor $F$ op een symmetrisch monoidale gesloten categorie $\mathcal{C}$. De auteurs gaan ervan uit dat $\mathcal{C}$ lokaal presentabel is en dat $F$ een toegankelijke, lax symmetrische monoidale endofunctor is. Zij construeren een verrijking van de categorie van $F$-algebra's ($\text{Alg}_F$) over de categorie van $F$-coalgebra's ($\text{coAlg}_F$).

Belangrijke technische stappen zijn onder meer:

• Het definiëren van measurings (afbeeldingen $C \otimes A \to B$) en partiële homomorfismen (afbeeldingen $C \to [A, B]$) voor $F$-algebra's en $F$-coalgebra's.
• Het bewijzen van het bestaan van een universele meetende coalgebra $\text{Alg}(A, B)$, die dient als het hom-object in de verrijkte categorie.
• Het construeren van de meetende tensor $C \triangleright A$ en de convolutie-algebra $[C, B]$ om vast te stellen dat de categorie getensoreerd en cotensoreerd is.
• Het generaliseren van het begrip initiële algebra's naar $C$-initiële algebra's, waarbij $C$ een coalgebra is, analoog aan gewogen limieten in verrijkte categorietheorie.

Kernbijdragen en Resultaten

1. Verrijking van Algebra's in Coalgebra's (Stelling 10):
   Het centrale resultaat stelt dat voor een lokaal presentabele, gesloten symmetrische monoidale categorie $\mathcal{C}$ en een toegankelijke, lax symmetrische monoidale endofunctor $F$, de categorie van $F$-algebra's verrijkt, getensoreerd en cotensoreerd is over de categorie van $F$-coalgebra's.

   • In plaats van een verzameling homomorfismen $\text{Alg}(A, B)$, bestaat er een coalgebra $\text{Alg}(A, B)$ die alle mogelijke partiële homomorfismen representeert.
   • Deze verrijking wordt gekenmerkt door natuurlijke isomorfismen:
     $$\text{coAlg}(C, \text{Alg}(A, B)) \cong \text{Alg}(C \triangleright A, B) \cong \text{Alg}(A, [C, B])$$

2. Generalisatie van W-Typen:
   De auteurs generaliseren het concept van W-typen (initiële algebra's van polynomiale endofunctoren) naar $C$-initiële algebra's. Een $C$-initiële algebra is een algebra $A$ waarvoor voor elke algebra $X$ een uniek coalgebra-homomorfisme $C \to \text{Alg}(A, X)$ bestaat. Dit maakt een meer genuanceerde classificatie van inductieve typen mogelijk op basis van de "vorm" of "diepte" die door de coalgebra $C$ wordt gecodeerd.

3. Toren van Partiële Homomorfismen:
   Het artikel construeert een toren van coalgebra's $\text{Alg}_n(A, B)$ die $n$-partiële homomorfismen representeert. Het limiet van deze toren, $\text{Alg}_\infty(A, B)$, komt overeen met $\infty$-partiële homomorfismen, die totale algebra-homomorfismen benaderen. Dit biedt een formeel mechanisme voor "partiële inductie", waarbij men homomorfismen inductief laag voor laag kan opbouwen.

4. Expliciete Voorbeelden en Berekeningen:
   De theorie wordt toegepast op verschillende standaarddatatypen in de informatica, waaronder:

   • Unit en Lege Typen: Het demonstreren van triviale verrijkingen.
   • Monoid Typen: Het tonen van hoe de monoidale structuur "twists" in measurings introduceert.
   • Natuurlijke Getallen: Het berekenen van de universele meetende coalgebra voor pre-initiële algebra's (eindige afkortingen van $\mathbb{N}$) en het bewijzen dat de eindige afkorting $n$ de tertimale $n^\circ$-initiële algebra is.
   • Lijsten en Bomen: Het uitbreiden van de theorie naar lijst-typen (over een monoid) en binaire/algemene bomen. De auteurs laten zien hoe measurings zowel de "vorm" (diepte/vertakking) als de "twist" (element-gewijze modificatie) van datastructuren kunnen controleren. Zo tonen ze bijvoorbeeld aan dat hoewel een totale algebra-homomorfisme van een afgekortte lijst naar het volledige lijst-type mogelijk niet bestaat, een measuring dat wel doet.

Betekenis en Claims
Het artikel claimt de "zuiverste vorm" van het Sweedler-fenomeen te bieden door het toe te passen op endofunctoren, die een gebrek hebben aan de coherentie-beperkingen (eenheden, vermenigvuldiging) van traditionele algebra's. De auteurs stellen dat deze verrijking een hogere precisie biedt voor het bestuderen van interacties tussen algebra's, waarbij men verder gaat dan de binaire distinctie van "is een homomorfisme" of "is geen homomorfisme".

De betekenis is tweeledig:

1. Zuivere Wiskunde: Het verenigt de theorie van meetende coalgebra's met de theorie van W-typen, en breidt de reikwijdte van de Sweeder-theorie uit naar een bredere categorische setting. Het generaliseert het begrip van initiële algebra's naar $C$-initiële algebra's, wat een nieuw perspectief biedt op inductieve typen.
2. Programmeerentalentheorie: Het kader biedt een categorische rechtvaardiging voor "partiële" operaties op inductieve typen. De auteurs suggereren dat deze structuur uiteindelijk de implementatie van inductieve typen in functionele programmeertalen (zoals Haskell) zou kunnen informeren, wat potentieel meer flexibele afhandeling van partiële data of oneindige stromen (streams) mogelijk maakt.

Het artikel merkt expliciet op dat het een uitgebreide versie is van een eerder werk [20], waarbij expositieve introducties, volledige bewijzen en een gegeneraliseerde torenconstructie voor partiële inductie zijn toegevoegd. Er wordt erkend dat hoewel de theorie is vastgesteld voor specifieke endofunctoren (zoals die voor lijsten en bomen), de functorialiteit van de constructie in de categorie $\mathcal{C}$ en de endofunctor $F$ een onderwerp blijft voor toekomstig werk. Ook worden concrete implementaties in programmeertalen geïdentificeerd als een toekomstige richting in plaats van een huidig resultaat.