OCaml modules: formalization, insights and improvements - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Mémoires D'étudiants -- Hal-Inria+ Année : 2021

OCaml modules: formalization, insights and improvements

Résumé

Modularity is a key tool for building reusable and structured code. While the OCaml module system is known for being expressive and powerful, specifying its behavior and formalizing its properties has proven to be hard. We propose a comprehensive description of a generative subset of the OCaml module system (called the source system), with a focus on the signature avoidance problem. By extending the signature syntax with existential types (inspired by Fω ), we describe an alternate system (called canonical ) with a simpler set of judgments that both solves the issues of the source description and provides formal guarantees through elaboration into Fω . We show that the canonical system is more expressive than the source one and state at which conditions canonical typing derivations can be translated back into the source typing. As a middle point between the path-based representation of OCaml and the formal description of Fω , the canonical presentation is a framework which we believe could support numerous features (applicative functors, transparent ascription, module aliases, etc.) and could serve as a basis for a redefinition of module system of an industry-grade language as OCaml.
Fichier principal
Vignette du fichier
main.pdf (991.45 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03526068 , version 1 (14-01-2022)

Identifiants

  • HAL Id : hal-03526068 , version 1

Citer

Clément Blaudeau. OCaml modules: formalization, insights and improvements: Bringing the existential types into a generative subset. Computer Science [cs]. 2021. ⟨hal-03526068⟩
58 Consultations
253 Téléchargements

Partager

Gmail Facebook X LinkedIn More