Discussion :

[alex_pi]

Voici un exemple qui me semble significatif de l'utilité de pouvoir surcharger les constructeurs (tag-names en ocaml).

Dans le fichier 'library/web/making_a_web_site.anubis', il y a toute une interface avec l'HTML (qui fait qu'on écrit jamais une ligne d'HTML pour faire un site). Dans cette interface, j'ai poussé le vice (si j'ose dire) jusqu'à définir deux types différents pour représenter en Anubis les éléments HTML qui sont dans un formulaire et ceux qui sont hors de tout formulaire. Mon idée était d'obliger à respecter la règle de la norme HTML4 qui interdit d'imbriquer les formulaires.

Je conseille de jeter un oeil à Ocsigen qui permet d'écrire des programmes *statiquement* typés assurant que le code produit sera intégralement du XHTML 1.1 strict. On est un ou deux niveaux aux dessus de l'imbriquation de formulaires.

[SpiceGuid]

Les données cycliques je les considère comme l'équivalent (pour les données) de la récursion mutuelle (pour les fonctions). Autant dire que je n'envisage pas d'y renoncer, ou alors il faudrait m'expliquer pourquoi la récursion mutuelle est devenue obsolète.

Ce n'est pas parce que vos utilisateurs actels ne vont pas prostester que "ça ne sert à rien", le langage doit bien entendu élargir sa base d'utilisateurs sans devenir trop permissif. Interdire n'est pas une qualité en soi, il n'y a rien de honteux à remplacer le comptage de références par un mark & sweep.

Ma liste du père noël pour le langage:

• une plus grande facilité pour créer des données cycliques
• une simulation des enregistrements (par les n-uplets) encore plus poussée
• une simulation des exceptions encore plus poussée
• le filtrage exhaustif

Et pourquoi pas des facilités de preuves (notamment pour les invariants structurels) avec égalités et inégalités.

Et puis ma liste du père noël pour l'implémentation:

• un ramasse-miettes mark & sweep
• un interpréteur interactif
• un compilateur vers du code natif

[DrTopos]

Les données cycliques je les considère comme l'équivalent (pour les données) de la récursion mutuelle (pour les fonctions).

Je ne suis pas de cet avis, et je m'en expliquerai dans un prochain post consacré aux données cycliques.

une plus grande facilité pour créer des données cycliques

En Anubis 2 il n'y aura pas de données cycliques, car cela mettrait à mal la logique. J'expliquerai tout cela comme je l'ai promis, et aussi pourquoi, quand on veut faire un graphe (comportant éventellement des cycles bien sûr), il vaut mieux le faire sans données cycliques.

une simulation des enregistrements (par les n-uplets) encore plus poussée

Je ne vois pas très bien de quoi tu veux parler.

une simulation des exceptions encore plus poussée

Ici aussi il faudra préciser ta pensée. Tu sais qu'en Anubis il n'y a pas d'exception et que c'est la façon de typer qui en tient lieu. En Anubis 2 ce sera encore différent à cause de la présence de nouveaux types qui permettent d'introduire la logique mathématique. Dans la proposition que j'ai envoyée au comité 'défis fonctionnels', je propose un jeu logique et fonctionnel qui décrit ces types.

le filtrage exhaustif

Pas de problème. Il y aura possibilité de condenser les imbrications de conditionnelles (qui sont déjà exhaustives) sous forme de filtrage.

Et pourquoi pas des facilités de preuves (notamment pour les invariants structurels) avec égalités et inégalités.

Il y aura mieux que cela, puisqu'il y aura toute la logique mathématique aussi bien constructive que classique.

un ramasse-miettes mark & sweep

J'ai prévu qu'on puisse choisir son type de GC à la compilation (sous forme d'option). Il y en aura plusieurs sortes. Peut-être qu'une au début, mais les collaborations seront bienvenues. Ceci-dit, le GC générationnel est le successeur logique du mark & sweep, qui présente aujourd'hui peu d'intérêt.

un interpréteur interactif

Tu le feras toi-même. Quand il y aura le système de macros (inspiré de Lisp) ça sera facile. Ce que je trouve plus intéressant (j'y travaille aussi) est un éditeur graphique sous lequel le compilateur travaille en continu, pour vérifier la syntaxe et la sémantique en temps réel.

un compilateur vers du code natif

Tu penses bien que je ne penses qu'à ça. C'est au centre de mon travail actuel.

[SpiceGuid]

Je n'insisterai pas davantage sur les données cycliques, je préfère vous laisser l'initiative de l'innovation et/ou de l'explication.

Voici les précisions demandées, l'une porte sur les agglomérations l'autre sur les alternatives:

• Il nous a été dit qu'il est prévu pour la version 1.8 de pouvoir accéder aux composantes d'une agglomération par la notation pointée, cette idée a été favorablement accueillie. Il serait élégant que la construction d'une agglomération soit également possible en associant une valeur à chacune des composantes, de sorte que l'ordre des composantes n'intervienne plus du tout dans la construction (cette idée a été proposée par alex_pi). De manière cohérente la même facilité serait offerte dans les motifs (d'un filtrage) de sorte que l'ordre des composantes n'intervienne plus du tout dans la déconstruction.
  De cette façon on pourrait librement choisir entre la contrainte de respecter l'ordre de toutes les composantes ou la contrainte de nommer toutes les composantes.
  L'ambition est de rendre, autant que possible, obsolète et redondant le type enregistrement tel qu'il existe en Caml.
• Plusieurs intervenants ont fait la remarque selon laquelle il faut 'capturer' une sorte d'exception my_error("mon message d'erreur") dans toutes les fonctions (à cause du filtrage exhaustif), or la plupart du temps cette capture prends la forme suivante:
  

  Code :

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

  1
  2
  3
  4
  5
  6
  7
  if expr is
  {
  ... 
  my_error1(msg) then my_error1(msg),
  my_error2(msg) then my_error2(msg)
  }

  L'idée serait d'automatiser ce code en déclarant un filtrage par défaut pour certaines alternatives, lorsqu'il est compatible avec le type de la conditionnelle, exemple ici avec le type Expr:
  

  Code :

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

  1
  2
  3
  4
  5
  type Expr:
    ...,
    my_error1(String msg) then my_error1(msg),
    my_error2(String msg) then my_error2(msg).

  Le filtrage reste totalement exhaustif.
  L'ambition est de rendre, autant que possible, obsolète et redondant le type exception tel qu'il existe en Caml.

Bien entendu aucune de ces deux propositions n'a d'intérêt théorique, il ne s'agit que d'extensions de confort destinées à mieux recouvrir des facilités qui ont fait leurs preuves, sans recourir à l'ajout de nouvelles constructions.

[DrTopos]

Il est possible en effet que la définition que j'ai donnée de la notation pointée ne compile pas en version 1.7 (où le point ne doit pas être reconnu comme opérateur binaire).

Pour ce qui est des problèmes de lourdeur du genre:

Code :

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

1
2
    failure then failure,

ou

Code :

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

1
2
    error(msg) then error(msg),

on peut les résoudre en définissant un produit de Kleisli (un pour Maybe et un pour Result), de la façon suivante:

Code :

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

1
2
3
4
5
6
7
8
9
define $T -> Maybe($V)
    $T -> Maybe($U) f * $U -> Maybe($V) g
        =
    ($T x) |-> if f(x) is 
                     {
                        failure then failure, 
                        success(y) then g(y)
                     }.

Pour Result, cela donne:

Code :

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

1
2
3
4
5
6
7
8
9
define $T -> Result($E,$V)
    $T -> Result($E,$U) f * $U -> Result($E,$V) g
       = 
    ($T x) |-> if f(x) is 
                    {
                        error(msg) then error(msg), 
                        ok(y) then g(y)
                    }.

Dès lors, on peut composer des fonctions produisant des exceptions en écrivant f * g sans se preoccuper de transmettre l'exception à chaque fonction. On remarquera que les monades d'Haskell ne sont pas loin. En fait (f * g)(x) correspond à quelquechose comme (f x) >>= g en Haskell, où >>= est le 'bind' de la monade de Maybe.

Mais là encore, je ne sais pas si la syntaxe de la version 1.7 le supporte.

Il est largement temps que la 1.8 sorte. Si elle ne sort pas, c'est qu'on a encore du travail dessus, et que par ailleurs on est débordé par toutes sortes d'autres activités. Je ne peux rien promettre, mais on fait le maximum.

[DrTopos]

J'en viens donc aux données cycliques.

Certains d'entre vous ont l'impression que c'est seulement le fait que j'ai choisi un
GC par incrément-décrément qui me fait avoir cette position anti-données cycliques, et
que cela serait donc une mauvaise raison. Ce n'est pas du tout cela. Je réalise des
interpréteurs et compilateurs depuis plus de 20 ans maintenant, et je sais que le GC
par incrément-décrément ne gère pas les cycles depuis que j'ai réfléchi à cette
question pour la première fois, c'est à dire vers 1985. A cette époque j'ai réalisé un
interpéteur Lisp avec un GC mark & sweep. En 1988, je l'ai bootstrapé en réécrivant le
compilateur en Lisp et je l'ai muni d'une machine virtuelle (écrite en assembleur 16
bits !) avec un GC par incrément-décrément. J'ai réalisé par ailleurs un compilateur
Prolog vers 1995, qui produisait du code pour une variante de la WAM (Warren's Abstract
Machine) et j'ai fait Anubis en 2000. Tout cela pour dire que j'ai eu de nombreuses
occasions d'être confronté au choix d'un GC, que je suis au courant de ce qui se fait
pour avoir lu de nombreux documents sur le sujet, et que si j'ai choisi
l'incrément-décrément pour Anubis, ce n'est pas au hazard.

En fait, mes motivations anti-données cycliques sont surtout de nature théorique (même
si je vais donner aussi plus loin quelques arguments de nature pratique). Mes
motivations pro-GC par incrément-décrément sont aussi essentiellement de nature
théorique. Mes arguments ne font que refléter ma formation de matheux (et de logicien)
alors que la position des pro-données cycliques est très clairement une conséquence de
leur culture essentiellement fondée sur la programmation (et sans doute aussi sur le
choix de certains langages de programmation).

Je comprends qu'on puisse penser ``pourquoi s'en priver puisqu'on l'a et que ça
marche''. Je pense que ceux qui commencent à me connaître auront compris que je ne
raisonne pas de cette façon, et que les maths et la logique mathématique (et en
particulier la logique constructive) jouent un rôle de premier plan dans ma façon de
voir les choses.

Je vais commencer par les arguments de nature pratique, parce que ce sont peut-être
ceux qui seront les plus convainquants pour des développeurs.

Alex_pi a parlé d'arbre et de pointeur pour remonter au père. J'ai très souvent
programmé avec des arbres et autres structures récursives similaires, et je n'ai jamais
eu besoin d'une telle chose. La programmation avec les données des types récursifs se
fait par des fonctions définies récursivement. C'est normal. D'ailleurs, en Théorie des
Catégories, on définit les types récursifs par un problème universel (un type récursif
est un objet initial dans une catégorie de diagrammes appropriée), et cette définition
définie en même temps un schéma de récursion (duquel on peut d'ailleurs déduire le
schéma de récursion primitive asssocié au type), qui nous dit comment programmer avec
les données de ce type. Comme les problèmes universels caractérisent les objets qu'ils
définissent, il est clair qu'on n'a besoin de rien d'autre pour programmer. La remontée
au père dans un arbre se fait au moment du retour de l'appel récursif (quand il est non
terminal). En fait, on sait comment revenir au père tout simplement parce qu'on a
empilé une addresse de retour dans la pile avant de quitter ce père. Remonter au père
par des pointeurs reviendrait à ignorer les principes mêmes de la programmation
récursive (c'est à dire essentiellement à faire des récursions sauvages ne satisfaisant
pas le schéma de récursion) et à les remplacer par des promenades dans un arbre devenu
un graphe, avec tous les alea que cela comporte. Dans ces conditions inutile de
continuer à utiliser un langage fonctionnel, on peut tout aussi bien le faire avec un
impératif de base. Cela ne sera pas plus dangereux.

Par ailleurs, si on implémente un graphe avec des cycles de références (i.e. de
pointeurs), on rencontre au moins deux problèmes (indépendamment du GC): (1) On doit
avoir au moins une référence sur un sommet de ce graphe, sinon on ne peut rien faire de
son graphe. On privilégie donc un sommet pour des raisons d'implémentation, alors que
le problème qu'on a à traiter ne l'impose sans doute pas. (2) C'est même pire que cela,
car si par exemple le graphe a trois sommets A, B et C et deux arêtes, une de A vers B
et une de C vers B:

Code :

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

1
2
   A -----> B <----- C

Il n'existe aucun sommet du graphe qui permette d'atteindre tous les autres.
Evidemment, le problème se complique encore quand le graphe n'est pas connexe. En
définitive, on va être obligé de mettre tous les sommets du graphe dans une liste (non
cyclique) ou un tableau, et là on va s'apercevoir qu'en définitive les cycles de
pointeurs ne servent à rien.

La bonne façon de représenter des graphes est celle que j'ai toujours vue appliquer
partout, à savoir qu'on réserve un tableau (ou une liste ou un B-tree) pour y mettre
pour chaque sommet du graphe les informations liées à ce sommet, y compris la liste des
arêtes qui partent de ce sommet. La cible d'une de ces arêtes est tout simplement
l'indice du sommet cible dans le tableau (ou une clef dans le cas des listes ou des
B-tree). Autrement-dit, bien que le graphe soit tout à fait général et puisse contenir
des cycles d'arêtes, l'implémentation ne demande aucune donnée cyclique.

