Fortement typé
Valeurs, types, kinds — tous inférés et vérifiés. Une incohérence ne compile pas.
Déterministe & fini
Aucun ordre de règles à régler, aucun réglage caché. Tout programme termine — prouvé, pas espéré.
Calcule seul
Une requête rend l'ensemble complet des solutions, indépendant de l'ordre des règles.
% un graphe typé — les nœuds forment un type fermé :- type noeud = a | b | c | d. :- sig(edge, [noeud, noeud]). edge(a, b). edge(b, c). edge(c, d). % edge(a, z) ne compilerait pas — « z » n'est pas un nœud path(X, Y) :- edge(X, Y). path(X, Z) :- path(X, Y), path(Y, Z). ?- path(a, d). % vrai — la fermeture transitive, calculée
Les types sont des programmes
has_type et kind_of sont des relations ordinaires : tu écris des règles dessus — au niveau des types (L₁) comme des kinds (L₂). Et un type peut porter une valeur que le moteur calcule : les types dépendants.
% deux vecteurs — la longueur est portée par le type has_type(v1, vec(int, 3)). has_type(v2, vec(int, 5)). % une règle AU NIVEAU DES TYPES : la longueur s'additionne 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) % 3 + 5, calculé dans le type
Ton propre langage
Fix n'est pas qu'un solveur : chaque langage a son namespace de syntaxe (er:, uml:) et son propre AST. Passer d'un langage à l'autre, c'est une règle. C'est le cœur du TDE.
% vocabulaire commun : un type par rôle :- type ename = user. :- type fname = id. :- type ftype = int. :- type attr = attr(fname, ftype). % langage ER : son namespace de syntaxe, son AST :- type er_ast = entity(ename, attr). er: entity(N, A) := "entity" N "has" A "end". % langage UML : son namespace de syntaxe, son AST :- type uml_ast = class(ename, attr). uml: class(N, A) := "class" N "has" A "end". % modèle ER → modèle UML par une règle er_model(entity(user, attr(id, int))). uml_model(class(N, A)) :- er_model(entity(N, A)). ?- uml_model(X). % X = class(user, attr(id, int))