K7PL

1.6. Table des glyphes🔗

La table 6 complète la dualité glyphe/alias construite au chapitre 5 (§5.2) : chaque ligne est une seule macro de la bibliothèque standard, montrée sous ses deux noms, strictement équivalents au niveau de l'AST. La colonne du point de code n'est pas un choix de typographie : elle est la forme normative du glyphe. Un glyphe se déclare par son code positionnel Unicode, de sorte que la table reste vérifiable sans dépendre de la fonte qui l'affiche, et que la cinquième règle d'admission — aucun couple de glyphes ne se ressemble à l'œil — porte sur des objets identifiés plutôt que sur des dessins. Le glyphe n'est pas une primitive du noyau — l'arbitrage qui le fixe est écrit au chapitre 5, et cette table en est la table des noms, non celle des constructions.

Tableau 6 :

Glyphes de la bibliothèque standard de couche 3 et leurs alias textuels

Glyphe

Point de code

Alias

Sémantique

+

U+002B

add

Somme élément par élément

-

U+002D

sub

Différence élément par élément

×

U+00D7

mul

Produit élément par élément

÷

U+00F7

div

Quotient élément par élément

⌊

U+230A

min

Minimum élément par élément

⌈

U+2308

max

Maximum élément par élément

≠

U+2260

neq

Inégalité stricte

⊏

U+228F

select

Sélection par indices

⊔

U+2294

group

Regroupement par clé

⍋

U+234B

grade-up

Indices du tri ascendant

⍒

U+2352

grade-dn

Indices du tri descendant

↕

U+2195

windows

Découpage en fenêtres glissantes

∾

U+223E

join

Concaténation verticale

⊣

U+22A3

left-id

Retourne l'argument de gauche

⊢

U+22A2

right-id

Retourne l'argument de droite

⥊

U+294A

reshape

Change la forme d'un tableau

∧

U+2227

and

Conjonction bit-à-bit

∨

U+2228

or

Disjonction bit-à-bit

¬

U+00AC

not

Négation bit-à-bit

=

U+003D

eq

Égalité structurée

<

U+003C

lt

Comparaison stricte

>

U+003E

gt

Comparaison stricte

≤

U+2264

le

Comparaison large

≥

U+2265

ge

Comparaison large

⍟

U+235F

repeat

Applique une fonction n fois

⊘

U+2298

compose

Composition de fonctions

↢

U+21A2

bind-left

Applique f puis g

↣

U+21A3

bind-right

Applique g puis f

Deux lignes de cette table portent une décision de notation qu'il faut écrire, car elle s'écarte de la source dont le reste s'inspire. Les glyphes de liaison empruntés à BQN étaient ⟜ et ⊸ ; le second est l'implication linéaire de Girard, employée dans tout ce document au sens logique, et un signe ne peut pas porter deux travaux. Ce n'est pas le signe logique qui cède. Les deux glyphes de liaison ont alors été changés ensemble, et non le seul fautif : bind-left et bind-right sont une paire, et une paire dont un membre garde sa forme d'emprunt quand l'autre reçoit une forme improvisée n'est plus une paire. Le couple retenu, ↢ et ↣, est image l'un de l'autre, chacun tient en un point de code, et la pointe désigne le côté où l'argument s'attache. Ce qui se perd est la familiarité pour un lecteur venu de BQN, et c'est le seul coût — un argument de familiarité, non de devinabilité.

Trois signes de ce document servent à plusieurs endroits, et la séparation qui les rend sans danger doit être dite plutôt que supposée. Le tourniquet ⊢ marque le jugement dans la notation mathématique, l'identité droite dans la notation de couche 3, et le groupement non capturant dans celle des R-expressions. Trois emplois, trois contextes que rien ne mélange — les mathématiques ne s'écrivent pas dans un programme, et une R-expression a ses propres délimiteurs. Le sigil # marque l'évaluation à la compilation et rien d'autre ; il est réservé à cet usage, et toute intention ultérieure de l'employer pour autre chose doit céder, l'usage écrit primant l'usage projeté. Le point . enfin sert la projection et la décimale, séparés par la position. Aucune de ces trois coexistences n'est un accident, et chacune tient à ce que le langage sépare lui-même les contextes ; c'est la même règle qui gouverne ses dix espaces de noms.

