Discussion :

[alex_pi]

Je ne sais pas si vous étiez au courant de son existance :
http://www.ccs.neu.edu/home/samth/typed-scheme/

[LLB]

Dans la même idée, il y a aussi le langage Qi qui est très intéressant :
http://www.lambdassociates.org

C'est basé sur Lisp, ça offre des fonctionnalités venant de ML (pattern matching, lambda calcul et applications partielles) et possède un système de typage statique très puissant (plus que celui de ML, parait-il).

[alex_pi]

Dans la même idée, il y a aussi le langage Qi qui est très intéressant :
http://www.lambdassociates.org

C'est basé sur Lisp, ça offre des fonctionnalités venant de ML (pattern matching, lambda calcul et applications partielles) et possède un système de typage statique très puissant (plus que celui de ML, parait-il).

Déjà, être plus puissant que ML, ce n'est pas très difficile. En effet, ML (OCaml en particulier) a fait le choix du "tout inférable", ce qui limite un certain nombre de chose (entre autre au niveau du polymorphisme, les "pourtout" sont en début de type, et pas au milieu)

Ensuite j'ai jeté un coup d'oeil a leur définition de type par calcul des séquents. Je suis un peu sceptique. Le typage d'un programme m'a l'air fortement indécidable, et je ne vois pas suffisement d'aspect "système de preuve" pour mettre le compilo sur la bonne voie. Typiquement l'exemple donné de liste de 0 et de 1, je dis chapeau si le compilo est capable de trouver qu'une fonction qui prend en argument une liste d'entier et retourne la liste où on a divisé chaque élément non nul par lui même retourne bien une liste de type "que des 0 et des 1".

Pour résumer, ça m'a l'air à mi chemin entre un langage de programmation "normal" et un système de preuve, mais dans une situation peu utile. Mais je n'ai pas regardé en détail, ce n'est donc pas un jugement catégorique !

[LLB]

Déjà, être plus puissant que ML, ce n'est pas très difficile. En effet, ML (OCaml en particulier) a fait le choix du "tout inférable", ce qui limite un certain nombre de chose (entre autre au niveau du polymorphisme, les "pourtout" sont en début de type, et pas au milieu)

En effet. Mais on trouve assez peu de systèmes de typage plus fins que celui d'OCaml (parmi les langages "classiques").

Je suis un peu sceptique. Le typage d'un programme m'a l'air fortement indécidable, et je ne vois pas suffisement d'aspect "système de preuve" pour mettre le compilo sur la bonne voie.

Je n'ai pas eu le temps de regarder comme je l'aurais voulu, mais j'ai lu que : le système de typage est décidable ; c'est un "vrai" langage de programmation (pas un système de preuves).

Typiquement l'exemple donné de liste de 0 et de 1, je dis chapeau si le compilo est capable de trouver qu'une fonction qui prend en argument une liste d'entier et retourne la liste où on a divisé chaque élément non nul par lui même retourne bien une liste de type "que des 0 et des 1".

Je suis d'accord, j'imagine qu'il échoue ici. Il faut peut-être l'indiquer à la main (si x / x = 1, ajouter 1, sinon 0). Je ne suis pas sûr, je regarderai.

Pour résumer, ça m'a l'air à mi chemin entre un langage de programmation "normal" et un système de preuve, mais dans une situation peu utile. Mais je n'ai pas regardé en détail, ce n'est donc pas un jugement catégorique !

Je n'ai pas regardé en détail non plus, mais j'ai vu que :
- le typage statique est optionnel
- c'est basé sur Lisp (c'est donc au moins aussi utilisable que Lisp)
- ça supporte des fonctionnalités de ML : lambda, applications partielles, pattern matching.

Tout laisse à croire que le langage est réellement utilisable. Le résultat me semble très intéressant : les exemples sont élégants, et ils annoncent du code 30% plus concis que Lisp.

Pour un développeur Lisp, ça peut être une alternative à étudier. Pour un développeur ML/Haskell, ça peut être l'occasion d'apprendre un dialecte Lisp.

[Garulfo]

Quel est l'intérêt de faire du Scheme typé ?
L'intérêt principal que je trouve à Scheme est qu'il n'a pas de typage.
S'il n'y a plus ça, il me semble qu'un langage comme ocaml ou haskell est plus intéressant.

[alex_pi]

Quel est l'intérêt de faire du Scheme typé ?
L'intérêt principal que je trouve à Scheme est qu'il n'a pas de typage.
S'il n'y a plus ça, il me semble qu'un langage comme ocaml ou haskell est plus intéressant.

En gros l'idée c'est : les gens ont craché un programmes de 60 000 lignes de scheme, je dois le maintenir, mais je vais pas le réécrire. Le typer me permettra d'être plus sûr de comprendre ce qu'il fait. (enfin si j'ai bien compris l'idée J'ai jamais fait de Scheme de ma vie, je copiais le lien ici pour faire profiter ceux que ça intéresse :-))

[LLB]

S'il n'y a plus ça, il me semble qu'un langage comme ocaml ou haskell est plus intéressant.

Je trouve ca assez réducteur.

Le système de typage est optionnel : tu peux l'activer dans certaines fonctions et le désactiver dans d'autres. Cela t'assure donc une compatibilité avec les programmes existants (et tu n'as pas besoin d'apprendre un nouveau langage). De plus, tu bénéficies toujours de la puissance de Lisp (entre autres, son système de métaprogrammation super puissant).

Pour mieux comprendre le système de typage de Qi :
http://programmingkungfuqi.blogspot....rime-type.html
Cet exemple crée et utilise le type "nombre premier". C'est assez intéressant ; le système est toujours décidable (mais s'il n'a pas assez d'information, il ne réussira pas à typer).

Pour l'exemple de la liste de 0, 1, il ne devinera en effet pas que x / x renvoie 1 ou que x % 2 renvoie 0 ou 1. Mais, on peut lui dire : il suffit d'ajouter une règle dans le système de typage. Ce système n'est pas parfait, mais ca me semble relativement intelligent.

Et si je devais me mettre un jour à Lisp, il y a des chances pour que je me tourne vers Qi.