Si on regarde par exemple l'automate (qui est un graphe avec des cycles) fabriqué par
YACC/BISON, on constate qu'il sagit d'un ensemble de tableaux ne contenant que des
nombres. De même, bien sûr pour l'automate fabriqué par LEX/FLEX. J'ai réalisé en
Anubis un programme analogue à BISON (qui fabrique d'ailleurs exactement le même
automate que BISON pour la même grammaire) et bien entendu je suis obligé de gérer un
graphe qui contient des cycles. Le graphe n'est rien d'autre qu'une liste de ses
sommets, avec dans chaque élément de la liste les données pertinentes, y compris la
liste des transitions vers les autres états de l'automate. L'automate est plein de
cycles, mais il n'y a aucune donnée cyclique fabriquée en mémoire.

Je pourrais donner d'autres exemples, mais je crois que ceux-ci devraient suffire à
convaincre que même si on souhaite avoir des données cycliques, on peut s'en
passer. D'ailleurs, en ce qui concerne les graphes, je crois qu'on doit s'en passer, vu
les problèmes que j'ai évoqués plus haut.

Les données cycliques sont par ailleurs en lien avec la notion de programmation
déterministe. C'est une chose qui est bien connue depuis les débuts de Lisp. Si on fait
une paire en Lisp, disons (a . b) on calcule a, puis on calcule b, puis le système
alloue un petit segment de mémoire pour y mettre a et b cote à cote. Par la suite, les
deux emplacements contenant a et b ne changent jamais de valeur tant qu'on n'utilise
pas les fonction rplaca et rplacd (appellées ``chirurgicales'') qui opèrent un
remplacement destructif de la tête ou de la queue de la paire, et qui sont donc par
essence non déterministes. Autrement-dit, sans chirurgie (et sans effet de bord) la
programmation Lisp est complètement déterministe. C'est ce qu'on appelle du
``fonctionnel pur''. Il est facile de prouver que dans ces conditions, aucune donnée
cyclique ne peut être crée. En effet, ceci résulte du fait que le segment alloué pour
la paire (a . b) est ``plus jeune'' que les segments qui ont alloués pour construire a
et b. Les références vont donc toujours des plus jeunes vers les plus vieux, ce qui
interdit les cycles. Sauf bien sûr, si on fait de la chirurgie, car alors on peut
placer dans un segment un pointeur sur un segment plus jeune que lui.

