Sous-typage décidable des types existentiels en Julia

Dispatch multiple et sous-typage en Julia

Julia repose sur le dispatch multiple : la méthode exécutée est sélectionnée à l'exécution en fonction des types de tous les arguments. Ce dispatch implique d'évaluer des relations de sous-typage au runtime — par exemple Vector{Int64} <: AbstractVector{Number}.

Julia supporte les types existentiels use-site : une annotation comme Vector{T} where T <: Integer introduit une variable de type bornée. C'est expressif — et c'est la source du problème.

Indécidabilité du sous-typage original

Belyakova et al. prouvent que le système de types Julia antérieur à leur correctif est indécidable. La preuve consiste à réduire l'implication de contraintes dans FP≤ — un calcul de sous-typage dont l'indécidabilité est connue — au sous-typage Julia.

Le mécanisme d'encodage : les interactions entre plusieurs variables existentielles bornées permettent de simuler des contraintes de premier ordre arbitraires. En pratique, le compilateur Julia pouvait diverger sur certaines annotations de types sans aucun signal d'erreur.

Stratification : la correction

La solution n'est pas de supprimer les types existentiels — ce qui casserait l'essentiel de l'écosystème. C'est une stratification : séparer le système en deux couches.

• Types de signatures de méthode — apparaissent dans les déclarations f(x::T) where T <: .... Variables existentielles bornées autorisées.
• Types de valeurs — types des valeurs concrètes à l'exécution. Variance use-site restreinte : les imbrications arbitraires de variables existentielles y sont interdites.

Cette séparation bloque l'encodage de FP≤ : les contraintes de premier ordre ne peuvent plus s'exprimer dans les types de valeurs. La décidabilité est restaurée par une mesure structurelle qui décroît strictement à chaque étape du proof search.

Algorithme : proof search par backtracking

L'algorithme procède en deux phases pour chaque sous-problème de sous-typage :

• Collecte de contraintes — chaque variable existentielle accumule des bornes inférieures et supérieures au fil du proof search.
• Résolution — les contraintes collectées sont vérifiées pour cohérence. Si elles sont satisfaisables, la relation de sous-typage est établie.

Le backtracking intervient quand une branche échoue. La stratification garantit que la profondeur de récursion est bornée — la complexité reste exponentielle dans le pire cas, mais bornée.

Validation empirique

Les auteurs ont analysé 9 335 packages du registre Julia officiel, soit 16,5 millions de lignes de code. Parmi l'ensemble des annotations de type de ce corpus, exactement 4 ne sont pas conformes au système stratifié — et les 4 ont été identifiées comme des bugs par leurs auteurs respectifs. La rétrocompatibilité est quasi-totale.

Échange avec Julia Belyakova

Pour vérifier notre compréhension du papier, j'ai voulu exécuter le prototype de référence — implémenté en Racket et publié avec l'article. Une dépendance manquait dans les instructions : racket-langserver n'était pas documenté. J'ai ouvert une issue GitHub, puis contacté Julia Belyakova directement par email pour poser la question qui me bloquait davantage : dans quelle mesure le prototype reflète-t-il ce qui tourne dans le compilateur Julia réel ?

Sa réponse est utile à garder en tête pour lire le papier : le système formel et l'implémentation compilateur divergent sur plusieurs points d'optimisation. L'article décrit la sémantique cible — ce que le sous-typage devraitcalculer — pas l'implémentation production, qui s'en écarte pour des raisons de performance. Ce gap n'est pas formalisé dans le papier, ce qui rend les claims sur la correction de l'implémentation réelle difficiles à évaluer. Elle a aussi recommandé les travaux de Francesco Zappa Nardelli sur la sémantique opérationnelle de Julia pour contextualiser.

Limites de l'article

• Complétude partielle — la décidabilité est prouvée, mais la complétude du proof search (trouver une preuve quand elle existe) n'est établie que sous certaines hypothèses sur les types d'entrée.
• Complexité non bornée en pratique — la validation empirique montre la rétrocompatibilité, pas les performances. La complexité exponentielle dans le pire cas n'est pas discutée sur des cas réels.
• Fragment formalisé — le modèle n'inclut pas les types Union ni les traits de Julia. La décidabilité du système complet reste ouverte.
• Distance prototype / compilateur — non formellement caractérisée. Le prototype Racket est une référence sémantique, pas une preuve d'implémentation.