Xalg / Fix / Les types dépendants : quand le type calcule
Navigation
Apprendre
Recettes
Référence
Comprendre
Bonnes pratiques
En pratique
Explications

Les types dépendants : quand le type calcule

Dans la plupart des langages, un type décrit une forme : « une liste d'entiers », « une paire de chaînes ». Il ne sait rien des valeurs. Une liste de 3 éléments et une liste de 300 ont le même type — et c'est à toi de te souvenir laquelle fait quoi.

Les types dépendants (RDT, Relational Dependent Types) cassent cette frontière : le type peut porter une valeur comme indice. Pas « un vecteur d'entiers », mais « un vecteur d'entiers de longueur 3 ». Et cette longueur, Fix sait la calculer.

L'idée en une ligne

Le type n'est plus seulement une étiquette. C'est une donnée que le moteur manipule — au même titre que tes faits.

has_type(v1, vec(int, 3)).
has_type(v2, vec(int, 5)).

vec(int, 3) est un type, mais 3 dedans est une vraie valeur. Rien de spécial : c'est un terme composé ordinaire, et Fix le traite comme tout le reste.

Le moteur calcule l'indice

Concatène deux vecteurs : quelle est la longueur du résultat ? Tu ne la donnes pas — tu écris la relation entre les longueurs, et Fix la résout.

result_type(A, B, vec(T, N)) :-
    has_type(A, vec(T, M)),
    has_type(B, vec(T, K)),
    add(M, K, N).
?- result_type(v1, v2, T).
T = vec(int, 8)

add(M, K, N) n'est pas un calcul impératif : c'est la relation « M + K = N ». Fix lie M à 3, K à 5, et en déduit N = 8. La longueur du type a été calculée par inférence — avant la moindre exécution.

Le type qui refuse

C'est là que ça devient utile. Multiplier deux matrices n'a de sens que si les dimensions intérieures coïncident. Exprime cette contrainte dans le type, et le produit mal formé ne type tout simplement pas.

has_type(a, matrix(float, 2, 3)).
has_type(b, matrix(float, 3, 4)).
has_type(c, matrix(float, 5, 4)).

matmul(A, B, matrix(T, R, C)) :-
    has_type(A, matrix(T, R, M)),
    has_type(B, matrix(T, M, C)).

Le M partagé fait tout le travail : la colonne de gauche est la ligne de droite, par unification. Donne-lui des dimensions qui collent, il calcule le type du résultat ; donne-lui un cas absurde, il n'y a aucune solution.

?- matmul(a, b, R).
R = matrix(float, 2, 4)

?- matmul(a, c, R).
false.        % 3 ≠ 5 : pas de produit

Le bug classique — « j'ai inversé deux dimensions » — est attrapé par la structure du type, pas par un test que tu aurais pu oublier d'écrire.

Programme réel : examples/dependent-types/02-matrix.fix — et six autres exemples dans le même répertoire (unités, typestate, AST typé…).

Note le geste : le type dérivé vit dans son propre prédicat (matmul/3, result_type/3), pas dans une tête has_type(mul(X, Y), …) — construire un terme neuf en tête d'une règle récursive est refusé par la garde de terminaison (voir La terminaison). On nomme les objets, on relie leurs types.

Ce n'est pas un système de types dépendants

C'est le point qui surprend. Fix n'a pas de système de types dépendants — pas de vérificateur dédié, pas de langage de preuve, pas de théorie posée par-dessus le langage. D'autres approches ajoutent une couche entière pour soutenir la dépendance type↔valeur ; Fix n'ajoute rien.

Parce qu'en Fix, deux choses sont déjà vraies :

Du coup, les types dépendants ne sont pas une feature : ils tombent de là. Un type indexé, c'est un terme composé ; la contrainte entre indices, c'est une règle ; la vérification, c'est le même calcul qui fait le reste. Tu en fais sans le savoir dès que tu écris une règle dont la tête porte une valeur calculée.

Autrement dit : Fix ne fait pas « des types dépendants ». Il fait « programmer les types comme des données » — et les types dépendants en sont un cas particulier.

Le tour relationnel

Comme une règle est une relation, l'indice se lit aussi à l'envers. Tu peux demander « quels vecteurs donneraient un résultat de longueur 8 ? » et Fix remonte la contrainte — tant que tu n'as pas jeté l'information en chemin (voir la bidirectionnalité). Le type n'est pas une voie à sens unique : c'est une relation entre des formes et des valeurs, parcourable dans les deux sens.

Les bords honnêtes

À côté