3.2. Les contraintes de valeur🔗

Deux filiations gouvernent cette section. Les types liquides de Rondon, Kawaguchi et Jhala établissent qu'un raffinement reste décidable si sa vérification est déléguée à un solveur plutôt qu'intégrée à l'unification — c'est le partage que K7PL reprend entre le narrowing et la Phase 5 (chapitre 6). Le tracé exact de ce partage est assumé pour ce qu'il est : il ne suit d'aucune nécessité logique. Certaines contraintes de taille se vérifieraient par narrowing au prix d'annotations supplémentaires, certaines existentielles se délégueraient au solveur. Le critère retenu est empirique et gouverné par P3 — reste au narrowing ce dont le coût de vérification est prévisible sans recherche, part au solveur ce qui exige une exploration dont la durée ne se borne pas syntaxiquement.

Les types dépendants pragmatiques de Xi et Pfenning montrent qu'une fraction utile de la dépendance — tailles, indices — se vérifie sans les coûts d'annotation de la dépendance générale. C'est cette fraction, et non le calcul des constructions, que ce chapitre adopte. Deux langages récents confirment que l'économie n'est pas propre à K7PL : Futhark obtient la mise à jour en place d'un tableau immuable par une simple analyse d'unicité, Dex élimine les vérifications de bornes par des indices typés sans recourir à la dépendance complète.

Une contrainte de valeur ne dit rien de la modalité d'une ressource ; elle restreint ce que son contenu peut légitimement être — une taille, un intervalle, un état, un protocole, une dimension physique.

Un cas est à écarter de cette liste, où il figurait naguère sans y appartenir : la confidentialité. Le niveau de sécurité d'une valeur n'est pas une contrainte sur son contenu mais sur son usage — qui peut la lire, et ce qu'il peut en dériver —, et le chapitre 2 (§2.4) le loge donc là où il appartient, dans le grade, comme modalité sur un treillis de niveaux. Le distinguer importe, parce qu'un raffinement se décharge au cas par cas quand un grade se propage par les règles.

Ces contraintes, en apparence hétérogènes, ne se distinguent que par le moyen de leur vérification. Certaines s'établissent directement dans le système de types, sans engager de calcul supplémentaire. D'autres délèguent la preuve à un solveur externe. D'autres enfin ne sont pas des propriétés fixes mais des états qui évoluent, et se vérifient comme des automates. Dans tous les cas, une fois établie, la contrainte disparaît du binaire — c'est la même exigence d'effacement que le chapitre 2 imposait à la modalité (P3), appliquée cette fois à la valeur.

Cet effacement n'est cependant pas gratuit. Abel, Danielsson et Eriksson [2] établissent que la correction d'une fonction d'extraction n'est acquise que pour une classe restreinte de modalités. Sur les programmes ouverts, trois réserves conjointes s'y ajoutent : toutes les variables du contexte effaçables, contexte cohérent, et filtrage interdit sur un paquet dont le témoin est effacé. Lever cette dernière suffit à perdre la canonicité, contre-exemple à l'appui. K7PL adopte ces trois réserves comme conditions de sa propre garantie d'effacement, la troisième prenant la forme d'une restriction sur les existentielles (§3.3). Une voie alternative existe, qui encode l'effacement comme distinction de phase et en tire la conservativité sur la théorie des types sous-jacente [24]. Ce document ne l'emprunte pas, mais elle reste disponible si la restriction du §3.3 se révélait trop coûteuse.

Les contraintes de taille en sont l'illustration la plus directe : Vector(n, T) n'introduit aucun mécanisme propre, elle réutilise l'isomorphisme \text{Hom}(\text{Fin}(n),T) \cong \text{Vec}(n,T) établi au chapitre 2 (§2.4). Cet isomorphisme fixe la sémantique du type, non sa représentation machine : celle-ci relève de l'abaissement (chapitre 6, §6.1), et le choix d'empaqueter une représentation d'exécution efficace avec des invariants effaçables reste explicite — c'est à cette condition que la complexité de la structure résultante demeure prévisible, comme P3 l'exige [25]. L'accès (arr i) porte la contrainte 0 \le i < n ; le compilateur en prouve la validité, ou la transforme en Result(T, OutOfBounds) lorsque la preuve échoue — jamais une vérification dynamique silencieuse. Les dimensions physiques (types SI, Velocity = Length / Time) suivent le même principe par des paramètres fantômes : la contrainte est vérifiée puis intégralement effacée, sans laisser au binaire final la moindre trace de son unité.

