Découvrir MetaOCaml dans son navigateur

a marqué ce sujet comme résolu.

(gustavi travaille en ce moment sur des tribunes pour ZDS, qui seraient un peu comme des billets de blog, pas des news ni vraiment des topics sur le forum. Je pense que le contenu ci-dessous serait adapté à une tribune, mais comme ça n'existe pas pour l'instant je le mets sur le forum; ça fait un peu bizarre hors contexte, mais c'est comme ça.)

OCaml est un langage de programmation généraliste, fonctionnel et statiquement typé.

MetaOCaml est une extension, un dialecte non-standard du langage qui a une longue histoire. Dérivée de MetaML il y a environ 15 ans, c'est toujours resté un prototype de recherche, avec une base d'utilisateur petite mais active au fil des années – au contraire de la plupart des prototypes de recherche qui meurent de mort naturelle assez vite. Le "Meta" dans le nom fait référence à la méta-programmation, l'écriture de programmes qui manipulent de programmes, et MetaML et MetaOCaml sont dans la catégorie de la méta-programmation "étagée" (staged), où il y a un nombre arbitraire de "niveaux d'exécution" qui construisent des morceaux de programme des niveaux précédents et les font tourner. (Par opposition il y a des langages où il y a un nombre fixe de niveau, par exemple "statique / à la compilation" et "dynamique / à l'exécution", comme en C++ ou D, beaucoup de langage à "macros" où la méta-programmation se résume à une passe de récriture de code, et des langages où la notion de niveaux est plus floue et plus complexe, et est combinée avec des récritures syntactiques de nature un peu différente et moins structurée, comme en Scheme, Lisp ou Racket).

Une façon de penser à MetaOCaml, c'est que c'est un langage pour décrire des optimisations de la forme "et si on spécialise comme-ci ou comme-ça à la compilation, on peut obtenir du super code au final", mais où la distinction entre ce qui est spécialisé "à la compilation" et ce qui est exécuté au final est explicite, elle ne repose pas sur l'intelligence du compilateur mais sur des marqueurs explicites insérés par le programmeur ou la programmeuse. (Il y eu beaucoup de recherche sur l'évaluation partielle comme super-optimisation, et le consensus de la communauté c'est que c'est puissant mais trop fragile / difficile à prévoir pour qu'on puisse laisser le compilateur le faire sans guidage humain).

Un récent exemple d'utilisation de la technique est Stream Fusion, to Completeness, un article qui utilise cette forme de méta-programmation pour optimiser des programmes décrivant des manipulations de flots de données, avec une version en OCaml (utilisant MetaOCaml) et une version en Scala (utilisant "LMS", Lightweight Modular Staging, une autre approche de la méta-programmation par étage), et qui implémentent comme une librairie des optimisations puissantes de "fusion" qui sont traditionellement espérées du compilateur. (Ce travail va être présenté à Paris en janvier 2017, puisque les universités Paris 6 et Paris 7 accueillent et organisent cette année une des principales conférences de recherche en langages de programmation, et d'ailleurs si vous êtes étudiants et que vous voulez y aller et manger sur place mais pas payer les frais d'inscriptions vous pouvez vous proposer comme volontaire pour aider.)

Ne nous laissons pas distraire. Le sujet de ce post c'est un cours sur MetaOCaml disponible en ligne, créé par Jeremy Yallop à l'université de Cambridge, C'est une sous-partie du cours Advanced Functional Programming, qui s'adresse à des gens connaissant déjà la programmation fonctionnelle mais pas forcément ses aspects les plus avancés. La partie sur MetaOCaml est à la fin, et elle est disponible (comme le reste) sous la forme de cahiers interactifs dans le navigateur (ça utilise IOCamlJS, un noyau IPython/Jupyter pour OCaml):

Voilà, bonne lecture.

+11 -0

Oh, ça a l’air bien tout ça. Ça fait un moment que je me dis qu’il faut que je me (re)mette à l’OCaml, notamment pour travailler avec l’extraction de Coq. Ça peut être l’occasion de me replonger dans le language et d’apprendre des nouveaux trucs.

+0 -0

Les Haskelleux qui ont l'occasion de programmer en OCaml ont tendance à se pincer un peu le nez, principalement à cause de l'absence de type-classes (il y a un projet là-dessus en court mais il n'est pas encore question de l'intégrer dans le langage), mais c'est effectivement un langage qui est rigolo aussi, et MetaOCaml peut être une raison de venir voir par chez nous. Par ailleurs, Coq a aussi une extraction expérimentale vers Haskell, qui marche moins bien car elle n'a pas d'utilisateur assez actif – si des gens étaient prêt à mieux la maintenir, ça pourrait devenir un outil plus complet.

Je maîtrise mal (pas du tout) l’extraction encore. J’ai pu pas mal bidouiller le côté preuves de Coq, mais à part extraire des choses un peu au pif pour voir quelle tête ça a, je n’ai pas d’experience dedans.

J’ai vu que certains ont commencé à réimplémenter des bouts de Prelude en Coq, notamment pour améliorer l’expérience d’extraction vers Haskell et aussi, j’imagine, pour être en mesure de prouver les différentes lois de type-classes. J’ai trouvé ça rigolo.

+0 -0

Les Haskelleux qui ont l'occasion de programmer en OCaml ont tendance à se pincer un peu le nez, principalement à cause de l'absence de type-classes (il y a un projet là-dessus en court mais il n'est pas encore question de l'intégrer dans le langage)

gasche

Parce que c'est trop tôt ? Ou il y a d'autres raisons ?

Je ne travaille pas dessus moi-même donc je n'ai pas une vision claire – il s'agit de modular implicits – mais je pense que la réponse est plus proche de "c'est trop tôt": à ma connaissance les gens qui travaillent dessus n'ont pas encore décidé que c'était "prêt" à être proposé à l'inclusion. Mais les dernières versions que j'ai vues semblent vraiment abouties, donc j'espère que ce sera le cas bientôt¹.

¹: Le temps de la recherche est un temps long. Bientôt ça peut vouloir dire "je vais bosser sur autre chose pendant 8 mois et ensuite m'y remettre".

Ce qui me semble clair à moi c'est qu'il y a consensus aujourd'hui dans la communauté que tout langage typé a besoin d'un mécanisme de code inféré/deviné à partir des types (type-classes ou implicits), parce que c'est la bonne façon de gérer beaucoup de choses importantes pour l'utilisabilité du langage (sérialisation, affichage, surcharge des opérateurs numériques…). Modular implicits est un bon travail, il y a eu en particulier un super travail pour avoir une implémentation utilisable et on a des retours dessus, j'ai confiance que ça va aboutir à quelque chose.

Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte