2.4. Adjonctions et enrichissement🔗

La fermeture de C, construite en §2.1 comme l'adjonction (- \otimes A) \dashv [A \multimap -], n'est pas qu'une clause de définition : c'est elle qui légitime, au chapitre 6, l'effacement du curryfiage à la compilation. La bijection naturelle de l'équation 5 identifie, pour tout \Gamma, une fonction de deux arguments \Gamma \otimes A \to B à sa forme curryfiée \Gamma \to [A \multimap B] — les deux dénotent le même élément, de part et d'autre d'un isomorphisme naturel, donc sémantiquement transparent au sens de P1a, et la correction de la compilation de cette équivalence relève de P1b, non établie (chapitre 1). Un programme K7PL à plusieurs arguments admet ainsi indifféremment une présentation curryfiée, en fermetures successives, ou une présentation directe (X \otimes Y \otimes Z) \to R. La monomorphisation du chapitre 6, qui compile systématiquement vers la seconde, n'est donc pas une heuristique risquant d'altérer le sens du programme : l'argument est syntaxique — chaque présentation se transforme en l'autre par substitution, les règles de l'abstraction et de l'application étant inversibles —, et ne requiert pas l'interprétation P1b. C'est le choix, parmi les représentants d'une même classe d'isomorphisme, de celui qui n'alloue aucune fermeture intermédiaire, conformément à P3.

Une seconde conséquence de la fermeture concerne la représentation des tableaux, et elle appelle d'abord une déclaration sur la classe à laquelle appartiennent les types de K7PL — car c'est cette classe, et non un artifice local, qui la rend possible.

Les types de K7PL sont des conteneurs indexés. La notion syntaxiquement riche de famille strictement positive s'y réduit à une théorie noyau munie d'un nombre fixe de constructeurs de types, les conteneurs indexés en fournissant les formes normales, et cette réduction s'obtient sans étendre la théorie noyau [39]. Trois conséquences en découlent, énoncées ici plutôt que redécouvertes au chapitre 3. D'abord la condition de clôture posée au chapitre 1 (§1.4) cesse d'être une discipline de conception pour devenir un résultat, du moins sur le versant qui concerne la grammaire des types. Un nombre fixe de constructeurs suffit à toute famille strictement positive, de sorte qu'aucune extension n'a besoin d'en ajouter un.

Le mot est fixé ici, ce chapitre lui donnant trois emplois : les composantes du jugement sont les trois du chapitre 1, \Delta, A et \mathcal{E} ; les composantes du grade sont les coordonnées de son produit ; et les constructeurs de la théorie noyau sont ce dont il est question dans cette phrase. Ce sont ces derniers dont le nombre est fixe, et cela ne dit rien du nombre des deux autres.

Ensuite les familles indexées que le chapitre 3 emploie — Vector(n,T), les rangées à grade de présence, Incomplete A B dont la forme change à chaque remplissage — sont admises d'office, sans qu'aucune primitive ne soit ajoutée pour les accueillir. Enfin, et c'est ce dont le §2.3 a besoin, les conteneurs préservent les plus petits et les plus grands points fixes [29] : \mu F et \nu G restent l'un et l'autre dans la classe, et leur emboîtement aussi.

Cela posé, un tableau de taille n sur T n'est pas un conteneur distinct des fonctions : c'est un élément de \text{Hom}(\text{Fin}(n), T), où \text{Fin}(n) est le coproduit de n copies de l'unité, \text{Fin}(n) = \underbrace{I \oplus \dots \oplus I}_{n}. Puisque le foncteur \text{Hom}(-, T) transforme les coproduits en produits, et que les éléments globaux \text{Hom}(I,T) s'identifient aux valeurs de T elles-mêmes, il vient

C'est cette lecture — un conteneur fini est déterminé par la façon dont il s'observe depuis un objet représentable, l'intuition centrale du lemme de Yoneda — que la théorie des types du chapitre 3 exploite pour encoder les contraintes de taille sans recourir à des types dépendants complets : Vec n T n'est pas un type primitif supplémentaire, c'est une notation pour \text{Hom}(\text{Fin}(n), T).

