[Débat] Que pensez-vous du Langage Anubis ?

[SpiceGuid]

Je vous concède bien volontiers que:

• Vous pouvez qualifier ma lecture de naïve dans le sens où je suis un béotien en matière de théorie des catégories, de même ma compréhension de la correspondance de Curry-Howard est sans doute la plus superficielle que vous puissiez concevoir.
• Ce que j'appelle résumé n'est que mon compte-rendu d'un point de vue purement calculatoire, j'assume complètement la possibilité voire la certitude d'être totalement passé à côté de la véritable valeur ajoutée de votre travail. Ce faisant je n'ai pas l'impression de minimiser la qualité de cet exposé, seulement j'en omet volontaire la partie (même si pour vous c'est cette partie qui constitue le véritable fond) dont j'ai la conviction (à tort ou à raison) qu'elle n'apportera aucun bénéfice calculatoire.
• La lisibilité est forcément un critère déterminant de la qualité c'est pourquoi je ne m'interdis pas les remarques sur la syntaxe concrête même si je sais que la syntaxe abstraite n'est pas en cause

Dire que le programmeur Anubis compile lui-même le filtrage c'est une remarque de syntaxe concrête, il est trop tôt pour dire la part due à la jeunesse de l'implémentation et celle due à votre intransigeance sur le filtrage. Je profite de l'occasion pour faire encore quelque remarque de syntaxe concrête:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
define (List($T),List($T)) 
  split (List($T) l)
    =
  if l is
    {
      [ ] then ([ ],[ ]),
      [ha . ta] then 
         if ta is
           {
             [ ] then ([ha],[ ]),
             [hb . tb] then 
                with w = split(tb),
                if w is { (u,v) then ([ha . u],[hb . v]) }
           }   
    }.

define List($T)
  merge
    (
      ($T,$T) -> Bool less,
      List($T) l1, 
      List($T) l2
    ) =
  if l1 is 
    {
      [ ] then l2,
      [h1 . t1] then
        if l2 is
          {
            [ ] then l1,
            [h2 . t2] then
               if less(h1,h2) then [h1 . merge(less,t1,l2)]
               else [h2 . merge(less,l1,t2)]
          }  
    }. 

define List($T)
  msort
    (
      ($T,$T) -> Bool less,
      List($T) l 
    ) =
  if l is
    {
      [ ] then [ ],
      [ha . ta] then
        if ta is
          {
            [ ] then [ha],
            [hb . tb] then
              with w = split(l),
              if w is { (u,v) then merge(less,msort(less,u),msort(less,v)) }
          }
    }.

Vous aurez reconnu une implémentation du tri fusion.
Je trouve cette expresssion désagréable:

Code :

1
2
3
                with w = split(tb),
                if w is { (u,v) then ([ha . u],[hb . v]) }

Celle-ci serait davantage dans mes habitudes:

Code :

1
2
3
                with (u,v) = split(tb),
                ([ha . u],[hb . v])

Et de façon similaire, à ceci:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
  if l1 is 
    {
      [ ] then l2,
      [h1 . t1] then
        if l2 is
          {
            [ ] then l1,
            [h2 . t2] then
              ...
          }
    }

Je préfèrerais cela:

Code :

1
2
3
4
5
6
7
8
9
  if (l1,l2) is 
    {
      ([ ],[ ]) then [],  // pour disjoindre les deux gardes suivantes
      ([ ],_) then l2,
      (_,[ ]) then l1,
      ([h1 . t1],[h2 . t2]) then
          ...
    }

Voilà, j'en ai fini avec la syntaxe concrête.

Au tour de la sémantique maintenant.

with x = a, t

Notez que with x = a, t est un terme, et que son type est le type de t. Le terme t est la portée de la définition locale. Autrement-dit, le symbole x défini après le mot clef with n’est utilisable que dans le terme t.

Sachant la rigueur qui vous caractérise, x n'est donc pas utilisable dans a.

C'est gênant, cela signifie que vous n'accordez pas aux données la contrepartie de la récursion que vous accordez aux fonctions. Cela a forcément un coût en terme d'expressivité, tôt ou tard une fonction récursive ne pourra pas être écrite parce qu'elle n'aura pas droit à sa donnée duale. En clair un traitement récursif ne sera pas spécifiable parce que sa sémantique sera rejetée. Ou, dit plus brutalement, Anubis n'est pas vraiment un langage récursif.

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
read tools/basis.anubis

type Expression:
  variable  (Int32 bruijn),
  lambda    (Expression body),
  apply     (Expression f, Expression arg), 
  let_in    (Expression e, Expression body),
  letrec_in (Expression e, Expression body).

type Value:
  error_bruijn_index,
  ok_function(Value -> Value).
      
define Value
  eval
    (
      Expression expr,
      List(Value) env
    ) =
  if expr is
    {
	   variable(n) then
	     if nth(n,env) is
	       {
   	      failure then error_bruijn_index,
   	      success(v) then v  
   	    }
	   lambda(body) then
	     ok_function((Value x) |-> eval(body, [x . env]))
	   apply(f,arg) then
	     if eval(f,env) is
	       {
   	      error_bruijn_index then error_bruijn_index 
   	      ok_function(f) then f(eval(arg,env))
	       }
	   let_in(e,body) then
	     eval(body, [eval(e,env) . env])
	   letrec_in(e,body) then
	     with f = ok_function((Value x) |-> eval(e,[x . [f . env]])),
	     eval(body, [f . env])
    }.

À mon grand regret ce code ne compile pas.
La faute en incombe au f à droite du with:

Code :

1
2
3
4
	   letrec_in(e,body) then
	     with f = ok_function((Value x) |-> eval(e,[x . [f . env]])),
	     eval(body, [f . env])

Pourtant ce code me paraît légitime, le let rec a bien pour but d'étendre l'environnement env avec une nouvelle fonction qui pourra s'évaluer dans l'environnement étendu, si la récursion sur la donnée est impossible alors le let rec n'a pas de sémantique possible.

Bien sûr il faut rejeter les cas pathologiques tels que:

Code :

with x = x, x

Mais il faut tout de même autoriser les cas légitimes.
Vous auriez anticipé cela si vous aviez programmé le compilateur Anubis en OCaml, au lieu de choisir un langage qui se rapproche au plus d'Anubis vous avez mis les mains dans le cambouis du C et il vous a caché vos vrais besoins. Je suis certain qu'en y réfléchissant vous trouverez dans les topos une raison pour laquelle le with devrait autoriser certaines formes de récursion. Et cette raison serait apparue bien plus vite à vos yeux si vous utilisiez OCaml. Sans doutes l'approche qui voit les besoins dans la beauté est la plus louable, mais l'approche duale qui voit la beauté dans les besoins est tout autant complémentaire car elle dissipe la fascination qui vous masque une beauté encore plus désirable.

[DrTopos]

@SpiceGuid: je tiens d'abord à vous dire que vous voir utiliser Anubis comme vous le faites ne peut que me réjouir. Anubis n'a encore que trop peu d'utilisateurs surtout de votre niveau en programmation fonctionnelle.

J'aurais beaucoup de choses à dire sur votre messages, et aussi sur ceux des autres utilisateurs de ce forum. Dans ce post, je vais me contenter de répondre à votre question sur la récursion, et en particulier à propos de la ligne:

Code :

1
2
with f = ok_function((Value x) |-> eval(e,[x . [f . env]])),

qu'il suffit d'écrire comme ceci:

Code :

1
2
with f = ok_function((Value x) |-f-> eval(e,[x . [f . env]])),

pour obtenir ce que vous voulez.

Je vous demande pardon, mais je crois que je ne suis pas complètement tombé de la dernière pluie en matière de récursion, ayant pratiqué Lisp pendant de nombreuses années (et ayant également fait un compilateur pour ce langage), et ayant par ailleurs fait (il y a assez longtemps c'est vrai) un cours de fonctions récursives et machines de Turing dans la Maîtrise de Maths de l'université de Nantes. Vous remarquerez que la notation |-f-> est beaucoup plus propre que ce que vous suggériez y compris en utilisant un mot clef comme 'letrec'. En effet, la ligne ci-dessus peut aussi bien être écrite:

Code :

1
2
with f = ok_function((Value x) |-g-> eval(e,[x . [g . env]])),

cela marchera encore. Comme vous le voyez c'est vraiment la fonction définie 'à la volée' qui est récursive, et cela n'a rien à voir avec le 'with', d'où l'inutilité du 'letrec'.

Je vous concède que la documentation d'Anubis est incomplète, et que cette formulation ne s'y trouve peut-être pas. En fait elle se trouve dans l'ancienne doc, celle qui se trouve dans le répertoire 'library/manuals/en' de la distribution. Désolé, mais quand on est tout seul (ou à peu près) pour mener une tel projet, il y a des choses qui peuvent manquer.

[SpiceGuid]

Comme vous le voyez c'est vraiment la fonction définie 'à la volée' qui est récursive, et cela n'a rien à voir avec le 'with', d'où l'inutilité du 'letrec'.

Malheureusement ce que je vois c'est exactement le contraire: c'est bien le with que je veux récursif, pas la fonction anonyme, mon problème a tout à voir avec le with et rien à voir avec la fonction anonyme (qui ira très bien sans récursivité).

Donc (sans surprise aucune) votre code ne compile pas, parce que f est un constructeur ok_function, pas une fonction.

Et comme, avec le typage fort et l'évaluation stricte, vous ne pouvez pas avoir accès à un combinateur de point fixe, je ne vois pas bien comment vous pourriez séparer la déclaration locale du mécanisme de récursion

Croyez bien que je me représente la difficulté de la tâche et combien mes objections doivent vous paraître ingrates face au labeur qui est le vôtre.

[DrTopos]

J'essaye une petite analyse du résumé fait par SpiceGuid de mon exposé.

Envoyé par SpiceGuid

* D'un point de vue architectural le système exposé propose une formalisation à deux niveaux, le premier niveau est un lambda-calcul, le second niveau est un calcul des séquents, les deux niveaux sont isomorphes mais seul le premier niveau (les valeurs) est équipé de règles de réduction (la béta-réduction), la réduction du second niveau (les énoncés et les preuves) est à la charge du lecteur et/ou de l'assistant de preuve

Il me semble que les deux niveaux sont équipés de règles de réduction. Voir le tableau en page 29, qui est justement séparé en deux parties, une pour chaque niveau. Par ailleurs, je n'ai pas mis que la béta-reduction, mais aussi la éta-réduction, et pas seulement pour les fonctions mais aussi pour les produits. La éta-réduction est la traduction en termes de réécriture de la propriété d'unicité des problèmes universels qui définissent les produits et les puissances (types fonctionnels). Je ne risque donc pas de l'oublier. Par ailleurs, il n'y a pas besoin d'assitant de preuve en plus du système que je propose, qui fait par lui-même office d'assistant de preuve.

Par ailleurs, les deux niveaux ne sont pas isomorphes (contrairement à ce qu'il se passe avec Martin-Löf), et c'est précisément ce point qui est essentiel dans mon exposé, puisqu'il résulte de l'indiscernabilité des preuves. Je crois que vous avez lu mon exposé vraiment en diagonale pour ne pas vous en être aperçu.

Envoyé par SpiceGuid

* D'un point de vue qualitatif on peut s'attendre à une meilleure lisibilité et une meilleure prouvabilité par rapport à un typage Hindley-Milner qui ne vise qu'à se prémunir des erreurs à l'exécution sans chercher à améliorer la prouvabilité de la post-condition

Il ne me semble pas que le typage de Hindley-Milner fasse allusion à des énoncés et des preuves, sauf à en faire une traduction en changeant de niveau. Par ailleurs, qu'entendez-vous par 'erreur d'exécution' ? Lancement d'une exception ? De même je ne comprends absolument pas ce que vous voulez dire par 'améliorer la prouvabilité de la post-condition'.

Envoyé par SpiceGuid

* L'avantage du système proposé par rapport au typage Martin-Löf c'est le découplage de la charge du calcul d'avec la charge de la preuve, de sorte que l'on peut choisir son système de preuve indépendamment du système de calcul

On ne peut pas choisir son système de preuve, puisqu'il fait déjà partie du système. Par ailleurs, encore une fois le sujet de mon exposé est de nature sémantique (il s'agit de savoir si les mathématiques représentées par le langage sont ou non celles de 'tout le monde', c'est à dire celles qu'on enseigne à l'université et non pas de savoir s'il y a une charge de calcul plus ou moins forte (même si ce genre de question me préoccupe pour Anubis 2, bien sûr).

Envoyé par SpiceGuid

* L'inconvénient c'est qu'au contraire d'un typage à la Martin-Löf le système de preuve ne pourra pas être utilisé pour guider l'écriture simultanée du calcul et de la preuve, de ce fait lorsque la preuve est obligatoire elle sera plus coûteuse en va-et-vient de réécritures

Dans le système que je propose, les calculs et les preuves sont intimement liés, et peuvent être mêlés. Je ne comprends donc pas votre remarque. Qu'entendez-vous par 'va-et-vient' de réécritures ? (réécriture, je connais, mais va-et-vient, je ne vois pas).

Envoyé par SpiceGuid

* Au final on pourrait dire qu'il s'agit d'une version pessimiste du typage Martin-Löf qui se révèlera moins handicapante dans le cas défavorable mais aussi moins payante dans le cas favorable

Là non plus, je ne comprends pas ce que vous entendez par 'pessimiste' appliqué à un système de types. Je ne vois pas non plus quels sont ces cas favorables ou défavorables.

Envoyé par SpiceGuid

* Le système n'exclut pas une extension intégrant une réduction sur le calcul des séquents qui le rendrait équivalent au typage Martin-Löf, mais l'auteur doute qu'une telle extension soit réellement bénéficiaire, en particulier il avance des arguments selon lesquels un calcul des séquents complètement isomorphe au lambda-calcul n'est pas un calcul confluent (ne satisfait pas le 1er théorème de Church-Rosser)

Le système exclut tout à fait une telle extension. Il me semble avoir démontré que le théorème de Diaconescu est indémontrable dans le système de Martin-Löf, alors quil l'est dans celui que je propose. J'en ai aussi expliqué les raisons. Par ailleurs, je n'ai pas émis d'avis sur la confluence dans cet exposé. J'ai simplement précisé que je n'avais pas complètement adapté le théorème de Tait à ce système (lequel n'a d'ailleurs rien à voir avec la confluence, mais seulement avec la noethérianité), mais que je ne doutais pas qu'il pouvait s'adapter.

[DrTopos]

Envoyé par SpiceGuid

Et comme, avec le typage fort et l'évaluation stricte, vous ne pouvez pas avoir accès à un combinateur de point fixe, je ne vois pas bien comment vous pourriez séparer la déclaration locale du mécanisme de récursion

Permettez-moi de vous faire remarquer que |-f-> est une déclaration du symbole f.

[SpiceGuid]

Non, et vous l'avez dit vous-même: c'est la déclaration du symbole g.
C'est le with qui déclare f.


Pour mon commentaire sur votre exposé il est évident que je l'ai lu en diagonale, j'ai interprété au-delà de ce qu'autorisent mes connaissances, mais je ne regrette pas de l'avoir fait si cela a le mérite de nous valoir votre clarification sur chacun des points soulevés, l'exposé n'en est pas plus abordable mais petit à petit il devient moins obscur pour le béotien que je suis.

[DrTopos]

Code :

1
2
(T x) |-f-> E

où T est un type et E un terme contenant des occurences de f, est bien une fonction récursive. Par ailleurs, le symbole f est lié (muet) dans cette expression qui est donc alpha-équivalente à:

Code :

1
2
(T x) |-g-> E[g/f]

C'est donc la flèche avec nom |-f-> qui joue le rôle du letrec. Je ne vois pas ce que vous voulez de plus, à part changer la syntaxe de mon langage.

[SpiceGuid]

C'est le with qui devrait être un let rec, pas la fonction anonyme que vous vous entêtez à vouloir nommer alors que je ne vous l'ai jamais demandé.

Je ne vois pas ce que vous voulez de plus, à part changer la syntaxe de mon langage.

Que vous me donniez les 2 lignes de code qui doivent remplacer celles-ci:

Code :

1
2
with ok_f = ok_function((Value x) |-> eval(e,[x . [ok_f . env]])),
eval(body, [ok_f . env])

Et qu'elles se compilent cette fois-ci (autant faire vous-même le test c'est plus sûr).
Mais cela risque de vous prendre un certain temps alors je serai patient.

[DrTopos]

Ok j'ai compris ce que vous voulez (que je n'avais pas vu à première lecture de votre programme).

J'ai donc fait un couper-coller de votre programme, qui effectivement ne compile pas, même avec la correction que j'avais suggéré. Par contre la version ci-dessous compile:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
read tools/basis.anubis

type Expression:
  variable  (Int32 bruijn),
  lambda    (Expression body),
  apply     (Expression f, Expression arg), 
  let_in    (Expression e, Expression body),
  letrec_in (Expression e, Expression body).

type Value:
  error_bruijn_index,
  ok_function(Value -> Value).
      
define Value
  eval
    (
      Expression expr,
      List(Value) env
    ) =
  if expr is
    {
	   variable(n) then
	     if nth(n,env) is
	       {
   	      failure then error_bruijn_index,
   	      success(v) then v  
   	    }
	   lambda(body) then
	     ok_function((Value x) |-> eval(body, [x . env]))
	   apply(f,arg) then
	     if eval(f,env) is
	       {
   	      error_bruijn_index then error_bruijn_index 
   	      ok_function(f) then f(eval(arg,env))
	       }
	   let_in(e,body) then
	     eval(body, [eval(e,env) . env])
	   letrec_in(e,body) then
	     with f = (Value x) |-f-> eval(e,[x . [ok_function(f) . env]]),
	     eval(body, [ok_function(f) . env])
    }.

Cela correspond-il à ce que vous vouliez faire ? Il me semble que oui.

Alors en effet, la récursion en Anubis ne s'applique qu'aux fonctions, et non pas aux données quelconques. Mais il me semble que c'est normal. En tout cas, les modèles catégoriques pour la récursion, autorisent les types récursifs (bien sûr) et les fonctions récursives. Ceci résulte du problème universel qui définit les types récursifs. Je sais que dans certains langages on peut définir des objets récursifs non fonctionnels, qui ont donc un caractère 'infini', mais cette construction ne me semble pas avoir de sens mathématique. En tous cas, les mécanismes de types récursifs et de fonctions récursives tels qu'ils existent en Anubis et qui seront encore plus restrictifs en Anubis 2 (puisque la récursion y sera contrôlée par des schémas de récursion, ce qui est nécessaire pour que les preuves soient correctes), sont suffisants pour faire toutes les mathématiques. Si j'introduis un nouveau concept dans Anubis 2, je dois être extrêmement prudent, car je ne veux pas faire effondrer sa logique.

[SpiceGuid]

Et oui! Et c'est plus propre, pas de récursivité dans le with!
Il y a 5mins encore j'avais peur d'avoir raison, et maintenant c'est tellement limpide!

Voilà, vous tenez l'exemple qui achève de me convaincre qu'avec des constructions linguistiques plus simples vous arrivez à gagner en spécification sans perdre en expressivité.

Evidemment il va falloir modifier quelques habitudes et se reconstituer un catalogue d'astuces pour affronter les situations les plus alambiquées, mais à priori il me semble que l'on puisse attaquer des problèmes aussi difficiles qu'avec OCaml et ceci avec probablement encore davantage de confiance dans des outils certes moins nombreux mais plus pures et moins redondants.

En tout cas je vous souhaite une bonne continuation et j'aurai certainement dans le futur des opportunités pour pousser Anubis encore plus loin j'espère.

[SpiceGuid]

Je me suis inscrit sur www-anubis-langage.com, le forum a l'air plus "débutants" que celui-ci, je promet je n'irai pas leur filer la pétoche avec des sources ésotériques.

Il m'a semblé que le letrec_in est encore insuffisant à lui tout seul, il faudrait au moins lui adjoindre le letrec_and_in qui est la version qui peut introduire deux définitions locales mutuellement récursives.

Et bien voici son implémentation qui a au moins le mérité d'avoir occupé ma fin de soirée:

Code :

1
2
3
4
5
6
7
     letrec_and_in (e1,e2,body) then
       with g1 = (Value -> Value f2) |-g1-> (Value x) |->
       with f1 = g1(f2), eval(e1,[x.[ok_function(f1).[ok_function(f2).env]]]),
       with g2 = (Value x) |-g2-> with f2 = g2,
       with f1 = g1(f2), eval(e2,[x.[ok_function(f1).[ok_function(f2).env]]]),
       eval(body,[ok_function(g1(g2)).[ok_function(g2).env]])

Par curiosité: vous avez une implémentation plus simple?
(ce n'est pas une critique de ma part, peu de membres du forum www-anubis-langage.com auront à écrire un jour ce genre de charabia qui n'amuse que vous et moi)

Il semble qu'Anubis soit accessible aux débutants, et cela m'étonne un peu dans le sens où il est explicitement encore plus exigeant. Mais il est vrai que les débutants sont très sensibles à la syntaxe concrête et la première parenthèse mal placée leur fera abandonner OCaml pour une syntaxe plus conservatrice. Puissent-ils se tourner alors vers Anubis plutôt qu'une fadaise du genre Java.

[DrTopos]

En effet, la flèche nommée |-f-> est encore insuffisante pour faire des fonctions mutuellement récursives. On doit faire une petite acrobatie. Ce n'est qu'un problème de syntaxe en fait. Il s'agit de trouver une syntaxe aussi élégante et 'locale' que possible.

Pour les fonctions mutuellement récursives définies à la volée, voici l'exemple que j'ai donné dans l'ancienne doc d'Anubis (anubis/manuals/en/anubis_doc.txt dans la distribution).


Now, what if you want to construct cross recursive functions with the arrow '|->' ?
Assume that we want to construct two cross recursive functions 'f' and 'g', and that we
begin by 'f'. The problem is that we cannot call 'g' from within the body of 'f',
because 'g' is not yet declared. However, there is a beautiful (and functional) trick
to solve this problem. It is not always obvious to put it at work. I will just examine
an example.

Assume that the functions 'f' and 'g' could be defined at the top level as follows:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
      type U:...  // forward declaration for cross recursive types

      type T: 
        a,
        b(T,U). 
   
      type U:
        c,
        d(T,U). 
   
      define T g(U u).  // forward declaration for cross recursive functions

      define T f(T t) = if t is 
                          {
                            a        then a, 
                            b(t1,u1) then b(f(t1),g(u1))
                          }.
   
      define T g(U u) = if u is 
                          {
                            c        then a, 
                            d(t1,u1) then b(f(t1),g(u1))
                          }.

You can see that f and g are cross recursive, and that the recursion is correct
(terminates). Define them with labelled arrows as follows:

Code :

1
2
3
4
5
6
7
8
9
10
11
12
   
      with phi = (T t, U -> T g) |-phi-> if t is 
                                           {
                                             a        then a, 
                                             b(t1,u1) then b(phi(t1,g),g(u1))
                                           },
             g = (U u)|-g-> if u is 
                              {
                                c        then a, 
                                d(t1,u1) then b(phi(t1,g),g(u1))
                              },
             f = (T t) |-> phi(t,g),

at that point you have f and g at hand.

Il est vrai que le code que vous avez proposé est particulier. Il ne préoccupe que les gens qui écrivent des compilateurs ou des interpréteurs. Je suis en train d'écrire le compilateur Anubis 2 en Anubis (bootstrap oblige), et je fais des choses dans ce genre (également avec des profondeurs de De Bruijn d'ailleurs).