D'ailleurs, à ce sujet, je ferai une remarque sur Haskell, qui se dit ``langage
fonctionnel pur'' tant qu'on n'utilise pas de monade (puisqu'il enferme les effets de
bord dans les monades). En Haskell, on peut écrire:

Code :

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

1
2
   ones = 1 : ones

ce qui fabrique une liste ``infinie'' de 1. En fait, bien sûr c'est une donnée
cyclique. Cette donnée est nécessairement fabriquée par chirurgie, puisque ones ne peut
pas être contruit complètement au moment où on alloue le segment pour ones. Le fait de
mettre dans la queue de cette liste cette liste elle-même est une chirurgie. Par
conséquent, c'est non déterministe puisque c'est une affectation et par conséquent
Haskell n'est pas un langage fonctionnel pur, même sans utilisation des monades. C'est
un effet pervers des données cycliques.

J'en viens maintenant à des arguments en lien avec la volonté de concevoir un langage
incluant des mécanismes de preuve. Ce n'est pas le cas d'Haskell ni de Caml, ni
d'Anubis 1. Mais c'est le cas d'Anubis 2. Il existe, parait-il, 17 systèmes de
formalisation de preuves, dont COQ, Nuplr, HOL, Isabelle, PVS, etc... Ces systèmes sont
soumis à des contraintes bien plus sévères que les langages fonctionnels. En effet, si
on inclus des mécanismes de preuve, c'est pour prouver quelque chose à propos des
données qu'on manipule dans le langage, sinon ça ne sert à rien. On utilise donc ces
données dans les preuves. Si ces données créent des incohérences logiques, on rend
l'énoncé ``faux'' démontrable dans le système, donc tout énoncé devient démontrable, et
le système de preuve n'a plus aucun intérêt.

