Retrofitting OCaml modules - ENS de Lyon - École normale supérieure de Lyon Accéder directement au contenu
Communication Dans Un Congrès Année : 2023

Retrofitting OCaml modules

Résumé

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, requiring heavy machinery to prove their soundness. Building on a previous translation from ML modules to Fω , we propose a new comprehensive description of a generative subset of OCaml modules, embarking on a journey right from the source OCaml module system, up to Fω , and back. We pause in the middle to uncover a system, called canonical that combines the best of both worlds. On the way, we obtain type soundness, but also and more importantly, a deeper insight into the signature avoidance problem, along with ways to improve both the OCaml language and its typechecking algorithm.
Fichier principal
Vignette du fichier
main.pdf (612.59 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03936636 , version 1 (12-01-2023)
hal-03936636 , version 2 (24-01-2023)

Identifiants

  • HAL Id : hal-03936636 , version 2

Citer

Clément Blaudeau, Didier Rémy, Gabriel Radanne. Retrofitting OCaml modules: Fixing signature avoidance in the generative case. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.59-100. ⟨hal-03936636v2⟩
148 Consultations
201 Téléchargements

Partager

Gmail Facebook X LinkedIn More