Anubis peut être utilisé par des débutants. Il est d'ailleurs curieux de constater que les personnes qui n'ont jamais fait d'informatique s'y mettent très facilement, alors que ceux qui en ont fait beaucoup mais uniquement avec des langages impératifs, ont beaucoup de mal à se débarrasser des 'mauvaises habitudes'. Il me semble qu'on devrait commencer par un langage non impératif (qui d'une certaine façon est plus simples à utiliser, justement parce que la sémantique est statique) et que l'impératif ne devrait intervenir que lorsqu'il devient nécessaire. Il me semble qu'avoir fait croire en son temps que le BASIC était un langage pour débutants est une escroquerie (même si les concepteurs n'en étaient pas conscients).

Je ne connais pas bien Java, mais il me semble que le paradigme OO y remplace pour une bonne part le système de types (essentiellement absent de ce langage) et je crois que cette philosophie est très néfaste. Le paradigme OO est le fruit des expériences des programmeurs, et même s'il contient des aspects intéressants, il est loin de pouvoir remplacer une théorie de types (quelle qu'elle soit), seule capable de nous mettre sur des bases solides. La bonne solution est de concilier les deux, la notion d'objet étant importante pour la programmation non déterministe, par exemple pour les logiciels interactifs, mais elle ne doit pas prendre toute la place, et en particulier je la crois particulièrement néfaste là où tout peut être déterministe (calcul pur sans effet de bord).