Parmi les mécanismes qui créent de telles incohérences et sont donc incompatibles avec
la présence d'un système de preuves, il y a les exceptions (non capturées) et les
données cycliques. En voici la preuve pour les données cycliques. Je reviens à mon
exemple en Haskell d'une liste infinie de 1. En Haskell, on a une fonction 'length' qui
calcule la longeur d'une liste. Cette fonction est hyper classique et elle est définie
exactement de la même façon en Haskell, en Caml et en Anubis. Je l'écris en Haskell
pour pouvoir m'en servir:

Code :

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

1
2
3
4
   length        :: [a] -> Int
   length []     = 0
   length x : y  = 1 + length y

Dans un système avec des preuves, on doit avoir des axiomes exprimant les propriétés
standard des données du système. Une fonction comme celle définie ci-dessus (par une
conditionnelle, car il y a deux cas) jouit d'un certain nombre de propriétés. Parmi
elles, on a sûrement celle qui est exprimée par l'égalité (où x et y sont
universellement quantifiés):

Code :

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

1
2
   length x : y = 1 + length y

Maintenant, ma liste infinie ones a elle aussi une propriété:

Code :

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

1
2
   ones = 1 : ones

A l'aide des deux équations ci-dessus, je peux faire le calcul suivant:

Code :

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

1
2
   length ones = length (1 : ones) = 1 + length ones

d'où je déduis: 0 = 1, c'est à dire ``faux'', et j'ai fait effondrer mon système
logique.

Dès lors, il est facile de comprendre pourquoi on ne peut pas admettre les données
cycliques dans un système qui prétend maintenir sa cohérence logique. En fait, ces
données sont tout simplement des paradoxes, puisqu'elles permettent de démontrer
``faux''. Bien entendu, rien de tout cela n'arrive si on n'a pas de données cycliques.

On peut voir l'argumentation ci-dessus d'une autre façon. La fonction length est de
type [a] -> Int. Autrement-dit, elle associe un entier à chaque liste. Par ailleurs,
c'est une fonction sensée être totale (partout définie). Ce qui arrive, comme on le
voit est qu'elle n'est pas définie pour la liste ones, car l'infini n'est pas un
élément de Int. En fait, ma conclusion est que ones n'est tout simplement pas une
liste, car toute liste est finie par définition du type des listes (cela peut se
démontrer par induction). En fait, la construction de données cycliques détruit la
sémantique des types récursifs, et ce faisant, fait effondrer toute la logique du
système.


Je reviendrai sans doute sur les garbage collectors dans un prochain post.

[LLB]

Message très intéressant.

Mais qu'en est-il des fonctions récursives ? Rien n'empêche une fonction récursive de faire une récursion infinie (et ça me semble difficile de détecter ce cas, en général). Que penser alors du code (non testé) suivant ?

Code :

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

ones x = 1 : ones x

C'est la même chose que le précédent, sauf que la récursion passe par un appel de fonction. Le résultat me semble être le même, puisque Haskell est paresseux. Et pourtant, cela se fait sans effet de bord (sans chirurgie).

[LLB]

Mon cher ami, tu as encore mal lu le manuel. Il n'y a pas de else, et le compilateur le sait bien. Cela tient au fait que le type MonObjet n'a qu'une seule alternative. Si tu ajoute une alternative à MonObjet, le compilateur va te réclamer le else.

Ah oui, désolé. J'ai lu plusieurs fois le manuel d'Anubis ces 3 dernières années, mais j'ai peu d'expérience. Je suppose que la lecture est plus facile quand on a l'habitude, mais je ne pense pas qu'utiliser le mot-clef "if" là où il n'y a pas de condition soit une bonne idée.

[DrTopos]

Rien n'empêche une fonction récursive de faire une récursion infinie (et ça me semble difficile de détecter ce cas, en général).

Une fonction définie récursivement peut en effet tomber dans une boucle infinie, si la récursion est ``mauvaise''. Contôler ce phénomène n'est pas facile (ni Haskell, ni Caml ni Anubis 1 ne le font). Toutefois, les systèmes à preuves sont obligés de la faire. Je peux te fabriquer un paradoxe avec une fonction récursive ayant une mauvaise définition aussi facilement qu'avec une donnée cyclique.

J'en profite pour répondre à l'une des questions de SpiceGuid: l'analogie correcte n'est pas entre les données cycliques et les fonctions récursives (fusses-t-elles mutuelles, ce qui ne change rien), mais entre les données cycliques et les mauvaises récursions seulement.

En Théorie des fonctions récursives, on démontre que l'ensemble des fonctions récursives totales de N vers N n'est lui-même pas récursif. Ce que signifie ce théorème est qu'il n'existe pas d'algorithme capable de déterminer si une fonction définie récursivement est bonne (le calcul s'arrête pour toute valeur de l'argument) ou mauvaise. Si on veut contrôler la récursion, on est donc contraint de trouver un moyen de délimiter algorithmiquement un sous-ensemble de l'ensemble des fonctions de N vers N contenu dans (mais nécessairement non égal à) l'ensemble des fonctions récursives totales.

L'ensemble qu'on choisit logiquement est le plus petit qui contienne les fonctions ``primitivement récursives'' et qui soit stable par les opérations standard sur les fonctions. Pour être sûr que les fonctions définies par l'utilisateur restent dans ce sous-ensemble, il suffit de lui imposer (à l'utilisateur) de respecter le schéma de récursion primitive.

