Langage Anubis

Anubis (langage)

Anubis est un langage fonctionnel créé en 2000 par le mathématicien français Alain Prouté en se basant sur la théorie des catégories.

Description

Le principe de la construction d'Anubis est de définir chaque élément du langage au moyen de la théorie des catégories bicartésiennes fermées. L'objectif est d'obtenir un langage sûr, facilitant l'écriture de démonstrations de correction de programmes à la manière d'un assistant de preuve.

Parmi les éléments qui contribuent à cette sûreté figurent le branchement conditionnel d'Anubis, qui oblige le programmeur à traiter tous les cas possibles, et l'absence d'exceptions. Cette dernière oblige le programmeur à tenir compte de tous les résultats possibles d'une opération. Ainsi, la division d'entiers peut renvoyer un entier ou une valeur indiquant l'absence de résultat, car la division par zéro provoque une erreur.

Exemple de programme

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 un filtre car il est obligatoire de prévoir un unique traitement par cas possible. 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. Cette caractéristique est une source essentielle de sûreté et de facilité de maintenance des programmes.

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.

Anubis 2

La deuxième version d'Anubis est en préparation. Basée sur des catégories particulières appelées topos, elle sera plus proche d'un assistant de preuve.

Critiques

Si les constructions d'Anubis garantissent la sûreté, c'est au prix de programmes longs car ils doivent traiter tous les cas possibles, même lorsque l'on peut démontrer qu'ils ne peuvent pas se produire. Par exemple, écrire x/2 oblige à traiter le cas de la division par zéro alors que 2 est différent de zéro.

Voir aussi

• (en) Charity, un autre langage de programmation fondé sur la théorie des catégories.

Liens externes

• Site officiel

Ce document provient de « Anubis (langage) ».