Tom est un langage de programmation développé au sein de l'INRIA et qui ajoute des capacités de réécriture à des langages de programmation impératifs (actuellement Java, C et OCaml). Concrètement, cela signifie que Tom permet de décrire des transformations de structures de données par un mécanisme de filtrage (pattern-matching) puissant et de spécifier comment ces transformations s'appliquent à l'aide d'un langage de stratégie.
Ce style de programmation est particulièrement adapté à la manipulation d'arbres, comme des arbres XML par exemple, mais aussi des arbres représentant des programmes (cf. la dépêche de jeudi concernant CFE). Ces arbres peuvent être des structures de données du langage hôte (on pourrait par exemple fournir une description à Tom des arbres générés par CFE), ou simplement des termes algébriques à la Caml, pour lesquels Tom fournit une implémentation efficace en Java.
Il est activement utilisé par des équipes de recherche ainsi que des industriels pour :
- développer des compilateurs (comme le compilateur Tom lui-même) ;
- transformer à la volée du bytecode Java ;
- le développement d'un assistant à la démonstration ;
- la traduction de requêtes vers des bases de connaissance.
La documentation est exhaustive et à jour. Le compilateur est stable et mature. Il est accompagné des outils indispensables à son utilisation : greffon pour Eclipse, mode pour vim et tâche ant. Le tout est publié sous licences libres (GPL, APL et BSD). Cette version s'inscrit dans la continuité de notre travail d'intégration de capacités de filtrage de motif et programmation par règles dans les langages C et Java. Sa conception fait suite aux recherches de l'équipe en matière de compilation efficace des langages à base de règles (cf. ELAN, développé au Loria).
Voyons un petit exemple pour éclairer les choses. Imaginons que nous voulions écrire un petit optimiseur qui applique la transformation suivante à un programme C par exemple :
if ( ! /* condition */) { /* bloc1 */ } else { /* bloc2 */ }
se transforme en :
if (/* condition */) { /* bloc2 */ } else { /* bloc1 */ }
À supposer que nous ayons un arbre représentant le programme, une règle de réécriture opérant ce genre de transformation se décrit simplement comme ceci (à quelques variations syntaxiques près, cf. le tutoriel) :
%strategy Optimize() {
if_then_else(not(c),b1,b2) -> { return `if_then_else(c,b2,b1); }
}
Il reste ensuite à indiquer à Tom l'ordre d'application de cette règle dans l'arbre représentant notre programme, par exemple de la racine aux feuilles :
Program optimized = `TopDown(Optimize()).visit(prog);
Et voilà !
Les originalités de Tom, mise à part son intégration transparente à des langages de programmation classiques, sont d'une part l'expressivité des motifs acceptés par l'algorithme de filtrage :
- non-linéarité : f(x,x) ; f a deux fils identiques ;
- associatif : (_*,x,_*,x,_*) ; la liste contient deux éléments identiques
- antipatterns : (_*,x,_*,y@!x,_*) ; la liste contient deux élément x et y différents
- associatif avec élément neutre : plus(x,y) peut filtrer "3" en instanciant x par 0 et y par 3.
... et d'autre part son langage de stratégie qui permet de décrire simplement des stratégies de parcours complexes comme TopDown.
Une bonne façon de commencer à programmer en Tom est de parcourir les exemples du Guided tour ou de se plonger dans le tutoriel.
Cette nouvelle version contient de nombreuses améliorations et nouvelles fonctionnalités :
- Un compilateur entièrement refondu, basé sur la propagation de contraintes. Cela rend le code plus simple, et ouvre la voie à la combinaison de théories de filtrage.
- Une nouvelle bibliothèque de stratégies, plus simple à utiliser, plus efficace, et prête pour les transformations de graphes.
- Une nouvelle construction pour exprimer des paquets de règles conditionelles, qui sont appliquées systématiquement (la structure de données est en forme normale pour le paquet de règles par contruction).
- Le support complet des opérateurs de liste dont le domaine est égal au co-domaine. Ceci correspond au filtrage modulo associativité et élément neutre (AU).
- Toutes les combinaisons de motifs, anti-motifs et opérateurs de liste sont maintenant supportées.
- Il est maintenant possible de définir des termes avec pointeurs. Ceci est particulièrement utile pour représenter, analyser et transformer des termes/graphes, comme les graphes de flot de contrôle, par exemple.
Aller plus loin
- Page principale du langage Tom (70 clics)
- Page du projet sur GForge INRIA (40 clics)
- Guided Tour (33 clics)
- Tutoriel (41 clics)
- Dépêche précédente (29 clics)
# Merci
Posté par reno . Évalué à 4.
Je me demande si ça pourrait remplacer XSLT (qui a une syntaxe très moche)?
Je voulais vérifier sur le site du langage, mais il ne répond pas, ça doit être l'effet linuxfr :-)
[^] # Re: Merci
Posté par Ontologia (site web personnel) . Évalué à 2.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Merci
Posté par _ . Évalué à 4.
Le gros avantage par rapport à XSLT c'est qu'on contrôle explicitement la stratégie d'application des règles, qui d'habitude doit être gérée par un ensemble de règles artificielles mélangées aux règles qui ont du sens. Sur de gross projets, ça devient simplement impossible à maintenir.
# Text2Model ?
Posté par Axel . Évalué à 2.
Est ce que c'est ce langage qui est utilisé par le projet Kermeta/Sintaks (de l inria) ?
Quoi qu'il en soit, si j'ai bien compris, je pense que ça intéresserait les projets Eclipse EMF et EMFT.
[^] # Re: Text2Model ?
Posté par Ontologia (site web personnel) . Évalué à 3.
http://codeworker.free.fr/
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Text2Model ?
Posté par _ . Évalué à 3.
Ce travail n'est pas complètement terminé car la grammaire complète de Java est un gros morceau, mais il est bien sûr déjà possible de prendre un parser Java existant et ne récupérer que la partie intéressante pour bosser dessus.
Un interfaçage encore plus transparent avec Antlr est prévu pour la prochaine version.
# Mais alors ...
Posté par Camille Vacher . Évalué à 4.
[^] # Re: Mais alors ...
Posté par galactikboulay . Évalué à 1.
--->[]
# Anubis et les "catégories bicartésiennes fermées"
Posté par Ontologia (site web personnel) . Évalué à 2.
Alain Prouté, l'auteur d'Anubis (Prof à l'université Paris 13) développe un point de vue très tranché concernant les formalismes utilisés dans les langages comme Caml et Haskell (logique combinatoire).
Dans les systèmes logiques classiques, explique t-il, seul le produit (cartésien) et la puissance (composition de fonction) sont disponibles.
Dans le système utilisé pour Anubis, les catégories bicartésiennes fermées, on ajoute la somme.
Cela implique que les filtrages effectués dans le code sont vérifiés à la compilation, car le formalisme permet de s'assurer que les élements filtrés sont tous disjoint mais aussi que leur union soit égal à l'ensemble filtrés.
Cela permet d'éviter les exceptions sur filtrages.
De plus, en terme de performances, les filtres ne sont pas essayés les uns après les autres, mais seul le bon est choisi (comment ? j'en sais rien)
Dans [3], Alain Prouté revient sur la gueguerre de chapelle entre les lambda-calculistes et les catégoriciens, en défendant évidemment la deuxième voie.
Il propose carrément de jeter aux orties la correspondance de Curry-Howard !!!!
Dans sa futur version 2, Anubis deviendra le premier langage fonctionnel auto-prouvé (!), à la compilation.
Il en donne quelques explications ici [4]
TOM est basé sur du ro-calcul si j'ai bien compris, c'est quoi la différence avec le lambda calcul ?
[1] http://www.anubis-language.com
[2] http://fr.wikipedia.org/wiki/Langage_Anubis
[3] http://www.developpez.net/forums/showthread.php?t=38275&(...)
Alin Prouté = Dr Topos
[4] http://www.developpez.net/forums/showthread.php?t=46904&(...)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Axel . Évalué à 6.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par brouillon . Évalué à 1.
pas trop ouvert comme attitude :
"En fait la distribution est personalisée (c'est un système expérimental anti-pirates en vue d'une commercialisation éventuelle). C'est la raison pour laquelle l'inscription est nécessaire. Ce serait dommage de vous priver d'Anubis pour si peu de chose. Il est quand même gratuit."
... ouais ouais gratuit ... c'est cela ...
Je ne pense pas que ce soit une bonne chose de chercher à "commercialiser" des langage aussi experimentaux.
Il me semble au contraire plus intéressant de liberer completement
ces langages de manière permettre à une communauté de se créer dessus et à le faire réellement exister et se repandre.
Il me semble d'ailleur que nombres de langages se sont saborder en devenant "commerciaux" .
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Axel . Évalué à 2.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Vivi (site web personnel) . Évalué à 3.
et aucune référence vers des publis présentant la théorie sous-jacente ou les techniques de compilation.
ça fait pas réver :(
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par _ . Évalué à 2.
Je ne comprends pas non plus ce que "jeter curry-howard à la poubelle" signifie. Est-ce que cela veut dire que le langage fonctionnel en question ne repose pas sur la théorie des types ?
Le rho-calcul est un lambda-calcul avec patterns, où l'on peut abstraire sur des patterns. Par exemple : (lambda P(x,y) . x P(a,b)) -> a.
L'idée au départ était de canaliser la réécriture au travers de stratégies exprimées dans ce calcul. On peut également le voir comme un calcul plus proche des langages usuels de programmation fonctionnelle que ne l'est le lambda-calcul.
Les originalités du langage sont la capacité à traiter les cas d'erreur (contrainte de filtrage non satisfaites) et la gestion du filtrage non unitaire (collection de résultats). Dans certaines de ses versions, il est muni d'un système de types (à la PTS) avec les meta-propriétés qui en découlent et il y a des versions qui typent les point fixes.
Pour plus d'infos : http://rho.loria.fr
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Ontologia (site web personnel) . Évalué à 1.
Le terme est en effet inexact.
Je te renvoi à ce document, qui est une conférence d'Alain Prouté à l'université de Marseilles.
http://www.math.jussieu.fr/~alp/luminy_05_2007.pdf
Quand à jeter curry-howard à la poubelle, cela provient de sa conviction que la théorie des topos est plus puissante que la théorie classiquement utilisée en Haskell, Caml, etc...
Je me suis planté de lien, aussi vais-je corriger mon erreur.
Il explique ici, pourquoi il faut abandonner Curry-Howard
http://www.developpez.net/forums/showthread.php?t=46904&(...)
Je cite :
"prétendre qu'il y a 'isomorphisme' (c'est à dire similitude parfaite) entre preuves et programmes conduit à concevoir des systèmes formels dans lequels aucune notion correcte de sous-ensemble ne peut être définie. C'est un fait dont les logiciens et théoriciens de l'informatique commencent tout juste à prendre conscience aujourd'hui. Des langages avec preuve comme LEGO ou COQ souffrent de ce problème, qui rend quasiment impossible la manipulation de sous-ensemble ou d'ensemble quotients. Il faut donc abandonner l'isomorphisme de Curry-Howard. La théorie des topos donne une bien meilleure modélisation de ces questions."
Pour une comparaison avec les systèmes de type d'Haskell et d'Anubis, il explique cela ici :
http://www.developpez.net/forums/showpost.php?p=513888&p(...)
En espérant t'avoir éclairé.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par schount . Évalué à 3.
Bien qu'il soit difficile de confirmer ou d'infirmer, en une nuit, le fondement du systeme deductif du Professeur Prouté, les arguments qu'il avance afin d'ecarter la theorie des types sont fumeux.
Il semble evident que la plupart des arguments qu'il apporte n'ont aucun fondement :
page 5, section 2.1 :
"meme si la facon de demontrer un theoreme peut pour diverses raisons interesser le mathematicien, ce dernier ne se soucie aucunement de la facon dont un theoreme a ete demontre pour l’appliquer."
Les mathematiciens peuvent rester tres deconnectés du monde materiel. Ils ne se soucient donc pas forcement de l'adequation entre les preuves des theoremes et le monde reel. Au contraire, lorsque l'on veut "prouver" que tel avion n'explosera pas en vol, il faut rester beaucoup plus proche de l'implementation effective (le programme informatique). Il faut alors se soucier de la facon dont le theoreme est demontré (ce qui implique de se soucier du sens de demontrer un theoreme)
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique
page 5, section 2.1 :
"Si pour appliquer un theoreme, il fallait tenir compte de la facon dont il a ete demontre, les mathematiques serait beaucoup plus complexes qu’elles ne le sont deja."
On peut (et dans certains cas, il faut) tenir compte de la facon dont un theoreme est demontre, ce que ne font generalement pas les mathematiciens. Il est evident que les mathematiques sont bien plus complexes que ce qui est decrit par les mathematiciens. Cet argument n'est pas fonde non plus.
page 6, section 2.3 :
"On n’ecrit pas non plus [des preuves] de la meme facon pour des mathematiciens chevronnes et pour des etudiants de premiere annee. [...] Les preuves supportent donc l’a peu pres, contrairement aux calculs, qui doivent etre beaucoup plus precis"
Qui peut definir la difference entre ce qu'est un calcul et ce qu'est une preuve ? Et si l'on ecrit plus (en quantité) pour les mathematiciens chevronnes, n'est-ce pas parce qu'ils demandent plus ? Et les etudiants ne sont-ils pas capable de chercher une preuve complete si ils ne sont pas convaincus par leur cours ?
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique.
page 6, section 2.4
"Si les informaticiens avaient autant de chance que les mathematiciens, ils leur suffirait de lire les types des fonctions pour pouvoir les utiliser"
Parce qu'il suffit a un mathematicien de lire un enoncé "vrai" pour en avoir la preuve ? Tout cela depend bien evidemment du systeme deductif considere. Par exemple en Coq, un type peut definir complement le comportement d'une fonction.
page 9, section 3.2 :
"Le systeme de Martin–Lof est consistant. S’il ne l’est pas, il sera de toute facon sans interet. Il semble toutefois que sa consistance absolue ait ete prouvee par les methodes de la normalisation forte (Tait, Girard, Coquant,. . .)."
Le fait que sa non-consistance aneantisse son interet suffit-elle a prouver sa consistance ? Que signifie "consistance absolue" ??? La normalisation forte d'un systeme ne permet que de prouver sa consistance si l'on suppose le meta-systeme consistant. En bref, cette phrase ne semble pas avoir de sens.
(au fait, le mot francais est "coherent")
la suite dans le post suivant
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par schount . Évalué à 5.
page 11, section 3.2 :
Toutefois, quelle que soit cette facon, il n’en reste pas moins vrai que le theoreme de Diaconescu demeurera indemontrable [dans la theorie des types de Martin-Lof]"
(rappel : le theoreme de Diaconescu enonce que axiome du choix implique intuitionistiquement le tiers exclus)
A-t-on une PREUVE que ce theoreme n'a pas de demonstration dans la theorie des types de Martin-Lof ? Et si oui, cette preuve utilise quel systeme ? L'avis du Professeur Prouté semble bien tranché alors que bien des questions restent sans reponse.
page 12, avant la section 4:
"Le fond du probleme est donc me semble–t–il le fait que le systeme de Martin–Lof est en contradiction avec le principe de l’unicite du temoin, ou de l’indiscernabilite des preuves. Il en va de meme de tous les systemes de type “Curry–Howard”"
Il est facile de renoncer a toute la theorie des types sur un "me semble-t-il". N'est-ce pas plutot le principe d'indiscernabilite des preuves qui est en contradiction avec Curry-Howard que le contraire ?
On peut continuer ainsi en listant tous les arguments du Professeur Prouté qui ne reposent que sur des affirmations et des arguments purement philosophiques et subjectifs. Le refus de la theorie des types du Professeur Prouté ne tient donc pas.
En esperant t'avoir obscurci.
PS : les numeros de page et de section correspondent au document
http://www.math.jussieu.fr/~alp/luminy_05_2007.pdf
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Alain_P . Évalué à 2.
Je suis Alain Prouté, auteur de l'article dont parle shount.
Si je réponds à ce message c'est surtout parce qu'il me semble qu'il contient plus d'attaques personnelles que d'arguments scientifiques. Pourquoi shount m'appelle-t-il ironiquement 'Professeur Prouté' et non 'Alain Prouté' comme cela aurait dû être le cas ? Tout cela ressemble fort à du dénigrement.
Il y a une chose qui est claire en tous cas. C'est que shount s'est contenté de feuilleter mon article avec le pouce.
Il est très facile évidemment de dénigrer le travail des autres quand on est assuré d'un parfait anonymat. En ce qui me concerne, on connait mon nom et mon prénom, et on peut facilement trouver sur le net ma photo, mon email, mon age et l'adresse de mon employeur.
Que shount ait le courage de se faire connaitre, et je répondrai à ses critiques (fort mal fondées d'ailleurs) point par point.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Framasky (site web personnel) . Évalué à 1.
Cela montre plutôt une marque de respect que d'appeler quelqu'un par son titre universitaire, non ?
Par contre vous auriez pu, vous qui semblez susceptible, faire attention à l'orthographe exacte de Schount (et pas shount) et utiliser une majuscule lors de l'utilisation de son nom.
Et au cas où des personnes se poseraient la question, non je ne suis pas Schount sous un autre pseudo.
Being a sysadmin is easy. As easy as riding a bicycle. Except the bicycle is on fire, you’re on fire and you’re in Hell.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par pasSteve pasJobs . Évalué à 4.
En OCaml, le filtrage est aussi vérifié à la compilation : le compilateur affiche un warning si un cas n'est pas traité (ie. si leur union est différente de l'ensemble filtré). En Haskell ce n'est pas le cas par défaut à ma connaissance (pas avec GHC en tout cas), mais le travail de Neil Mitchell sur Catch[0] permet de vérifier qu'il n'y a pas d'erreur de filtrage à l'exécution, c'est à dire qu'un chemin du code ne mène pas à un cas non traité dans un filtrage non exhaustif.
[0] : http://www-users.cs.york.ac.uk/~ndm/catch/
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par Vivi (site web personnel) . Évalué à 2.
tout à fait, on ne devrait pas pouvoir te prendre une erreur de filtrage à l'execution sans avoir eu un warning lors de la compil'...
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.