Lorsque la contrainte ne se laisse pas encoder aussi directement, K7PL délègue. Un type de raffinement {x : T | p} engage une obligation de preuve résolue par le solveur SMT du chapitre 6, sur des théories dédiées : K7PL.Map pour les cartes finies, K7PL.SI pour les dimensions physiques, K7PL.Age pour l'ordre linéaire des destinations. Des lemmes explicites la guident si nécessaire. Lorsque le prédicat porte sur les valeurs internes à une structure — les éléments d'une carte, les composantes d'un CRDT composé —, ces lemmes ne sont pas facultatifs. Ils sont les principes d'induction profonde du type porteur [23], sans lesquels l'obligation reste indéchargeable quel que soit le solveur. Le sous-typage entre deux raffinements de même support n'est alors rien d'autre qu'une implication logique entre leurs prédicats, vérifiée automatiquement.

Une famille de contraintes s'ajoute à celles-ci lorsque le prédicat porte sur une ressource consommée plutôt que sur une valeur : l'annotation de potentiel, portée par la déclaration d'un type de données et indiquant comment le potentiel s'y répartit. Elle n'est pas un ornement. L'analyse automatique de ressources échange l'automatisation contre la flexibilité — les techniques entièrement automatiques se restreignent à des familles de bornes contraintes, les bornes dépendantes des valeurs relevant sinon de preuves écrites à la main —, et c'est l'annotation de potentiel qui permet de sortir de ce dilemme [26]. K7PL ne peut donc revendiquer simultanément l'automatisation complète des bornes de coût, trois familles de bornes hétérogènes selon la couche, et l'absence de toute annotation de ressource. L'inférence des bornes n'est automatique que sur les familles que le solveur atteint, et une borne dépendante d'une valeur demande une annotation.

Ces conditions se laissent ramener à une règle unique, et c'est sous cette forme que K7PL la retient : aucun éliminateur ne discrimine sur un argument appartenant à la phase de compilation — ni projection existentielle sur un témoin effacé, ni match sur un paramètre de typestate, ni cond sur un paramètre fantôme. La règle n'est pas une précaution locale : c'est ce qui rend la non-interférence du §1.4 démontrable plutôt que postulée. Sa nécessité est établie. Sans elle, un terme construit par élimination sur une donnée effacée cesse de se réduire vers une valeur canonique [27] ; et les cadres qui autorisent davantage doivent restreindre ailleurs, en cantonnant certains constructeurs au code de compilation [28]. La question symétrique — quand une valeur effacée peut-elle être ressuscitée ? — reçoit la réponse habituelle : seulement sur un type stable au sens de [27], c'est-à-dire un type dont un habitant se reconstruit depuis sa version effacée.

Son statut, en revanche, est moins bon que son contenu, et se corrige ici. Elle est ici une règle à faire respecter, vérifiée cas par cas — trois interdictions énumérées et une quatrième à ajouter le jour où un quatrième éliminateur apparaîtra. Une distinction de phase synthétique fait mieux : la phase y étant une proposition du contexte, la discrimination n'est pas interdite, elle est inexprimable, et la conservativité dans les deux phases s'en déduit au lieu d'être vérifiée [24]. La règle devient alors une conséquence de l'encodage plutôt qu'une condition de bord, ce qui est la transformation que ce document a opérée ailleurs pour l'hygiène — passer d'une discipline appliquée à une propriété du type. Le contenu ne change pas ; ce qui change est qu'il n'y aura plus de liste à tenir à jour.

