Type Annotations

Sommaire

Référence unique des annotations de type. La syntaxe, les positions, les types acceptés, les coercions et les deux moments de vérification (statique et à la frontière d'exécution) sont regroupés ici ; chaque page de langage garde le détail de son domaine et est reliée en fin de section.

Une annotation est un contrat, pas un commentaire. Deux conséquences tiennent toute la sémantique :

  • si une annotation est présente, elle est vérifiée — pas de mode décoratif, pas de drapeau pour l'éteindre ;
  • si elle est absente, le code reste dynamique comme avant — on ne paie pas pour ce qu'on n'écrit pas.

Si on écrit du code, c'est pas pour décorer.

Optionnel, mais pas facultatif

L'annotation est optionnelle : le langage n'en exige aucune, et son absence laisse le code dans la zone dynamique classique (dispatch par tag à chaque opération). Ce qui n'existe pas, c'est le milieu — une annotation posée est un contrat, jamais une intention. Il n'y a pas de type Any : la porte de sortie du typage, c'est l'absence d'annotation, pas un type qui dit « n'importe quoi ».

Positions annotables

L'annotation prend la forme nom: type. Cinq positions la portent :

Position Syntaxe Vérifiée
Paramètre (fonction/lambda) (x: int) => { ... } à l'entrée de la fonction
Type de retour (x): int => { ... }, m(self): int => { ... } à chaque appel (voir plus bas)
Champ de struct struct P { x: int; y: int } au constructeur et à chaque écriture
Champ de payload d'union union U { A(x: int) } à la construction de la variante
Paramètre de type union Option[T] { Some(value: T); None } substitué à l'usage (x: Option[int])

Un paramètre de type ([T]) n'est pas une annotation de valeur mais une variable de type : il se fixe au moment où le type paramétré est utilisé comme annotation (x: Option[int] fixe T := int).

Les variables locales ne portent pas d'annotation explicite : leur type vient de l'inférence, pas d'une déclaration. Au niveau d'un statement, a: int n'est pas une position annotable et est refusé au parse (E100).

Types acceptés

Famille Exemple Coercion Détail
Primitifs int float str bool None oui, tour numérique (sauf str) TYPES
Nominaux struct, enum, union, trait non, sous-typage STRUCTURES, ENUMS, UNIONS
Union de types int \| str, Point \| None non FUNCTIONS
Composites list[T] set[T] dict[K, V] tuple[...] littéral covariant / valeur invariante ; tuple covariant FUNCTIONS
Génériques nominaux Option[int], Result[T, E] non, substitution paramétrique UNIONS
Types de fonctions (int) -> int, (int, str) -> bool sans objet (callable + arité) FUNCTIONS

Les composites sont vérifiés conteneur et paramètres, récursivement : list[list[int]] contrôle la liste, puis chaque sous-liste, puis chaque int. Les génériques nominaux vérifient l'appartenance à l'union et substituent l'argument de type dans le payload (Option[int] exige un Option dont la charge satisfait int). Un type de fonction décrit un callback : types des paramètres entre parenthèses, retour après la flèche ->, absorbante à droite ((int) -> int | None retourne int | None ; parenthéser pour une union de fonctions).

Un nom de type inconnu, ou un composite dont un paramètre n'est pas modélisé, laisse l'annotation inerte : on ne rejette jamais sur une preuve qu'on n'a pas.

Coercion : la tour numérique, et rien d'autre

Une seule coercion existe, sur les primitifs, le long de la tour numérique bool <: int <: float : un int (ou bool) fourni à un slot float est stocké en float, un bool fourni à int devient int. str n'est jamais coercé (seule une chaîne satisfait str). Cette coercion agit aux positions à contrat primitif simple : paramètre, champ de struct, champ de payload, type de retour.

Partout ailleurs, la valeur passe inchangée ou est refusée :

  • un nominal est accepté par sous-typage, jamais transformé ;
  • une union ne coerce pas — elle ne saurait pas vers quel membre ;
  • un composite déjà typé est invariant (muter à travers l'alias serait incohérent) ; seul un littéral fraîchement construit est covariant.

Une annotation primitive est un contrat sur ce qui franchit la porte, pas sur le fait qu'on frappe. Annoter x: int ne rend pas x obligatoire : un paramètre annoté omis vaut None.

Deux moments de vérification

Un contrat se contrôle à deux instants, selon qu'il est décidable à la compilation ou seulement à l'exécution.

Statique — l'erreur E300

Quand l'incompatibilité est prouvable (valeur littérale, ou type inféré concret), c'est une erreur de compilation. Le linter émet E300. Sites couverts :

  • défaut de paramètre vs annotation ((x: int = "no")) ;
  • défaut de champ de struct vs annotation (struct P { x: int = "no" }) ;
  • type de retour déclaré vs type produit par le corps ((): int => { "no" }) ;
  • argument vs paramètre au site d'appel d'une fonction à liaison prouvablement unique (f("no")), positionnel ou par mot-clé ;
  • argument vs champ au constructeur d'un struct (P(1, "no")) ;
  • charge d'une variante d'union à champ concret (Shape.Circle(1.5) sur Circle(radius: int)).

La vérification des appels est monomorphe : elle ne s'applique qu'aux cibles statiquement uniques (assignées une seule fois, jamais réassignées, jamais passées comme valeur ni masquées). C'est un choix de soundness — zéro faux positif — pas une limite d'ambition : résoudre une cible réassignable exigerait une analyse de flot d'ordre supérieur (k-CFA, Shivers 1991) dont le coût n'est pas justifié. Détail : lint — E300.

À la frontière — le contrôle d'entrée

Ce qui n'est pas prouvable à la compilation (une valeur issue d'un appel, d'une frontière Python) est contrôlé au moment où elle entre dans une zone typée : à l'entrée de la fonction, au constructeur, à la construction de la variante, et à l'écriture d'un champ annoté. Un tag faux lève TypeError. Une fois passé, la zone typée est sûre par construction.

Cette dernière position est ce qui rend la garantie transportable. Un champ vérifié au seul constructeur décrit le passé de la valeur, pas son état : p.x = "oops" sur x: int passait, donc aucun invariant ne survivait à la ligne suivante et le champ pouvait contenir un int là où sa déclaration annonçait un float, selon le chemin qui l'avait rempli.

La frontière n'est pas une politesse : un tag NaN-box incorrect est une faute mémoire, pas un comportement dynamique tolérable. On vérifie là, ou on ne vérifie jamais.

Le cas des types de fonctions

Un callback fait exception : une frontière ne peut pas établir qu'une fonction respecte sa signature — c'est indécidable sans l'appeler. Le contrat se répartit donc sur trois temps :

  • statiquement, une lambda littérale passée à un slot fonction est comparée composant par composant (arité exacte, paramètres contravariants, retour covariant) ;
  • à l'entrée, la valeur reçue doit être callable et son arité doit accepter l'arité déclarée (un callable Python passe sur sa seule callabilité, son arité n'étant pas introspectable) ;
  • au retour de chaque appel, côté appelant, la valeur rendue est vérifiée contre le type de retour déclaré — un callback qui ment sur son retour est arrêté là où le mensonge devient observable.

Outillage

  • Le formatter préserve les annotations et normalise leur espacement interne ((cb: (int,int)->bool) → (cb: (int, int) -> bool)) : le round-trip ne supprime jamais un contrat. Voir format.
  • Le linter émet E300 sur les incompatibilités prouvables, et exploite les annotations au-delà : un paramètre ou un champ typé fournit le type du scrutinee d'un match, ce qui affine le contrôle d'exhaustivité (I103). Voir lint.

Détails par sujet