Je suis récemment tombé sur le site du langage Anubis[1][2], et comme on parle pour une fois de langages et de maths ici, je ne résiste pas à la tentation de signaler ce langage très intéressant.
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 ?
# Anubis et les "catégories bicartésiennes fermées"
Posté par Ontologia (site web personnel) . En réponse à la dépêche Sortie de la version 2.5 du langage Tom. É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