FLIN infère les types. Vous écrivez count = 0 et le compilateur sait que c'est un entier. Vous écrivez name = "Juste" et le compilateur sait que c'est du texte. Vous écrivez items = [] et le compilateur lui assigne un type polymorphe qui sera résolu quand vous ajouterez un premier élément. L'algorithme derrière tout cela est Hindley-Milner -- un système d'inférence de types inventé indépendamment par Roger Hindley en 1969 et Robin Milner en 1978, et utilisé sous une forme ou une autre par Haskell, OCaml, F#, Rust (partiellement) et maintenant FLIN.
Implémenter Hindley-Milner dans un langage personnalisé est l'une de ces tâches qui paraissent intimidantes et se révèlent étonnamment compactes. Le moteur d'inférence de types complet de FLIN -- unification, substitution, généralisation, instanciation et polymorphisme let -- tient en environ 200 lignes de Rust. Il a été construit en une seule session de 25 minutes. Et il fonctionne.
Cet article explique l'algorithme, parcourt l'implémentation et montre comment FLIN l'utilise pour détecter les erreurs au moment de la compilation sans imposer aux développeurs d'écrire des annotations de type.
Pourquoi l'inférence de types compte
FLIN est conçu pour les développeurs qui veulent construire des applications rapidement. Les forcer à écrire des types explicites sur chaque variable, chaque paramètre de fonction, chaque valeur de retour les ralentirait et ajouterait du bruit visuel à un langage par ailleurs propre.
Mais FLIN est aussi un langage compilé avec de la vérification statique de types. Le compilateur a besoin de connaître le type de chaque expression pour vérifier que les opérations sont valides (on ne peut pas additionner un booléen et une chaîne), pour générer le bon bytecode (l'addition d'entiers et l'addition de flottants sont des instructions différentes), et pour détecter les erreurs avant que le programme ne s'exécute.
L'inférence de types résout cette tension. Le développeur écrit du code sans annotation. Le compilateur détermine les types. Si les types sont incohérents -- si vous essayez d'utiliser la même variable à la fois comme entier et comme chaîne -- le compilateur rapporte une erreur à l'emplacement exact où l'incohérence apparaît.
La question est : quel algorithme d'inférence de types ? L'approche la plus simple, l'inférence locale, regarde juste le côté droit de chaque assignation et infère le type à partir du littéral. count = 0 est int parce que 0 est un entier. Cela fonctionne pour les cas simples mais échoue pour les structures de données génériques : quel est le type de items = [] ? L'inférence locale ne peut pas répondre parce que le côté droit ne contient aucune information de type.
Hindley-Milner gère cela en introduisant des variables de type -- des placeholders pour des types inconnus qui sont résolus par un processus appelé unification. Il supporte aussi le polymorphisme let, qui permet à une variable d'avoir des types différents dans des contextes différents. Ces deux fonctionnalités en font le bon choix pour FLIN.
Les trois piliers : unification, substitution et variables de type
La fondation de Hindley-Milner est la variable de type. Quand le compilateur rencontre une expression dont le type n'est pas immédiatement connu, il crée une variable de type fraîche -- un placeholder comme ?T0, ?T1, ?T2. Ces variables ne sont pas des types en elles-mêmes ; ce sont des promesses qu'un type sera déterminé plus tard.
Les variables de type sont résolues par l'unification. L'unification prend deux types et tente de les rendre égaux en liant des variables de type. Par exemple :
- Unifier
?T0avecint-- lier?T0àint. Succès. - Unifier
intavecint-- déjà égaux. Succès. - Unifier
intavectext-- impossible de les rendre égaux. Erreur. - Unifier
[?T0]avec[int]-- récursivement unifier?T0avecint. Lier?T0àint. Succès.
L'algorithme d'unification dans FLIN :
rustpub fn unify(&mut self, a: &FlinType, b: &FlinType) -> Result<(), TypeError> {
let a = self.substitute(a);
let b = self.substitute(b);
match (&a, &b) {
// Mêmes types concrets
(FlinType::Int, FlinType::Int) => Ok(()),
(FlinType::Text, FlinType::Text) => Ok(()),
(FlinType::Bool, FlinType::Bool) => Ok(()),
(FlinType::Float, FlinType::Float) => Ok(()),
(FlinType::Time, FlinType::Time) => Ok(()),
(FlinType::Money, FlinType::Money) => Ok(()),
// Variable de type : la lier
(FlinType::TypeVar(id), other) | (other, FlinType::TypeVar(id)) => {
if let FlinType::TypeVar(other_id) = other {
if id == other_id {
return Ok(()); // Même variable, rien à faire
}
}
// Vérification d'occurrence : prévenir les types infinis
if self.occurs_in(*id, other) {
return Err(TypeError::InfiniteType(*id, other.clone()));
}
self.substitutions.insert(*id, other.clone());
Ok(())
}
// Types structurels : récursion
(FlinType::List(inner_a), FlinType::List(inner_b)) => {
self.unify(inner_a, inner_b)
}
(FlinType::Optional(inner_a), FlinType::Optional(inner_b)) => {
self.unify(inner_a, inner_b)
}
// Int peut être coercé vers Float
(FlinType::Int, FlinType::Float) | (FlinType::Float, FlinType::Int) => Ok(()),
// Incompatibilité
_ => Err(TypeError::Mismatch(a.clone(), b.clone())),
}
}Deux choses méritent attention. Premièrement, chaque appel à unify commence par appliquer les substitutions existantes aux deux types. Si ?T0 était précédemment lié à int, alors unifier ?T0 avec text unifie en réalité int avec text, ce qui produit correctement une erreur. Sans cette étape de substitution, l'algorithme accepterait silencieusement des liaisons contradictoires.
Deuxièmement, la vérification d'occurrence : avant de lier une variable de type ?T0 à un type, nous vérifions que ?T0 n'apparaît pas à l'intérieur de ce type. Sans cette vérification, unifier ?T0 avec [?T0] créerait un type infini ([[[[[...]]]]]), ce qui ferait boucler l'algorithme de substitution indéfiniment. La vérification d'occurrence prévient cela en rejetant la liaison avec une erreur claire.
Substitution : appliquer ce que nous savons
La substitution remplace les variables de type par leurs types liés dans une expression :
rustpub fn substitute(&self, ty: &FlinType) -> FlinType {
match ty {
FlinType::TypeVar(id) => {
if let Some(bound) = self.substitutions.get(id) {
self.substitute(bound) // Suivre la chaîne
} else {
ty.clone()
}
}
FlinType::List(inner) => {
FlinType::List(Box::new(self.substitute(inner)))
}
FlinType::Optional(inner) => {
FlinType::Optional(Box::new(self.substitute(inner)))
}
_ => ty.clone(),
}
}L'appel récursif dans le cas TypeVar est important. Les substitutions peuvent s'enchaîner : ?T0 -> ?T1 -> int. La méthode substitute suit la chaîne jusqu'à atteindre un type concret ou une variable non liée. C'est parfois appelé "compression de chemin" par analogie avec les structures union-find, bien que notre implémentation ne compresse pas réellement le chemin en place.
Polymorphisme let : la fonctionnalité clé
L'inférence de types locale ne peut pas gérer ce code :
flinx = []
y = x
z = xQuel est le type de x ? C'est une liste vide, mais une liste de quoi ? Avec l'inférence locale, il faudrait choisir un type ou rapporter une erreur. Avec Hindley-Milner, on peut donner à x un type polymorphe : "pour tout type a, x a le type [a]". Puis y et z reçoivent chacun leur propre copie fraîche de ce type polymorphe, et ils peuvent indépendamment être contraints à des types d'éléments différents.
C'est le polymorphisme let : les variables liées par let (ou dans le cas de FLIN, par =) peuvent avoir des types polymorphes qui sont instanciés fraîchement à chaque site d'utilisation.
L'implémentation a deux parties : la généralisation et l'instanciation.
La généralisation se produit quand une variable est définie. Après avoir inféré le type de l'initialiseur, le vérificateur de types trouve toutes les variables de type qui sont libres (non liées par une portée englobante) et quantifie sur elles :
rustpub fn generalize(&self, ty: &FlinType) -> TypeScheme {
let env_free_vars = self.env.free_type_vars();
let ty_free_vars = self.free_vars_in(ty);
// Variables libres dans le type mais pas dans l'environnement
let quantified: Vec<TypeVar> = ty_free_vars
.difference(&env_free_vars)
.cloned()
.collect();
if quantified.is_empty() {
TypeScheme::mono(ty.clone())
} else {
TypeScheme::poly(quantified, ty.clone())
}
}Pour x = [], le type inféré est [?T0] où ?T0 est libre. La généralisation produit le schéma de type forall T0. [T0] -- pour tout type T0, x est une liste de T0.
L'instanciation se produit quand une variable est utilisée. Le vérificateur de types remplace chaque variable quantifiée par une variable de type fraîche :
rustpub fn instantiate(&mut self, scheme: &TypeScheme) -> FlinType {
if scheme.is_mono() {
return scheme.inner().clone();
}
let mut substitution = HashMap::new();
for var in &scheme.vars {
substitution.insert(*var, FlinType::TypeVar(self.fresh_var()));
}
self.apply_scheme_substitution(&scheme.ty, &substitution)
}Quand le vérificateur de types rencontre y = x, il cherche le schéma de type de x (forall T0. [T0]), l'instancie avec une variable fraîche ([?T5]) et l'assigne à y. Quand il rencontre z = x, il instancie à nouveau avec une variable fraîche différente ([?T6]). Maintenant y et z peuvent indépendamment être contraints à des types d'éléments de liste différents.
Le struct TypeScheme
Le struct TypeScheme fait le pont entre les types monomorphes (un seul type concret) et les types polymorphes (un type avec des variables quantifiées) :
rustpub struct TypeScheme {
pub vars: Vec<TypeVar>, // Variables liées (quantifiées)
pub ty: FlinType, // L'expression de type sous-jacente
}
impl TypeScheme {
pub fn mono(ty: FlinType) -> Self {
TypeScheme { vars: Vec::new(), ty }
}
pub fn poly(vars: Vec<TypeVar>, ty: FlinType) -> Self {
TypeScheme { vars, ty }
}
pub fn is_mono(&self) -> bool {
self.vars.is_empty()
}
pub fn inner(&self) -> &FlinType {
&self.ty
}
}L'environnement de types stocke des valeurs TypeScheme, pas des valeurs FlinType. Cela signifie que chaque liaison de variable peut potentiellement être polymorphe, même si la plupart seront monomorphes en pratique (leur liste vars sera vide). La représentation uniforme simplifie la logique de recherche : vous instanciez toujours, mais pour les schémas monomorphes, l'instanciation est un no-op.
Vérification de types des instructions
Le vérificateur de types parcourt l'AST instruction par instruction, maintenant un environnement de types qui associe les noms de variables aux schémas de types :
Pour les déclarations de variables, il infère le type de l'initialiseur, l'unifie avec toute annotation explicite, généralise le résultat et stocke le schéma dans l'environnement.
Pour les déclarations d'entités, il enregistre le type de chaque champ dans l'environnement, créant une nouvelle portée pour l'entité. Les types de champs d'entité sont toujours explicites (la syntaxe FLIN exige des annotations de type sur les champs), donc aucune inférence n'est nécessaire -- mais le vérificateur de types vérifie quand même que les valeurs par défaut sont compatibles avec leurs types annotés. Si un champ est count: int = "hello", le vérificateur de types rapporte une incompatibilité.
Pour les instructions if, il vérifie que la condition a le type bool et vérifie récursivement les deux branches. Pour les boucles for, il vérifie que l'itérable a un type liste et lie la variable de boucle au type d'élément de la liste.
Pour les instructions save et delete, il vérifie que l'expression a un type entité. Vous ne pouvez pas faire save 42 -- le vérificateur de types l'attrape.
Vérification de types des expressions
La vérification de types des expressions est là où l'unification fait la plupart de son travail :
Expressions binaires : le vérificateur de types infère les types des deux opérandes, puis vérifie que l'opérateur est valide pour ces types. + fonctionne sur int + int (produisant int), float + float (produisant float), int + float (produisant float, avec coercition), et text + text (produisant text, pour la concaténation). Toute autre combinaison est une erreur de type.
Accès aux membres : user.name requiert que user ait un type entité et que l'entité ait un champ nommé name. Le type résultant est le type du champ.
Appels de méthode : items.count() requiert que items ait un type liste. La méthode count est une méthode intégrée qui retourne int. Le vérificateur de types a une table de méthodes intégrées pour chaque type.
Accès temporel : user.name @ yesterday requiert que user.name ait un type et que yesterday soit une expression temporelle. Le type résultant est le même que le type de l'opérande -- l'accès temporel change le quand, pas le quoi.
Expressions ask : ask "requête" requiert que la requête soit une expression text. Le type résultant est text -- la réponse de l'IA.
Construction d'entité : User { name: "Juste", age: 30 } requiert que User soit une entité définie, que tous les champs requis soient fournis, et que la valeur de chaque champ corresponde au type déclaré du champ. Le type résultant est Entity("User").
Assembler le tout : un exemple complet
Considérez ce programme FLIN :
flinentity User {
name: text
age: int
}
user = User { name: "Thales", age: 28 }
greeting = "Bonjour, " + user.nameLe vérificateur de types le traite étape par étape :
- Déclaration d'entité. Enregistrer
Useravec les champsname: textetage: int.
- Variable
user. Inférer le type deUser { name: "Thales", age: 28 }. L'entitéUserexiste. Le champnameattendtext, et"Thales"esttext-- correspondance. Le champageattendint, et28estint-- correspondance. Tous les champs fournis. Type résultant :Entity("User"). Généraliser :userest monomorphe (Entity("User")).
- Variable
greeting. Inférer le type de"Bonjour, " + user.name. Opérande gauche :"Bonjour, "esttext. Opérande droit :user.name-- chercheruser(typeEntity("User")), accéder au champname(typetext). Opérateur+surtext + textproduittext. Type résultant :text. Généraliser :greetingest monomorphe (text).
Aucune annotation de type écrite. Aucune erreur. Chaque expression a un type connu. Le générateur de code peut maintenant émettre le bytecode correct : StoreGlobal pour les variables, CreateEntity pour la construction d'entité, GetField pour l'accès aux membres, StringConcat pour l'addition de texte.
Messages d'erreur
Un moteur d'inférence de types n'est aussi bon que ses messages d'erreur. Quand l'unification échoue, le vérificateur de types doit expliquer ce qui a mal tourné en des termes que le développeur comprend, pas en termes de variables de type et de chaînes de substitution.
Le vérificateur de types de FLIN produit des erreurs comme :
- "Incompatibilité de types : attendu
int, trouvétextdans l'assignation àcount" - "Impossible d'appliquer l'opérateur
+aux typesbooletint" - "L'entité
Usern'a pas de champ nomméemail" - "Impossible de sauvegarder une valeur de type
int--saverequiert un type entité"
Chaque erreur inclut le span de l'expression problématique, pour que le développeur sache exactement où regarder. Les messages d'erreur utilisent les noms de types FLIN (text, int, bool) plutôt que les représentations internes (FlinType::Text, TypeVar(3)), parce que le développeur a écrit du code FLIN, pas du code Rust.
La session en chiffres
La session 8 -- la session qui a implémenté Hindley-Milner -- a pris environ 25 minutes et a produit ces résultats :
| Métrique | Valeur |
|---|---|
| Durée | ~25 minutes |
| Lignes ajoutées | ~320 (120 types, 200 vérificateur) |
| Nouveaux tests | 17 |
| Total tests qui passent | 193 |
| Complétion du système de types | 100 % |
| Complétion de la partie 1 | 92 % |
Du polymorphisme Hindley-Milner complet en environ 200 lignes de logique de vérification de types. Ce n'est pas parce que l'algorithme est trivial -- c'est parce que le système de types de Rust fait une grande partie du travail. L'enum FlinType avec TypeVar transporte le polymorphisme dans la structure de données elle-même. Le pattern matching rend les cas d'unification exhaustifs et clairs. La map de substitution HashMap<u32, FlinType> est tout l'état dont l'algorithme a besoin.
Limitations et travail futur
L'implémentation Hindley-Milner actuelle de FLIN a des limitations délibérées :
Pas de types de kind supérieur. FLIN ne peut pas exprimer "un conteneur de n'importe quel type" comme concept de première classe. Les listes sont paramétrées, mais la paramétrisation est intégrée dans la variante FlinType::List, pas exprimée à travers un mécanisme général de constructeur de types. C'est suffisant pour le domaine de FLIN -- les applications web n'ont typiquement pas besoin de polymorphisme de kind supérieur.
Pas de polymorphisme de lignes. Les entités ont des ensembles de champs fixes. Vous ne pouvez pas écrire une fonction qui accepte "toute entité avec un champ name". C'est une simplification délibérée : les entités FLIN sont plus proches des tables de base de données que des types structurels, et les tables de base de données ont des schémas fixes.
Restriction de valeur. La généralisation ne se produit qu'aux liaisons let (déclarations de variables), pas à des positions d'expression arbitraires. C'est la restriction de valeur standard de ML, qui prévient le polymorphisme incorrect en présence d'état mutable. Puisque les variables FLIN sont mutables, la restriction de valeur est nécessaire pour la correction.
Ces limitations sont des compromis, pas des oublis. Chacune garde le système de types plus simple, l'implémentation plus petite et les messages d'erreur plus clairs. Si la base d'utilisateurs de FLIN grandit au point où les types de kind supérieur ou le polymorphisme de lignes sont nécessaires, la fondation est là -- le noyau Hindley-Milner est extensible.
Ce qui a suivi
Avec le vérificateur de types complet, chaque expression dans l'AST a un type connu. La phase suivante -- la génération de code -- parcourt l'AST typé et émet des instructions bytecode pour la machine virtuelle de FLIN. La session 9 a implémenté le générateur de code entier en 30 minutes : 75 opcodes, un pool de constantes avec déduplication, le patching de sauts pour les conditionnelles et les boucles, et un désassembleur pour le débogage.
Le générateur de code est couvert dans le prochain lot d'articles. Mais d'abord, reconnaissons ce que nous avons accompli dans les neuf premières sessions : un lexer, un parser Pratt, un AST, un vérificateur de types Hindley-Milner et un générateur de code. Un pipeline de compilation complet du code source au bytecode. Construit par un CEO à Abidjan et une IA CTO, en environ quatre heures de temps de session total.
Ce pipeline a compilé l'exemple du compteur -- count = 0 / <button click={count++}>{count}</button> -- en 26 octets de bytecode. Vingt-six octets qui représentent une interface utilisateur réactive, à état, avec gestion d'événements et mises à jour DOM automatiques. De quatre lignes de FLIN à vingt-six octets d'instructions. C'est ce que fait un compilateur.
Ceci est la partie 15 de la série "Comment nous avons construit FLIN", qui documente comment un CEO à Abidjan et une IA CTO ont construit un langage de programmation en partant de zéro.
Navigation de la série : - [11] Session 1 : mise en place du projet et 42 mots-clés - [12] Construire un lexer en partant de zéro en Rust - [13] Pratt Parsing : comment FLIN lit votre code - [14] L'arbre syntaxique abstrait : la représentation interne de FLIN - [15] L'inférence de types Hindley-Milner dans un langage personnalisé (vous êtes ici)