[SpiceGuid]

Il y a également ce code dans mon interpréteur:

if eval(f,env) is
{
error_bruijn_index then error_bruijn_index
ok_function(f) then f(eval(arg,env))
}

Comme si je capturais l'exception pour la regénérer.

On pourrait (méchamment) résumer OCaml ainsi:
* OCaml est trop permissif
* OCaml cumule les difficultés des syntaxes concrêtes du C et du Lisp

Ou alors on pourrait (méchamment) résumer Anubis ainsi:
* vous compilez vous-même le filtrage
* vous compilez vous-même certaines formes de let rec
* vous compilez vous-même la gestion des exceptions

Vous avez entièrement raison quand vous dites qu'il s'agit d'un arbitrage sur la syntaxe concrête et nul doute que si vous cherchez quelque amélioration sur le typage alors votre choix vous place dans une situation beaucoup plus favorable. La sémantique du let en Caml n'est pas limpide: il défini et il filtre. Cela va à l'encontre du principe du découplage.

Il est effectivement beaucoup trop tôt pour changer de syntaxe concrête sans grandement compromettre les avantages potentiels de la syntaxe abstraite, même si la pression des utilisateurs va dans ce sens (pour l'avantage à court terme).

Pour l'instant Anubis a un "avantage" de syntaxe concrête sur OCaml: les débutants préfèrent f(x) à (f x), c'est fort heureux car sinon vous auriez autant d'utilisateurs qu'Epigram. C'est l'atout que vous devez jouer pour l'instant, en attendant Anubis 2. Je n'hésiterai pas à recommander Anubis quand je sens qu'un débutant veut quelque chose de robuste mais qu'il pourrait être rebuté par la syntaxe de Caml. Et ce avec d'autant plus de facilité que la documentation qui l'accompagne est de qualité. J'approuve donc le choix qui a été fait d'en supprimer les passages les plus difficiles, car:
* il faudrait déjà avoir l'expérience de la version 2 pour savoir quel est le gain de haut niveau (typage) apporté par la syntaxe de plus bas niveau (plus proche du lambda-calcul)
* il faudra encore plus d'expérience pour proposer une syntaxe concrête de plus haut niveau sans dégrader les nouvelles propriétés de typage

Cela promet d'être passionnant.

[DrTopos]

J'imagine que par syntaxe concrête tu entends la syntaxe qui est usuelle en mathématiques, c'est à dire celle à laquelle on est habitué dès le lycée.

Les problèmes de syntaxe depuis le début de la création d'Anubis m'ont bouffé énormément de temps. J'ai compilé des centaines de grammaires avec BISON avant de prendre certaines décisions. Pour la syntaxe Anubis 2, il y aura quelques innovations. Je n'en dis pas plus pour le moment, mais je confirme que je tends autant que possible à me rapprocher de l'aspect usuel des textes mathématiques (compte tenu des contraintes du code ASCII, contraintes qui tomberont avec un éditeur graphique spécialisé qui est en projet). Apparté: moi aussi j'ai du mal avec les syntaxes exotiques (Caml et surtout Haskell). Je sais que c'est idiot, mais c'est comme ça. Par exemple, je trouve que le choix des mots clefs dans le filtrage Caml est obscur du point de vue de la langue naturelle par rapport aux conditionnelles d'Anubis. De même, je préfère 'with ...' à 'let ... in ...'. C'est l'avantage évidemment de créer un nouveau langage, on définit la syntaxe dont on a envie.

Pour ce qui est du filtrage, je ne suis pas aussi intransigeant que j'ai pu en avoir l'air. L'origine du filtrage est syntaxique et vient de Lisp (petit livre de C. Queinnec sur le sujet). J'en ai surtout après la façon dont les informaticiens le comprennent sur le plan théorique. Les conditionnelles sont clairement structurellement liées aux types sommes (elle font partie du problème universel qui définit les sommes en théorie des catégories), et le filtrage ne m'apparaît que comme une facilité syntaxique permettant d'éviter l'emboîtement des conditionnelles. Vu comme cela je n'ai rien contre (c'est assez byzantin, car au final ça revient au même pour l'utilisateur, mais j'aime bien comprendre ce que je fais). En Anubis 2 on pourra donc filtrer (ouf !).

Pour ce qui est des exceptions, c'est une interpretation possible en effet de dire qu'on les compile soi-même. Pour moi c'est un peu différent. Je considère qu'elles n'existent pas. Autrement-dit, le comportement est toujours normal. L'expérience montre que l'approche exception-free d'Anubis est un atout important pour la sûreté. Et puis, en mathématiques, il n'y a pas cette notion. Comme ce sont elles qui me guident...

Pour ce qui est du nombre d'utilisateur d'Anubis, c'est vrai qu'on les compte sur les doigts des mains. Mais je pense que tout cela va changer avec la version 2, car il y aura de vraies nouveautés qui n'existent nulle part ailleurs. Ceci dit, Anubis , pour si peu qu'il soit utilisé, est utilisé dans des (petites) entreprises (3 pour le moment) avec des enjeux économiques derrière. Ceci montre la confiance que les dirigents de ces entreprises ont dans mon système. Ils ont bien compris en fait qu'Anubis leur offre un moyen de développement rapide (peu de programmeurs nécessaires) et où le risque de régression est extrêmement faible.

[Garulfo]

Envoyé par SpiceGuid

[...]
Pour l'instant Anubis a un "avantage" de syntaxe concrête sur OCaml: les débutants préfèrent f(x) à (f x), c'est fort heureux car sinon vous auriez autant d'utilisateurs qu'Epigram.[...]

Qu'est ce qui t'empêche de taper f(x) avec ocaml ?
Je ne comprends pas ton problème... tu ne parlais pas de la syntaxe de Lisp plutôt ?

Personnellement j'apprécie beaucoup de chose dans la syntaxe d'ocaml. La syntaxe du filtrage particulièrement que, contrairement à Dr Topos, je trouve assez « naturelle ». Bien sûr, encore une fois, on est dans le subjectif.

Une notation plus mathématique pourrait aussi être celle du lambda-calcul... est-ce mieux ou pire ? moins classique, c'est pratique pour limiter les parenthèses.

[Garulfo]

Mon cher Dr Topos,

il manque une version MacOS à Anubis -_-

[DrTopos]

Envoyé par Garulfo

Mon cher Dr Topos,

il manque une version MacOS à Anubis -_-

C'est juste et nous y avons pensé. Mais personne dans notre équipe n'a pratiqué le Mac. Peut-être es-tu candidat pour faire ce portage ? Si c'est le cas, tu es dix mille fois le bienvenu dans notre équipe.

Pour l'instant nous avons une version Windows, une version Linux et une version MIPS (non encore distribuée, mais dispo sur demande). Pour ma part je n'ai fait que la version originale (Linux), les portages Windows et MIPS sont de David René.

Faire un portage n'est pas un énorme travail. Il faut seulement bien connaitre la machine cible, en avoir une bien sûr, et avoir un compilateur C/C++ sur cette machine.

[Montaigne]

Envoyé par DrTopos

C'est juste et nous y avons pensé. Mais personne dans notre équipe n'a pratiqué le Mac. Peut-être es-tu candidat pour faire ce portage ? Si c'est le cas, tu es dix mille fois le bienvenu dans notre équipe.

Pour l'instant nous avons une version Windows, une version Linux et une version MIPS (non encore distribuée, mais dispo sur demande). Pour ma part je n'ai fait que la version originale (Linux), les portages Windows et MIPS sont de David René.

Faire un portage n'est pas un énorme travail. Il faut seulement bien connaitre la machine cible, en avoir une bien sûr, et avoir un compilateur C/C++ sur cette machine.

MacOS X est un Unix (une sorte de BSD, qui descend en majeur parti des premières heures de FreeBsd).
Donc si ça compile sous Linux avec Gcc en utilisant des librairies assez standard, ça devrait compiler sans trop de problème, avec Gcc, sous Mac..

Après, j'ai pas essayé..

[gorgonite]

Envoyé par Montaigne

Donc si ça compile sous Linux avec Gcc en utilisant des librairies assez standard, ça devrait compiler sans trop de problème, avec Gcc, sous Mac..

ben non, pas mal d'appels systèmes sont différents, mais on peut les récupérer (je crois) en utilisant l'entête "unix.h"

[BigTotoro]

Bonjour à tous,

Je suis David René, l'auteur des portages Windows, MIPS, BeOS, Zeta d'Anubis.
Effectivement le portage ne pose aucun problème en ce qui concerne le compilateur écrit quasiment en ANSI C avec des touches de C++. Par contre en ce qui concerne la machine virtuelle, la problématique vient de la couche graphique du système hôte. Mais, avec un peu de patience, du café, du paracetamol c'est faisable.
D'ailleurs pour Mac OS, est-ce que la couche graphique s'appuit sur Xwindow ou bien est-ce complètement différent?
Parce que si c'est XWindow le portage devrait être presque une formalité.
Par ailleurs, tout les candidats au portage d'Anubis sur différentes plate forme sont les bienvenues et peuvent soumettre leur candidature en m'envoyant un mail privé par (MP).