La dernière structure que C doit porter est la relation de précision \sqsubseteq annoncée au chapitre 1 (P2). Sur chaque catégorie d'artefacts syntaxiques — types, termes, contextes, effets, grades — \sqsubseteq est un demi-treillis supérieur borné, de joint \sqcup et d'élément minimal : A \sqsubseteq B se lit « A est une version au plus aussi précise que B ». Pourquoi cette structure et pas une plus riche ? Une version antérieure de ce texte déclarait un treillis distributif borné et l'engagement était plus lourd que l'usage. Le joint sert : aux branchements du chapitre 3, où il sur-approxime les effets d'un filtrage, et à la relation de sous-typage du §3.6, dont le théorème 31 montre qu'il conditionne la cohérence. La rencontre ne sert nulle part, et la distributivité n'est invoquée par aucune démonstration. Déclarer moins n'affaiblit donc rien~; cela retire seulement une dette de justification qu'aucun résultat ne réclamait.

Il faut en revanche dire de quel ordre il s'agit, car deux théories de l'information portent le même mot sans être le même ordre. Celle de Shannon ordonne par ce qu'on sait — des relations d'équivalence sur le domaine, formant un treillis complet —, celle de Scott par ce qui est défini, au sens du progrès du calcul [40]. La relation de précision compare des raffinements, donc ce qu'un type garantit : elle est du côté de Shannon. La conséquence n'est pas verbale, les deux ordres n'ayant pas les mêmes propriétés de complétude — et il n'est pas indifférent que la composante de niveau du grade emploie ce même treillis, redécouvert plusieurs fois dans la littérature du flot d'information.

K7PL étend cette relation aux morphismes de C eux-mêmes et exige que la composition et le tenseur soient monotones : si f \sqsubseteq f' et g \sqsubseteq g', alors g \circ f \sqsubseteq g' \circ f' et f \otimes g \sqsubseteq f' \otimes g'. C'est la structure d'une catégorie enrichie sur les préordres — C ne perd rien de sa structure ordinaire, elle gagne un ordre compatible sur chaque ensemble de morphismes parallèles et sur ses objets.

Cette exigence de monotonie ne pèse pas sur chaque primitive séparément : elle est portée par les types, au même titre que l'usage l'est par les grades. Le grade d'une liaison acquiert à cette fin une seconde composante, discrète ou monotone, et une fonction dont le grade porte la seconde marque est astreinte à préserver \sqsubseteq. Le procédé est celui de Datafun, qui suit la monotonie par les types en distinguant deux sortes de variables et deux flèches [41]. K7PL n'en retient pas la présentation à deux zones, qu'il a écartée au chapitre 1 (§1.4), mais l'idée que la monotonie est une propriété déclarée et vérifiée plutôt qu'une charge de preuve reconduite à chaque extension. Une construction nouvelle n'a donc pas à démontrer qu'elle respecte l'ordre : elle porte un grade qui l'y oblige, ou n'en porte pas et se voit refuser l'accès aux constructions qui l'exigent.

Ce procédé n'est pas propre à la monotonie, et s'énonce une fois dans sa forme générale. Soit (P, \preceq) une structure ordonnée. Une modalité graduée sur P est une famille de comonades \{!_p\}_{p \in P} sur C, indexée par P, telle que p \preceq q induise une coercion !_q A \to !_p A et que l'ordre gouverne la composition. Le grade d'une liaison porte alors une composante dans P, et la contrainte que cette composante exprime est toujours de la même forme : une flèche graduée en p ne peut employer que ce qui est disponible en deçà de p.

Ce procédé a plus d'instances que le document ne le laisse voir, et les compter est ce qui mesure sa portée. Les voici toutes, avec la structure ordonnée que chacune prend pour paramètre.

Neuf instances, et aucune n'a demandé de mécanisme propre. RMQ 24. Neuf applications d'une construction écrite une fois. C'est la mesure de ce que le procédé vaut, et elle ne se lisait nulle part. Deux données complètent le tableau sans être des modalités, et il faut dire pourquoi : le mode — une algèbre, un idéal de contraction, un booléen d'affaiblissement — fixe les règles structurelles admissibles plutôt qu'une contrainte sur les liaisons ; et la zone y ajoute un ordre propre. Ce sont les paramètres du procédé, non ses produits.

Ce que ce tableau établit n'est pas une économie d'écriture, c'est la portée de la condition de clôture. Une extension qui réclamerait une dixième modalité ne demanderait rien de neuf — il lui suffirait de nommer sa structure ordonnée. C'est ce que la distribution a fait, et c'est pourquoi elle a pu entrer sans quatrième place dans le jugement.