Une troisième famille de contraintes ne porte pas sur une valeur figée mais sur son évolution. Le typestate est un paramètre de type qui suit une grammaire d'états — File(Open), File(Closed) — chaque transition validée par unification de ce paramètre, sans le moindre coût à l'exécution. La règle ci-dessus en fixe le prix, et il faut l'écrire : un typestate se vérifie, il ne se filtre pas. Un programme qui aurait besoin de brancher à l'exécution sur l'état d'un fichier doit porter un tag explicite, lequel appartient alors à la phase d'exécution et cesse d'être gratuit. C'est le seul point où l'effacement de K7PL restreint ce que le développeur peut écrire, et il le restreint dans le sens de ce que le paragraphe précédent revendique. Un type de session n'en est que la version distribuée : le même automate, sauf que ses transitions sont déclenchées par l'échange de messages entre deux extrémités plutôt que par des appels locaux.

Figure 5 :

Un protocole de session comme automate à états

Un protocole vu comme la suite de ses états, avant que le §3.2 ne le relise comme un échange entre deux extrémités.

L'automate représenté est celui du protocole Send(Int, Recv(Bool, End)).

Chaque extrémité d'un canal de session est une ressource linéaire de \Delta (chapitre 2, §2.2), et le protocole qu'elle porte s'accompagne de son dual — à un Send(T,P) correspond nécessairement un Recv(T,P^⊥) du côté opposé. Cette dualité n'est ni une hypothèse ni même une définition : elle est une conséquence, et c'est ce qui permet à ce chapitre de n'ajouter aucun constructeur de type.

La grammaire ci-dessus — \mathsf{Send}, \mathsf{Recv}, \mathsf{select}, \mathsf{offer}, \mathsf{End} — est une syntaxe de surface. L'élaboration la traduit en emboîtements d'implications linéaires, seule construction que le chapitre 2 ait eu à fournir (§2.1). La dualité tombe alors du retournement des arguments : \tau_1 \multimap \tau_2 est dual de \tau_2 \multimap \tau_1, le constructeur de fonction linéaire étant dual de lui-même. Émettre et recevoir sont les deux lectures d'une même flèche, selon le côté où l'on se tient. Il n'y a pas d'involution à définir, pas de squelette à munir de duaux, pas de théorème d'adéquation à démontrer entre une involution syntaxique et une négation catégorique. C'est la démarche minimale attestée pour ajouter des sessions à un \lambda-calcul linéaire, où l'on obtient absence de blocage et progrès global du seul système de types linéaire, par des preuves plus courtes que celles des systèmes à constructeurs dédiés [29]. Un bénéfice second, et il n'est pas mince : l'ambiante C n'a besoin d'aucune négation. Elle reste une catégorie monoïdale symétrique close, cadre dans lequel les exponentielles du §2.2 sont parfaitement définies — la structure sans négation de la logique linéaire multiplicative supporte ! et ?, la relation de De Morgan y étant remplacée par la force tensorielle [30].

Le motif est celui que la condition de clôture du chapitre 1 (§1.4) impose : toute extension doit se projeter sur les composantes existantes plutôt que d'en ajouter. Faire des cinq formes de protocole autant de constructeurs primitifs y contreviendrait — cinq primitives, une définition de dualité, une structure catégorique et un théorème là où \multimap, présent depuis le §2.1, suffit.

Une dette naît de ce choix : la préservation des types par cet encodage est établie dans la littérature pour la grammaire de GV, non pour celle de K7PL. Ce document la revendique et ne la démontre pas.

Deux hypothèses tombent avec cet encodage. La première voulait que C, restreinte aux objets utilisés dans les protocoles, fût \ast-autonome — formulation dont le quantificateur portait au surplus sur les charges utiles, que la dualité ne touche pas, K7PL n'ayant pas de délégation de session. La seconde, qui l'avait remplacée, munissait un squelette fini de duaux choisis. Ni l'une ni l'autre n'a plus d'objet : il n'y a pas de squelette, seulement des flèches.

