Discussion :

[gorgonite]

DrTopos est en vacances, ce sont des choses qui arrive, surtout pendant la période d'été.
Donc laissons lui le temps de rentrer afin de poursuivre le débat sur les points de détail que seul lui à le secret.

ça semblait évident, étant donné qu'il répond d'ordinaire très rapidement... et que les universitaires prennent souvent la période mi-juillet à mi-août

[SpiceGuid]

Et par rapport à d'autres langages fonctionnels à typage fort, genre Caml, Haskell ou F#, qu'apporte Anubis ?

À lire la documentation il semble qu'Anubis remplace les 'enregistements' OCaml par des étiquettes dans les types produits (ou agglomérations), je ne sais pas si l'idée est nouvelle (j'en doute) mais j'ai toujours trouvé que le type enregistrement est redondant avec le type produit et avec les classes.

Toute bonne idée, aussi minime soit-elle, est bonne à prendre si elle est séduisante et qu'elle résiste à l'épreuve du réel.

Dans ce sens l'expérimentation doit être encouragée plutôt que découragée, il est difficile d'être compétitif face aux meilleures offres déjà existantes, mais cela ne doit pas se traduire par trop de scepticisme. En tout cas la plupart de ceux qui ont commenté Anubis ont fait l'effort d'installer le compilateur, de lire la documentation, puis de se livrer à une batterie de test afin de donner honnêtement leur verdict en toute connaissance de cause. Ils n'ont rien rejeté à priori, si leur jugement a été trop sévère c'est en grande partie une réaction à la communication faite autour d'Anubis (qui, en caricaturant, tuerait les bugs comme Javel-la-croix tue les microbes).

[alex_pi]

À lire la documentation il semble qu'Anubis remplace les 'enregistements' OCaml par des étiquettes dans les types produits (ou agglomérations), je ne sais pas si l'idée est nouvelle (j'en doute) mais j'ai toujours trouvé que le type enregistrement est redondant avec le type produit et avec les classes.

J'ai pas vraiment réussi à comprendre comment cela fonctionnait avec Anubis, mais il me semble que quand tu as une aglomération, tu peux facilement en tirer le champ que tu veux en appelant le destructeur approprié. En revanche, il me semble que pour construire une aglomération, il faut connaitre l'ordre des champs, mais je me trompe peut être (je n'ai pas regardé beaucoup d'exemples de code à ce sujet.). Si c'est bien le cas, en tant que programmeur, je pense que c'est une erreur (sur le plan théorique, ça ne change évidement rien). Quand un enregistrement à de nombreux champs, dont plusieurs ont le même type, il me semble qu'il est beaucoup plus clair dans le code source d'indiquer le nom de chacun des champs. Et cela permet ensuite des sucres syntactiques tel quel

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
let newenr = {oldenr with champ42 = newValue}

[SpiceGuid]

Les accesseurs sont des fonctions, pas des constructeurs.
Pour construire il faut connaître l'ordre des champs puisqu'il s'agit d'un n-uplet.

Voilà un exemple pour illustrer comment ça marche:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

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
55
56
57
58
read tools/maybefloat.anubis

type Intersection:
  none,
  interval (Maybe(Float), Maybe(Float)).

type Vector:
  vector (Maybe(Float) x, Maybe(Float) y, Maybe(Float) z).

define Vector
  make (Vector a, Vector b) =
  vector (x(b) - x(a), y(b) - y(a), z(b) - z(a)).
  
define Maybe(Float)
  square (Vector v) =
  x(v) * x(v) +
  y(v) * y(v) +
  z(v) * z(v).

define Maybe(Float)
  prod (Vector a, Vector b) =
  x(a) * x(b) +
  y(a) * y(b) +
  z(a) * z(b).

define Maybe(Float)
  max (Maybe(Float) a, Maybe(Float) b) =
  if a > b then a else b.  

define Maybe(Float)
  zero = success(0.0).

define Intersection
  // Intersection d'un rayon s + tv, de source s et de direction v
  // avec une sphère de centre c et de rayon r
  ray_sphere (Vector s, Vector v, Vector c, Maybe(Float) r) =
  // Carré du rayon de la sphère
  with r2 = r * r,
  // Vecteur de la source au centre de la sphère
  with sc = make(s,c),
  // Carré de la distance de la source au centre de la sphère
  with sc2 = square(sc),
  with v2  = square(v),
  with p   = prod(sc,v),
  with p2  = p * p,
  // Carré de la distance du rayon au centre de la sphère
  with d2 = sc2 - p2 / v2,
  with delta = r2 - d2,
  if delta =< zero then
    none
  else
    with sq = sqrt (delta / v2),
    with t1 = p / v2 - sq,
    with t2 = p / v2 + sq,
    if t2 < zero then
      none
    else
      interval(max(zero,t1), t2).

Le mieux: on déclare le Vector avec la même syntaxe que les n-uplets.

Les moins:
1. Mon code OCaml faisait un alias type Point = Vector ensuite la source du rayon et le centre de la sphère étaient déclarés de type Point au lieu de Vector, je n'ai pas trouvé comment faire cela avec Anubis
2. Il n'y a pas de notation pointée, tu accède par la notation fonctionnelle habituelle, ça dois vite devenir illisible pour des calculs plus chargés

Note: pour que ce code compile j'ai du moi-même éditer tools/maybefloats.anubis, je reviens sur Maybe dans le post suivant

[SpiceGuid]

J'en viens à la "philosophie" de la "sécurité" en Anubis.

L'idée principale va à l'encontre de tous les principes établis: elle commande de signaler l'erreur au plus tard et même si possible de l'étouffer car comme dit le dicton: pas vu, pas pris.

Voici l'exemple sur lequel j'appuie cette opinion:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
// Ma comparaison
public define Bool
  Maybe(Int32) x < Maybe(Int32) y = 
    if x is  
      {
        failure then alert, 
        success(x1) then 
          if y is
            {
              failure then alert, 
              success(y1) then x1 < y1 
            }           
      }. 

// Mon programme
global define
  One main (List(String) args) =
  with n = (Maybe(Int32))1/0,
  with one = (Maybe(Int32))success(1),
  with two = (Maybe(Int32))success(2),
  if one < n then print("n > 1") else print("n =< 1");
  print("\n");
  if n < two then print("n < 2") else print("n >= 2");
  print("\n").

Ce code compile et s'exécute en générant une alert.
Mes remarques:
1. À l'exécution, n'importe quel langage arrêterait le programme à l'expression 1/0, sauf Anubis, Anubis pense que l'erreur est encore récupérable, alors il la perpétue aussi longtemps que possible.
2. La bonne nouvelle c'est qu'il ne la perpétue pas indéfiniment, une fois arrivé à la comparaison < il génère une alert comme je le lui ai demandé.

Donc Anubis signale l'erreur mais plus tard que les autres, la source de l'erreur sera donc plus difficile à localiser, Anubis est donc plus difficile à débogger.

Malheureusement l'erreur ne s'arrête pas là.
Il suffit de le lire dans predefined.anubis:

'alert' will disappear from version 2, because it becomes useless in the presence of
higher order logic (using mathematical statements and proofs). In version 2, such
problems may be detected at compile time.

Mais alors, avec Anubis 2, quelle valeur dois-je mettre en lieu et place de alert?
La réponse est donnée dans le fichier tools/maybefloats.anubis: je dois mettre false.

J'essaye alors avec false.
Dans ce cas l'erreur continue tranquillement sa progression, Anubis effectue la comparaison et il est même capable de termine le programme et tout fièrement il affiche:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
n =< 1
n >= 2

Et bien entendu il n'y a même plus à débogger puisque le programme ne fait plus d'erreur (selon lui).

[alex_pi]

Les accesseurs sont des fonctions, pas des constructeurs.
Pour construire il faut connaître l'ordre des champs puisqu'il s'agit d'un n-uplet.

Dans ce cas, je confirme ce que je disais, je pense que l'absence d'enregistrement avec des champs només à la construction est un gros manque. Avec des enregistrements, si pour une raison ou une autre je modifie mon type, le compilo "ne me lachera pas" pour reprendre une expression de ce fils avant que j'ai modifié chaque construction de l'enregistrement. Avec des simples n-uplets, si je n'ai pas modifié la taille et l'ordre des types (mais juste les significations), le compilo ne dira rien, et tout glissera sous le tapis. Et les accesseurs ne sont que des sucres syntactiques que l'ont peu reproduire trivialement.

[ricard33]

2. Il n'y a pas de notation pointée, tu accède par la notation fonctionnelle habituelle, ça dois vite devenir illisible pour des calculs plus chargés

En fait, la notation pointée fut l'une de nos demandes et apparait avec la version 1.8 (actuellement en phase bêta).

Donc avec la déclaration suivante (en reprenant ton exemple):

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
type Vector:
  vector (Maybe(Float) x, Maybe(Float) y, Maybe(Float) z).

tu peux accéder directement à chaque membre :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
define Maybe(Float)
  square (Vector v) =
  v.x * v.x +
  v.y * v.y +
  v.z * v.z.

Le '.' est une fonction définie dans "tools/basis.anubis" :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
public define $U
   $T x .$T -> $U f
     =
   f(x).

En revanche, je ne sais pas si cela fonctionne avec la version 1.7 car il est possible que la grammaire ait subit quelques modification pour supprimer l'ambigüité avec le '.' de fin de paragraphe (= fin de fonction).

[SpiceGuid]

En fait, la notation pointée fut l'une de nos demandes et apparait avec la version 1.8 (actuellement en phase bêta).

Merci.
Un petit mieux est toujours bon à prendre.

Mais la critique de alex_pi reste valable (et je la partage).
Je ne peux pas le justifier (puisqu'en théorie ça ne change rien) mais l'expérience (en tout cas la mienne) abonde dans son sens. L'élégance, au sens d'un minimum de moyens, et qui est une grande vertue, abonde au contraire dans le sens d'Anubis. Après c'est une question de goût.

Le problème de la sécurité me paraît bien plus crucial, parce qu'il est au coeur de l'approche de Dr Topos et qu'il résume assez bien tout ce qui sépare le catégoricien et le lambda-calculiste.


PS: et pour définir un type Point qui soit synonyme de Vector ?

[DrTopos]

Bonsoir à tous.

Effectivement, je suis en vacances, et me suis trouvé sans accès Internet pendant une semaine.

J'ai pu constater une intense activité sur ce fil, avec une petite montée de fièvre, qui est finalement retombée. Je crois qu'il est important que tout le monde reste courtois. On peut toujours critiquer, et même on doit le faire. C'est cela qui fait avancer les choses. Cela ne me gène en rien. Mais il vaut quand même mieux éviter les attaques personnelles. En particulier j'aurai à répondre sur ma ``méthode scientifique''.

Je n'ai parcouru ces pages que rapidement pour le moment, mais je répondrai dès demain:

• (1) sur ma méthode scientifique,
• (2) sur certains des points techniques concernant Anubis,
• (3) sur ce qui différencie Anubis 1 d'Anubis 2, et sur le rôle que jouent les topos dans tout cela.

En ce qui concerne les points techniques, je confirme que certaines des critiques faites par alex_pi sont tout à fait justifiées. Anubis 1 est loin d'être parfait. D'autres sont exagérées, ou mal renseignées (il y a quelques malentendus). Je suis bien d'accord avec lui: il y a quelques horreurs en Anubis. Mais bien entendu elles n'attendent qu'à être corrigées. Ce sera fait pour les plus voyantes d'entre elles dans la version 1.8. Ces horreurs ont par ailleurs une histoire, qui ne les justifie pas, mais qui en expliquent la provenance. J'en raconterai éventuellement quelques unes.

Merci bien sûr à ceux qui ont reconnu qu'Anubis contenait ``quelques idées intéressantes''.

Je tiens à dire tout de suite que je sais parfaitement que certains problèmes (comme de savoir si un terme vaut zéro) ne sont pas décidables par algorithme. Je ne prétends pas détenir des algorithmes miraculeux (qui seraient d'ailleurs en contradiction avec les résultats de Gödel et Turing). Pour ceux qui ne l'ont pas compris, je rappelle qu'Anubis 2 est un langage permettant l'écriture des énoncés mathématiques et des preuves (démonstrations). J'ai déjà eu l'occasion de discuter de ces question sur un autre fil de ce forum (en particulier, le post numéro 40 page 3).

A demain.

[DrTopos]

Bonjour.

On m'a reproché de ne pas avoir de méthode ``scientifique'', au titre que, créant un langage fonctionnel, je n'avais pas lu la littérature sur les langages fonctionnels.

Il est vrai que je n'ai pas lu toute la littérature sur ce sujet, mais enfin, j'en ai lu quand même un peu, et en particulier sur Lisp qui m'a occupé durant de nombreuses années. En fait, ce qu'on m'a plus précisément reproché est de ne pas bien connaître les détails des autres langages fonctionnels, et surtout d'avoir dit qu'ils ne m'intéressaient pas. C'est vrai qu'ils ne m'intéressent que modérément, car ce qui m'intéresse est d'avoir des fondements théoriques solides. Ce n'est pas dans ce genre de littérature qu'on les trouve. Il faut bien se rendre compte qu'un langage de programmation n'est qu'une réalisation particulière de certaines idées, mais pas la source de ces idées.

Ceci est d'autant plus vrai d'ailleurs, que Caml et Haskell (puisque c'est d'eux qu'il s'agit) ne sont pas fondés sur les catégories, quoi qu'on en dise. En effet, ils sont tous deux fondés sur ML, lui-même sans rapport avec les catégories, puisqu'il a été conçu comme un outil pour LCF, lui même sans rapport avec les catégories. Les monades et les foncteurs (qui sont bien des concepts catégoriques) n'ont été introduits qu'après coup (et en fait seulement certains aspects de ces concepts).

J'ai été d'ailleurs fortement etonné quand j'ai assisté à la création de Caml au début des années 80, du fait que Cousineau et Curien, qui avaient créé la machine virtuelle CAM (c'est à dire un langage de bas niveau) à partir de principes catégoriques, n'aient pas envisagé de créer un langage de haut niveau sur ces même principes. Ils ne sont probablement pas responsable de cet état de fait, car il ne sont sans doute pas à l'origine de l'initiative Caml.

Ma démarche est totalement différente. D'abord, je n'ai jamais eu l'intention de créer un langage fonctionnel. Anubis est fonctionnel par la force des choses, pas par intention. Je me suis rendu compte au cours des années 80 du caractère effectif des concepts catégoriques, et j'ai seulement voulu les mettre en oeuvre, quils soient fonctionnels ou non. Par conséquent, à motivations différentes, méthodes différentes. Cela va de soi.

Ceci dit, je voudrais me placer sur un plan plus général en ce qui concerne la méthode du chercheur. L'histoire a montré que la science progresse par ruptures. Galilée a rompu avec le modèle ptolémaïque, et a récusé la notion pourtant tellement ``évidente'' d'immobilité absolue. Einstein à récusé la loi pourtant tellement ``évidente'' de composition des vitesses. On pourrait multiplier les exemples. Ces gens là ont réussi à révolutionner la science précisément parce qu'ils ont été capables d'ignorer la culture ambiante. Ce n'est pas en imitant l'existant qu'on progresse. Ce n'est pas en croyant que ce qui est admis par la majorité (le dogme) est définitif et intangible qu'on progresse. Les gens qui font avancer les choses sont avant tout des iconoclastes. C'est une chose dont j'ai été persuadé dès mes débuts dans ce métier. Je vais peut-être être le premier à créer (avec Anubis 2) un langage basé sur les topos. Je ne vais certainement pas, alors que j'ai l'occasion de faire quelque chose d'original, m'obliger à respecter les dogmes à la mode. Je le répète: faire comme tout le monde ne m'intéresse pas. Si je n'avais pas sous la main une théorie capable de me conduire à un système original, je n'aurais sans doute jamais fait d'informatique.

Je crois que cette démarche est tout à fait respectable. Quant-à la question des publications, je n'ai effectivement rien écrit sur Anubis 1 (qui ne le mérite peut-être pas), par contre j'ai publié un papier en théorie des topos (``On the role of description'', Journal of Pure and Applied Algebra 2000) qui a un rapport étroit avec ce que je veux faire pour Anubis 2. Il y a aussi bien sûr mon récent exposé de Luminy, cité dans un post précédent.

[InOCamlWeTrust]

Créer un langage à partir de rien est une chose difficile, c'est vrai. Cependant, il y a surtout deux choses qui me dérangent dans les commentaires vus ici et sur le site d'Anubis.

La première chose est cette volonté accablante de vouloir démontrer qu'Anubis est meilleur que le C parce que patati-patata... Pourquoi se comparer à un autre langage ? Et pourquoi justement le C ? N'est-il pas évident que le C reste et restera encore longtemps un langage de choix pour un nombre colossal d'applications et de programmeurs ? Pourquoi, à titre d'argument, balancer des affirmations aussi gratuites que "Anubis est 40 fois plus rapide à débugger" (ce qui est faux : en deux mois de stage, je n'ai qu'un seul segfault et la seule partie posant problème concerne les aspects numériques), ou encore "Anubis est beaucoup plus robuste et sûr que le C" ?

La deuxième chose, concerne cette pointe de prétention, volontaire ou non dans les messages, qui donne un peu l'impression que DrTopos est le seul à posséder la vérité parce qu'elle lui est tombé du ciel on ne sait trop comment. Je crois qu'avant d'affirmer des choses comme "Caml ne repose sur aucune base théorique" ou encore "Les gens n'ont pas compris les types somme" (vu sur la page d'Anubis), il faudrait savoir ce dont on parle. Caml ne repose peut-être pas sur tes bases théoriques à toi, car ça tombe bien, les personnes de la Caml Team, à l'inverse d'autres, plutôt que de rester plantés là à admirer la théorie des autres, essayent d'en proposer une autre, qui fera peut-être un langage de demain. Bref, ce sont des gens qui ont compris depuis longtemps, je crois, que l'informatique est un domaine d'expérimentation.

P.S.: Caml, ça s'écrit C a m l et non C A M L.
Merci.

Signé: un chameau

[DrTopos]

Ce qui se trouve sur le site Anubis n'est pas de ma seule responsabilité mais de celle de l'équipe (c'est à dire en fait essentiellement David et moi). On n'est pas toujours d'accord sur ce qu'il faut mettre et on a parfois des discussions difficiles. David a une expérience de la vente de logiciel (dans plusieurs sociétés) que je n'ai pas. J'aurai plutôt tendance à modérer les affirmations, mais il paraît qu'en marketing il ne faut pas hésiter à marteler. Mais je suis d'accord avec InOCamlWeTrust on exagère un peu. On va changer cela. Ce n'est pas toujours facile de trouver le bon ton dès le début. De plus, on n'a pas retravaillé sur le site depuis plus d'un an, par manque de temps.

Le choix du C pour la comparaison vient essentiellement du fait qu'il faut comparer avec quelque chose que tout le monde connait. Il y a très peu de gens finalement qui connaissent Caml (et encore moins qui connaissent Anubis évidemment).

J'ai moi-même beaucoup programmé dans plusieurs langages de haut et de bas niveau (MASM, C, Lisp, Prolog, Anubis essentiellement). Dans le cas du bas niveau j'essaye toujours de me prémunir par des méthodes systématiques (disons un ``style'', par exemple, beaucoup d'assert en C, mais pas seulement évidemment) pour compenser les faiblesses du langage, mais même comme cela j'ai eu des séances mémorables de débogage. Je pense que le rapport de 40 est assez réaliste, mais c'est une estimation à la louche, et bien sûr il concerne deux langages très différents, et je comprends que le choix de cette comparaison soit choquant.

Par ailleurs, il ne me semble pas avoir affirmé que Caml ne repose sur aucune base théorique. J'ai seulement dit que ML ne repose pas sur les catégories. Reste à savoir où est la frontière en une théorie et un design. J'ai lu beaucoup de choses en logique depuis 20 ans, aussi bien dans la mouvance lambda-calcul/logique combinatoire de Curry, qu'en logique catégorique. Je maintiens ma position. Il y a une différence de profondeur conceptuelle très importante entre ces deux voies. La première est d'inspiration essentiellement syntaxique, et passablement exotique du point de vue mathématique, alors que la deuxième est profondément sémantique et proche des mathématiques usuelles. Il faut avoir touché aux deux pour s'en rendre compte, et cela demande des efforts. Des deux cotés il y a des choses ardues et difficiles à lire.

Je reviens sur cette dichotomie syntaxe/sémantique. Une chose qui me frappe avec la plupart des langages formels, et parmi eux le lambda-calcul originel de Church, est le fait que le langage est créé avec certes une idée derrière la tête (celle de fonction dans le cas de Church), mais pas d'idée précise sur la sémantique. Pour preuve les nombreux ``paradoxes'' avec les points fixes etc... Il aura fallu attendre le typage du lambda-calcul et le théorème de normalisation forte de Tait, pour que le lambda-calcul commence à avoir une sémantique solide. On voit passer de nombreux articles qui s'intitulent ``une sémantique pour tel langage''. Comment se fait-il que la langage préexiste à la sémantique ? C'est quand même étrange et pas naturel. Les langues naturelles par exemple, sont toutes postérieures à leur propre sémantique, en d'autres termes on a inventé des mots et des phrases pour représenter des objets qu'on connaissant parfaitement ou exprimer des faits de la vie courante. Au contraire, les systèmes comme ML, Martin-Löf, Coq (les constructions), etc... et même le système F de Girard, sont avant tout des conceptions syntaxique, et ceci surtout, il me semble, parce que les concepteurs raisonnent en terme de calcul (manipulation de nature syntaxique). Ma démarche est complètement différente. Je pars de la théorie des topos qu'on peut considérer comme une sémantique sans langage. En effet, l'exemple qui a inspiré cette théorie est le topos (la catégorie) des ensembles, c'est à dire l'univers des objets qui sont réellement les objets dont on veut parler. Dans cette théorie, tout a un sens. On n'a pas besoin de se demander ce que peut signifier telle ou telle expression. A contrario, elle paraît non effective, c'est à dire ne se prêtant pas au calcul (c'est d'ailleurs sans doute la raison pour laquelle elle n'a pas encore été utilisée pour le design d'un langage). Toutefois, c'est un fait établi qu'elle est effective (théorème de Burroni), et l'essentiel de mon travail a été de pousser cette idée aussi loin que possible. Le langage (je parle ici d'Anubis 2, mais la démarche a été la même pour Anubis 1) est donc postérieur à sa propre sémantique. Je trouve cette façon de faire non seulement plus naturelle, mais plus logique. On ne devrait pas créer un langage en se demandant ensuite ce qu'il peut signifier, mais le créer parce qu'on a besoin d'exprimer des choses qui sont déjà là.

Je n'ai effectivement inventé aucune théorie. J'ai simplement choisi la théorie des topos parce qu'elle m'a inspiré. Elle est le point de départ (et en fait avant elle la théorie des catégories, à l'époque où je ne connaissais pas encore les topos) de mon travail. Si les personnes de la Caml Team (dont tu fais peut-être partie) veulent en proposer une autre, très bien. Il y a de la place pour tout le monde. Ceci dit, la théorie des topos ne répond pas à toutes les question qu'on peut se poser quand on crée un langage de programmation, et en particulier les questions non déterministes (effet de bord), du moins compte tenu de la façon dont je l'utilise. Pour ces question, j'en suis moi aussi au stade expérimental. Ce qui explique évidemment pas mal de choses sur les quelques ratés d'Anubis 1.

[DrTopos]

J'en viens au remarques d'alex_pi.

Quand je dis que le filtrage n'est qu'une facilité d'écriture pour simplifier les emboîtements de conditionnelles, je parlais bien entendu des conditionnelles au sens d'Anubis, qui ont des symboles résurgents analogues à la liaison de variables que tu évoques. Il ne s'agit pas bien sûr du seul ``if then else''. Donc je maintiens ce que j'ai dit. En définitive, il y aura sans doute les mêmes facilités de filtrage en Anubis 2 qu'en Caml, mais la discussion que je voulais mener était surtout sur la justification théorique du filtrage. Le filtrage est né avec Lisp, et se trouvait dans ce langage assez bien justifié du fait que le langage est plongé dans son propre univers sémantique par le mécanisme quote/eval. Je fais remarquer que les types de listes sont des sommes (récursives bien sûr), ce qui est implicite en Lisp, puisqu'on n'a pas à les définir. Pour ma part, j'ai abordé la conception d'Anubis, sans rien savoir ou presque du filtrage, et j'ai conçu les conditionnelles d'Anubis d'après les propriétés équationnelles des problèmes universels (au sens de la théorie des catégories) qui définissent les sommes et les produits, puisqu'elles servent de destructeurs au deux. Ces conditionnelles sont donc parfaitement justifiées sur le plan sémantique. Il se trouve que le passage de ces conditionnelles au filtrage (exhaustif et exclusif) peut être vu comme une façon simplifiée d'écrire les emboîtements de conditionnelles (au sens d'Anubis, bien sûr). C'est tout. Il y aura donc du filtrage en Anubis 2 (ou quelque chose de similaire), non pas parce que j'imite Caml, mais parce que j'en ai une justification qui me satisfait, qui est un mélange de raisons sémantiques et de raisons pratiques. Dire, comme je me souviens de l'avoir lu dans un livre sur Caml, que le filtrage est une notion liée à la notion de fonction est parfaitement absurde, et démontre, n'en déplaise à certains, que la pensée des informaticiens (peut-être pas tous bien sûr) se situe plus à un niveau syntaxique qu'à un niveau sémantique.

Je ne pense pas avoir craché avec mépris, comme tu le dis, sur Haskell et sur Caml. J'ai simplement émis un avis, et je croyais avoir pris suffisamment de précautions oratoires pour ne blesser personne. Je ne les connais effectivement que par quelques lectures. Je ne les ai jamais utilisé.

Les exécutions devraient toujours être ``normales'', car l'anormalité signifie que le programme ne peut pas faire face à une situation particulière, autrement-dit que quelquechose n'a pas été prévu. De toute façon, ce qu'on appelle ordinairement ``exception'' est traité en Anubis par le moyen du typage. Cela rend la chose plus sûre, plus explicite, et nous fait faire l'économie d'un concept, ce qui n'est pas négligeable. On a écrit des millions de lignes d'Anubis qui fonctionnent très bien, et je crois par conséquent qu'on a largement fait la preuve qu'on peut programmer sans notion d'exception. J'applique le rasoir d'Occam (et dans mon enseignement mathématique aussi) autant qu'il m'est possible. Dans l'exemple que tu donnes, je comprends très bien ta réticence à gérer à la main le retour de l'exception dans toutes les fonctions appelées. J'ai toutefois, souvent fait ce genre de choses en Anubis, sans en avoir été épuisé. Toutefois, on peut très bien, même en Anubis, contourner le problème en définissant un produit de Kleisli qui permettra de composer une fonction de type T -> Maybe(U) avec une fonction de type U -> Maybe(V), le résultat de cette composition étant une fonction de type T -> Maybe(V). En fait, voila une monade qui pointe son nez. Je l'ai fait aussi. Mais en définitive je ne trouve pas le résultat plus clair à la relecture, même s'il est plus compact.

Toutes mes excuses pour ce qui est du script d'installation. Je ne suis pas un spécialiste d'Unix, encore moins du shell, et n'ai aucune prétention dans ce domaine. J'ai fait de mon mieux, et j'aimerais bien avoir un collaborateur connaissant bien ces question.

En ce qui concerne l'horreur des tableaux, je suis parfaitement d'accord avec toi. En fait, cela est même contraire à l'esprit du système. Au moment où j'ai fait cela, j'avais déjà bien expérimenté avec les Maybe, et j'avais envie d'essayer autre chose. C'était une mauvaise idée, et j'aurais du corriger cela. Comme personne n'utilisait ces tableaux, je n'y ai pas repensé. Tout à fait récemment, je les ai utilisés pour faire des hashtables, et j'ai conclu qu'il fallait revenir à de meilleures pratiques. Ce sera corrigé dans la prochaine version.

Ton exemple (la fonction 'foo') fait effectivement bouffer toute la mémoire. Je suis d'accord qu'il y a un problème. Toutefois, ma position n'est pas la même que la tienne. Je considère qu'une variable dont la valeur contient une variable dont la valeur contient la première variable est un non sens (une sorte de paradoxe). En tout cas, je ne peux pas lui trouver de justification théorique. C'est comme une boîte, qui en contient une deuxième qui en contient une troisième qui s'avère être la même que la première. On voit cela dans les films de fiction. Je sais qu'on va trouver des informaticiens théoriciens qui ont des théories pour expliquer cela. Mais je ne trouve pas cela convainquant. Donc la solution n'est pas selon moi de perfectionner le garbage-collector (ce que j'aurais pu faire, n'étant pas aussi ignorant de ce type de problème qu'on peut le croire), mais de trouver un moyen d'interdire de telles constructions. J'avais envisagé un système, que je voulais statique bien sûr, c'est à dire interdisant cela dès la compilation, mais il m'avait semblé trop restrictif (il était basé sur une détection de la circularité dans le typage). Je n'ai en définitive rien fait en ce qui concerne Anubis 1, mais je reconnais le problème. De toute façon, cette programmation n'est pas déterministe, et mon intention est d'encadrer très sévèrement la programmation non déterministe dans Anubis 2. J'ai quelques idées sur le sujet, mais n'ai pas encore pris de décision. Je fais remarquer que la théorie des catégories ne me dit pour le moment rien (ou pas grand chose) sur les question non déterministes, puisqu'elle modélise essentiellement des mécanismes purement mathématiques donc déterministes (je vais revenir sur le sens que je donne à ce terme plus loin).

Quand tu dis qu'Anubis est mauvais, évidemment cela ne me fait pas plaisir, mais là n'est pas question. Je reconnais qu'il a des défauts que je compte corriger bien sûr. Maintenant quand tu dis qu'il est inutilisable, je peux t'affimer que ce n'est pas vrai. Il est parfaitement utilisable, et les quelques programmes qui ont été faits avec en sont la preuve, par exemple, le site du langage Anubis lui-même, que tu as utilisé, et qui comporte plus de 20000 lignes de source. La mémoire n'est pas abusivement bouffée puisqu'on le laisse tourner sans le relancer, parfois pendant plusieurs mois. Les autres programmes qui ont été faits avec par Calexium et CRP Patrimoine fonctionnent sans problème.

Je te confirme que ton exemple 'print_string("kikoo") est non déterministe, puisque si tu l'exécutes deux fois, tu obtiendras deux kikoo à deux emplacements différents dans ta console. Cela ne dépend sans doute pas de la variable x, mais change l'état de la console. C'est clairement un effet de bord, donc non déterministe. En particulier, le terme 'print_string("kikoo") ne satisfait pas le critère que je donne dans la doc d'Anubis pour détecter si un terme est déterministe ou pas. Imprimer une fois "kikoo" n'est pas équivalent à l'imprimer deux fois. Par ailleurs, le vocablaire que j'emploie, à savoir déterministe/non déterministe me semble être tout à fait orthodoxe. Je l'ai appris il y a déjà bien longtemps dans des livres d'informatique théorique, mais peut-être que le vocabulaire a évolué depuis.

Pour ce qui est des entrèes-sorties et des Int8, j'avais à l'origine l'idée qu'on devrait pouvoir lire ou écrire des données de n'importe quel type, ce qui me semblait être raisonnable. Je n'ai implémenté que Int8 dans un premier temps, puis j'ai écrit des commandes dans basis.anubis pour traiter les autres cas. J'en suis donc resté là. Evidement, c'est incohérent, mais c'est encore un problème de jeunesse qui a d'ailleurs déjà été corrigé dans la version 1.8, où le paramètre de type a disparu.

Ton astuce sur la récursivité est intéressante, mais ce n'était pas mon propos dans la doc où je voulais présenter quelques possibilités de la programmation fonctionnelle d'un point de vue surtout pédagogique. Je n'ignore pas, pour avoir fait beaucoup de Lisp et d'Anubis, qu'il y a de très nombreuses astuces fonctionnelles. Je te fais aussi remarquer que quand je fais des cours de calcul différentiel (par exemple en L3 cette année), j'use et j'abuse du fonctionnel, évidemment fondamental dans cette discipline. Je déplore d'ailleurs que la plupart des étudiants en maths ignorent tout de l'informatique et de la programmation.

Je suis bien d'accord avec toi, certaines propriétés sont indécidables (il ne faut quand même pas me prendre pour un ignorant). Ce que tu n'as peut-être pas compris est qu'Anubis 2 permet la formalisation des énoncés mathématiques et des preuves, et que quand le compilateur ne trouve pas seul une preuve il l'exige de l'utilisateur (comme dans tous les systèmes à preuves: Coq, système B, pour ne citer que ceux-là).

Mon système de surveillance des variables et de tickets est totalement expérimental. Reconnais au moins qu'il est original. Je ne prétend pas qu'il persistera en Anubis 2, du moins pas sans de profonds changements. Prends-le seulement comme une idée à creuser. Je l'ai quand même utilisé avec succès dans un système (incomplet à ce jour) de widgets, mais il est sûr qu'il présente certains dangers et en particulier de deadlocks. Travail en cours, dirai-je.

Je me réjouis quand même que tu ais trouvé Anubis ``amusant'', même pour une journée. Allons, ne sois pas aussi catégorique. Si jamais tu te lances seul (parce que tes idées sont trop originales pour qu'on te suive) dans un projet de la taille d'un langage conçu par toi avec compilateur, machine virtuelle et tout le reste, je pense que tu et rendras compte que si on veut sortir quelquechose avant la fin de sa vie, il faut faire des concessions, quitte à les corriger plus tard.

[alex_pi]

On m'a reproché de ne pas avoir de méthode ``scientifique'', au titre que, créant un langage fonctionnel, je n'avais pas lu la littérature sur les langages fonctionnels.

Il est vrai que je n'ai pas lu toute la littérature sur ce sujet, mais enfin, j'en ai lu quand même un peu, et en particulier sur Lisp qui m'a occupé durant de nombreuses années.

Le langage Lisp fut inventé par John McCarthy en 1958

On ne se sent pas particulièrement à la pointe de la technologie là :-\

En fait, ce qu'on m'a plus précisément reproché est de ne pas bien connaître les détails des autres langages fonctionnels, et surtout d'avoir dit qu'ils ne m'intéressaient pas.

Personnellement, je ne pense pas qu'il faille connaitre tous les détails. Juste s'intéresser suffisement aux langages pour comprendre les choix qui sont faits et leurs raisons, histoire de ne pas commetre les erreurs que ces choix résolvent.

Il faut bien se rendre compte qu'un langage de programmation n'est qu'une réalisation particulière de certaines idées, mais pas la source de ces idées.

Ceci est d'autant plus vrai d'ailleurs, que Caml et Haskell (puisque c'est d'eux qu'il s'agit) ne sont pas fondés sur les catégories, quoi qu'on en dise.

A vous lire, hors théorie des catégories point de salut... Faut arrêter un peu...

. Einstein à récusé [...] Ces gens là ont réussi à révolutionner la science [...] Les gens qui font avancer les choses sont avant tout des iconoclastes. Je vais peut-être être le premier à créer [...]

Alors je sais, on m'a dit plusieurs fois que je ne mets pas une bonne ambiance sur ces fora, et qu'il faut éviter les attaques personnelles. Je suis d'accord. Mais là quand même ! Vous en arrivez à vous comparer à Galilée et à Einstein ? Parce que vous avez eu l'idée révolutionnaire de faire un langage
basé sur la théorie des catégories.

Pour les topos, personne n'y a jamais pensé, et c'est pourquoi on ne lit jamais

Toposes (or computable subcategories thereof) have often been thought the correct arena for programming language semantics.

Arrêtez cinq minutes de lancer des affirmations sans fondement à tout va (et cela recoupe le "martelage marketing" de votre site), ceci n'est définitivement pas une méthode scientifique.

[SpiceGuid]

@InOCamlWeTrust

Un site web est une vitrine, et par définition une vitrine c'est promotionnel.

@Dr Topos

Les monades et les foncteurs (qui sont bien des concepts catégoriques) n'ont été introduits qu'après coup (et en fait seulement certains aspects de ces concepts).

C'est ce que j'avais cru comprendre: les 'fonctor' de OCaml n'offrent qu'une petite partie des 'foncteurs' en théorie des catégories. Un peu de la même façon que les fonctions en C n'offrent qu'une petite partie des 'lambda abstractions'. C'est l'aspect le plus prometteur d'Anubis et au regard de cette (future) nouveauté le reste n'est que considérations syntaxiques.
Il est donc trop tôt pour critiquer certains choix qui n'ont éventuellement comme raison d'être que de faciliter (ou d'accélérer) le passable à un niveau supérieur d'abtraction.
Quand le "plus produit" sera là il sera bien temps de le mettre en pratique pour voir quelle syntaxe en tire le meilleur profit.

Cependant certains choix me paraissent tout de même critiquables dès aujourd'hui.
Par exemple l'utilisation 'abusive' de Maybe.
Maybe existe en Haskell, il existe en OCaml (il s'appelle option), et il n'est pas question de l'enlever.
Je comprends qu'un dictionary ne contienne pas forcément la key recherché, et je pense aussi qu'une requête dans un dictionnaire ne devrait pas échouer. Elle réussit toujours et elle renvoie found(value) ou alors elle renvoie not_found. Par contre l'idée que l'addition de deux Float ne renvoie pas un Float va à l'encontre de mon bon sens mathématique (même s'il n'est pas aussi affuté que le vôtre) tout en apportant aucune sécurité informatique.

Les considérations syntaxiques ont leur importance, par exemple:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
type Maybe($T):
  yes($T),
  no.

est le même type que celui de predefined.anubis mais me paraît meilleur, parce qu'une réponse négative est une bonne réponse, pas une failure.

Il n'y a pas de honte à écrire alert, je ne vois pas pourquoi Anubis génère si peu d'alert, la division par zéro doit générer un alert.

Ce qui m'inquiète dans les Maybe(Float) et autres Maybe(Int32) (dont la comparaison renvoie un Maybe(Bool) ce qui rend impossible la conditionnelle qui attend un Bool) c'est le rapprochement avec les nombres transréels si controversés.

[DrTopos]

Toposes (or computable subcategories thereof) have often been thought the correct arena for programming language semantics.

have often been thought ne veut pas dire qu'on ait effectivement fait quelquechose avec.

[InOCamlWeTrust]

Le choix du C pour la comparaison vient essentiellement du fait qu'il faut comparer avec quelque chose que tout le monde connait. Il y a très peu de gens finalement qui connaissent Caml (et encore moins qui connaissent Anubis évidemment).

Certainement, mais du coup la comparaison en devient complètement risible : c'est comme comparer un torchon et un éléphant... rien à voir ! De plus, étant donné que le C fonctionne différemment, on utilise rarement les mêmes algorithmes dans les deux langages (Caml, Haskell ou autre fonctionnel), donc les comparer n'a aucun sens.

Par ailleurs, il ne me semble pas avoir affirmé que Caml ne repose sur aucune base théorique. J'ai seulement dit que ML ne repose pas sur les catégories. Reste à savoir où est la frontière en une théorie et un design.

Je pense qu'il n'y en a tout simplement pas. Les théories ne sont là que pour essayer de mettre des mots sur des concepts et idées difficilement expliquables autrement. Je me considère un géomètre euclidien, et dans cet esprit, la théorie, le formalisme, n'a pas sa place, sinon parce que tout est théorie et que tout peut se réduire à l'état de théorie.

Faire un langage à sémantique forte (comme le C ou pire encore, FORTRAN) ou un langage dont la sémantique vient à posteriori, c'est au fond la même chose, à ceci près que la sémantique risque d'être beaucoup plus simple dans le deuxième cas car, étant donné que la syntaxe impose ses règles, elle les impose aussi d'une façon ou d'une autre sur la sémantique.

Un bon exemple en est le système de types du C et de Caml, ou Haskell (dans leurs versions "simples"), par exemple : en Caml, il y a une corrélation très forte entre la façon dont on écrit un type et la façon dont on l'interprète. En C, rien de tout cela : un gros document décrit tout ce que l'on peut construire, en fournit la syntaxe et au revoir tout le monde ! Etant donné une expression du langage, en suivant la façon dont l'expression est construite, on peut reconstruire le type de l'expression de façon entièrement transparente. Le C tente de faire la même chose (théoriquement, le type est conforme à l'utilisation), mais pêche trop souvent.

D'ailleurs, ce n'est pas pour rien que l'on parle de traduction dirigée par la syntaxe !

Si les personnes de la Caml Team (dont tu fais peut-être partie) veulent en proposer une autre, très bien. Il y a de la place pour tout le monde.

Non, je ne fais pas partie de la Caml Team, mais je sais un tout petit peu ce qui s'y trame ; entre autres, le fait de construire des bases pouvant regrouper l'approche objet, les modules/foncteurs et les enregistrements extensibles est à l'étude, entre beaucoup d'autres choses intéressantes.

Je crois que dans le domaine des langages de programmation, il ne faut pas chercher à trop formaliser : le but essentiel, est de rester naturel, ce que la dernière norme de FORTRAN (la 2003) fait à merveille, pour prendre un exemple récent.

[DrTopos]

@alex_pi

je crois que tu es franchement de mauvaise foi. Il est très facile en déformant les propos des autres de leur faire dire n'importe quoi.

Je ne me suis pas comparé à Galilée ou Einstein. J'ai simplement fait une remarque sur la façon dont leurs idées se trouvaient en opposition avec la science d'alors. Et ce ne serait même pas se comparer à eux que de les prendre pour modèles, ce que je ne fais même pas.

Je connais la thèse d'Hagino, en fait depuis qu'elle a été écrite. C'est David Rydeheard qui me l'a communiquée. Elle n'est pas basée sur les topos. Hagino avait l'idée de généraliser l'utilisation des foncteurs adjoints, en implémentant en mécanisme général pour les construire. Ce n'est pas pareil.

Je le répète, haskell n'a pas été conçu d'après la théorie des catégories, mais bien entendu, on en a trouvé une interprétation catégorique après coup. De toutes façon la théorie des catégories est tellement générale, qu'on peut l'appliquer à beaucoup de choses, et pas seulement en programmation.

Tu penses bien par ailleurs que je connais Barr et Wells. Encore une fois, tu me prends pour un ignorant.

Si tu continues à être de mauvaise foi, à déformer mes propos, et à me provoquer, je cesserai de te répondre.

[alex_pi]

Quand je dis que le filtrage n'est qu'une facilité d'écriture pour simplifier les emboîtements de conditionnelles, je parlais bien entendu des conditionnelles au sens d'Anubis, qui ont des symboles résurgents analogues à la liaison de variables que tu évoques.

Effectivement, la conditionnelle Anubis étant, disons, une forme simplifié de ce que j'appellerai informellement filtrage, je suis d'accord que le filtrage est un sucre syntactique pour emboîtement de vos conditionnelles.

Pour ma part, j'ai abordé la conception d'Anubis, sans rien savoir ou presque du filtrage,

Je sais que je me répète, mais encore une fois, dire que l'on conçoit un langage mieux que les autres, et dire qu'on ne sait rien des autres est fortement contradictoire.

Il y aura donc du filtrage en Anubis 2 (ou quelque chose de similaire), non pas parce que j'imite Caml,

Et ça aussi il faut arrêter. C'est normal, et même sain en recherche de s'inspirer de ce qu'on fait les autres, personne ne vous le reprochera, au contraire.

Je ne pense pas avoir craché avec mépris, comme tu le dis, sur Haskell et sur Caml. J'ai simplement émis un avis, et je croyais avoir pris suffisamment de précautions oratoires pour ne blesser personne. Je ne les connais effectivement que par quelques lectures. Je ne les ai jamais utilisé.

Disons que vos simples avis sont souvent ponctués de "contrairement à ce que l'on peut lire", "c'est profondément absurde" et autre "je suis le premier" qui finissent par lasser. Surtout quand la conclusion est "mais en fait je n'en sais rien puisque je ne les ai jamais utilisés".

Les exécutions devraient toujours être ``normales'', car l'anormalité signifie que le programme ne peut pas faire face à une situation particulière, autrement-dit que quelquechose n'a pas été prévu.

La question qui se pose est "faites vous un langage de programmation purement théorique ou voulez vous que des *gens* l'utilisent ?". Parce que si c'est le second cas, il va falloir vous faire une raison, les gens ne pensent pas à tout. Par exemple, pour le premier défi des langages fonctionnelles, j'ai ajouté une fonction de mémoization. J'avais envie de modifier le moins possible mon code, j'ai donc fait ça à la mode impérative, en mettant les valeurs de retour de la fonction dans un tableau. Petit hic, la valeur d'entrée de mon programme étant lu sur la ligne de commande, la taille de mon tableau n'est pas connue lors de la définition de ma fonction de mémoization, et je ne peux donc pas instancier le tableau dans une variable globale. Qu'à cela ne tienne, je mets une référence sur un tableau de taille nul qui sera instancié par la fonction main(). Je fais mon ptit bazar, je lance le programme, et BOOM, instantanément, il se banane. "Exception: Invalid_argument "index out of bounds".". J'avais oublié de changer mon tableau. Je m'en suis rendu compte instantanément. En anubis, puisqu'il n'y a pas d'exception et que tout se passe toujours bien, que ce serait-il passé ? Le tableau n'aurait pas été de taille nulle mais de taille 1, j'aurais toujours accédé à la même case, j'aurais mémoizé n'importe quoi, et mon programme aurait eu n'importe quelle valeur de retour.
Il ne faut pas se leurrer, le programmeur ne pense pas à tout, et le langage doit l'aider. Et une bonne méthode est de lui mettre une grosse baffe rapidement quand il fait une erreur, pour corriger au plus vite. Et rien de telle qu'une bonne exception pour ça.

De toute façon, ce qu'on appelle ordinairement ``exception'' est traité en Anubis par le moyen du typage. Cela rend la chose plus sûre, plus explicite, et nous fait faire l'économie d'un concept, ce qui n'est pas négligeable. On a écrit des millions de lignes d'Anubis qui fonctionnent très bien, et je crois par conséquent qu'on a largement fait la preuve qu'on peut programmer sans notion d'exception. [...] J'ai toutefois, souvent fait ce genre de choses en Anubis, sans en avoir été épuisé.

Je suis actuellement en stage, et nous développons un langage de programmation (oui, nous aussi :-) Mais ce n'est pas un langage généraliste, il est très loin d'être turing complet, bref, rien à voir.). Et un jour, nous avons rajouté un test de typage sur les valeurs d'entrée. Ce tests s'effectue au niveau d'une fonction qui est appelé après un emboîtement dans une quinzaine d'autre fonctions. Grâce aux exceptions, le typeur vérifie le type, s'il est correct (exécution *normale*), on continue, sinon on lance une exception, qui est rattrapée à la racine des appels, qui affiche un message d'erreur et interromps le programme. En Anubis, on aurait du modifier les 15 fonctions, ainsi que tous les types de retour, pour ajouter une alternative "le typage s'est mal passé". Manque de bol il y a plein d'autres erreurs possibles. On se trouverait alors avec des types long comme le bras, des tests à chaque niveau etc. Alors qu'il suffit de lancer une exception en cas d'entrée exceptionnelle, et de faire un seul filtrage à la racine. Ceci permet un découpage logique du code, entre le flux normal, et la gestion des erreurs, les deux étant proprement séparés.

Parce que ce qu'il faut bien comprendre quand même, c'est qu'un programme est sensé travailler sur une entrée que lui fourni un utilisateur. Et qu'il n'est pas toujours possible de filtrer cette entrée dès la racine, et que l'on peut s'apercevoir de certaines erreurs finalement assez tard.

En ce qui concerne l'horreur des tableaux, [...] Ce sera corrigé dans la prochaine version.

D'accord

Ton exemple (la fonction 'foo') fait effectivement bouffer toute la mémoire. Je suis d'accord qu'il y a un problème. Toutefois, ma position n'est pas la même que la tienne. Je considère qu'une variable dont la valeur contient une variable dont la valeur contient la première variable est un non sens (une sorte de paradoxe). [...] On voit cela dans les films de fiction. Je sais qu'on va trouver des informaticiens théoriciens qui ont des théories pour expliquer cela. Mais je ne trouve pas cela convainquant. Donc la solution n'est pas selon moi de perfectionner le garbage-collector (ce que j'aurais pu faire, n'étant pas aussi ignorant de ce type de problème qu'on peut le croire), mais de trouver un moyen d'interdire de telles constructions.

Et voilà, encore un exemple de ce que je n'aime vraiment pas dans votre approche. Tout est dans la phrase

Je sais qu'on va trouver des informaticiens théoriciens qui ont des théories pour expliquer cela. Mais je ne trouve pas cela convainquant.

Vous ne trouvez pas cela convainquant avant même d'avoir écouté :-\
L'informaticien extrêmement théorique qui est en moi va donc vous parlez d'une notion à la pointe de la pointe de la recherche totalement non appliqué en informatique : le graphe.
Un graphe est un objet très abstrait que personne n'envisagerait d'utiliser par exemple pour implémenter des reconnaissances d'expression régulière par le biais d'automate. Mais néanmoins, bien qu'objet fantasmagorique issus de l'imagination maniaque d'un chercheur fou, il arrive parfois que ces graphes, qui auraient plus leur place dans un épisode de série Z, soient cycliques. Et là, si dans un délire psychotique, il me venait à l'esprit d'implémenter cela en Anubis, le garbage collector serait incapable de le récupérer. Mais j'attends avec impatience la suppression des types récursifs, qui me permettront d'éviter un tel non sens.

Je te confirme que ton exemple 'print_string("kikoo") est non déterministe, puisque si tu l'exécutes deux fois, tu obtiendras deux kikoo à deux emplacements différents dans ta console.

Vous dites que lorsque je fais deux fois une action, j'ai deux fois le résultat de cette action, ce qui signifie que mon action est non déterministe ? Je ne vous suis vraiment pas.

Cela ne dépend sans doute pas de la variable x, mais change l'état de la console.

L'état de la console ne fais pas parti de mon programme, et n'a rien à voir avec les notions de déterminisme ou non de mon programme. A ce compte là, rien n'est déterministe, parce que si le système n'a plus de mémoire ou crash lors de l'exécution d'une fonction, le résultat n'est pas le même que s'il n'avait pas crashé :-\

Ton astuce sur la récursivité est intéressante, mais ce n'était pas mon propos dans la doc où je voulais présenter quelques possibilités de la programmation fonctionnelle d'un point de vue surtout pédagogique.

Il me semble bien plus pédagogique de mettre le doigt sur la très forte réutilisabilité d'un code fonctionnel polymorphe, mais disons que ça se discute.

Ce que tu n'as peut-être pas compris est qu'Anubis 2 permet la formalisation des énoncés mathématiques et des preuves, et que quand le compilateur ne trouve pas seul une preuve il l'exige de l'utilisateur (comme dans tous les systèmes à preuves: Coq, système B, pour ne citer que ceux-là).

Effectivement, pour l'instant Anubis2 n'est pour moi qu'une vue de l'esprit, puisque l'on ne sait rien de lui.

Mon système de surveillance des variables et de tickets est totalement expérimental.

Peut être faudrait-il le préciser ? On retombe toujours sur le même problème. Anubis est un prototype, un jouet dont vous vous servez pour appliquer des théories qui vous plaisent. Il n'y a rien à critiquer là dedans. Le problème est que vous le présentez comme un langage aboutit, pleinement fonctionnel (au sens de "qui marche vachement bien"). Si vous l'aviez présenté honnêtement, en disant ce qu'il est, je me serais fait un plaisir de souligner le plus gentiment du monde tous ce que j'aurais considéré comme étant une erreur, pour apporter une modeste contribution à un projet de grand ampleur. Ce n'est malheureusement pas le cas.

[Nemerle]

Quel sujet-fleuve!! J'ai parcouru quelques échanges, mais tout lire!!!!

Juste 2 remarques:

1. Une futile: la théorie des topos, que l'on doit à Alexandre Grothendieck, fait partie de la géométrie algébrique (ah! les cohomologies étales!); elle n'a été à raison reprise en logique que peu de temps après.

2. Une pratique: ancien catégoricien, je loue la création d'Anubis. Mais de façon purement "business", je préfère m'adosser à des companies qui se "couvrent" lorsque de gros développements sont nécessaires. DONC, esclave de 'Crosoft, je préfère me pencher dans le détail sur la technologie LINQ plutôt que sur Anubis.