Deux instances suffisent à montrer que la forme est la bonne. La monotonie est la modalité sur l'ordre à deux points \{\text{discret} \prec \text{monotone}\} : une flèche graduée monotone ne peut employer ses arguments que d'une manière qui préserve \sqsubseteq, et la coercion descendante dit qu'une fonction monotone s'emploie partout où une fonction quelconque est admise. La confidentialité est la modalité sur un treillis de niveaux (\mathcal{L}, \leq) : une flèche graduée en \ell ne peut employer que des valeurs de niveau au plus \ell, et la coercion monte l'information sans jamais la redescendre. Le mécanisme est identique, seule change la structure ordonnée sur laquelle il opère [42] — de sorte que la confidentialité n'ajoute pas un axe au langage mais instancie celui que la monotonie a ouvert.

Un dispositif reste à mentionner, sans lequel cette modalité serait impraticable et avec lequel elle est fragile. Un programme utile doit parfois abaisser délibérément un niveau — vérifier un mot de passe consiste à révéler un bit d'une valeur secrète, et le refuser rendrait le langage inutilisable. Ce mécanisme, la déclassification, coerce le niveau vers le bas et sert d'échappatoire au régime ordinaire. Son risque propre porte un nom : l'attaque par blanchiment, où l'échappatoire est employée pour faire sortir davantage que ce qu'elle était censée libérer, une valeur secrète transitant par la fonction déclassifiante sous un déguisement quelconque [43]. Il en résulte que spécifier la déclassification demande deux choses et non une : une règle qui l'autorise, et une garantie de bout en bout qui borne ce qu'elle peut libérer — la divulgation délimitée, dont il est établi qu'un système de types l'impose. Une règle sans cette garantie rendrait le grade de confidentialité contournable par construction, et ce document ne donne pour l'instant ni l'une ni l'autre. Il donne les deux ici.

