Les classes de type marchent assez bien pour gérer le type Dyntype a, parce que c'est typiquement le genre de valeurs que tu veux passer implicitement, et pour lequel tu n'as pas envie/besoin d'avoir plusieurs implémentations pour un même type.
On en revient toujours au fait que les modules implicites seraient une fonctionnalité géniales pour OCaml. Elle rendrait les modules encore moins citoyen de seconde classe que ne le font les first-class modules. ;-)
Lorsque j'avais mentionné à Leo White l'article-tutoriel sur les structures canoniques en Coq, il m'a répondu l'avoir déjà lu (effectivement, cela fait même partie des références de l'article de présentation du prototype sur les modules implicites). Cela étant, ils mentionnent un autre article intéressant, qui pourrait servir de base pour la formalisation, dans leurs références : The Implicit Calculus: A New Foundation for Generic Programming qui mentionne aussi le tutoriel sur les structures canoniques. Mais il me vient à l'esprit une interrogation :
l'article sur le calcul implicite se limite au système F ;
les auteurs précisent que les structures canoniques n'ont pas été formellement spécifiées ;
le mécanisme des arguments implicites est décrit pour tous les système du lamda-cube dans la partie 4 de la thèse de Amokrane Saïbi (en français \o/).
S'il est vrai que dans sa thèse il décrit un algorithme d'unification plutôt qu'une formalisation à base de règles d'inférence à la Gentzen, les deux approches ne me semblent pas si éloignées et je ne vois pas ce qu'il manque à ce système pour fournir ce dont ont besoin les modules implicites pour synthétiser les arguments implicites.
Dans un autre registre, sur le statut des modules dans le langage : que penses-tu des travaux de Rossberg, Russo et Dreyer sur 1ML présentés à l'ICFP en 2015 ? Cela demanderait trop de modifications à apporter au langage pour avoir cela dans OCaml ?
An alternative view is that 1ML is a user-friendly surface syntax for System Fω that allows combining term and type abstraction in a more compositional manner than the bare calculus.
et ça résoudrait les incompréhensions de Nicolas Boulay, ils y définissent les modules avec la syntaxe des enregistrements. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: go 2.0
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 21 octobre 2017 à 15:10.
On en revient toujours au fait que les modules implicites seraient une fonctionnalité géniales pour OCaml. Elle rendrait les modules encore moins citoyen de seconde classe que ne le font les first-class modules. ;-)
Lorsque j'avais mentionné à Leo White l'article-tutoriel sur les structures canoniques en Coq, il m'a répondu l'avoir déjà lu (effectivement, cela fait même partie des références de l'article de présentation du prototype sur les modules implicites). Cela étant, ils mentionnent un autre article intéressant, qui pourrait servir de base pour la formalisation, dans leurs références : The Implicit Calculus: A New Foundation for Generic Programming qui mentionne aussi le tutoriel sur les structures canoniques. Mais il me vient à l'esprit une interrogation :
S'il est vrai que dans sa thèse il décrit un algorithme d'unification plutôt qu'une formalisation à base de règles d'inférence à la Gentzen, les deux approches ne me semblent pas si éloignées et je ne vois pas ce qu'il manque à ce système pour fournir ce dont ont besoin les modules implicites pour synthétiser les arguments implicites.
Dans un autre registre, sur le statut des modules dans le langage : que penses-tu des travaux de Rossberg, Russo et Dreyer sur 1ML présentés à l'ICFP en 2015 ? Cela demanderait trop de modifications à apporter au langage pour avoir cela dans OCaml ?
et ça résoudrait les incompréhensions de Nicolas Boulay, ils y définissent les modules avec la syntaxe des enregistrements. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.