Langage Qi - une opinion ?

[Canvas]

Bonjour,

Quelqu'un aurait-il une opinion sur le langage fonctionel Qi :

http://www.lambdassociates.org/

créé par Mark Tarver de l'Université d'État de New York.

Comment se positionne-t-il par rapport à des langages tels que Haskell ou OCaml ? (Est-ce que cette question a un sens ?).

Merci.

----
Canvas

[LLB]

On en a parlé un petit peu ici : http://www.developpez.net/forums/sho...d.php?t=475194

La différence avec Caml/Haskell, c'est que c'est avant tout un Lisp (s-expressions, macros...). Le langage me semble très intéressant et j'attends Qi II pour le tester vraiment. J'imagine que Qi offre beaucoup moins de garanties que Caml/Haskell et qu'il tend à être moins sûr (mais plus flexible, puisque le typage statique est optionnel).

[gorgonite]

Envoyé par alex_pi

Il faut vraiment que je regarde ca en detail un de ces 4. La possibilite d ajouter des regles de typage a volonte peut etre ammusant, mais je n'ai pas bien compris quelles garanties on obtient. Parce que quand on defini un nouveau systeme de type (ce que semble autoriser Qi), il est rarement trivial d en prouver la coherence (qu'en s'evaluant, une expression garde le meme type et qu'elle ne se trouve jamais bloquee). Parce que c'est bien d avoir un systeme de type plus "puissant" que celui d'Haskell, reste a voir s il est aussi fiable
Bref, je remets ca dans ma toread list!

Envoyé par bluestorm

En tout cas, le système de typage étant turing-complet, tu peux facilement te faire exterminer par le compilateur si tu fais pas gaffe.

La puissance vient avec des désavantages, forcément.

Ca y est, j ai un peu regarde Qi. Pour la faire courte, je ne suis pas franchement fan !

Pour commencer, je n'aime vraiment pas la syntaxe, mais bon, on va dire que ce sont les gouts et les couleurs hein

Par contre, je pense que c'est une tres mauvaise idee d'avoir une environnement globale d'association symbole<-> valeur et qu'il ne soit pas concerve dans les fermeture (chose heritee de Lisp, si je ne m'abuse) Je m'explique :

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(2-) (define f X -> 3)
f

(3-) (f 12)
3

(4-) (define g X -> (+(f X) (f X)))
g

(5-) (g 1)
6

(6-) (define f X -> X)
f

(7-) (g 1)
2

Moralite, on definit une fonction, on la teste, tout marche bien, et un jour on casse tout parcequ'on reutilise un nom sans faire attention..

Ensuite le systeme de type :

D'abord la partie "classique" du systeme de type : Je n'aime pas leur facon de definir des structures. En effet, on ne nomme pas les champs a la construction de la structure. Donc si on redefini un jour la structure (parcequ'on n'avait pas pense a tout des le debut, ce qui peut arriver ), mais que malheureusement les nouveaux champs sont differents pas avec le meme type que les anciens, on n'a aucun message d'erreur du typeur, mais la semantique se trouve etre mauvaise. Ensuite, je n'ai pas trouve comment rendre un champs de la structure mutable(mais je n'ai pas tout lu en detail). Enfin, je n'ai pas l'impression que l'on puisse faire de patern matching sur les structures.

A premiere vue, on se dit que c'est vachement puissant de pouvoir jouer avec le calcul des sequents dans un systeme de type. Ca donne effectivement beaucoup de liberte. Mais en fait tellement de liberte qu'il n'y a plus aucune surete de typage. Il est vraiment facile de s'emmeler les pinceau.
Premiere erreur, utiliser une fonction qui ne termine pas dans la definition d'un type

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
(1+) (define f
{A --> bool}
X -> (f X))
f : (A --> bool)

(2+) (datatype foo
if (f Foo)
___________
Foo : foo;)        
foo : unit

(3+) foo : foo

Hop, le typage ne terminera jamais... On va dire qu'il "suffit" de faire attention aux fonctions qu'on utiliser

Par contre ce qui est beaucoup plus problematique est que la theorie des types de Qi n'apporte aucune securite. En effet, puisqu'on peut y ajouter n'importe quel axiome ou n'importe quelle regle, et que la coherence est evidement indecidable, on peut facilement se retrouver avec une theorie totalement incoherente.
Avec une simple mauvaise regle, on retourne aux erreur de typage dynamique :

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
(0-) (+ "kikoo" "lol")

+: "kikoo" is not a number


(1-) (tc +)
true

(2+) (+ "kikoo" "lol")
error: type error