Reste la règle qui exige qu'aucun couple de glyphes ne se ressemble à l'œil. Elle était jusqu'ici un jugement humain, et elle a désormais un instrument : la norme de sécurité d'Unicode définit la confusabilité de deux chaînes par l'égalité de leur squelette, transformation qui remplace chaque caractère par le prototype que lui associe une donnée normative et versionnée [50]. Deux glyphes sont donc admissibles ensemble si et seulement si leurs squelettes diffèrent, ce qui est décidable et vérifiable par machine plutôt qu'apprécié.

L'instrument appliqué à cette table rend un résultat en deux temps, et le second est plus utile que le premier. Aucun couple des vingt-huit ne partage un squelette : la règle est satisfaite à l'intérieur du jeu. Mais quatre de ces glyphes ont un confusable hors du jeu, et deux d'entre eux visent une cible qui est un caractère d'identifiant légal — le signe de multiplication se confond avec la lettre x, la disjonction logique avec la lettre v. Les deux autres, une étoile cerclée et une rune, sont sans portée pratique.

Ce que ce constat corrige n'est pas le jeu de glyphes mais la portée de la règle. Elle regardait à l'intérieur du jeu quand le danger est au-dehors : un programme peut porter x là où son auteur voulait le signe de multiplication, et rien ne le signalerait, l'un et l'autre étant licites à cette position. La règle se réénonce donc en deux clauses — aucun couple du jeu ne partage un squelette, et tout glyphe dont le squelette est un caractère d'identifiant est déclaré comme tel. La seconde clause est celle qui manquait, et c'est l'instrument qui l'a fait apparaître.

Une réserve de transport doit accompagner cet emprunt. Cette norme vise la sécurité des identifiants et l'usurpation d'adresses, non la conception d'un jeu de glyphes~; sa donnée est calibrée sur ce que confondent des lecteurs de langues diverses devant une chaîne isolée, non sur ce que confond un programmeur devant une ligne de code. Elle est employée ici parce qu'elle est le seul instrument normatif disponible, et non parce que son cadre serait le nôtre.

La table 6 couvre les opérations de calcul de couche 3 ; les R-expressions (chapitre 4, §4.2) portent leur propre vocabulaire glyphique, organisé selon la même hiérarchie de complexité qui détermine l'automate vers lequel chaque niveau s'abaisse.

Tableau 7 :

Glyphes des R-expressions, par niveau de complexité

Catégorie

Glyphe

Sémantique

Atomes

ℓ

Littéral textuel

Atomes

⊙

Classe de caractères

Atomes

℘

Classe de propriété Unicode

Quantification

◇ / ◆ / ◈

Quantificateur avide / paresseux / possessif

Composition

⊕ / ⊞

Séquence / alternance

Composition

⊢

Groupement non capturant

Capture

⋈

Groupe de capture

Assertions

⊲ / ⊳

Début / fin de chaîne

Assertions

⊴ / ⊵

Frontière / non-frontière de mot

Assertions

⇒ / ⇸

Anticipation positive / négative

Assertions

⇐ / ⇷

Rétrospection positive / négative

Avancé

⟲

Référence arrière

Avancé

∞

Récursion

Contrôle

↯

Transformation de contrôle (échec, coupure, engagement...)

Approximatif

≈ / ≈ᵘ

Correspondance floue (distance de Levenshtein)

Binaire

ß

Filtrage binaire sub-octet

Méta

⟦⟧ / ⟨⟩

Annotation / composition nommée

