Tweag a représenté les faisceaux en Haskell en rendant explicites les opérations de collage

Arnaud Spiwack voulait représenter les faisceaux en Haskell, mais la définition des manuels posait un problème pratique : les cribles contiennent de nombreuses représentations redondantes de la même information de correspondance, et leur construction dépendante par produit fibré exigeait trop de typage dépendant pour Haskell. L'approche évidente — traduire la définition littéralement — rendrait représentables des états illégaux et noierait le programme dans des données non pertinentes.

Il a d'abord construit un exemple concret autour d'expressions arithmétiques. Un préfaisceau pouvait tirer des valeurs en arrière le long d'expressions, mais l'opération conditionnelle souhaitée exigeait un faisceau pour coller deux branches sur un recouvrement booléen. L'implémentation a donc fait du collage une opération explicite de classe de types, puis l'a généralisée en un Site dont les familles typées Cover et Gen décrivent quelles pièces peuvent être assemblées.

Le site typé supprime la charge du crible par produit fibré : le collage peut opérer sur n'importe quelle flèche, et les générateurs n'ont pas besoin d'être représentés comme de véritables flèches. Les produits, les exponentielles, les plongements de Yoneda, les coproduits et les listes récursives peuvent alors être définis dans le même style. Sheafify agit comme une construction de faisceau libre en stockant les opérations de collage plutôt qu'en les évaluant prématurément, tandis que PFun porte la variance nécessaire aux exponentielles.

Le résultat est un dépôt de démonstration et une implémentation à la manière de Haskell de l'idée abstraite, et non l'affirmation que chaque détail mathématique disparaît. Spiwack laisse explicitement les points fixes non résolus, mais le projet convertit une définition trop lâche pour le langage en briques opérationnelles typées et rend précise l'inconnue restante.

Représenter les recouvrements comme des types, puis coller explicitement

Les cribles littéraux encodent des valeurs redondantes de familles de correspondance et autorisent des états qui devraient être impossibles.

Le crible par produit fibré nécessaire aux exponentielles exige un typage dépendant au-delà de ce que l'implémentation Haskell pouvait exprimer confortablement.

Les recouvrements et générateurs typés gardent petite l'interface de collage valide tout en supprimant les représentations non pertinentes.

Sheafify stocke la syntaxe de collage, permettant des constructions libres telles que les coproduits et les listes récursives sans exécuter les opérations trop tôt.

Faire des points fixes une frontière explicite non résolue empêche l'implémentation de prétendre résoudre ce qu'elle ne sait pas encore.

Lorsqu'une définition formelle crée des états illégaux et un typage dépendant impossible, encodez les recouvrements valides dans les types et n'exposez que des opérations de collage exécutables. Réservez les constructions libres à la composition.

Le projet a produit un dépôt de démonstration avec des instances concrètes et abstraites de Site/Sheaf, ainsi qu'une frontière plus claire autour de ce que l'encodage peut et ne peut pas exprimer. Les points fixes restent non résolus, mais l'approche par recouvrements typés rend les opérations de faisceau utilisables en Haskell sans importer tout le poids de la machinerie dépendante des cribles.