(3+) (datatype subtype
X : string;
__________
X : number;)
subtype : unit

(4+) (define bad
{A --> number}
X -> (+ "kikoo" "lol"))
bad : (A --> number)

(5+) (bad 4)

+: "kikoo" is not a number

On peut ensuite utiliser la redefinition de fonction pour casser le systeme de type, etc.

On pourrait se dire a la rigueur que ce n'est pas bien grave, qu'il suffit de ne pas utiliser les sequents si on n'est vraiment pas sur de soi, mais malheureusement, un simple type union a besoin du calcul des sequents pour etre defini.

Pour resumer, je ne vois pas dutout l'interet d'avoir un systeme de type s'il n'apporte au final aucune securite. Si tout repose sur le programmeur, autant ne pas s'embeter et simplement faire du typage dynamique.
Je pense que s'il on veut un systeme de type tellement puissant, il faut carrement un prouveur de theoreme. Parceque c'est bien beau de pouvoir definir le type "entier positif", mais il y peu de chance qu'on puisse faire autre chose que definir l'addition dessus, sauf a rajouter a chaque fois de nouveaux axiomes au type pour typer chaque fonction, ce qui finalement n'apporte plus rien.

Sinon, est ce que quelqu'un a trouve comment faire un set quand on est en mode type, ou comment definir des variables locales ? Pour mes tests de "desucre" la definition de variable par application de fonction, mais c'est inbouffable !

Ah ouais, j'aime pas non plus le fait que l'on puisse definire des tableaux sans rien mettre dedans :

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(0-) (set *blih* (make-array [1]))
#[#\Escape]

