Septembre 2001 - Septembre 2003: Didier Rémy et moi-même (Didier Le Botlan) avons étudié et conçu le système de types MLF, qui correspond à mon travail de thèse.
J'ai présenté MLF à ICFP 2003.
L'article (en anglais) est disponible ici,
mais est soumis à un copyright :
mlf-icfp.pdf
mlf-icfp.ps.gz
mlf-icfp.ps
mlf-icfp.dvi
BibTeX :
mlf-icfp.bib
Les transparents peuvent être vus avec
Active-DVI
ou Ghostview :
mlf-icfp-slides.dvi
mlf-icfp-slides.ps.gz
(mise à jour Septembre 2003)
Ma thèse constitue la version longue de MLF. Elle est accessible sur ma nouvelle page à l'université de Sarrebruck.
J'ai également présenté MLF à APPSEM 2003, à Nottingham (Mars 2003).
Je me penche actuellement sur une possible extension de ML permettant d'avoir du polymorphisme d'ordre supérieur, comme dans Système F, mais en étant toujours capable d'inférer les types, sauf lorsqu'un argument est utilisé de manière polymorphe.
En bref, on type tout ML (et on infère les types). La nouveauté consiste à pouvoir également typer les fonctions qui attendent un argument polymorphes grâce à des annotations de type. Les annotations nécessaires sont relativement restreintes car elles se limitent aux fonctions qui utilisent vraiment le polymorphisme. Alors que la fonction fun (x:'a . 'a -> 'a) x x doit être annotée explicitement, la fonction fun x -> [x], qui met son argument dans une liste, n'a pas besoin d'être annotée, même pour être appliquée à un argument polymorphe.
Grâce à MLF, il devient possible d'encoder le Système F, en ne conservant que les annotations sur les lambda-abstractions. En particulier, les abstractions de types et les applications de types sont effacées. De plus, les annotations sur les lambda-abstractions qui n'utilisent pas le polymorphisme (ce qui inclut notamment les annotations monomorphes) peuvent être effacées également.
Cette extension est le prolongement d'un travail déjà effectué par Didier Rémy et Jacques Garrigue dans le papier "Semi-Explicit First Class Polymorphism". Dans cette version, les objets polymorphes sont explicitements crées, et explicitement ouverts (utilisés) par un mot-clé. Grâce à MLF, la création et l'ouverture sont complètement automatiques. Une bonne dose de réflexion montre qu'il n'est a priori pas possible de résoudre seulement le problème de l'ouverture (ou seulement celui de la fermeture) : si on devine l'un, on doit deviner l'autre.
Le système MLF est maintenant bien formalisé, et prouvé quasiment entièrement. Les résultats fondamentaux sont tous prouvés en détail et s'appuient sur des résultats secondaires, prouvés pour la plupart, ou simplement esquissés pour deux d'entre eux. Je travaille en partie à terminer ces preuves secondaires, ainsi qu'à une mise au propre de l'ensemble : il reste à organiser plus joliment les résultats, à simplifier la présentation et la preuve de certains concepts.
Dans le bêtisier, j'explique comment j'ai cherché à démontrer une proposition qui avait tout l'air d'être vraie, mais qui avait le mauvais goût d'être fausse.
J'ai implémenté un prototype de MLF (en Ocaml bien sûr). Ne pas hésiter à me contacter si vous voulez l'essayer (mon email se trouve sur la page principale).
À la fin de la version anglaise se trouve un exemple de session avec le prototype de mlf.