Cela peut se faire de plusieurs façons. La façon la plus facile pour l'implémenteur est d'interdire tout appel récursif, et de produire automatiquement pour chaque définition de type récursif le schéma de récursion primitive correspondant. Dès lors, si l'utilisateur veut définir une fonction récursive, il ne peut le faire que via ce schéma. La fonction length telle quelle est définie en Haskell satisfait le schéma, alors que

Code :

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

ones x = 1 : ones x

ne le satisfait pas. Par ailleurs, effectivement, cet exemple ne comporte pas de chirurgie, seulement une mauvaise récursion.

Comme je souhaite bien entendu faciliter le travail de l'utilisateur, j'ai étudié un moyen de faire détecter par le compilateur une large classe de fonctions satisfaisant les chémas de récursion, plutôt que de l'obliger à utiliser les schémas de récursion primitive à la main. Ce n'est pas facile, et je n'ai pas encore pris de décision définitive sur cette question.

Note: Pour ce qui est du 'if' avec un seul cas, on peut écrire 'since' à la place de 'if' en Anubis.

[DrTopos]

Il serait élégant que la construction d'une agglomération soit également possible en associant une valeur à chacune des composantes, de sorte que l'ordre des composantes n'intervienne plus du tout dans la construction (cette idée a été proposée par alex_pi). De manière cohérente la même facilité serait offerte dans les motifs (d'un filtrage) de sorte que l'ordre des composantes n'intervienne plus du tout dans la déconstruction.
De cette façon on pourrait librement choisir entre la contrainte de respecter l'ordre de toutes les composantes ou la contrainte de nommer toutes les composantes.

C'est à dire qu'en supposant que mon type soit défini par:

Code :

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

1
2
type T: t(String a, String b, String c).

on pourait écrire par exemple t((a: "toto", c:"baba", b:"zonzon") au lieu de t("toto","zonzon","baba"). Il me semble qu'il y a un langage de la fin des années 50 (ALGOL ?) qui le permet. Cela se rapprocherait assez de la langue naturelle. par exemple, on peut dire:

Je vais à Lyon en train

ou

Je vais en train à Lyon

Ici c'est le groupe sujet-verbe Je vais qui joue le rôle de t, les deux arguments étant 'train' et 'Lyon'. Les mots 'à' et 'en' jouent le rôle des noms des composants.

Je ne suis pas opposé à cette facilité. D'ailleurs, ce n'est pas tellement le fait qu'on puisse changer l'ordre qui est intéressant, mais plutôt le fait qu'on peut rendre le texte plus lisible par l'indication du nom des composants.

Par contre pour ce qui est de permettre de mettre les cas des conditionnelles dans un ordre quelconque, je crois que c'est une mauvaise idée. Cela n'apporte pas plus de précision, et ne reduit pas la taille du texte. Je ne pense pas qu'il y ait un bénéfice à en tirer. Je pense même, que quand on définit un type somme, on choisit en général soigneusement l'ordre des alternatives. Le fait d'imposer le même dans les conditionnelles me semble être au contraire la garantie d'une meilleure clarté du texte.

[InOCamlWeTrust]

Ceci-dit, le GC générationnel est le successeur logique du mark & sweep, qui présente aujourd'hui peu d'intérêt.

Ah oui... et pourquoi ? Donc, d'après toi, le GC de OCaml est à foutre en partie à la poubelle ?

Tu penses bien que je ne penses qu'à ça. C'est au centre de mon travail actuel.

Le faire sous forme de front-end pour GCC est peut-être une idée intéressante : ça évite d'avoir à coder tout plein de choses difficiles.

[DrTopos]

Ah oui... et pourquoi ? Donc, d'après toi, le GC de

Ma phrase était mal tournée. J'ai voulu dire qu'à cause des perfectionnement apportés par le générationnel, le mark & sweep a peu d'intérêt.

[EDIT]
En y regardant de plus près, je constate que ma phrase n'était pas du tout mal tournée. Elle l'aurait été si j'avais mis 'et' à la place de 'qui'. Il faudrait apprendre à lire le Français, jeune homme.
[/EDIT]

[alex_pi]

Alex_pi a parlé d'arbre et de pointeur pour remonter au père. J'ai très souvent
programmé avec des arbres et autres structures récursives similaires, et je n'ai jamais
eu besoin d'une telle chose. La programmation avec les données des types récursifs se
fait par des fonctions définies récursivement.

Il peut arriver que les structures que l'on manipule soient trop grosses pour la pile système, et que l'on veuille donc faire une récursion plus "manuelle". Ceci ne signifie pas que l'on a besoin de le faire à chaque fois, et surtout, ceci ne signifie en rien que l'on abandonne la programmation récursive. Simplement, on rend la récursion terminale en ne dupliquant pas la structure (garder le chemin d'appel dans la pile revient à dupliquer la partie de l'arbre entre la racine et l'endroit où l'on se trouve).

C'est normal. D'ailleurs, en Théorie des
Catégories, on définit les types récursifs [...]

Il faut quand même parfois comprendre que l'informatique n'est pas *exactement* les mathématique, qu'on est parfois confronté, qu'on le veuille ou non, à certaines réalités et contraintes liées entre autre à l'implémentation ! Par exemple, une pile système de taille finie (plus limitée que la taille du tas typiquement)

Comme les problèmes universels caractérisent les objets qu'ils
définissent, il est clair qu'on n'a besoin de rien d'autre pour programmer.

Il s'avère aussi que l'on peut se limiter aux huit instructions de BrainFuck pour programmer, ceci ne signifie pas pour autant que l'on vise ce minimalisme...

(1) On doit
avoir au moins une référence sur un sommet de ce graphe, sinon on ne peut rien faire de
son graphe. On privilégie donc un sommet pour des raisons d'implémentation, alors que
le problème qu'on a à traiter ne l'impose sans doute pas.

Dans le cas classique de l'automate, on a quand même d'assez bonne raison de privilégier les états d'entrés...

En définitive, on va être obligé de mettre tous les sommets du graphe dans une liste (non
cyclique) ou un tableau, et là on va s'apercevoir qu'en définitive les cycles de
pointeurs ne servent à rien.

C'est quoi le lien logique entre "il faut pouvoir acceder à tous les sommets" et "les cycles de pointeurs ne servent à rien". Pour moi, un des principes de base de la programmation (sauf quand je veux à tout prix aller chercher l'optimisation) est de faire une implémentation naturelle. Quand je pense "graphe", je pense petits ronds avec des fleches qui en sortent, donc je programme petit rond avec des fleches qui en sortent plutôt que matrice de transition...

