Je ne sais pas si vous étiez au courant de son existance :
http://www.ccs.neu.edu/home/samth/typed-scheme/
Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter
Typed Scheme (Un système de type pour Scheme)
Je ne sais pas si vous étiez au courant de son existance :
http://www.ccs.neu.edu/home/samth/typed-scheme/
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)Envoyé par LLB
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 !
En effet. Mais on trouve assez peu de systèmes de typage plus fins que celui d'OCaml (parmi les langages "classiques").
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).
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.
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.
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éeJ'ai jamais fait de Scheme de ma vie, je copiais le lien ici pour faire profiter ceux que ça intéresse :-))
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.
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éeAttention, je reprécise ce que j'ai dit : parfois je trouve très intéressant d'avoir un système de typage, mais la force de Scheme pour moi réside dans l'absence de typage.
@Alex_pi: Le typage ne t'aidera pas à comprendre si le programme est mal fait. Du moins ça n'a jamais été un avantage mis en avant pour argumenter pour le typage. Le lisp, en général, et le scheme, en particulier, se lise très bien car tu retrouves souvent la même liberté qu'en mathématique. MAIS il y a aussi des développeurs qui sont mauvais.
Donc, je réitère ce que je disais: bien que comprennant l'avantage d'avoir un système de typage, il me semble que si je voulais vraiment du typage, je m'orienterais vers autre chose que Scheme + Qi... plutôt vers Haskell maintenant. Avec du typage, je perds la liberté de faire du lambda calcul pur.
Finis le (lambda (a b) (a b a))
Je sais que certains pensent que ça n'a aucun intérêt pratique, mais je pense que ça en a théorique et notamment en recherche.
Là je ne suis pas vraiment d'accord. Quand je regarde http://caml.inria.fr/pub/docs/manual...ref/Map.S.html, je lis généralement la signature d'une fonction plus que sa description pour savoir dans quel sens mettre les arguments et même simplement pour comprendre ce qu'elle va faire (bon, avec l'aide du nom aussi :-)
Mais justement... le nom est 1000 fois plus significatifs que la signature qui donne une idée de l'interface. Et si tu veux connaitre les préconditions tu n'as pas le choix de regarder la documentation ou lire un peu plus le code. La signature ne suffit pas.
Encore une fois, je n'ai pas dit que le typage est inutile: dans ma réponse je disais que si le programme est mal fait le typage ne t'aide pas ! Si le programme est bien fait, le typage aide c'est sûr.
Exemple:
je ne vois pas à quoi servent les signatures pour comprendre les fonctions. J'ai volontairement changé le nom de la fonction bien sûr
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2
3f: (key -> 'a -> 'b) -> 'a t -> 'b t g: (key -> 'a -> unit) -> 'a t -> unit h: ('a -> 'b) -> 'a t -> 'b t– même en sachant qu'on parle des associations (Map.S).
Bah justement, je vois directement ce que fait chacune de ces fonctions rien qu'en regardant la signature...
Exemple:
je ne vois pas à quoi servent les signatures pour comprendre les fonctions. J'ai volontairement changé le nom de la fonction bien sûr
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2
3f: (key -> 'a -> 'b) -> 'a t -> 'b t g: (key -> 'a -> unit) -> 'a t -> unit h: ('a -> 'b) -> 'a t -> 'b t
Pour le coup je suis complètement d'accord avec AlexPi, sauf erreur, ces fonctions correspondent à "map_with_key", "iter_with_key" et "map" pour le type t.
--
Jedaï
100% d'accord avec alex_pi :
- je lis la signature
- je lis le nom
- s'il reste encore un doute je lis la documentation
Exemple:
Clairement la doc ne sert à rien: tout est dit dans la signature.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2# List.map;; - : ('a -> 'b) -> 'a list -> 'b list = <fun>
Mouais vous ne me convainquez pas.
Vous saviez ce que vous cherchiez, et Jedaï connait bien le module (n'est-ce pas?) Puis vous ne connaissez toujours pas les préconditions.
Si je vous donne une fonction comme ça:
vous savez à quoi elle correspond ?
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2f: ('a -> 'b) -> 'a -> 'b
Soit vous êtes extrêmement fort, soit j'ai raté un énorme morceau dans ce cas.
Tout est dit ?
Donc la fonction que j'ai signé au dessus est quoi (juste avec la signature puisque tout est dit) ?
Remarquez que si le nom n'est pas utile, on peut jouer à un jeu.
Je vous donne les signatures d'un programme que j'ai écris et vous devinez ce qu'elles font ? Inversement je vous donne un programme en Scheme sans les signatures et vous me dites ce que vous comprennez. On verra si les signatures sont plus importantes que les noms.
Je vois mal comment ta fonction pourrait être autre chose que l'identité:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2# let f (g:'a->'b) = g;; val f : ('a -> 'b) -> 'a -> 'b = <fun>
Non, je ne me souviens pratiquement pas des modules OCaml, les noms que j'ai donné sont descriptifs mais ça m'étonnerait qu'il correspondent exactement au noms du module.
Tu as beau t'obstiner, le type de ces fonction était parfaitement suffisant dans ce cas pour deviner leur but. Ce n'est pas toujours le cas, entendons nous, mais plus la fonction est polymorphe plus c'est simple (les possibilités sont plus restreintes), ajoute à ça l'indice que constitue le nom de type "key"...
Bien sûr un type comme "int -> double -> double" ou autre du genre n'est pas suffisant, il nous faut le nom de la fonction, et éventuellement de la doc.
Dans un langage comme OCaml ou Haskell, cette fonction ne peut être que l'identité (ou bottom pour Haskell), aucune autre fonction n'appartient à ce type, sauf si tu triches en fouillant les entrailles du langage (ou plutôt d'une de ses implémentations, distinction plus valide en Haskell qu'en OCaml bien sûr).
(Ou tu peux la voir comme l'application, mais c'est la même chose, à l'interprétation du nombre d'argument près)
--
Jedaï
100% avec Jedaï, tout était dit dans la signature.
On n'a pas dit que le nom était inutile, on a dit que dans plein de cas, la signature seule donne énormément d'information (parfois plus que le nom) sur la fonction. Tu as l'air de penser que la signature ne sert pratiquement à rien (excepté du point de vue mécanique de vérification de la correction), c'est ce point de vue que nous contestons.
--
Jedaï
Répondre avec citation
Partager