Cette absence de délégation situe par ailleurs K7PL sur le clivage qui sépare les interprétations de la logique linéaire en types de session. Les présentations classique et intuitionniste ont engendré des courants distincts, dont la comparaison formelle est récente, et le trait qui les départage est le principe de localité — imposé par les interprétations intuitionnistes, non par les classiques [31]. Aucun message de K7PL ne transportant d'extrémité de canal, la localité y est satisfaite par construction : le langage se range du côté intuitionniste, où la dualité n'a pas besoin de la forme classique la plus forte.

Reste un comportement que le chapitre 4 pratique et que ce chapitre ne type pas. Une session peut être abandonnée — le Timeout et le circuit breaker du §4.5 le font —, et la grammaire ci-dessus décrit des protocoles qui ne peuvent pas échouer. L'écart se comble sans quitter le cadre : la logique linéaire classique s'étend conservativement de deux modalités duales capturant une (co)monade additive, ce qui accueille non-déterminisme et abandon en garantissant globalement progrès et fidélité [32]. Le résultat est cité pour la forme de l'extension, non pour son cadre : K7PL travaille en logique linéaire intuitionniste, et le chapitre 4 (§4.5) dit pourquoi — c'est de là que vient la localité des noms partagés, qu'il revendique comme structurelle. Transporter l'extension au cadre intuitionniste est donc une obligation et non un acquis, et elle est consignée comme telle. K7PL ne conduit pas cette extension ; il la nomme, et son encodage dans \multimap ne s'y oppose pas.

Une limite du régime asynchrone doit être connue avant d'être rencontrée. Le sous-typage de K7PL est modal — il relie les trois fragments d'usage (chapitre 1) — et ne porte pas sur les protocoles. S'il devait un jour s'y étendre, il buterait sur un résultat établi : la vérification du sous-typage asynchrone est indécidable, et les algorithmes déployés dans les outils existants sont corrects sans être complets [33]. C'est une frontière du langage, non un défaut du présent document ; elle est énoncée ici pour que le choix du régime asynchrone soit fait en connaissance de ce qu'il ferme.

Un dernier point doit être fixé, que ce document laissait ouvert et dont la preuve d'absence de blocage dépend : les sessions de K7PL sont asynchrones. Un Send dépose dans une boîte aux lettres et rend la main ; un Recv bloque sur une boîte vide, non sur l'absence d'un correspondant prêt. Ce régime est celui que le chapitre 4 met en œuvre par anneaux verrou-libres (§4.5), et le déclarer ici évite que le chapitre 3 raisonne en rendez-vous pendant que le chapitre 4 transporte par messages. L'écart entre les deux régimes n'est pas une nuance d'implémentation : c'est un écart sémantique, dont le franchissement demande un encodage explicite par protocoles d'appel-retour [34]. Le graphe des sessions ainsi obtenu doit être acyclique ; c'est cette même construction, réalisée matériellement, qu'un runtime L1 vérifie par comparaison d'un simple tag d'état à l'exécution (chapitre 4).

Un protocole se déclare en couche 1 comme un arbre de transitions, dont le compilateur dérive automatiquement la dualité client/serveur (1) :

{defprotocol oauth-flow
  (send Credentials
    (offer (:success (recv Token end))
           (:denied end)))}

Un raccourci est à écarter avant l'énoncé, car il commande la forme que celui-ci prend. Les sessions étant asynchrones (§3.2), un Recv ne bloque pas sur l'absence d'un Send correspondant mais sur une boîte aux lettres vide. La dualité garantit qu'un Send est typé de l'autre côté, elle ne garantit pas qu'il ait été émis, l'émetteur pouvant être lui-même bloqué sur un troisième canal. Un contre-exemple d'une ligne suffit à le montrer, et explique du même coup pourquoi l'acyclicité est nécessaire : trois participants deux à deux duaux, chacun attendant du suivant avant d'émettre vers le précédent, forment un cycle qui bloque [9]. La dualité établit la bonne formation des protocoles, jamais la progression, et c'est pourquoi elle assure la fidélité de session et la sûreté de communication mais non l'absence de blocage mutuel [35]. L'hypothèse d'acyclicité fait ici tout le travail, et figure à ce titre dans l'énoncé plutôt que dans la preuve.