La bonne façon de représenter des graphes est celle que j'ai toujours vue appliquer
partout, [...]Si on regarde par exemple l'automate (qui est un graphe avec des cycles) fabriqué par
YACC/BISON [...]

Je trouve ça quand même ammusant pour quelqu'un qui clame faire un langage "à la pointe de la recherche", qui prétend continuellement qu'il permet de débuger 40 fois plus vite qu'en C, etc etc. de prendre comme exemple pour justifier "c'est évidement comme ça qu'il faut faire" un programme qui a été programmé il y a 20 ans, en C justement.

Je pourrais donner d'autres exemples, mais je crois que ceux-ci devraient suffire à
convaincre que même si on souhaite avoir des données cycliques, on peut s'en
passer.

Bien sûr que l'on peut s'en passer, puisqu'encore une fois, on peut réduire un langage de programmation à 8 instructions... Et pourquoi n'avez vous pas répondu sur le coup de la liste doublement chaînée. Vous aurez peut être un peu plus de mal à justifier que ce n'est pas une structure de donnée *ultra-classique*

Les données cycliques sont par ailleurs en lien avec la notion de programmation
déterministe.

Là encore, je ne suis toujours pas convaincu par vos définitions... Le code

Code :

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

1
2
3
4
5
6
int i = 0;
int j = 0;
for(i = 0; i <10; i++){
   j = 42;
}

Est *parfaitement* déterministe. Vous pouvez danser la lambada devant votre PC, lancer firefox ou vous faire du café avec Anubis2, à la fin, j vaudra 42 et i vaudra 10.

D'ailleurs, à ce sujet, je ferai une remarque sur Haskell, qui se dit ``langage fonctionnel pur''. En Haskell, on peut écrire:

Code :

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

1
2
   ones = 1 : ones

ce qui fabrique une liste ``infinie'' de 1. En fait, bien sûr c'est une donnée
cyclique. Cette donnée est nécessairement fabriquée par chirurgie, puisque ones ne peut
pas être contruit complètement au moment où on alloue le segment pour ones. Le fait de
mettre dans la queue de cette liste cette liste elle-même est une chirurgie. Par
conséquent, c'est non déterministe puisque c'est une affectation et par conséquent
Haskell n'est pas un langage fonctionnel pur, même sans utilisation des monades. C'est
un effet pervers des données cycliques.

Alors là, on atteind des sommets de n'importe quoi quand même
Une liste, en mémoire, c'est deux mots mémoire cote à cote, le premier contient la valeur, le second un pointeur vers la suite. Si vous avez une liste et que vous voulez rajouter "1" en tête, vous alouez deux mots mémoires, et vous mettez la valeur "1" dans le premier, et l'adresse de votre liste dans le second, puis vous retourner le pointeur qui vous a été donné lors de l'affectation. Quand vous voulez faire la liste one = 1 :: one, vous alouez deux mots mémoire, vous mettez "1" dans le premier, puis vous mettez la valeur retournée par l'allocation dans le second, et enfin vous retournez cette même valeur. J'avoue ne pas bien voir la différence profonde.

Il est évident qu'aucun langage n'a une implémentation fonctionelle, puisqu'au final, c'est de l'assembleur (enfin même du langage machine), et que c'est tout sauf fonctionnel. Donc dire qu'un langage n'est pas fonctionnel parce que son implémentation ne l'est pas est un non sens.

J'en viens maintenant à des arguments en lien avec la volonté de concevoir un langage
incluant des mécanismes de preuve.[...]

Parmi les mécanismes qui créent de telles incohérences et sont donc incompatibles avec
la présence d'un système de preuves, il y a les exceptions (non capturées) et les
données cycliques. [...]En Haskell, on a une fonction 'length' qui
calcule la longeur d'une liste. [...]

Code :

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

1
2
   length ones = length (1 : ones) = 1 + length ones

d'où je déduis: 0 = 1, c'est à dire ``faux'', et j'ai fait effondrer mon système
logique.

Ouille.... Les maths, c'est joli, mais encore faut-il savoir les adapter... Une fonction informatique de type "'a list -> int" est une fonction mathématique allant vers l'ensemble des entiers *PLUS* un élément particulier, botom, qui signifie "la fonction ne termine pas". En conséquence, la "fonction mathématique" length appelé sur une liste cyclique infinie a la "valeur" botom. Ensuite, botom + 1 vaut bel et bien botom. La logique est conservé, les maths ne s'effondrent pas, la physique tiens le coup, et on survit. Ouf...

Un second post arrive sur d'autres problèmes.

[InOCamlWeTrust]

Ma phrase était mal tournée. J'ai voulu dire qu'à cause des perfectionnement apportés par le générationnel, le mark & sweep a peu d'intérêt.

[EDIT]
En y regardant de plus près, je constate que ma phrase n'était pas du tout mal tournée. Elle l'aurait été si j'avais mis 'et' à la place de 'qui'. Il faudrait apprendre à lire le Français, jeune homme.
[/EDIT]

Non, j'avais bien compris, rassure-toi, mais je ne comprends toujours pas tes remarques étant donné que le GC d'OCaml est générationnel et fonctionne grâce à un mark & sweep et est loin d'être inefficace !

[alex_pi]

