Discussion :

[millie]

Effectivement, si l'on utilise la fonction max avec un objet qui ne peut pas utiliser l'opérateur <, cela va provoquer une erreur de compilation (j'ai du adapter le code pour le faire fonctionner avec des classes et pas uniquement avec les types primitifs) :

Code C++ :

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
#include <iostream>
 
template<typename T>
const T& max(const T & a, const T & b) {
  if(a<b)
   return b;
 else
   return a;
}
 
class A {
 
};
 
class B {
  public:
    bool operator<(const B& a) const {
      return true;
    }
};
 
int main()
{
	int i = 2;
	int j= 3;
   const int & maxi = max(i,j);
 
   B b1;
   B b2;
   const B & maxb = max(b1, b2);
 
   A a1;
   A a2;
   const A & amax = max(a1,a2);
 
   return 0;
}

Il y a une erreur au niveau de la ligne : const A & amax= max...




Pour Java, en fait, il n'y a qu'un code "exécutable" (bytecode plutôt) dont tous les paramètres sont toujours : Object (car toutes les classes héritent d'Object). Il n'y a qu'une vérification des types passées lors de la compilation (et non de l'exécution).

[DrTopos]

Okay, donc il me semble que le sens du template que tu donnes en exemple est:

``Pour tout type T pour lequel il existe une fonction '<' de type T*T -> Bool, ....''

C'est à dire qu'en fait la quantification sur le type T est bien universelle, mais elle est conditionnée par une seconde quantification (tout aussi implicite, mais existentielle celle-là) sur la fonction < .

Cette seconde quantification est de fait une contrainte sur T. Est-elle de même nature que celles dont parlait LLB ?

[DrTopos]

Puisque certains d'entre vous font des essais avec Anubis en essayant (tout à fait légitimement) d'en exhiber les défauts, je me suis dit que je pourrais bien de mon coté en faire autant avec ocaml (par exemple).

J'ai donc tapé ceci dans un fichier:

Code :

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

1
2
3
4
5
6
type toto = A | B ;;
   
type bubu = A | C ;;
   
let x =  A = B ;;

et voici ce qu'il se passe quand je compile:

Code :

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

1
2
3
4
alp@alp-laptop:~$ ocaml exemple.ocaml
File "exemple.ocaml", line 7, characters 12-13:
This expression has type toto but is here used with type bubu

Maintenant, voici la même chose en Anubis:

Code :

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

1
2
3
4
5
6
type Toto: a, b. 
   
type Bubu: a, c. 
   
define Bool x = a = b.

et là le compilateur Anubis ne dit rien.

Lequel a raison à votre avis ?

[LLB]

Je répondrai aux autres messages (s'il y a besoin) plus tard.

Pour cette dernière question : je préfère la solution d'Anubis, puisqu'il comprend tout seul qu'on utilise le type toto.

Mais, je trouve ça très amusant. OCaml et Anubis se ressemblent sur le fait qu'ils privilégient par endroit la sûreté et la clarté à l'expressivité (mais les choix qui sont faits en pratique s'opposent en plusieurs endroits).

C'est un bon exemple : en Caml, on ne définit pas deux types sommes en utilisant un même identifiant. C'est la même chose pour les structures : les champs doivent avoir un nom différent.

Du coup, on peut te retourner la remarque : le fait d'utiliser deux fois le "a" ne réduit-il pas la clarté et la facilité de relecture ? Dans le code, ce n'est pas écrit quel "a" est utilisé : le compilateur le déduit. Je trouve ça étonnant de faire ce choix, alors que l'on refuse le typage implicite aux autres endroits.

[DrTopos]

Ce qui m'etonne le plus dans le comportement de ocaml, c'est pourquoi on ne peut pas surcharger un symbole sous pretexte qu'il est un constructeur (tag-name dans le vocable ocaml) ? Je ne vois pas de raison à cette restriction.

Le compilateur Anubis trouve deux interprétations pour a, et comme b n'en a qu'une, il élimine l'une des deux car l'égalité est typée ($T,$T) -> Bool. C'est un effet de l'inférence de types.

Par contre, si j'avais mis:

Code :

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

1
2
define Bool x = a = a.

le compilateur Anubis aurait protesté que c'est ambigu, car a a deux types possibles, alors que (je viens de faire l'expérience) le compilateur ocaml ne dit plus rien.

[LLB]

Parce que OCaml refuse toute forme de surcharge. Chaque symbole n'a qu'un seul type. 0 est forcément un entier. + est forcément l'addition de 2 entiers. +. est forcément l'addition de 2 flottants.

On peut redéfinir un symbole, mais pas le surcharger (l'ancienne valeur est donc masquée).

Certains prétendent que ça améliore la lisibilité et supprime toute forme d'ambiguité, au prix parfois d'une lourdeur syntaxique. Un peu pour la même raison que tu refuses le typage implicite.

Edit : d'ailleurs, si les symboles pouvaient être surchargés, cela nécessiterait parfois des annotations de type, comme tu le signales. En Caml, on n'est (quasiment) jamais obligé de typer à la main.

[DrTopos]

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.

Il y a donc deux types de noms 'HTML_In_Form' et 'HTML_Off_Form', avec chacun de nombreuses alternatives (variants en ocaml), chaque alternative représentant un élément HTML particulier. Bien entendu, l'alternative 'form(...)' figure dans 'HTML_Off_Form', mais pas dans 'HTML_In_Form'.

Il y a de nombreux éléments HTML qui peuvent figurer à la fois dans les formulaires et hors des fomulaires: le texte, les images, les tables, ... ce qui fait que mes deux types ont des alternatives écrites exactement de la même façon (avec le même nom en particulier), ce qui ne serait donc pas possible en ocaml.

C'est très imortant que ces alternatives soient écrites exactement pareil dans les deux types, car le programmeur, quand il compose sa page HTML n'a pas à se soucier, quand il met du texte ou une image, de savoir s'il est ou non dans un formulaire. Par contre, s'il essaye de mettre un champ de saisie 'input' hors d'un formulaire, il se fait taper sur les doigts par le compilateur.

N'est-ce pas un + pour la sûreté ?

[DrTopos]

Parce que OCaml refuse toute forme de surcharge. Chaque symbole n'a qu'un seul type. 0 est forcément un entier. + est forcément l'addition de 2 entiers. +. est forcément l'addition de 2 flottants.

On peut redéfinir un symbole, mais pas le surcharger (l'ancienne valeur est donc masquée).

Ceci explique cela.

Certains prétendent que ça améliore la lisibilité et supprime toute forme d'ambiguité, au prix parfois d'une lourdeur syntaxique. Un peu pour la même raison que tu refuses le typage implicite.

De toute façon, le compilateur Anubis détecte toutes les ambiguïtés. Il n'en laisse pas passer une seule. Il veut absolument tout comprendre. Je fais aussi remarquer que dans l'exemple que j'ai donné (avec a = a), bien que ocaml ne détecte pas d'ambiguïté, l'utilisateur peut avoir dans sa tête pensé au premier a, or il n'est pas prévenu qu'il s'agit du second. Je ne trouve pas cela très bon pour la sûreté. De toute façon, dans le cas d'Anubis, cela ne pose pas de problème de sûreté, puisque toute ambiguïté est systématiquement signalée.

Edit : d'ailleurs, si les symboles pouvaient être surchargés, cela nécessiterait parfois des annotations de type, comme tu le signales. En Caml, on n'est (quasiment) jamais obligé de typer à la main.

Effectivement, si on typait aussi peu en Anubis qu'en Caml, on aurait plein de choses ambiguës. Il y a donc deux approches différentes.

[SpiceGuid]

Qu'en est-il de la limitation empéchant d'implémenter des listes doublement chaîné et des graphes cycliques (entre autre).

Cette limitation n'existe pas (au niveau du langage), elle n'existe qu'au niveau du ramasse-miettes (par comptage de références) qui sera incapable de récupérer la mémoire allouée par des structures cycliques. Il s'agit donc d'une limitation de l'implémentation et pas d'une limitation du langage, or tu l'as dis toi-même le sujet est "que pensez-vous du langage?".

À propos de l'inférence de type:

Anubis ne demande que de 'prototyper' les fonctions.
Je crois que les langages fonctionnels à équations (Haskell/Miranda) demandent également de 'prototyper' les fonctions. Je n'ai jamais lu ni sur ce forum ni ailleurs que Haskell ou Miranda ne pratiqueraient pas l'inférence de type.

Pour les fonctions anonymes (en Anubis 1.7) il faut donner le type des arguments formels mais pas celui du résultat. À l'usage cela ne m'a pas paru excessivement verbeux, par contre ça responsabilise davantage, avec Caml j'ai un peu tendance à me reposer sur l'inférence de types, par exemple pour l'argument d'un fold_left ou d'un fold_right j'utilise l'interpréteur pour m'éviter de réfléchir, si ça ne passe pas l'inférence de type alors j'échange les deux arguments et je ne m'interroge que si ça ne passe toujours pas. Anubis demande plus d'attention (l'absence d'un interpréteur interactif y est sans doute pour quelque chose).

Des versions récentes de C++ et Java possèdent le polymorphisme paramétrique, mais aucun des deux ne possède l'inférence de type (ou typage à la Hindley-Milner). Par exemple Anubis ne vous demande pas de déclarer le type de vos variables locales.

Qu'est ce qui t'empêche de taper f(x) avec ocaml ?

Personnellement ça ne me dérange pas de taper f x plutôt que f(x), mais ça démotive nombre de débutants ayant une formation en mathématiques. Evidemment, en OCaml la syntaxe f(x,y,z) est à éviter puisqu'on y perd la curryfication, et en plus on alloue un n-uplet à chaque appel. Sinon je suis d'accord: c'est idiot mais on peut le faire.


J'aimerais bien que l'on puisse reparler du langage et de son futur, plutôt que de s'acharner sur les détails d'une implémentation qui aura fait son temps.

[DrTopos]

Diverses remarques à propos de la surcharge.

Il y a en gros deux façons de traiter les collisions de noms de variables: la surcharge et la préemption. Si on admet la surcharge, les ambiguïtés doivent être résolues par inférence de types. Si on utilise la préemption (ce qui semble être le cas de Ocaml pour tous les symboles) on peut soit masquer la définition précédente, soit interdire de masquer.

En ce qui concerne Anubis, j'ai choisi la surcharge pour les symboles globaux, et la préemption (sans interdiction de masquage) pour les symboles locaux. Ces derniers temps, on a eu parfois du mal à comprendre certains messages du compilateur, et on s'est aperçu qu'il y avait des masquages intempestif. Aussi, je pense que les symboles locaux en Anubis vont bientôt passer en préemption avec interdiction de masquer, pour éviter ce problème.

Quelques remarques plus théoriques.

Quand le compilateur Anubis interprète le symbole a dans l'exemple que j'ai donné, il trouve deux interprétations, l'une de type toto, l'autre de type bubu. En fait, il obtient une seule interprétation de a, mais cette interprétation est une méta-disjonction d'interprétations. De même, quand il interprète un symbole défini par un schéma, et qu'un paramètre de ce schéma n'est pas instancié, ce qu'il obtient est une interprétation méta-existentiellement quantifiée. Quand enfin, il ne trouve pas du tout d'interprétation (le symbol n'est pas défini), il obtient l'interprétation méta-faux.

Les trois connecteurs logiques 'ou' (disjonction), 'il existe' et 'faux' (élément neutre de la disjonction) sont les seuls connecteurs additifs de la logique. Tous les autres sont multiplicatifs. L'inférence de types n'est en fait qu'une manipulation de ces trois connecteur additifs au niveau méta. je ne vois pas de raison d'adopter le quantificateur existentiel, et de renoncer à la disjonction. Autrement-dit, si on a du polymorphisme paramétrique, on doit aussi avoir la surcharge. C'est logique.

[LLB]

Voici par exemple un problème avec la surcharge de valeurs :

Code :

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

1
2
3
4
5
6
7
8
define Float b = 1.

...
define Int32 b = 2.

...
    with c = b + 0.0,
    with d = b * (1 * 1),

Que penses-tu de ce code ? c vaut 1 et d vaut 2.

Est-ce qu'en mathématiques, deux identifiants de même nom peuvent exister, avec des valeurs différentes ?

La surcharge de valeurs simples (par opposition aux fonctions) me semble dangereuse. D'ailleurs, on ne la voit dans presque aucun langage.

[DrTopos]

J'ai compilé ton code sous la forme suivante:

Code :

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

1
2
3
4
5
6
7
8
define Float b = 1.
define Int32 b = 2.

define One essai = 
    with c = b + 0.0,
    with d = b * (1 * 1),
    unique.

et il passe. Il est en effet non ambigu. C'est dû au fait qu'Anubis ne convertit pas automatiquement les Int32 en Float (sauf dans le lexer). Ton exemple m'interpelle quand même, car si on remplace 0.0 par 0, ça passera toujours [edit] je me suis trompé, ça ne passe plus c'est ambigu si je mets 0, car 0 sera à la fois Int32 et Float, ce qui n'est pas le cas de 0.0[/edit] et on change la valeur de c. J'ai l'impression que le problème vient de ce que mentalement on identifie les Int32 et les Float, alors que pour le compilateur ce sont deux types qui n'ont rien à voir l'un avec l'autre.

Est-ce qu'en mathématiques, deux identifiants de même nom peuvent exister, avec des valeurs différentes ?

Oui bien sûr, en tout cas pour une opération comme + par exemple, qui sert à additionner aussi bien des nombres que des matrices que des polynômes et toute sortes d'autres choses.

La surcharge de valeurs simples (par opposition aux fonctions) me semble dangereuse. D'ailleurs, on ne la voit dans presque aucun langage.

Cette affirmation m'etonne un peu. Qu'en est-il de C++ par exemple ?

[LLB]

Oui bien sûr, en tout cas pour une opération comme + par exemple, qui sert à additionner aussi bien des nombres que des matrices que des polynômes et toute sortes d'autres choses.

OK, + est une fonction. Dans ce cas, ça me va. Pour les constantes, je veux bien que 0 puisse définir une valeur de N ou une valeur de R (Caml refuse ça et distingue 0. de 0 ; mais C et C++ l'acceptent).

Mais, avoir des variables a, l'une qui vaut 2 et l'autre qui vaut 4.2, ça m'interpelle vraiment. Dans tous les langages que j'ai vus, la 2e valeur masque la première (cela génère parfois une erreur si les 2 valeurs ont la même portée).

En revanche certains langages possèdent des conversions implicites. Si a est un entier qui vaut 2, il pourra être utilisé là où on attend un flottant (qui vaudra alors 2, lui aussi).

En C++, on peut surcharger une fonction (en faisant varier sa signature), mais pas une valeur simple. En fait, dans la plupart des langages, la surcharge fonctionne uniquement sur les arguments. Le type de retour ne fait bien souvent pas partie de la signature.

[DrTopos]

Pour 0 c'est aussi le cas, et d'ailleurs j'ai souvent besoin de le rappeler aux étudiants. Par exemple, si E est un espace vectoriel sur le corps K, on a un 0 dans K et aussi un 0 dans E, qui sont distincts évidemment. Au début, pour les aider on met E ou K en indice de 0, mais rapidement on cesse de le faire.

Pour la version 1.8, j'ai commencé à expérimenter un système de conversions automatiques qu'on définit soi-même. Si on définit une conversion de Int32 vers Float, le premier exemple deviendra ambigu et ça ne passera plus. L'erreur sera même générée dès la deuxième définition de b. C'est peut-être là la solution du problème, car il semble bien venir de la possibilité de convertir (y compris mentalement et inconsciemment).

[Jedai]

À propos de l'inférence de type:

Anubis ne demande que de 'prototyper' les fonctions.
Je crois que les langages fonctionnels à équations (Haskell/Miranda) demandent également de 'prototyper' les fonctions. Je n'ai jamais lu ni sur ce forum ni ailleurs que Haskell ou Miranda ne pratiqueraient pas l'inférence de type.

Haskell n'oblige nullement à "prototyper" ses fonctions ! On peut le faire, mais ce n'est absolument pas imposé.

Justement, là il y a quelque chose qui ne me plait pas. D'abord cette notion de 'type numérique'. Je ne vois pas pourquoi il devrait y avoir une telle notion. C'est une notion qui ne peut prétendre à aucune généralité, les nombres étant une sorte particulière de données parmi des milliers d'autres. Si on commence à faire cela, on va finir par avoir un catalogue de milliers de sortes de types qui n'ont aucun caractère structurel. Pour moi les nombres n'ont rien de particulier, ce sont des données 'ordinaires' si j'ose dire. Ce n'est pas le cas des fonctions qui ont un rôle structurel.

Le "type numérique" d'Haskell est en fait une classe de type (Num) représentant les types de données ayant (grossièrement, vu les limitations des représentations informatiques) une structure d'anneau. Je ne vois pas très bien pourquoi tu es opposé à classer les types alors que tu n'es pas opposé aux types eux-même ? On pourrait très bien se passer des types, d'ailleurs les gens qui font de l'assembleur ne manipule que des tas de bits et s'en sortent très bien... ou pas.
Tu remarqueras d'ailleurs que tu autorise la surcharge d'opérateur, n'est-ce pas une façon moins contrôlé d'autoriser le même genre de chose (que je sache tu utilises le même opérateur d'addition pour tous tes types "numériques" ?).

Alors, de fait, il y a une chose qu'Anubis n'a pas et qu'il pourrait avoir éventellement. Ce que je vais dire est sans doute une autre façon de reparler de ces contraintes. Imaginons qu'on définisse une fonction comme j'ai fait ci-dessus avec 'max', mais sans déclarer 'max_of_two' ni 'max_of_nothing'. Le compilateur pourrait inférer ces déclarations lui même. Bon. Lors de l'utilsation de 'max' les opérandes 'max_of_two' et 'max_of_nothing' ne seront donc pas fournis. Le compilateur aura alors à rechercher dans sa base de connaissances des fonctions ayant ces noms et des types qui pourraient être des instances des paramètres. Est-ce de ce mécanisme que sont capables Caml et Haskell ?

Techniquement, je crois qu'il est facile de modifier le comilateur Anubis pour qu'il le fasse. Maintenant, est-ce vraiment une bonne idée, et en particulier cela pose-t-il un problème de sûreté ? Il faut que j'y réfléchisse.

Il existe des moyens de faire ceci sans vraiment compromettre la sûreté, comme par exemple les typeclass en Haskell, pour reprendre l'exemple de maximum :

Code Haskell :

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

maximum = foldl1 max

dont le type serait inféré comme :

Code Haskell :

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

(Ord a, Foldable f) => f a -> a

(on n'est pas du tout obligé de le préciser)

Ainsi a doit être une instance de Ord, puisque max est utilisé sur a, et f doit être une instance de Foldable puisque j'utilise foldl1 (qui est un type de fold gauche ne fonctionnant que sur une structure non-vide (par contre là on aurait besoin des types dépendants pour le préciser, j'attend de voir Anubis2, pour l'instant Epigram est intéressant dans le domaine)).
Cette fonction maximum fonctionnerait bien sûr sur une liste, mais également sur un tableau, ou un arbre, ou un type défini par le programmeur et pour lequel il a écrit une instance de Foldable.

J'aimerais bien que l'on puisse reparler du langage et de son futur, plutôt que de s'acharner sur les détails d'une implémentation qui aura fait son temps.

Il me semble que la verbosité du langage n'est absolument pas un "détail" de l'implémentation. La possibilité de surcharge uniquement limitée par la globalité du symbole concerné est également intéressante... et dangereuse (du moins contestable).

--
Jedaï

[LLB]

Code :

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

1
2
3
4
5
6
7
define List($U)
   map
      (
         $T -> $U   f, 
         List($T)    l
      )  = ...

Le compilateur détermine les valeurs les plus générales lors de l'instanciation de ce schéma.

Ce code là restreint la fonction : la fonction n'est utilisable que sur des listes. Alors qu'a priori, la fonction map sur un tableau et sur une liste peut être de la même façon. Il "suffit" d'itérer sur l'ensemble et d'appliquer la fonction.

Il me semble donc que les valeurs trouvées pour $T et $U sont les plus générales possible.

Oui, j'ai bien compris que c'était unifié. Ce que je veux dire, c'est que c'est facile d'utiliser Int32 à la place de $T, si on ne pense pas au cas le plus générique. Le compilateur lui pense à tout.

Le terme 'typage structurel' est encore mystérieux pour moi dans ce contexte. Il faudrait savoir aussi ce qu'on entend par là. Je vais jeter un oeil dans le manuel OCaml.

Ce n'est pas très important ici. Pour la culture, Wikipedia en parle : http://fr.wikipedia.org/wiki/Syst%C3...tural_de_types

Ca se rapporte aux contraintes sur les types. On peut par exemple définir la fonction f(a) où a est n'importe quel objet possédant les méthodes x, y, z.

Je vais le faire pour une liste de choses pour lesquelles il y a une operation binaire 'max_of_two'

Code :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
define List($T) -> $T
   max
      (
         ($T,$T) -> $T  max_of_two,
         $T                 max_of_nothing
      ) =
    (List($T) l) |-> 
    if l is 
      {
         [ ] then max_of_nothing,
         [h . t] then max_of_two(h,max(t))
      }.

Voilà ! C'est la même "généricité" que dans Caml. C'est un style assez lourd et je suppose que c'est rarement employé en pratique. Demande à un utilisateur d'Anubis d'écrire cette fonction, sachant que tu souhaites l'utiliser sur une liste d'entiers. Je parie que la fonction qu'il écrira sera moins générale que celle que tu viens d'écrire. Il ne faut pas sous-estimer les méfaits d'une syntaxe trop lourde.

Sans compter qu'encore une fois, la fonction ne marche que sur des listes. Calculer le maximum d'une liste ou d'un tableau (et on peut imaginer beaucoup d'autres structures de données de nature similaire) est sensiblement la même chose.

Il faudrait qu'on éclaircisse cette notion de 'contrainte'. Sinon, on risque encore de mal se comprendre.

C'est pouvoir utiliser un type qui soit plus générique que Int32, mais moins générique que $T. Par exemple, une fonction peut accepter tout $T, à condition qu'on puisse écrire "$T + un entier". C'est cette condition que j'appelle contrainte.

D'abord cette notion de 'type numérique'. Je ne vois pas pourquoi il devrait y avoir une telle notion.

Imaginons que l'on ait une matrice contenant des Int32. Imaginons que l'on souhaite multiplier cette matrice par un Int32. La fonction aura un type du genre : Matrix(Int32) -> Int32 -> Matrix(Int32). Si on a besoin de multiplier ensuite une matrice de Float par un Float. Faut-il réécrire la fonction ?

La notion de type numérique est juste un regroupement de types. Par exemple, on pourrait dire que Int32, Int64, Float... font partie des types numériques. La fonction ci-dessus pourrait avoir pour type : Matrix($T) -> $T -> Matrix($T), à condition que $T soit un type numérique.

C'est une notion qui ne peut prétendre à aucune généralité, les nombres étant une sorte particulière de données parmi des milliers d'autres.

Je suis d'accord. Par exemple, les listes, les tableaux, les chaines de caractères, etc. peuvent faire partie de la famille des "conteneurs" (j'aime pas trop ce nom, mais j'ai pas trouvé mieux ; en F#, on appelle ça Seq ou IEnumerable).

Pour moi les nombres n'ont rien de particulier, ce sont des données 'ordinaires' si j'ose dire.

Entièrement d'accord, il n'y a pas de cas particuliers à faire dans le compilateur. Il y a de nombreuses façons d'implémenter ça. En F#, c'est entièrement défini dans la bibliothèque, et les entiers ne sont pas traités différemment des autres types.

En tout cas, cela réduit les temps et les efforts de relecture. J'en suis bien convaincu.

Non. Imaginons un code est écrit par un programmeur A et relu par un programmeur B. C'est le fait que B voie les types qui peut être utile, pas le fait que A les ait écrit. La différence est subtile, mais si un outil écrivait les types, plutôt que A lui-même, quel serait le problème ?

Avec Caml, il existe une option du compilateur pour générer le fichier interface. Avec F# et un bon éditeur, l'éditeur affiche les types sur simple demande.

Je vais reprendre l'exemple d'Alex :

Code :

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

1
2
3
4
5
6
7
8
9
define List($U)
   map
     (
       $T -> $U f,
       List($T) l
     ) =
   ...

let map f l = ...

Lequel des deux est le plus rapide à lire ? Quand on a un long fichier, laquelle des syntaxes est la plus agréable pour saisir la structure globale du programme ?

Et quand on a le moindre doute sur un type, il suffit de le demander.


Si tu n'es pas convaincu, je vais prendre un exemple un peu extrême.

Pourquoi ne pas obliger les programmeurs à écrire "a@12" plutôt que "a" quand on veut utiliser la valeur "a" ? Ici, le 12 représente le numéro de la ligne où est défini. Cela enlèverait les ambigüités quand des valeurs sont redéfinies. Cela simplifierait la relecture : quand une fonction est appelée, on pourrait aussitôt où elle est définie. Malgré une lourdeur syntaxique au moment de l'écriture, cela pourrait à la relecture... non ?

Je suis convaincu que ce n'est pas au programmeur de faire ça. Un bon éditeur devrait être capable de retrouver la définition d'une valeur sur un simple clic. Il devrait aussi être capable d'afficher le type d'une valeur sur simple demande.

Code :

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

1
2
3
4
5
6
7
8
define $U -> $V
   exemple
      (
         MonObjet m
      ) =
   if m is mon_objet(plus,times) then
   ($U u) |-> ... utiliser plus et times ici ...

mais ce n'est peut-être pas à cela que tu pensais.[/QUOTE]
Mmh... Et le else correspondrait à quoi ?
Si j'ai bien compris, cela fait ce que je veux... sauf qu'il n'y a pas de vérification statique. Si on passe un objet n'ayant pas plus ou times, l'erreur sera rencontrée à l'exécution.

Cette seconde quantification est de fait une contrainte sur T. Est-elle de même nature que celles dont parlait LLB ?

Oui.

Pour la version 1.8, j'ai commencé à expérimenter un système de conversions automatiques

Ca me semble dangereux. Cette fonctionnalité est typique des langages à typage faible / dynamique. Je ne suis pas sûr que ce soit dans la philosophie d'Anubis. Enfin, tout dépend comment c'est fait, mais faut faire très attention à ça.

[DrTopos]

Bon. J'ai fait une petite tentative d'imitation de la classe Ord d'Haskell. Tout ce qui suit compile sans problème.

La première définition a pour objet d'introduire la notation 'objet.membre'

Code :

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

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

J'introduis également le signe /= (= quant-à lui est primitif en Anubis et défini pour tous les types (sauf Float !)).

Code :

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

1
2
   
define Bool $T x /= $T y = if x = y then false else true.

J'essaye maintenant d'imiter la classe 'Ord' d'Haskell.

Code :

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

1
2
3
4
5
6
7
public type Ordering: eq, lt, gt.     Pas de pb. 
   
public type Ord($T):
   ord ( 
         ($T,$T) -> Ordering   compare
       ).

Dans le type ci--dessus, je ne mets que ce composant, car les autres se définissent en fonction de celui-ci. Seul celui-ci a donc besoin de figurer dans le schéma.

Maintenant voici les membres 'dépendants' de 'compare':

Code :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
   
public define ($T,$T) -> Bool lessoreq     (Ord($T) objet) = 
   ($T x, $T y) |-> objet.compare(x,y) /= gt. 
public define ($T,$T) -> Bool less         (Ord($T) objet) = 
   ($T x, $T y) |-> objet.compare(x,y) = lt. 
public define ($T,$T) -> Bool greateroreq  (Ord($T) objet) = 
   ($T x, $T y) |-> objet.compare(x,y) /= lt. 
public define ($T,$T) -> Bool greater      (Ord($T) objet) = 
   ($T x, $T y) |-> objet.compare(x,y) = gt. 
public define ($T,$T) -> $T   max          (Ord($T) objet) = 
   ($T x, $T y) |->  if objet.lessoreq(x,y) then y else x. 
public define ($T,$T) -> $T   min          (Ord($T) objet) = 
   ($T x, $T y) |->  if objet.lessoreq(x,y) then x else y.

On en écrit plus qu'en Haskell, mais pas tellement en fait. Il est vrai que là c'est assez redondant. Je pourrais rendre facultatif le typage entre 'define' et le nom de la fonction. C'est seulement l'obligation de typer les fonctions qui augmente le texte. Pour le reste, c'est à peu près pareil.

Comme en Anubis il n'y a pas de classes de types, ma pseudo-classe est plutôt un type, en fait un schéma de type. En maths, on dirait que Ord est une structure, qu'une donnée de type Ord(X) (pour un certain type X) est une instance de cette structure, et que X est l'ensemble sous-jacent à cette instance.

Maintenant, voyons l'utilisation de ma pseudo-classe (string_less est une primitive).

Code :

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

1
2
3
4
   
define Ord(String) ord_string = 
    ord((String x, String y) |-> 
       if x = y then eq else if string_less(x,y) then lt else gt).

J'ai donc créé un 'objet' de la 'classe' Ord.

Code :

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

1
2
   
define String test_max = ord_string.max("ga","bu").

Il est clair que je ne pourrai utiliser 'max' qu'avec un objet de type Ord(...), autrement-dit, pas avec n'importe quoi. Il me semble que la donnée 'ord_string' joue le rôle du type paramètre de la classe Ord en Haskell.

En définitive, y a-t-il une différence vraiment profonde avec Haskell ? Je veux dire, y a-t-il quelque chose facilement faisable en Haskell et vraiment difficile, voire impossible à faire en Anubis ?

En tout cas, il me semble que je vois une différence. En Haskell, la fonction max n'aura qu'un sens possible pour l'instance 'String', alors qu'en Anubis je peux fabriquer autant d'objets de type Ord(String) que je veux avec des fonctions de comparaison différentes.

[DrTopos]

@LLB: Pour ce qui est de la généralité du 'map' tu as raison. C'est une chose à laquelle j'ai réfléchi ces derniers temps, et voici ce que j'ai décidé de faire pour Anubis 2.

En fait la correspondance $T ---> List($T) est un 'foncteur' au sens des catégories. C'est a dire que non seulement elle transforme un type en un type, mais elle transforme une fonction en fonction. En Anubis 2, on n'aura pas besoin de définir 'map'. Une fois que le schéma List sera défini, il suffira d'écrire:

Code :

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

1
2
List(f)[1,2,3,4]

et ça donnera [f(1),f(2),f(3),f(4)]. De même si on définit le type d'arbre binaire suivant:

Code :

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

1
2
3
4
type Tree($T):
   leaf($T), 
   node(Tree($T),Tree($T)).

il suffira d'écrire:

Code :

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

1
2
Tree(f)(a)

pour que f (de type A -> B) soit appliquée à toutes les feuilles de l'arbre a (de type Tree(A)) , donnant un arbre de type Tree(B).


Pour ce qui est de ta remarque sur la généricité, j'encourage à mettre des paramètres chaque fois que cela est possible. Je pense que c'est assez facile d'éduquer les programmeurs dans ce sens. Ceci dit il est vrai que le compilateur pourrait détecter le fait qu'un paramètre irait aussi bien qu'un type précis dans une définition et le signaler. C'est une idée qui me plait assez (je la trouve 'pédagogique').


Concernant l'exemple avec Matrix, regarde ce que j'ai fait dans mon post précédent avec 'Ord'. Je donnerai un autre exemple plus mathématique plus tard.

Avec ton histoire de a@12, je crois que tu exagères un peu quand-même. Ceci dit, on a pour Anubis (sous Windows seulement malheureusement pour le,moment) l'IDE de Cédric Ricard qui fait le genre de choses que tu dis, et qui rend la programmation plus facile.

Code :

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

1
2
3
4
5
6
7
8
define $U -> $V
   exemple
      (
         MonObjet m
      ) =
   if m is mon_objet(plus,times) then
   ($U u) |-> ... utiliser plus et times ici ...

Mmh... Et le else correspondrait à quoi ?

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.

Si j'ai bien compris, cela fait ce que je veux... sauf qu'il n'y a pas de vérification statique. Si on passe un objet n'ayant pas plus ou times, l'erreur sera rencontrée à l'exécution.

Tu te trompes complètement sur ce point. Il est impossible qu'un objet de type MonObjet n'ait pas le plus et le times. Fais quelques expériences avec Anubis et tu va voir s'il n'y a pas de vérification statique. De toute façon, avec Anubis, il n'y a jamais d'erreur au run-time. C'est tout simplement impossible. Cela tient à la conception mathématique du système. Sauf, je le précise quand même: si on a une mauvaise récursion qui fait sauter la pile (en fait dans ce cas on a seulement blocage du process concerné) ou si on fait comme Alex_pi un piège a GC avec des données cycliques. mais normalement on ne doit faire aucune donnée cyclique, car ça ne sert à rien. Elles seront effectivement interdites par le compilateur en Anubis 2, lequel vérifiera aussi la bonne fin de la récursion en imposant l'utilisation de schémas de récursion.

[DrTopos]

Non. Imaginons un code est écrit par un programmeur A et relu par un programmeur B. C'est le fait que B voie les types qui peut être utile, pas le fait que A les ait écrit. La différence est subtile, mais si un outil écrivait les types, plutôt que A lui-même, quel serait le problème ?

Avec Caml, il existe une option du compilateur pour générer le fichier interface. Avec F# et un bon éditeur, l'éditeur affiche les types sur simple demande.

Le compilateur Anubis a une option -index qu'on utilise comme ceci:

anubis -index *.anubis

et qui fabrique un joli fichier HTML plein de jolies couleurs avec toutes les definitions de types publics et toutes les déclarations de données publiques, y compris les constructeurs des types publics et les destructeurs implicites, et bien sûr des liens pour trouver les prototypes. Bizaremment, on s'en sert assez peu, mais ça existe.

[alex_pi]

Sauf, je le précise quand même: si on a une mauvaise récursion qui fait sauter la pile (en fait dans ce cas on a seulement blocage du process concerné) ou si on fait comme Alex_pi un piège a GC avec des données cycliques. mais normalement on ne doit faire aucune donnée cyclique, car ça ne sert à rien. Elles seront effectivement interdites par le compilateur en Anubis 2, lequel vérifiera aussi la bonne fin de la récursion en imposant l'utilisation de schémas de récursion.

Mais faut arrêter avec ça ! Ce n'est pas un "piège à glaneur de cellules" ! Un graphe cyclique, une liste doublement chaînée, un arbre où l'on peut remonter d'un fils à son père ne sont pas des pièges à GC, ce sont des structures indispensable. Arrêtez de tenter de trouver des excuses bidons à la piètre implémentation de votre langage.

Et qu'on ne viennent pas me dire que le langage n'a rien à voir avec l'implémentation, ou alors qu'on me file un lien vers la norme Anubis1. Un langage à implémentation unique (comme Anubis ou OCaml) est défini par son compilateur. Et dire qu'il ne faut plus parler de "cette implémentation qui a fait son temps" n'est pas fort sympathique pour les gens qui ont basé leur buisness sur cette implémentation.


Pour revenir au "problème" de typage OCaml, qui a été bien expliqué après, je signale deux choses. La première est que l'on peut obtenir des messages d'erreurs bien plus ludique tel que :

Code :

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

1
2
3
4
5
type int = A
let _ = A + 3

This expression has type int but is here used with type int

Et ensuite, on peut parfaitement définir "ce qui est voulu" par :

Code :

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

1
2
3
4
5
6
7
8
9
type toto = [`A | `B];;
type tutu = [`A | `C];;
# `A = `A;;
- : bool = true
# `A = `B;;
- : bool = false
# `A = `C;;
- : bool = false

Les types OCaml sont quand même un poil plus complexes que

Code :

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

1
2
type = int | float | char | type -> type

et heureusement.