La règle procède par échappatoires nommées plutôt que par une permission générale de déclassifier. Une déclaration fixe un ensemble fini \mathcal{X} d'expressions — les échappatoires — dont chacune énonce ce qui est autorisé à sortir : le résultat de la comparaison d'un mot de passe, la somme d'une colonne, le rang d'un enchérisseur. Ces expressions sont closes, \forall e \in \mathcal{X},\ \mathrm{fv}(e) = \emptyset, et évaluées dans l'état initial : une échappatoire ouverte ouvrirait un contournement par substitution, puisque \mathbf{declassify}_{\ell'}(e)[v/x] = \mathbf{declassify}_{\ell'}(e[v/x]) sans que e[v/x] \in \mathcal{X}, et l'attaquant ferait comparer le secret à une valeur de son choix (§4.7). La règle ne s'applique qu'à elles :

Ce que cette règle laisse ouvert est ce qu'une garantie doit fermer : rien n'y interdit qu'une valeur secrète quelconque transite par une échappatoire sous un déguisement, et l'échappatoire libérerait alors bien plus que ce qu'elle nomme. La garantie qui l'écarte s'énonce sur les exécutions plutôt que sur les dérivations.

Le mode de défaillance que cette formulation ferme est celui contre lequel elle a été construite. RMQ 25. C'est la quantification, et elle seule, qui distingue cet énoncé de la non-interférence. Dans l'attaque par blanchiment, on fait transiter par une échappatoire une valeur qu'elle n'était pas censée révéler — comparer un secret non pas au mot de passe attendu mais à une valeur choisie par l'attaquant. Un tel programme échoue à l'énoncé, puisque deux états s'accordant sur la comparaison légitime peuvent différer sur celle-là. S'il tient, le grade de confidentialité reste une garantie de bout en bout malgré l'échappatoire. S'il tombe, il devient contournable par construction, et la déclassification doit être retirée du langage ou confinée à un mécanisme hors du système de types.

Cet énoncé est celui de la divulgation délimitée [43], transposé au régime gradué de ce chapitre. Ce document en reprend la formulation et n'en conduit pas la preuve pour K7PL. Il note en revanche que la voie est celle de la non-interférence graduée (théorème 13), la quantification sur les états s'obtenant par la relation qu'une lecture paramétrique fournit.

Deux conséquences en découlent, dont la seconde est celle qui compte. La première est que \mathcal{R} n'est pas un semi-anneau plat portant des composantes hétéroclites, mais un produit de structures ordonnées dont chacune contribue sa modalité : l'usage sur \mathbb{N}_\infty, la monotonie sur deux points, la confidentialité sur \mathcal{L}. La seconde est que ce dispositif a une duale dont le langage a également besoin. La confidentialité contraint ce qu'une flèche peut lire, et vit donc du côté du contexte, où les coeffets se posent ; l'intégrité contraint ce qu'elle peut écrire, et vit du côté des effets [42]. Les deux côtés de l'adjonction du chapitre 1 portent ainsi les deux propriétés. C'est du côté de l'intégrité que se dit ce que la frontière de confiance du chapitre 5 (§5.5) laisse aujourd'hui indéterminé. Une macro exécutée avant vérification, un import dont l'origine n'est pas attestée, produisent des valeurs de basse intégrité, et rien pour l'instant ne les distingue des autres.

Deux autres instances de ce même procédé achèvent de montrer qu'il est le bon, et toutes deux touchent au coût. Le budget que le chapitre 1 loge dans le grade est une modalité graduée sur un treillis de ressources, où la composition séquentielle et le branchement au pire cas sont deux opérations distinctes — l'une additionne, l'autre prend le maximum — et où !_r A se lit « un A réalisable sous le budget r » [45]. Sa formulation naturelle est celle d'un intérieur gradué, donc d'une comonade, ce qui confirme qu'elle appartient au côté du contexte et non à celui des effets.

Une seconde lecture du même budget existe, dénotationnelle plutôt que modale, et elle vaut d'être signalée pour ce qu'elle prouve de faisabilité. Le coût d'un programme se ramène d'abord par extraction syntaxique à une récurrence, avec un théorème de borne : tout programme source est majoré par la récurrence extraite. Le langage des récurrences reçoit ensuite une sémantique dénotationnelle qui abstrait les types de données [46–47]. Le budget de ce document n'est donc pas seul de son espèce : ce qu'il fait porter au type, cette voie le fait porter à une dénotation, et les deux se rejoignent sur le point qui compte — une borne établie sur la forme du programme plutôt que mesurée sur son exécution.

Le temps est la quatrième : une modalité sur l'ordre linéaire des instants, dont le chapitre 4 (§4.5) tire les calendriers de la couche 2. Quatre structures ordonnées, quatre modalités, un seul procédé — c'est la forme que prend ici la condition de clôture.

Que le grade soit un produit n'est pas un pari de ce document. Composer plusieurs structures de gradation en munissant le produit de l'ordre point par point est une construction standard des systèmes gradués, employée précisément pour combiner des analyses indépendantes en une seule [48]. Les lois de comonade graduée y passent parce que chaque coordonnée les satisfait et que les opérations sont définies coordonnée par coordonnée. Ce qui vaut ici du grade vaut de l'algèbre des effets, dont le chapitre 1 (§1.4) fait un produit par le même geste.

Une conséquence en découle, et elle porte sur ce qu'un développeur peut écrire. Un produit de structures ordonnées est plus large que l'ensemble des grades qu'un programme peut effectivement former, et pour une raison de fond : les coordonnées ne croissent pas au même rythme. La contraction additionne dans le facteur d'usage tout en saturant dans un facteur borné, de sorte qu'un grade dont la première composante s'est incrémentée sans que la seconde ait saturé ne s'obtient ni par usage de variable, ni par contraction [48]. De tels grades existent dans le produit sans être dérivables.

La distinction entre le domaine des grades et ceux que la dérivation habite n'est donc pas un détail de présentation, et deux conséquences pratiques en découlent. Une annotation écrite à la main peut être bien formée sans correspondre à aucun programme, et le vérificateur doit le signaler comme tel plutôt que d'échouer plus loin sur une unification qui n'aboutira pas. Et l'approximation par l'ordre — remplacer un grade par un majorant — est parfois le seul moyen d'atteindre une région du produit, ce qui rattache la question au joint des branchements du chapitre 3 (§3.1) : ce que ce joint sur-approxime, il le fait pour la même raison.

Ce second axe n'est pas gratuit et son bénéfice principal est ailleurs qu'ici. Une fonction monotone d'un type dans lui-même admet un plus petit point fixe dès que ce type possède un plus petit élément et une borne supérieure — un semi-treillis —, et ce point fixe se calcule par itération depuis le plus petit élément. Trois conditions le rendent effectif : le plus petit élément, la décidabilité de l'égalité pour détecter l'arrêt, et la hauteur finie du type pour garantir la terminaison [41]. Cette dernière est la position même de K7PL sur la terminaison (P3), appliquée à un opérateur que le langage ne possède pas encore ; Le §4.5 en tire ce qu'une extension déductive y gagnerait ; il reste à donner ici l'opérateur lui-même.

Sa règle de typage se lit sur le grade et non sur la forme du terme, ce qui est la manière propre à ce langage :

où \to_{\text{mon}} note une flèche dont le grade porte la marque monotone, et où \mathsf{Trellis}_{\text{fin}} rassemble les types satisfaisant les trois conditions nommées ci-dessus. K7PL ne les exprime pas par un mécanisme de classes, qu'il ne possède pas : ce sont des conditions syntaxiques sur la forme du type, décidables à la lecture de sa définition. Un type y appartient s'il est un ensemble fini sur un type d'égalité décidable, ou un produit fini de tels types, ou une somme finie — l'élément neutre étant l'ensemble vide, le joint l'union, et la hauteur le cardinal du plus grand support. Cette restriction est plus étroite que la condition sémantique, et c'est délibéré : elle est vérifiable sans preuve, à la manière dont le §2.3 approche la bonne fondation par un indice de taille.

Le mot « monotone » recouvre dans ce document trois notions qu'il faut tenir distinctes, une quatrième, la marque de monotonie du grade, étant une composante et non une propriété. Une fonction monotone f : S \to_{\text{mon}} S préserve l'ordre de S ; un domaine ordonné est un type S \in \mathsf{Trellis}_{\text{fin}}, muni d'un ordre et des conditions ci-dessus ; un ensemble de règles monotone est une méta-propriété du programme, qui garantit qu'ajouter un fait n'en retire aucun. Elles se composent — les règles d'un programme monotone se compilent en fonctions monotones sur un domaine ordonné, dont le point fixe est défini — sans se confondre.

C'est le troisième critère de terminaison de ce document, et les trois sont de même nature. RMQ 26. Trois critères, un seul geste. La garantie se lit sur le type, jamais sur la forme du terme. Le pli dépendamment typé termine parce que son type porte un indice décroissant, la coinduction produit parce que son type porte une taille, et fix termine parce que son type est de hauteur finie. Aucun des trois n'inspecte la syntaxe du terme, ce qui est la position que P3 énonce. S'il tient, l'opérateur n'affaiblit pas la garantie de terminaison de la couche 3 mais l'étend à un schéma qu'elle n'atteignait pas ; s'il tombe, le point fixe déductif doit sortir du langage, et l'extension déductive du chapitre 4 avec lui.

Deux réserves bornent l'énoncé. La borne h est celle du type et non du calcul : une itération peut converger bien plus tôt, et rien n'est dit du nombre d'itérations effectif — une borne serrée relèverait de la strate des obligations, comme toute proposition sur un résultat. Et l'hypothèse de monotonie porte plus qu'il n'y paraît : une règle qui conclut de l'absence d'un fait — la négation stratifiée du chapitre 7 (§7.3) — n'est pas monotone, et le point fixe qui la contiendrait ne relèverait pas de cet énoncé.

Cette monotonie a une conséquence directe, la garantie de gradualité statique : si \Delta' \sqsubseteq \Delta et e' \sqsubseteq e, toute dérivation de \Delta \vdash e : A se projette en une dérivation de \Delta' \vdash e' : A' pour un type A' \sqsubseteq A. L'esquisse en est immédiate : la dérivation de \Delta \vdash e : A s'obtient par composition et tensorisation de règles élémentaires. Remplacer, dans cette composition, chaque prémisse par une prémisse \sqsubseteq-inférieure produit, par monotonie, une composition encore valide, dont le type résultant ne peut qu'avoir perdu en précision. Dégrader une entrée ne casse donc jamais le typage : elle ne fait que dégrader, de façon prévisible, ce qui en dépend.

Cette structure ne referme pas seule la construction du chapitre : le §2.5 en montre l'origine. L'ordre de précision modal \text{Unr} \sqsubseteq \text{Aff} \sqsubseteq \text{Lin} du chapitre 1 est la restriction de \sqsubseteq à la seule dimension des modalités d'usage. Une modalité est d'autant plus précise qu'elle contraint davantage l'usage. Ce n'est pas le sous-typage \preccurlyeq des règles de typage, qui descend sur l'usage (!\omega\,A <: {!}1\,A) : les deux ordres sont opposés sur cette seule composante, ce que la table 10 donne composante par composante. Les foncteurs d'inclusion du §2.2 réalisent catégoriquement cette stratification sur les fragments eux-mêmes. Types dépendants, raffinements, sessions et existentielles, dont le chapitre 3 tire parti de cette même relation sur chacune de leurs propres dimensions, ne feront qu'instancier, pour un artefact syntaxique après l'autre, ce même treillis.