Je ne connais pas cette personne ni ce langage mais je ne comprends pas ce que "premier langage fonctionnel auto-prouvé (!), à la compilation" signifie.
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.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par _ . En réponse à la dépêche Sortie de la version 2.5 du langage Tom. É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