Références
  1. MUNCH-MACCAGNONI, Guillaume. Resource Polymorphism [en ligne]. 2018, p. 1–62 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.48550/ARXIV.1803.02796
  2. LORENZEN, Anton; WHITE, Leo; DOLAN, Stephen; EISENBERG, Richard A.; LINDLEY, Sam. Oxidizing OCaml with Modal Memory Management. Proceedings of the ACM on Programming Languages [en ligne]. 2024, vol. 8, no. ICFP, p. 485–514 [visité le 2025-05-08]. Disp. à l’adr. DOI: 10.1145/3674642
  3. ATKEY, Robert. Syntax and Semantics of Quantitative Type Theory. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science [en ligne]. Oxford United Kingdom: ACM, 2018, p. 56–65 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3209108.3209189
  4. MOON, Benjamin; EADES III, Harley; ORCHARD, Dominic. Graded Modal Dependent Type Theory. Programming Languages and Systems [en ligne]. Cham: Springer International Publishing, 2021, vol. 12648, p. 462–490 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-030-72019-3_17
  5. CHOUDHURY, Pritam; EADES, Harley; WEIRICH, Stephanie. A Dependent Dependency Calculus. Programming Languages and Systems [en ligne]. Cham: Springer International Publishing, 2022, vol. 13240, p. 403–430 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-030-99336-8_15
  6. LIU, Yiyun; CHAN, Jonathan; WEIRICH, Stephanie. Consistency of a Dependent Calculus of Indistinguishability. Proceedings of the ACM on Programming Languages [en ligne]. 2025, vol. 9, no. POPL, p. 183–209 [visité le 2025-05-19]. Disp. à l’adr. DOI: 10.1145/3704843
  7. DORÉ, Maximilian. Dependent Multiplicities in Dependent Linear Type Theory [en ligne]. 2025, p. 1–13 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3747531
  8. ORCHARD, Dominic; LIEPELT, Vilem-Benjamin; EADES III, Harley. Quantitative Program Reasoning with Graded Modal Types. Proceedings of the ACM on Programming Languages [en ligne]. 2019, vol. 3, no. ICFP, p. 1–30 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3341714
  9. BRODAL, Gerth Stølting; OKASAKI, Chris. Optimal Purely Functional Priority Queues. Journal of Functional Programming [en ligne]. 1996, vol. 6, no. 6, p. 839–857 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S095679680000201X
  10. APPEL, Andrew W. A Critique of Standard ML. Journal of Functional Programming [en ligne]. 1993, vol. 3, no. 4, p. 391–429 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S0956796800000836
  11. CHONG, Stephen. Required Information Release. In: 2010 23rd IEEE Computer Security Foundations Symposium [en ligne]. Edinburgh, United Kingdom: IEEE, 2010, p. 215–227 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1109/CSF.2010.22
  12. RAJANI, Vineet; COLEMAN, Alex; KANABAR, Hrutvik. A Graded Modal Approach to Relaxed Semantic Declassification. In: CSF [en ligne]. Santa Cruz, CA, USA: IEEE, 2025, p. 268–283. Disp. à l’adr. DOI: 10.1109/CSF64896.2025.00032
  13. OKASAKI, Chris. Purely Functional Data Structures [en ligne]. s. d.. Disp. à l’adr. DOI: 10.1017/CBO9780511530104
  14. BROWN, James A. A Development of APL2 Syntax. IBM Journal of Research and Development [en ligne]. 1985, vol. 29, no. 1, p. 37–48 [visité le 2025-04-18]. Disp. à l’adr. DOI: 10.1147/rd.291.0037
  15. HUDAK, Paul; HUGHES, John; PEYTON JONES, Simon; WADLER, Philip. A History of Haskell: Being Lazy with Class. In: Proceedings of the Third ACM SIGPLAN Conference on History of Programming Languages [en ligne]. San Diego California: ACM, 2007 [visité le 2025-05-07]. Disp. à l’adr. DOI: 10.1145/1238844.1238856
  16. REYNOLDS, John C. GEDANKEN - a Simple Typeless Language Based on the Principle of Completeness and the Reference Concept. Communications of the ACM [en ligne]. 1970, vol. 13, no. 5, p. 308–319 [visité le 2025-04-18]. Disp. à l’adr. DOI: 10.1145/362349.362364
  17. PRATT, Vaughan R. Transition and Cancellation in Concurrency and Branching Time. Mathematical Structures in Computer Science [en ligne]. 2003, vol. 13, no. 4, p. 485–529 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1017/S0960129503004031
  18. CASTELLAN, Simon; CLAIRAMBAULT, Pierre. The Geometry of Causality: Multi-Token Geometry of Interaction and Its Causal Unfolding. Proceedings of the ACM on Programming Languages [en ligne]. 2023, vol. 7, p. 689–717 [visité le 2025-05-07]. Disp. à l’adr. DOI: 10.1145/3571217
  19. LIEPELT, Vilem; MARSHALL, Danielle; ORCHARD, Dominic. Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types. Proceedings of the ACM on Programming Languages [en ligne]. 2026, vol. 10, p. 721–750 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.1145/3828697
  20. GORDON, Colin S. Polymorphic Iterable Sequential Effect Systems. ACM Transactions on Programming Languages and Systems [en ligne]. 2021, vol. 43, no. 1, p. 1–79 [visité le 2025-07-02]. Disp. à l’adr. DOI: 10.1145/3450272
  21. MATACHE, Cristina; LINDLEY, Sam; MOSS, Sean; STATON, Sam; WU, Nicolas; YANG, Zhixuan. Scoped Effects, Scoped Operations, and Parameterized Algebraic Theories. ACM Transactions on Programming Languages and Systems [en ligne]. 2025, vol. 47, no. 2, p. 1–33 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3731678
  22. VAN DER REST, Cas; BACH, Casper. Hefty Algebras: Modular Elaboration of Higher-Order Effects. Journal of Functional Programming [en ligne]. 2025, vol. 35, p. e25 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.1017/S0956796825100142
  23. LINDLEY, Sam; MATACHE, Cristina; MOSS, Sean; STATON, Sam; WU, Nicolas; YANG, Zhixuan. Scoped Effects as Parameterized Algebraic Theories. In: WEIRICH, Stephanie (éd.). Programming Languages and Systems [en ligne]. Cham: Springer Nature Switzerland, 2024, vol. 14576, p. 3–21 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.1007/978-3-031-57262-3_1
  24. DE VILHENA, Paulo Emílio; POTTIER, François. A Separation Logic for Effect Handlers. Proceedings of the ACM on Programming Languages [en ligne]. 2021, vol. 5, p. 1–28 [visité le 2025-05-07]. Disp. à l’adr. DOI: 10.1145/3434314
  25. JAKE FECHER. Algebraic Effects, Ownership, and Borrowing [en ligne]. Ante, 2024. Disp. à l’adr. https://antelang.org/
  26. GABOARDI, Marco; KATSUMATA, Shin-ya; ORCHARD, Dominic; BREUVART, Flavien; UUSTALU, Tarmo. Combining Effects and Coeffects via Grading. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming [en ligne]. Nara Japan: ACM, 2016, p. 476–489 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/2951913.2951939
  27. LI, Yongming; PEDRYCZ, Witold. Fuzzy Finite Automata and Fuzzy Regular Expressions with Membership Values in Lattice-Ordered Monoids. Fuzzy Sets and Systems [en ligne]. 2005, vol. 156, no. 1, p. 68–92 [visité le 2026-08-19]. Disp. à l’adr. DOI: 10.1016/j.fss.2005.04.004
  28. MANNUCCI, Mirco A.; THURO, Corey. Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities. arXiv.org [en ligne]. 2025, vol. abs/2512.6952, p. 1–20 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.48550/arXiv.2512.06952
  29. CAPORASO, Salvatore; COVINO, Emanuele; PANI, Giovanni. A Predicative Approach to the Classification Problem. Journal of Functional Programming [en ligne]. 2001, vol. 11, no. 1, p. 95–116 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S0956796800003853
  30. ATKEY, Robert. Polynomial Time and Dependent Types. Proceedings of the ACM on Programming Languages [en ligne]. 2024, vol. 8, no. POPL, p. 2288–2317 [visité le 2025-06-05]. Disp. à l’adr. DOI: 10.1145/3632918
  31. GHICA, Dan R.; SMITH, Alex I. Bounded Linear Types in a Resource Semiring. In: SHAO, Zhong (éd.). European Symposium on Programming [en ligne]. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, vol. 8410, p. 331–350 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-642-54833-8_18
  32. TORCZON, Cassia; SUÁREZ ACEVEDO, Emmanuel; AGRAWAL, Shubh; VELEZ-GINORIO, Joey; WEIRICH, Stephanie. Effects and Coeffects in Call-by-Push-Value. Proceedings of the ACM on Programming Languages [en ligne]. 2024, vol. 8, no. OOPSLA2, p. 1108–1134 [visité le 2025-05-08]. Disp. à l’adr. DOI: 10.1145/3689750
  33. KURA, Satoshi; GABOARDI, Marco; SEKIYAMA, Taro; UNNO, Hiroshi. A Category-Theoretic Framework for Dependent Effect Systems [en ligne]. 2026, p. 1–75 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-032-22720-1_15
  34. ÇIÇEK, E.; GABOARDI, M.; GARG, D. Cost-Analysis: How Do Monads and Comonads Differ?. 2016.
  35. AZEVEDO DE AMORIM, P. H. The Compositional Essence of Effectful Cost Analyses: Categorical Foundations and Fibered Logical Relations. Univ. of Bath, s. d..
  36. SAINATI, Daniel; CUTLER, Joseph W.; PIERCE, Benjamin C.; WEIRICH, Stephanie. Typing Strictness. Proc. ACM Program. Lang. [en ligne]. 2026, vol. 10, no. POPL, p. 413–443 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3776657
  37. DOWNEN, Paul; ARIOLA, Zena M. Classical (Co)Recursion: Mechanics. Journal of Functional Programming [en ligne]. 2023, vol. 33, p. e4 [visité le 2025-05-19]. Disp. à l’adr. DOI: 10.1017/S0956796822000168
  38. CHIRIMAR, Jawahar; GUNTER, Carl A.; RIECKE, Jon G. Reference Counting as a Computational Interpretation of Linear Logic. Journal of Functional Programming [en ligne]. 1996, vol. 6, no. 2, p. 195–244 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S0956796800001660
  39. SERGEY, Ilya; VYTINIOTIS, Dimitrios; JONES, Simon L. Peyton; BREITNER, Joachim. Modular, Higher Order Cardinality Analysis in Theory and Practice. Journal of Functional Programming [en ligne]. 2017, vol. 27, p. e11 [visité le 2025-05-19]. Disp. à l’adr. DOI: 10.1017/S0956796817000016
  40. PÉDROT, Pierre-Marie; TABAREAU, Nicolas. The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–28 [visité le 2025-05-05]. Disp. à l’adr. DOI: 10.1145/3371126
  41. BRACHTHÄUSER, Jonathan Immanuel; SCHUSTER, Philipp; OSTERMANN, Klaus. Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–30 [visité le 2025-05-06]. Disp. à l’adr. DOI: 10.1145/3428194
  42. SCHUSTER, Philipp; BRACHTHÄUSER, Jonathan Immanuel; OSTERMANN, Klaus. Compiling Effect Handlers in Capability-Passing Style. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–28 [visité le 2025-04-30]. Disp. à l’adr. DOI: 10.1145/3408975
  43. VÁKÁR, Matthijs. A Framework for Dependent Types and Effects [en ligne]. Version 2. 2015 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.48550/ARXIV.1512.08009
  44. NIU, Yue; STERLING, Jonathan; GRODIN, Harrison; HARPER, Robert. A Cost-Aware Logical Framework. Proc. ACM Program. Lang. [en ligne]. 2021, vol. 6, no. POPL, p. 1–31 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3498670
  45. KAVVOS, G. A. The Many Worlds of Modal λ-Calculi: I. Curry-howard for Necessity, Possibility and Time [en ligne]. 2016, p. 1–34 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.48550/ARXIV.1605.08106
  46. ALTENKIRCH, Thorsten; MORRIS, Peter. Indexed Containers. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science [en ligne]. Los Angeles, California, USA: IEEE, 2009, p. 277–285 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1109/LICS.2009.33
  47. OLIVEIRA VALE, Arthur; MELLIÈS, Paul-André; SHAO, Zhong; KOENIG, Jérémie; STEFANESCO, Léo. Layered and Object-Based Game Semantics. In: Proceedings of the ACM on Programming Languages [en ligne]. 2022, vol. 6, no. POPL, p. 1–32 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3498703
  48. CHOUDHURY, Vikraman; KRISHNASWAMI, Neel. Recovering Purity with Comonads and Capabilities. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–28 [visité le 2025-04-30]. Disp. à l’adr. DOI: 10.1145/3408993
  49. COLCOMBET, Thomas; PETRISAN, Daniela. Automata in the Category of Glued Vector Spaces. LIPIcs, Volume 83, MFCS 2017 [en ligne]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017, vol. 83, p. 52:1-52:14 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.4230/LIPICS.MFCS.2017.52
  50. The Unicode® Standard. Version 17.0. Unicode, Inc., 2025.