Une fonction définie récursivement peut en effet tomber dans une boucle infinie, si la récursion est ``mauvaise''. Contôler ce phénomène n'est pas facile (ni Haskell, ni Caml ni Anubis 1 ne le font).

[...] Si on veut contrôler la récursion, on est donc contraint de trouver un moyen de délimiter algorithmiquement [...]

L'ensemble qu'on choisit logiquement est le plus petit qui contienne les fonctions ``primitivement récursives'' et qui soit stable par les opérations standard sur les fonctions. Pour être sûr que les fonctions définies par l'utilisateur restent dans ce sous-ensemble, il suffit de lui imposer (à l'utilisateur) de respecter le schéma de récursion primitive.

Tiens, je ne savais pas que finalement Anubis2 ne serait pas Turing-complet. Je croyais qu'il serait comme Anubis1 mais en encore mieux, et qu'il écraserait C et C++ au niveau temps d'exécution.

Et là, on se retrouve avec un langage où toutes les fonctions se terminent, et qui n'est donc notoirement pas Turing-complet, ou alors dont on ne peut pas écrire de compilo.... Dommage non ?

[DrTopos]

Non, j'avais bien compris, rassure-toi, mais je ne comprends toujours pas tes remarques étant donné que le GC d'OCaml est générationnel et fonctionne grâce à un mark & sweep et est loin d'être inefficace !

J'ai simplement fait remarquer à SpiceGuid, qu'un mark & sweep simple comme on en faisait dans le temps ne se fait plus, puisqu'il a été perfectionné par le concept générationnel. Cela n'empêche pas le GC d'être sur une base de mark & sweep, mais sur une base seulement.

Je ne sais pas si c'est clair. Je vais essayer autre chose. Il a proposé un mark & sweep. Je lui ai répondu qu'il vaudrait mieux faire un générationnel.

Je ne suis pas contre un mark & sweep générationnel pour Anubis 2, puisque j'ai prévu qu'on puisse choisir son GC. Par contre, je ne sais pas si j'aurai le temps et le courage de le faire moi-même. Si ce genre de projet t'intéresse, tu peux prendre contact avec moi par mp.

[SpiceGuid]

Je crois que jusqu'ici je n'avais pas vraiment réalisé à quel point pour entrer dans le monde des preuves il faut d'abord sortir du monde de la programmation.

Qui dit preuves dit type inductifs et qui dit types inductifs dit pas de données cycliques.
Ou qui dit preuve dit terminaison de preuve donc preuve de terminaison donc pas de données cycliques.
Je vois bien pourquoi si on commence par preuve de données on retombe forcément sur pas de données cycliques.

Et comme on autorise toujours les fonctions cycliques, on établit une nette distinction entre fonctions et données, on sort du cadre du lambda-calcul. Ou alors on est pas Turing-complet, ce qui semble être le choix des systèmes de preuve.

Après c'est certain les cycles que les types inductifs n'ont pas pu construire on n'aura pas besoin d'un mark & sweep pour les détruire.

Pas de cycle c'est très limitant pour l'impératif, ce qu'il faut voir c'est à quel point c'est limitant pour le fonctionnel et pour le multi-paradigme. Certaines expressions du lambda-calcul deviennent irréalisables, c'est tout un pan de l'expérience qui s'évanouit, on ne peut pas le prendre à la légère.

En tout cas c'est à l'heure actuelle, parmi les systèmes du genre, celui qui s'est fixé l'objectif le plus ambitieux en matière d'accessibilité.

[DrTopos]

Je crois que jusqu'ici je n'avais pas vraiment réalisé à quel point pour entrer dans le monde des preuves il faut d'abord sortir du monde de la programmation.

Je crois plutôt que si on veut prouver quoi que ce soit à propos de programmes, il faut d'abord éliminer tout ce qui rendrait toute preuve vaine. Il ne faut donc pas sortir du monde de la programmation, il faut seulement avoir une discipline (beaucoup) plus stricte.

Et comme on autorise toujours les fonctions cycliques, on établit une nette distinction entre fonctions et données, on sort du cadre du lambda-calcul.

Cela dépend de quel lambda-calcul on parle. S'il s'agit de celui de Church, oui. Mais le lambda-calcul c'est aussi le lambda calcul avec couples (comme celui qu'utilise Girard dans le système F). Ceci signifie qu'on a un calcul qui ne se limite pas aux fonctions. On peut aller plus loin et introduire des constructions additives. Dans ce cas, on obtient un lambda-calcul qui traite les fonctions les couples et les données des types sommes. Evidemment avec un tel système on a trois règles de beta-réduction et trois règles de eta-réduction.

Ou alors on est pas Turing-complet, ce qui semble être le choix des systèmes de preuve.

Pour un système de preuves, je ne crois pas que Turing-complet ait beaucoup de sens. Mais de toute façon, être Turing-complet n'est pas très important. Dans la programmation usuelle, on n'en a pas besoin.

Après c'est certain les cycles que les types inductifs n'ont pas pu construire on n'aura pas besoin d'un mark & sweep pour les détruire.

Oui, mais il y a d'autres critères qui peuvent entrer en ligne de compte, par exemple de performances.

Pas de cycle c'est très limitant pour l'impératif, ce qu'il faut voir c'est à quel point c'est limitant pour le fonctionnel et pour le multi-paradigme. Certaines expressions du lambda-calcul deviennent irréalisables, c'est tout un pan de l'expérience qui s'évanouit, on ne peut pas le prendre à la légère.

Aucune expression du lambda-calcul ne risque de devenir irréalisable, puisqu'une espression de n'importe quel langage est de toute façon un arbre donc sans cycle. Je parle de l'expression elle-même, pas de ce qu'elle construit ou représente.

Il faut aussi faire la distinction entre le lambda-calcul non typé et le lambda-calcul typé. La différence est très importante. En lambda-calcul non typé on peut écrire:

Code :

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

1
2
(\x xx)(\x xx)