(1-) (get-array (value *blih*) [0] #\a)
#\a

(2-) (put-array (value *blih*) [0] #\b)
#\b

(3-) (get-array (value *blih*) [0] #\a)
#\b

(4-) (put-array (value *blih*) [0] #\Escape)
#\Escape

(5-) (get-array (value *blih*) [0] #\a)
#\a

Je fais comment pour mettre la valeur #\Escape dans un tableau ? ( bien sur, je pourrais dire que si c'est non defini, je veux recupere #\Escape, pas c'est completement pas pareil...)

[InOCamlWeTrust]

Si le mec qui a fait le langage est américain ou possède une culture américaine de la programmation, c'est vrai qu'il y aura des choses qui peuvent, à nous petits français, nous choquer. C'est une différence, voire une divergence, culturelle. Pourquoi les américains préfèrent-ils Scheme/Lisp à ML ? C'est purement culturel, je pense.

Ensuite, une personne fait un langage nouveau, avec des concepts novateurs, et bien moi, à défaut de l'applaudire, je le félicite, essentiellement pour l'initiative, l'informatique étant entrée, d'après moi, dans une longue léthargie depuis Java.

Enfin, il est sûr que la liberté se gagne en faisant des concessions sur la sûreté du typage, mais ça, tout le monde en est conscient. Mais, franchement, beaucoup de fois je me demande si le gros rouleau compresseur de l'inférence de types à la OCaml (n'oublions pas la couche objet !) est bien justifié dans la pratique.

En effet, c'est très joli de prouver que ta fonction retournera une valeure du type x non du type y ou tout autre type incompatible, mais ça ne fait faire, dans 99.99% des cas, aucun progrès quant à la preuve de l'algorithme !

Globalement, tout ce que je dis c'est que s'il n'y a pas de surete apporte par le typage, pourquoi s'emmerder a en avoir un ? Il faut le dire, un systeme de type, it's a pain in the ass, donc si tu n'as pas une bonne compensation, de la surete principalement, autant ne pas en avoir. Pour avoir tente d'ecrire un certain nombre de chose en Qi, je le trouve pas mal prise de tete (en mode type), alors qu'en python par exemple, tout coule de source. Et s'etre debarasse de l'affectation de variable des qu'on passe en mode type, ca fait un peu mal. Et des nouveaux langages, il y en a toutes les semaines.
Apres, pour la partie non type, c'est sans doute un gros progres pour Lisp, je ne dis pas le contraire.

PS : desole pour les accents, je n'en n'ai pas sur mon clavier...

[gorgonite]

Envoyé par InOCamlWeTrust

l'informatique étant entrée, d'après moi, dans une longue léthargie depuis Java.

Envoyé par alex_pi

Et des nouveaux langages, il y en a toutes les semaines.

des langages réellement utilisables, qui ne soient pas uniquement le fruit d'un délire de chercheur au fond de son labo qui a oublié qu'en l'informatique il faut parfois aussi penser à essayer de pouvoir faire quelque chose d'utile avec son "nouveau" langage, et non une simple variation à epsilon près d'un truc sorti 2 mois plus tôt dans le seul but de publier son 6ème papier de l'année... j'ai comme un doute sur la fréquence de sortie de "vrais" nouveaux langages


enfin de là à dire que depuis Java (qui n'est pas réellement une nouveauté au passage), il n'y a pas eu de vrais nouveaux langages... faut pas pousser


je dirais au moins C# (qui est une belle évolution de Java, même si je ne suis pas fan ), F# (qui n'est pas qu'un clone d'OCaml comme certains aimeraient le faire croire) et Fortress...
et n'oubliez pas Anubis de notre cher DrTopos (même si ce n'est pas forcemment une grande réussite en pratique, soyons réalistes, il a le mérite de fonctionner, et d'être nouveau)

Envoyé par InOCamlWeTrust

Enfin, il est sûr que la liberté se gagne en faisant des concessions sur la sûreté du typage, mais ça, tout le monde en est conscient.

pas toujours justement : il faut garder à l'esprit que la pensée unique des Design Pattern (qui sont souvent utiles ), prive bien plus les programmeurs de liberté que le typage fort... et lorsqu'ils sont utilisés à mauvais escient on se trouve dans des conglomérats extrêmement lourds d'encapsulation hasardeuses

Envoyé par InOCamlWeTrust

Mais, franchement, beaucoup de fois je me demande si le gros rouleau compresseur de l'inférence de types à la OCaml (n'oublions pas la couche objet !) est bien justifié dans la pratique.

En effet, c'est très joli de prouver que ta fonction retournera une valeur du type x non du type y ou tout autre type incompatible, mais ça ne fait faire, dans 99.99% des cas, aucun progrès quant à la preuve de l'algorithme !

perso, j'aurais deux "reproches" à faire :

• il semble désormais y avoir une pensée "unique" dans la façon de créer des langages fonctionnels typés fortement passant par des type checker, qui ne peuvent malheureusement pas toujours typer des fonctions mathématiquement correctes... je me demande juste si l'on ne peut avoir un langage fonctionnel à typage fort et explicite (ce qui reste possible étant donné qu'on joue surtout avec du polymorphisme paramétrique)
• pourquoi penser que seul les systèmes de type des langages fonctionnels peuvent être conceptuellement puissants ?

Envoyé par alex_pi

Globalement, tout ce que je dis c'est que s'il n'y a pas de surete apporte par le typage, pourquoi s'emmerder a en avoir un ? Il faut le dire, un systeme de type, it's a pain in the ass, donc si tu n'as pas une bonne compensation, de la surete principalement, autant ne pas en avoir.

le système de type peut également être très utile pour la réutilisation d'une bibliothèque par un "novice" qui va s'en servir, pour donner des informations aux analyseurs de code, de jolies documentations avec graphes de dépendances, etc

[LLB]

Envoyé par alex_pi

Globalement, tout ce que je dis c'est que s'il n'y a pas de surete apporte par le typage, pourquoi s'emmerder a en avoir un ?

Il y en a une, même si elle n'est pas parfaite. J'imagine tout à fait que l'on est loin de la sûreté offerte par Caml/Haskell, mais peut-être est-elle supérieure à ce que l'on a dans Java/C# ? Si c'est le cas, alors je trouve le concept très intéressant.

Si tout repose sur le programmeur, autant ne pas s'embeter et simplement faire du typage dynamique.

Puisque le typage est programmable, il a besoin d'être testé et débogué comme n'importe quel autre outil. C'est du travail et on ne veut pas s'amuser à le faire à tout va. Pour moi, ces règles de typage ont leur intérêt les bibliothèques. La bibliothèque standard fournit un certain nombre de règles, je crois, et les bibliothèques annexes peuvent faire de même. En imaginant que ces bibliothèques soient correctement conçues, on obtient un résultat assez sûr, non ?

On pourrait se dire a la rigueur que ce n'est pas bien grave, qu'il suffit de ne pas utiliser les sequents si on n'est vraiment pas sur de soi, mais malheureusement, un simple type union a besoin du calcul des sequents pour etre defini.

Pour moi, l'utilisateur moyen devrait éviter de définir ses propres règles. Est-ce qu'un type union est difficile à écrire ? Si non, alors ça me semble acceptable.

Envoyé par LLB

J'imagine tout à fait que l'on est loin de la sûreté offerte par Caml/Haskell, mais peut-être est-elle supérieure à ce que l'on a dans Java/C# ?

Justement non, il n'y a aucune sûreté. Par exemple si tu mets la rêgle

Code :

1
2
3
4
(datatype oops

__________
X : A;)

Tu peux donner n'importe quel type à n'importe quelle expression :

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
(0-) (3 4)
error: Odd application; 3 to 4


(1-) (tc +)
true

(2+) (3 5)
error: type error


(3+) (datatype oops

__________
X : A;)
oops : unit

(4+) (3 5)
error: Odd application; 3 to 5


(5+) "kikoo" : number
"kikoo" : number

(6+) "kikoo" : (number --> string)
"kikoo" : (number --> string)

Envoyé par LLB

Puisque le typage est programmable, il a besoin d'être testé et débogué comme n'importe quel autre outil.

Justement, ma vision du typage est que c'est un outil de débugage, qui doit aider à écrire des programmes "corrects". Quand j'écris un type union en Caml, je me demande s'il correspond à ce que j'attends, pas s'il est correct. Ce n'est pas mon boulot de programmeur de prouver mon système de type. (ou alors je fais du Coq..)

Envoyé par LLB

Pour moi, ces règles de typage ont leur intérêt les bibliothèques.

C'est un peu le principe de la programmation fonctionnelle de définir des types correspondant à chaque problème non ?

Envoyé par LLB

La bibliothèque standard fournit un certain nombre de règles, je crois, et les bibliothèques annexes peuvent faire de même. En imaginant que ces bibliothèques soient correctement conçues, on obtient un résultat assez sûr, non ?

A condition de ne pas les casser retrospectivement par redefinition malencontreuse de fonction, je suppose que oui.

Envoyé par LLB

Pour moi, l'utilisateur moyen devrait éviter de définir ses propres règles.

Dans le cas de Qi, clairement...

Envoyé par LLB

Est-ce qu'un type union est difficile à écrire ? Si non, alors ça me semble acceptable.

C'est un peu verbeux, mais pas "difficile", et si on s'y tiens bien, probablement peut sujet à erreur.

[LLB]

La philosophie de Lisp est de mettre le moins de contraintes possible. C'est à l'utilisateur de se limiter et de ne pas faire n'importe quoi, et non au langage d'imposer des limitations plus ou moins arbitraires. Je trouve que Qi respecte bien cette vision des choses.

Si on garde le système de types par défaut, c'est assez sûr. Si on n'est pas sûr de soi, on peut le garder tel quel. Tu as dit qu'ajouter un type somme n'est pas difficile. Au pire, je suppose qu'on pourrait même ajouter une macro defunion pour rendre ça plus facile, moins verbeux et moins sujet à erreur. Juste avec ça, je suis heureux.

De même, C++ est assez sûr comme langage, si on oublie un certain nombre d'héritages du C. Caml est très sûr, si on ne cherche pas à tout casser avec de la magie. Qi semble assez sûr, si on ne casse pas soi-même le système de typage.

L'approche de Qi me semble donc très intelligente.

[InOCamlWeTrust]

Pour moi, un langage sûr, c'est un langage qui ne segfault'e pas... Du moment que l'on a ça, je suis content !

Le gros problème du C et du Fortran vient du fait que l'on peut assez facilement segfault'er ; cependant, en programmant avec hygiène (comme les petits enfants, on se lave les mains avant de passer à table !), on ne segfault'e jamais. Pour ma part, mon dernier segfault en C remonte à il y a pas mal de temps ! En Fortran, c'est une autre paire de manches, surtout à cause du système de types qui est ultra-pourri-de-chez-pourri.

Le gros avantage de ces langages-là, c'est que bien maîtrisés, ils apportent une sûreté incomparable aux programmes.

Le gros avantage des langages un peu plus doux comme OCaml, Haskell et tout le tralala (mettre aussi Java), c'est que ça ne segfault'e jamais... mais ça jette des exceptions plein la gueule, et franchement, quand on lance Eclipse dans un terminal, il y a des fois on a vraiment très peur ! De plus, si l'implantation n'est pas toujours de qualité, on peut se retrouver avec des problèmes de segfault alors même que le code est simple et tout à fait valable et l'algorithme est juste. C'est ainsi que, sous une version antérieure de Hugs, j'avais des problèmes à cause d'une implantation qui buguait.

Là encore, le produit miracle vu à la TV n'existe pas : tout est question de juste mesure.

[HanLee]

Envoyé par InOCamlWeTrust

Pour moi, un langage sûr, c'est un langage qui ne segfault'e pas... Du moment que l'on a ça, je suis content !

Le gros problème du C et du Fortran vient du fait que l'on peut assez facilement segfault'er ; cependant, en programmant avec hygiène (comme les petits enfants, on se lave les mains avant de passer à table !), on ne segfault'e jamais. Pour ma part, mon dernier segfault en C remonte à il y a pas mal de temps ! En Fortran, c'est une autre paire de manches, surtout à cause du système de types qui est ultra-pourri-de-chez-pourri.

Le gros avantage de ces langages-là, c'est que bien maîtrisés, ils apportent une sûreté incomparable aux programmes.

Le gros avantage des langages un peu plus doux comme OCaml, Haskell et tout le tralala (mettre aussi Java), c'est que ça ne segfault'e jamais... mais ça jette des exceptions plein la gueule, et franchement, quand on lance Eclipse dans un terminal, il y a des fois on a vraiment très peur ! De plus, si l'implantation n'est pas toujours de qualité, on peut se retrouver avec des problèmes de segfault alors même que le code est simple et tout à fait valable et l'algorithme est juste. C'est ainsi que, sous une version antérieure de Hugs, j'avais des problèmes à cause d'une implantation qui buguait.

Là encore, le produit miracle vu à la TV n'existe pas : tout est question de juste mesure.

Ouaip, mais mieux vaut un segfault qui te met en face de tes problèmes qu'un programme qui tourne silencieusement avec des valeurs incorrectes, sans bug apparent, alors qu'il en cache un.

Envoyé par InOCamlWeTrust

Le gros avantage de ces langages-là, c'est que bien maîtrisés, ils apportent une sûreté incomparable aux programmes.

Le C ????

[gorgonite]

Envoyé par alex_pi

Le C ????

ben le dogme disant que seul OCaml peut apporter de la sureté en programmation, est tout aussi difficile à croire

Envoyé par gorgonite

ben le dogme disant que seul OCaml peut apporter de la sureté en programmation, est tout aussi difficile à croire

OCaml fait partit *des* langages qui apporte *de la* sureté en programmation. A la rigueur, on peut dire que le C apporte de la sureté de programmation par rapport à l'assembleur, ou bien on peut dire qu'un bon programmeur peut écrire en C des langage qui s'avèrent sûrs, mais le C en lui même n'y est pour rien :-\

[gorgonite]

Envoyé par alex_pi

on peut dire qu'un bon programmeur peut écrire en C des langage qui s'avèrent sûrs, mais le C en lui même n'y est pour rien :-\

ben un mauvais programmeur caml fera également plein de crash bizarres... pas de segfault, mais des exceptions à tout va et non récupérées

Envoyé par gorgonite

ben un mauvais programmeur caml fera également plein de crash bizarres... pas de segfault, mais des exceptions à tout va et non récupérées

Ca va finir par se voir là, la mauvaise foi :-p

[HanLee]

Envoyé par gorgonite

ben un mauvais programmeur caml fera également plein de crash bizarres... pas de segfault, mais des exceptions à tout va et non récupérées

Mais il fera moins d'erreurs du style accès à un pointeur nul s'il avait eu un type option, parce qu'il serait obligé de filtrer.

S'il manipule des arbres, il n'aura jamais de problème de pointeurs nul, mais que des algorithmes faux au pire ou qui ne terminent pas (à double tranchant ça, voir mon message précédent).

Il n'aura plus de problème dû à une conversion float > int implicite non désirée.

[gorgonite]

Envoyé par alex_pi

Ca va finir par se voir là, la mauvaise foi :-p

aucune mauvaise foi... trop de monde préféreront faire vite et sale

juste un constat qui déplait à une certaine élite :

1. la majorité des codeurs n'ont pas un Doctorat en Info, et il conviendrait que les langages qu'ils utilisent ne demandent pas de tels pré-requis
2. beaucoup de codeurs veulent pouvoir faire du "prêt-à-jeter" en raison des délais trop courts que leurs supérieurs incompétents leur imposent... donc si l'on peut se passer de certaines contraintes, on le fait
3. la conception devant être indépendante des langages (car les formateurs n'ont pas toujours le niveau dans le langage utilisé dans la boite, mais maitrise bien le domaine étudié (IHM, SGBD, protocole bancaire, etc), il serait bon de pouvoir avoir des outils de conversion automatiques depuis les trucs à la mode style UML vers le langage cible (sans forcemment devoir faire de l'objet )

Envoyé par gorgonite

la majorité des codeurs n'ont pas un Doctorat en Info, et il conviendrait que les langages qu'ils utilisent ne demandent pas de tels pré-requis

C'est justement ce que je reproche à Qi, c'est que son système de type nécessite un Doctorat, alors que celui de Caml ne nécessite qu'un master :-p