Langage Anubis

Un article de Wikipédia, l'encyclopédie libre.

Anubis est un langage fonctionnel créé en 2000 par un mathématicien français (Alain Prouté). Contrairement à la plupart des langages de cette catégorie, il n'est pas basé sur ML, mais sur la théorie des catégories bicartésiennes fermées.

Sommaire

[modifier] Description sommaire

Le design d'Anubis est guidé par la théorie des catégories bicartésiennes fermées. Cette théorie formalise trois constructions de types qu'on appelle somme (union disjointe), produit (produit cartésien) et puissance (types fonctionnels). Tous les langages fonctionnels depuis les premières versions de Lisp implémentent les produits et les puissances d'une façon satisfaisante (encore qu'il a fallu attendre l'introduction des fermetures pour avoir une implémentation correcte des puissances, évitant la trop tristement célèbre capture de variable). Par contre, Anubis semble bien être le premier à implémenter correctement les sommes. Ceci a pour conséquence que les conditionnelles en Anubis ont des caractéristiques qu'on ne trouve pas dans les langages de la famille ML, avec pour conséquence l'élimination d'un nombre beaucoup plus important de bugs potentiels, rendant en particulier complètement caduque la notion de test de couverture. D'ailleurs, ce traitement des sommes a permis d'éliminer complètement du langage la notion d'exception, le rendant ainsi beaucoup plus sûr.

[modifier] Exemple de programme

L'exemple est très classique en programmation fonctionnelle. Il s'agit de calculer la longueur d'une liste. D'abord, le type des listes est défini comme suit:

type List($T):
   [ ], 
   [$T . List($T)].

Dans cette définition, $T représente un type quelconque. Ceci est donc un schéma de définition de type. Le type a deux alternatives (deuxième et troisième ligne de la définition), qui représentent respectivement la liste vide et les listes non vides.

Le calcul de la longueur d'une liste oblige à détruire la donnée de type List($T) qui est fournie. Ceci est réalisé obligatoirement avec une conditionnelle:

define Int32 length(List($T) l) =
   if l is 
     {
        [ ]           then 0, 
        [head . tail] then 1 + length(tail)
     }.

Ce qui différencie fondamentalement Anubis des langages de la famille ML, est le fait qu'une telle conditionnelle ne constitue pas du filtrage. L'exécution du programme analogue en Caml ou en Haskell conduirait à essayer chaque filtre (ici [ ] et [head . tail]) jusqu'à ce que l'un d'eux laisse passer la donnée l. Éventuellement (ce n'est pas le cas de l'exemple bien sûr), plusieurs filtres seraient susceptible de laisser passer une donnée, ou au contraire aucun d'entre eux ne la laisserait passer. En Anubis, au contraire, il y a toujours un et un seul cas correspondant à la donnée fournie. Ainsi, il n'y a pas de problème lié à l'ordre des filtres, et il n'y a jamais d'exception lancée au cas où aucun filtre ne conviendrait. Il y a donc saut direct au cas concerné, sans essais successifs. Ce comportement est la traduction exacte du problème universel qui définit les sommes en théorie des catégories, alors que le filtrage modélise une union non nécessairement disjointe et ne couvrant pas nécessairement tous les cas possibles. Bien entendu, le compilateur Anubis oblige le programmeur à mettre dans chaque conditionnelle exactement un cas par alternative du type concerné. Cette caractéristique est une source essentielle de sûreté et de facilité de maintenance des programmes. Bien entendu, il n'y a pas de fonction head ou tail en Anubis. Les symboles (appelés résurgents) qui apparaissent en tête du deuxième cas de la conditionnelle, et qui constituent des déclarations, offrent l'accès à la tête et la queue de la liste seulement dans le cas où il est certain que cette tête et cette queue existent.

[modifier] Autres caractéristiques

Anubis est un langage à vocation universelle. Il autorise l'utilisation de constructions impératives (tout en recommandant de les limiter au strict nécessaire), ainsi que la programmation orientée objet.

[modifier] Liens externes