qui est un terme dont la beta-réduction ne s'arrête pas. C'est impossible en lambda-calcul typé où tous les calculs se terminent (théorème de W.W.Tait). Le lambda-calcul typé qui est sous une forme ou sous une autre (par exemple, sous la forme de la théorie de Martin-Löf pour COQ) à la base de tous les systèmes de preuves n'est donc pas Turing-complet.

[bassim]

Je programme le plus souvent en Java, et voilà qu'un nouveau langage vient et que son créateur fort d'une nouvelle théorie "mathématique" nous dis que tout les langages à part le sien sont médiocres ou ne lui arrivent même pas à la cheville.
Ok, mais que nous apporte votre langage par rapport à Java, C++, C# ... ;
la rapidité de développement :ben s'il faut 1 million de lignes de code pour programmer un site Web ,je suis consterné ;
La sécurité :j'ai jamais essayé, donc je me prononcerai pas !
L'évolutivité :Je suis allé sur le site du Langage Anubis, et j'ai lu ceci sur la Programmation Orienté Objet

Or en informatique, il n'y a pas que des données concrètes, il n'y a donc pas de raison de tout traiter comme des objets. D'ailleurs, traiter les notion abstraites (de nature mathématique) comme des objets revient à introduire du non déterminisme là où il ne se justifie pas, ce qui non seulement complique inutilement la programmation, mais augmente considérablement le risque d'erreur. Bien sûr, dans le cas de données concrètes, appliquer le principe d'identité est indispensable.

La POO a été inventée et adoptée par beaucoup de monde parceque elle se rapproche de la pensée humaine et de la vie autour de nous qui est faite d' objets de différentes natures. Je dirais plutôt qu'elle réduit le risque d'erreur parceque grâce à l'encapsulation, les objets ne communiquent entre eux que par le biais de d'interfaces externes.

un terme déterministe est beaucoup plus facile à comprendre qu'un terme non déterministe

D'un coté y a les mathématiques ou tout est preuve et l'informatique ou l'analyse prime sur tout et est basée sur des choix comme le choix d'un langage de programmation par exemple pour implémenter son système.

Un module est destiné à être utilisé par d'autres modules. Il fournit donc aux autres modules ce qu'on peut appeler des outils. Il y a toujours deux points de vue sur un outil donné: le point de vue du constructeur et le point de vue de l'utilisateur. L'utilisateur ne s'intéresse pas à la façon dont l'outil est construit, mais seulement à la façon de s'en servir. C'est pour cette raison que chaque outil a son mode d'emploi.

C'est drôle, j'ai presque envi de dire que c'est la définition même de l'Objet exprimée d'une autre façon.

La morale est que la justification du programme récursif est beaucoup plus facile à faire que la justification de la boucle, et donc beaucoup moins sujette à erreurs. D'ailleurs, ce qui rend la boucle plus difficile à justifier est simplement le fait que les boucles (en langage C du moins, et dans les langages similaires) imposent une programmation non déterministe, car une boucle ne renvoit pas de valeur, et est par conséquent obligée de produire des effets pour avoir une utilité

Vous êtes entrain de critiquer l'Algorithmie sans le savoir, qui est la base de l'informatique.

Je suis pas d'accord avec votre pensée comme quoi il faut empêcher le programmeur de faire des erreurs pour développer .Un langage qui "peut" provoquer des erreurs implique selon moi qu'il permet de faire vraiment beaucoup de choses et qu'en acquérant de l'expérience on peut éviter ces mêmes erreurs tout en gardant la puissance du langage .

Conclusion: je ne suis pas du tout convaincu par ce langage, et je trouve que l'absence d'erreurs dans un programme est une utopie !

[LLB]

Je programme le plus souvent en Java, et voilà qu'un nouveau langage vient et que son créateur fort d'une nouvelle théorie "mathématique" nous dis que tout les langages à part le sien sont médiocres ou ne lui arrivent même pas à la cheville.

Sur certains points.
Il me semble pas avoir lu qu'Anubis avait pour but de remplacer Java ou C#. C'est une philosophie différente.

Je dirais plutôt qu'elle réduit le risque d'erreur parceque grâce à l'encapsulation, les objets ne communiquent entre eux que par le biais de d'interfaces externes.

Je crois que ton point de vue est biaisé, je pense que tu raisonnes en impératif (et Anubis est fonctionnel). J'aime beaucoup l'objet, en particulier quand un langage en profite réellement via un système tout-objet, mais je sais aussi que l'on peut très bien s'en passer. Les arguments qui ont été utilisés pour vendre la POO proviennent pour la plupart du monde impératif.

Vous êtes entrain de critiquer l'Algorithmie sans le savoir, qui est la base de l'informatique.

Si tu crois que faire des boucles est indispensable pour l'algorithmique, tu te trompes lourdement. Et tu as beaucoup de choses à apprendre, choses qui te seront utiles même si tu te limites à Java/C#/C++.

je ne suis pas du tout convaincu par ce langage, et je trouve que l'absence d'erreurs dans un programme est une utopie !

Quel est le problème avec un langage n'ayant pas d'exceptions ? Si toutes les valeurs de retour sont correctement utilisées (et surtout, ne jamais avoir la valeur "null", qui est un problème de beaucoup de langages), ça me semble réalisable.

Je crois pourtant qu'avoir des exceptions, limitées au minimum, est une bonne chose. Mais cela dépend surtout de la philosophie du langage. Les problèmes rencontrés dans Anubis 1 pourraient être résolus, théoriquement.

je ne crois pas que Turing-complet ait beaucoup de sens. Mais de toute façon, être Turing-complet n'est pas très important. Dans la programmation usuelle, on n'en a pas besoin.

Je suis surpris, mais je ne demande qu'à voir.
Sera-t-il toujours possible, dans Anubis 2, de faire une boucle infinie ? Par exemple, comme dans le code du serveur (cf le défi).