Deux appuis techniques valent d'être nommés avant la preuve, puisqu'ils bornent ce qu'elle suppose. Le premier est que l'élimination des coupures y porte sur le seul fragment multiplicatif de la logique linéaire — celui qu'engendrent les types de session — et non sur la logique linéaire intuitionniste entière, dont la recherche de preuve certifiée est un problème à part entière [36]. Son admissibilité n'a d'ailleurs pas à être supposée, puisqu'elle s'obtient indépendamment de la théorie des modes dans les cadres qui paramètrent produits et implications — ordonnés, linéaires, affines, cartésiens — par une telle théorie [6]. Le second est que la preuve procède par coinduction sur le dépliage plutôt que par induction sur la structure, un graphe se laissant mieux traiter comme structure coinductive dès le départ, les algorithmes de graphes n'étant pas structurellement récursifs dans leurs présentations usuelles [37].

Deux graphes sont en jeu, et les confondre serait l'erreur à ne pas commettre. RMQ 36. Le câblage est donné, l'attente se déplie. Traiter le second comme le premier reviendrait à lire un objet coinductif par induction. Le graphe de câblage du §4.3 est donné en entier à la compilation : fini, statique, il se traite inductivement, et le tri topologique de la Phase 1.5 en établit l'acyclicité une fois pour toutes. Le graphe d'attente à l'exécution se déplie au fil des activations et n'est jamais donné. L'acyclicité du premier n'implique donc pas mécaniquement celle du second, et c'est pourquoi l'énoncé porte sur les états atteignables et non sur le câblage.

L'absence de blocage mutuel est donc une propriété de compilation, et non une promesse conditionnelle : le tri topologique de la Phase 1.5 la décide, et aucun mécanisme d'exécution — détection de cycle, temporisation globale — n'a à la surveiller. S'il tombe, la garantie retombe sur le Timeout, c'est-à-dire sur une détection à l'exécution, ce qui la ferait sortir du système de types et rentrer dans le coût.

Figure 6 :

Le même protocole, lu comme échange dual entre deux extrémités

Le protocole précédent vu depuis ses deux bouts, pour montrer que la dualité ne complète pas le type mais le relit.

Quand une contrainte de valeur échoue, K7PL distingue trois régimes plutôt qu'un seul. Un état illégal viole un invariant que le système de types rejette avant même la génération de code — l'accès hors bornes prouvé impossible en est un cas. Un état indésirable atteint l'exécution mais reste un échec ordinaire, représenté par un Result. Un état transitoire, enfin, n'est l'échec de rien : une condition temporaire — un tampon plein — résorbable par un gestionnaire, modélisée comme un effet algébrique (chapitre 2, §2.3) plutôt que confondue avec une erreur définitive. La théorie des roues instancie ce premier régime pour l'arithmétique : une opération invalide (0/0) ne lève pas d'exception mais produit une singularité — \bot, \infty, \circ, \delta, constructeurs d'un type algébrique Wheel<T> distinct du flottant IEEE 754 sous-jacent, dont la conversion reste explicite dans les deux sens. Ces singularités se propagent algébriquement à travers les opérations vectorielles, sans jamais introduire de branchement ; si \bot atteint la sortie d'une fonction, le résultat est simplement l'absence de donnée — un échec prouvé plutôt que silencieux.

Exigence vérifiée par test différentiel, non démontrée. Elle absorbe cinq dispositions : l'élision est bornée par une version de schéma, la purge par la rotation du journal, le bourrage par la règle d'abaissement, le NaN par la proposition 26, l'ordre des segments par la réallocation (mremap). Toutes disent la même chose.

L'overflow entier suit la même logique par couche : rejet statique en couche 3, où le solveur SMT doit prouver que l'opération reste dans les bornes ; Result(T, OverflowError) en couche 2, où l'origine des valeurs n'est plus toujours statiquement bornée. Dans les deux cas, aucun dépassement silencieux n'est jamais toléré.