Publications by Didier Rémy [ without abstracts | BibTeX source file ]

[1] Clément Blaudeau, Didier Rémy, and Gabriel Radanne. Avoiding signature avoidance in modules with zippers. Unpublished draft, available electronically, September 2024. [ bib | PDF | http ]
We present ZipML, a new path-based type system for a fully fledged ML-module language that avoids the signature avoidance problem. This is achieved by introducing floating fields, which act as additional fields of a signature, invisible to the user but still accessible to the typechecker. In practice, they are handled as zippers on module signatures, and can be seen as a lightweight extension on existing signatures. Floating fields allow to delay the resolution of signature avoidance as long as possible or desired. Since they do not exist at runtime, they can be simplified along type equivalence, and dropped once they became unreachable. We give a simple equivalence criterion for the simplification of floating components without loss of type-sharing. We present a principled strategy that implements this criterion and performs much better than OCaml. Remaining floating fields, instead of polluting the code, partially disappear at functor applications and fully disappear at signature ascription, including toplevel interfaces. Residual unavoidable floating fields can be shown to the user as a last resort, either to be explicitly resolved by the user, or kept until link time. The correctness of the type system is proved by elaboration into Mw , which has itself been proved sound by translation to Fw . The language includes module type definitions that are kept and returned in inferred types, as long as possible. ZipML has been designed to be a specification of an improvement over OCaml with transparent ascription, a better solution to signature avoidance, while staying close to the source language and to its implementation.
[2] Samuel Vivien, Didier Rémy, Thomas Réfis, and Gabriel Scherer. On the design and implementation of Modular Explicits. Presented at the OCaml 2024 workshop, available electronically, September 2024. [ bib | PDF | .html ]
We present and discuss the design and implementation of modular explicits, an extension of OCamlfirst-class modules with module-dependent functions, functions taking first-class modules as arguments. We show some difficulties with the present use of first-class modules and how modular explicitssolve them in a simpler, more direct way. Modular explicits are fully compatible with, and can be presented as an extension of, first-class modules. Interestingly, both the formalization and the implementation reuse the mechanism designed to ensure principal types in the presence of semi-explicit first-class polymorphism and OCamlpolymorphic methods. Modular explicits are also meant to be the underlying language in which modular implicits, i.e.,module arguments left implicit from their signatures, should be elaborated.
[3] Clément Blaudeau, Didier Rémy, and Gabriel Radanne. Fulfilling OCaml modules with Transparency. Proc. ACM Program. Lang., 8(OOPSLA'24):194--222, 2024. [ bib | DOI | PDF | http ]
ML modules come as an additional layer on top of a core language to offer large-scale notions of composition and abstraction. They largely contributed to the success of OCaml and SML. While modules are easy to write for common cases, their advanced use may become tricky. Additionally, despite a long line of works, their meta-theory remains difficult to comprehend, with involved soundness proofs. In fact, the module layer of OCaml does not currently have a formal specification and its implementation has some surprising behaviors. Building on previous translations from ML modules to Fw, we propose a type system, called Mw , that covers a large subset of OCaml modules, including both applicative and generative functors, and extended with transparent ascription. This system produces signatures in an OCaml-like syntax extended with Fw quantifiers. We provide a reverse translation from Mw signatures to path-based source signatures along with a characterization of signature avoidance cases, making Mw signatures well suited to serve as a new internal representation for a typechecker. The soundness of the type system is shown by elaboration in Fw. We improve over previous encodings of sealing within applicative functors, by the introduction of transparent existential types, a weaker form of existential types that can be lifted out of universal and arrow types. This shines a new light on the form of abstraction provided by applicative functors and brings their treatment much closer to those of generative functors.
[4] Clément Blaudeau, Didier Rémy, and Gabriel Radanne. Retrofitting OCaml modules. In Timothy Bourke and Delphine Demange, editors, JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pages 59--100, Praz-sur-Arly, France, January 2023. [ bib | See also | PDF | http ]
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 Fw, 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.
[5] Steve Kremer, Ludovic Mé, Didier Rémy, and Vincent Roca. Cybersecurity: Current challenges and Inria's research directions. Number 3 in Inria white book. Inria, January 2019. [ bib | PDF | http ]
[6] Lucas Baudin and Didier Rémy. Disornamentation. In ML Family Workshop 2018, St. Louis, Missouri, United States, September 2018. [ bib | http ]
[7] Didier Rémy. Ornamentation put into Practice in ML. In Seventh Workshop on Mathematically Structured Functional Programming (MSFP 2018), Oxford, United Kingdom, July 2018. [ bib | http ]
[8] Thomas Williams and Didier Rémy. A Principled Approach to Ornamentation in ML. Proceedings of the ACM on Programming Languages, 2(POPL):21:1--21:30, January 2018. [ bib | DOI | PDF | http ]
Keywords: ML ; Refactoring ; Logical Relations ; Dependent Types ; Functional programming ; Polymorphism ; Data types and structures ; Semantics ; Software maintenance tools ; Ornaments
[9] Thomas Williams and Didier Rémy. A Principled Approach to Ornamentation in ML (extended version). Research report, Inria, November 2017. [ bib | DOI | PDF | http ]
Keywords: ML ; Polymorphism ; Refactoring ; Data types and structures ; Dependent Types ; Logical Relations ; Ornaments ; Semantics ; Software maintenance tools
[10] Didier Rémy. Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (invited talk). In Haskell 2017: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, pages 1--1, Oxford, United Kingdom, September 2017. ACM Press. [ bib | http ]
[11] Didier Rémy. Type Systems for Programming Languages. Course notes, available electronically, 2015. [ bib | PDF ]
[12] Gabriel Scherer and Didier Rémy. Full Reduction in the Face of Absurdity. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pages 685--709, 2015. [ bib | DOI | PDF | http ]
[13] Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 243--255, 2015. [ bib | DOI | PDF | http ]
[14] Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? Extended version of [13], 2015. [ bib | PDF | http ]
[15] Gabriel Scherer and Didier Rémy. Full reduction in the face of absurdity. Research report, INRIA, December 2014. [ bib | PDF | http ]
[16] Thomas Williams, Pierre-Évariste Dagand, and Didier Rémy. Ornaments in Practice. September 2014. [ bib | PDF ]
Ornaments have been introduced as a way to describe some changes in datatype definitions that preserve their recursive structure, reorganizing, adding, or dropping some pieces of data. After a new data structure has been described as an ornament of an older one, some functions operating on the bare structure can be partially or sometimes totally lifted into functions operating on the ornamented structure. We explore the feasibility and the interest of using ornaments in practice by applying these notions in an ML-like programming language. We propose a concrete syntax for defining ornaments of datatypes and the lifting of bare functions to their ornamented counterparts, describe the lifting process, and present several interesting use cases of ornaments.
[17] Didier Rémy and Julien Cretin. From Amber to Coercion Constraints. In Martin Abadi, Philippa Gardner, Andrew D. Gordon, and Radu Mardare, editors, Essays for the Luca Cardelli Fest, number MSR-TR-2014-104 in TechReport. Microsoft Research, September 2014. [ bib | PDF | .pdf ]
[18] Julien Cretin and Didier Rémy. System F with Coercion Constraints. In Logics In Computer Science (LICS). ACM, July 2014. [ bib | See also | PDF ]
We present a second-order lambda-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This enables a uniform presentation of several type system features that had previously been studied separately: type containment, bounded and instance-bounded polymorphism, which are already encodable with parametric coercion abstraction, and ML-style subtyping constraints. Our framework allows for a clear separation of language constructs with and without computational content. We also distinguish coherent coercions that are fully erasable from potentially incoherent coercions that suspend the evaluation---and enable the encoding of GADTs.

Technically, type coercions that witness subtyping relations between types are replaced by a more expressive notion of typing coercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calculus is equipped with full reduction that allows reduction under abstractions---but we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the step-indexed semantics technique to full reduction, moving indices inside terms so as to control the reduction steps internally.

[19] Thomas Williams, Pierre-Évariste Dagand, and Didier Rémy. Ornaments in Practice. In WGP+ '14: Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming, New York, NY, USA, July 2014. ACM. [ bib | PDF ]
Ornaments have been introduced as a way to describe some changes in datatype definitions that preserve their recursive structure, reorganizing, adding, or dropping some pieces of data. After a new data structure has been described as an ornament of an older one, some functions operating on the bare structure can be partially or sometimes totally lifted into functions operating on the ornamented structure. We explore the feasibility and the interest of using ornaments in practice by applying these notions in an ML-like programming language. We propose a concrete syntax for defining ornaments of datatypes and the lifting of bare functions to their ornamented counterparts, describe the lifting process, and present several interesting use cases of ornaments.
[20] Julien Cretin and Didier Rémy. System F with Coercion Constraints. Rapport de recherche RR-8456, INRIA, January 2014. [ bib | PDF | http ]
We present a second-order lambda-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This allows to present in a uniform way several type system features that had previously been studied separately: type containment, bounded and instance-bounded polymorphism, which are already encodable with parametric coercion abstraction, and ML-style subtyping constraints. Our framework allows for a clear separation of language constructs with and without computational content. We also distinguish coherent coercions that are fully erasable from potentially incoherent coercions that suspend the evaluation---and enable the encoding of GADTs. Technically, type coercions that witness subtyping relations between types are replaced by a more expressive notion of typing coercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calculus is equipped with a strong notion of reduction that allows reduction under abstractions---but we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the step-indexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.
[21] Jacques Garrigue and Didier Rémy. Ambivalent Types for Principal Type Inference with GADTs. In 11th Asian Symposium on Programming Languages and Systems, Melbourne, Australia, December 2013. [ bib | See also | PDF ]
GADTs, short for Generalized Algebraic DataTypes, which allow constructors of algebraic datatypes to be non-surjective, have many useful applications. However, pattern matching on GADTsintroduces local type equality assumptions, which are a source of ambiguities that may destroy principal types---and must be resolved by type annotations. We introduce ambivalent types to tighten the definition of ambiguities and better confine them, so that type inference has principal types, remains monotonic, and requires fewer type annotations.
[22] Julien Cretin and Didier Rémy. Coherent Coercion Abstration with a step-indexed strong-reduction semantics. available at http://gallium.inria.fr/ remy/coercions/, July 2013. [ bib | See also | PDF ]
The usual notion of type coercions that witness subtyping relations between types is generalized to a more expressive notion of typing coercions that witness subsumption relations between typings, e.g.. pairs composed of a typing environment and a type. This is more expressive and allows for a clearer separation of language constructs with and without computational content. This is illustrated on a second-order calculus of implicit coercions that allows multiple but simultaneous type and coercion abstractions and has recursive coercions and general recursive types. The calculus is equipped with a very liberal notion of reduction. It models a wide range of type features including type containment, bounded and instance-bounded polymorphism, as well as subtyping constraints as used for ML-style type inference with subtyping. Type soundness is proved by adapting the step-indexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.
[23] Gabriel Scherer and Didier Rémy. GADTs Meet Subtyping. In Proceedings of the 22Nd European Conference on Programming Languages and Systems, ESOP'13, pages 554--573, Berlin, Heidelberg, 2013. Springer-Verlag. [ bib | DOI | See also | At Publisher's ]
While generalized abstract datatypes (GADT) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? answer turns out to be quite subtle and involves fine-grained properties of the subtyping relation that raise interesting design questions. annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.
[24] Didier Rémy and Boris Yakobowski. A Church-Style Intermediate Language for MLF. Theoretical Computer Science, 435(1):77--105, June 2012. [ bib | See also | PDF | At Publisher's ]
MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during reduction. All parameters of functions are explicitly typed and both type abstraction and type instantiation are explicit. However, type instantiation in xMLF is more general than type application in System F. We equip xMLF with a small-step reduction semantics that allows reduction in any context and show that this relation is confluent and type preserving. We also show that both subject reduction and progress hold for weak-reduction strategies, including call-by-value with the value-restriction.
[25] Jacques Garrigue and Didier Rémy. Tracing ambiguity in GADT type inference. Unpublished, June 2012. [ bib | PDF ]
GADTs, short for Generalized Algebraic DataTypes, extend usual algebraic datatypes with a form of dependent typing that has many useful applications, but raises serious issues for type inference. Pattern matching on GADTs introduces type equalities with limited scopes, which are a source of ambiguities that may destroy principal types---and must be resolved by type annotations. By tracing ambiguities in types, we may tighten the definition of ambiguities and confine them, so as to request fewer type annotations. Now in use in OCaml 4.00, this solution also lifts some restriction on object types and polymorphic types that appeared in a previous implementation of GADTs in OCaml.
[26] Julien Cretin and Didier Rémy. On the Power of Coercion Abstraction. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL 2012), Philadephia, PA, USA, January 2012. [ bib | See also | At Publisher's ]
Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain form of delayed type instantiation. We generalize F-eta by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the lambda-calculus but keeping track of which parts of terms are coercions. We obtain a language where coercions do not contribute to the reduction but may block it and are thus not erasable. We recover erasable coercions by choosing a weak reduction strategy and restricting coercion abstraction to value-forms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes F-eta, F-sub, and MLF in a unified framework.
[27] Julien Cretin and Didier Rémy. Extending System F-eta with Abstraction over Erasable Coercions. Research Report RR-7587, INRIA, July 2011. [ bib | See also | PDF | At Publisher's ]
Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain form of delayed type instantiation. We generalize F-eta by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the lambda-calculus but keeping track of which parts of terms are coercions. We obtain a language where coercions do not contribute to the reduction but may block it and are thus not erasable. We recover erasable coercions by choosing a weak reduction strategy and restricting coercion abstraction to value-forms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes F-eta, F-sub, and MLF in a unified framework.
[28] Didier Rémy and Boris Yakobowski. A Church-Style Intermediate Language for MLF. In Matthias Blume, Naoki Kobayashi, and German Vidal, editors, Functional and Logic Programming, volume 6009 of Lecture Notes in Computer Science, pages 24--39. Springer Berlin / Heidelberg, 2010. [ bib | DOI | See also | PDF | At Publisher's ]
MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during reduction. All parameters of functions are explicitly typed and both type abstraction and type instantiation are explicit. However, type instantiation in xMLF is more general than type application in System F. We equip xMLF with a small-step reduction semantics that allows reduction in any context and show that this relation is confluent and type preserving. We also show that both subject reduction and progress hold for weak-reduction strategies, including call-by-value with the value-restriction.
[29] Benoît Montagu and Didier Rémy. Modeling Abstract Types in Modules with Open Existential Types. In Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL'09), pages 354--365, Savannah, GA, USA, January 2009. [ bib | DOI | See also | PDF ]
We propose Fzip, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as done in module systems. The static semantics of Fzip adapts standard techniques to deal with linearity of typing contexts, its dynamic semantics is a small-step reduction semantics that performs extrusion of type abstraction as needed during reduction, and the two are related by subject reduction and progress lemmas. Applying the Curry-Howard isomorphism, Fzip can be also read back as a logic with the same expressive power as second-order logic but with more modular ways of assembling partial proofs. We also extend the core calculus to handle the double vision problem as well as type-level and term-level recursion. The resulting language turns out to be a new formalization of (a minor variant of) Dreyer's internal language for recursive and mixin modules.
[30] Didier Le Botlan and Didier Rémy. Recasting MLF. Information and Computation, 207(6):726--785, 2009. [ bib | DOI | See also | PDF | At Publisher's | http ]
The language MLF is a proposal for a new type system that supersedes both ML and System F, allows for efficient, predictable, and complete type inference for partially annotated terms. In this work, we revisit the definition of MLF, following a more progressive approach and focusing on the design-space and expressiveness. We introduce a Curry-style version iMLF of MLF and provide an interpretation of iMLF types as instantiation-closed sets of System-F types, from which we derive the definition of type instance in iMLF. We give equivalent syntactic definition of the type-instance, presented as a set of inference rules. We also show an encoding of iMLF into the closure of Curry-style System F by let-expansion. We derive the Church-style version eMLF by refining types of iMLF so as to distinguish between given and inferred polymorphism. We show an embedding of ML in eMLF and a straightforward encoding of System F into eMLF.
Keywords: ML
[31] Didier Rémy and Boris Yakobowski. Efficient Type Inference for the MLF Language: a graphical and constraints-based approach. In The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08), pages 63--74, Victoria, BC, Canada, September 2008. [ bib | DOI | See also | PDF ]
MLF is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or MLF. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent MLF types. We give a few semantic preserving transformations on constraints and propose a strategy for applying them to solve constraints. We show that the resulting algorithm has optimal complexity for MLF type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions.
[32] Xavier Leroy and Didier Rémy. Programmation du système Unix en OCaml. Course notes, available electronically, 2008. [ bib | PDF ]
[33] Benoît Montagu and Didier Rémy. Towards a Simpler Account of Modules and Generativity: Abstract Types have Open Existential Types. January 2008. [ bib | See also | PDF ]
We present a variant of the explicitly-typed second-order polymorphic lambda-calculus with primitive open existential types, i.e. a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. Traditional closed existential types can be defined as syntactic sugar. Conversely, programs with no free existential types can be rearranged to only use closed existential types, but the translation is not compositional.We argue that open existential types model abstract types and modules with generativity. We also introduce a new notion of paths at the level of types instead of terms that allows for writing type annotations more concisely and modularly.
[34] Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007. [ bib | See also | PDF | At Publisher's ]
The language MLF has been proposed as an alternative to System F that permits partial type inference a la ML. It differs from System F by its types and type-instance relation. Unfortunately, the definition of type instance is only syntactic, and not underpined by some underlying semantics. It has so far only been justified a posteriori by the type soundness result. In this work, we revisit MLF following a more progressive approach stepping on System F. We argue that System F is not a well-suited language for ML-style type inference because it fails to factorize some closely related typing derivations. We solve this problem in Curry's style MLF by enriching types with a new form of quantification that may represent a whole collection of System F types. This permits a natural interpretation of MLF types as sets of System-F types and pulling back the instance relation from set inclusion on the interpretations. We also give an equivalent syntactic definition of the type-instance, presented as a set of inference rules. We derive a Church's style version of MLF by further refining types so as to distinguish between user-provided and inferred type information. The resulting language is more canonical than the one originally proposed. We show an embedding of ML in MLF and an encoding of System F into MLF. Besides, as MLF is more expressive than System F, an encoding of MLF is given towards an extension of System F with local binders.
[35] Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time unification algorithm. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI'07), pages 27--38, Nice, France, January 2007. ACM Press. [ bib | http ]
MLF is a language that extends ML and System F and combines the benefits of both. We propose a dag representation of MLF types that superposes a term-dag, encoding the underlying term-structure with sharing, and a binding tree encoding the binding-structure. Compared to the original definition, this representation is more canonical as it factors out most of the notational details; it is also closely related to first-order terms. Moreover, it permits a simpler and more direct definition of type instance that combines type instance on first-order term-dags, simple operations on dags, and a control that allows or rejects potential instances. Using this representation, we build a linear-time unification algorithm for MLF types, which we prove sound and complete with respect to the specification.
[36] Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time incremental unification algorithm. Extended version of [35], July 2006. [ bib | See also | PDF | .ps.gz ]
MLF is a language that extends both ML and System F and combines the benefits of both. We propose a dag representation of MLF types that superposes a term-dag, encoding the underlying term-structure with sharing, and a binding tree, encoding the binding-structure. This representation is more canonical as it factors out most of the notational details of the original definition; it is also closely related to first-order terms. Moreover, it permits a simpler and more direct definition of type instance that combines type-instance on first-order term-dags, simple operations on dags, and a control that allows or rejects potential instances. Thanks to this representation, we obtain an incremental linear-time unification algorithm for MLF types, which we prove sound and complete with respect to the specification. We also extend term graphs to express constraints on graphs that can be rewritten incrementally, which suffices to describe all operations needed by type inference.
[37] Didier Rémy. Simple, partial type-inference for System F based on type-containment. In Proceedings of the tenth International Conference on Functional Programming, September 2005. [ bib | See also | PDF | .ps.gz ]
We explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified via type annotations on source terms. We allow implicit predicative type-containment and explicit impredicative type-instantiation. We obtain a core language that is both as expressive as System F and conservative over ML. Its type system has a simple logical specification and a partial type-reconstruction algorithm that are both very close to the ones for ML. We then propose a surface language where some annotations may be omitted and rebuilt by some algorithmically defined but logically incomplete elaboration mechanism.
[38] Roberto Di Cosmo, François Pottier, and Didier Rémy. Subtyping Recursive Types modulo Associative Commutative Products. In Seventh International Conference on Typed Lambda Calculi and Applications (TLCA'05), Nara, Japan, April 2005. [ bib | Long version .pdf | Long version | PDF | .ps.gz ]
This work sets the formal bases for building tools that help retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class interfaces. The tool returns classes in the library that can be used to implement the user's request and automatically builds the required glue code. We propose subtyping of recursive types in the presence of associative and commutative products---that is, subtyping modulo a restricted form of type isomorphisms---as a model of the relation that exists between the user's query and the tool's answers. We show that this relation is a composition of the standard subtyping relation with equality up to associativity and commutativity of products and we present an efficient decision algorithm for it. We also provide an automatic way of constructing coercions between related types.
[39] François Pottier and Didier Rémy. The Essence of ML Type Inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005. [ bib | http ]
[40] Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of System F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 27--38, August 2003. [ bib | PDF | http | .dvi.gz | .ps.gz ]
We propose a type system MLF that generalizes ML with first-class polymorphism as in System F. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred. All expressions of ML are well-typed without any annotations. All expressionsof System F can be mechanically encoded into MLF by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into MLF types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.
[41] François Pottier and Didier Rémy. The Essence of ML Type Inference. Extended preliminary version of [39], 2003. [ bib | See also | .ps.gz ]
[42] Didier Rémy. Using, Understanding, and Unraveling the OCaml Language. In Gilles Barthe, editor, Applied Semantics. Advanced Lectures. LNCS 2395., pages 413--537. Springer Verlag, 2002. [ bib | PDF | http | .ps.gz ]
These course notes are addressed to a wide audience of people interested in modern programming languages in general, ML-like languages in particular, or simply in OCaml, whether they are programmers or language designers, beginners or knowledgeable readers ---little prerequiresite is actually assumed.
They provide a formal description of the operational semantics (evaluation) and statics semantics (type checking) of core ML and of several extensions starting from small variations on the core language to end up with the OCaml language ---one of the most popular incarnation of ML--- including its object-oriented layer.
The tight connection between theory and practice is a constant goal: formal definitions are often accompanied by OCaml programs: an interpreter for the operational semantics and an algorithm for type reconstruction are included. Conversely, some practical programming situations taken from modular or object-oriented programming patterns are considered, compared with one another, and explained in terms of type-checking problems.
Many exercises with different level of difficulties are proposed all along the way, so that the reader can continuously checks his understanding and trains his skills manipulating the new concepts; soon, he will feel invited to select more advanced exercises and pursue the exploration deeper so as to reach a stage where he can be left on his own.
[43] Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Inheritance in the Join Calculus. In Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science. Springer, December 2000. [ bib | PDF | http | .ps.gz ]
We propose an object-oriented calculus with internal concurrency and class-based inheritance that is built upon the join calculus. Method calls, locks, and states are handled in a uniform manner, using labeled messages. Classes are partial message definitions that can be combined and transformed. We design operators for behavioral and synchronization inheritance. We also give a type system that statically enforces basic safety properties. Our model is compatible with the JoCaml implementation of the join calculus.
[44] Didier Rémy. Re-exploring multiple inheritance. Invited talk at FOOL'7, January 2000. [ bib ]
[45] Jacques Garrigue and Didier Rémy. Extending ML with Semi-Explicit Higher-Order Polymorphism. Information and Computation, 155(1/2):134--169, 1999. A preliminary version appeared in TACS'97. [ bib | PDF | http ]
We propose a modest conservative extension to ML that allows semi-explicit first-class polymorphism while preserving the essential properties of type inference. In our proposal, the introduction of polymorphic types is fully explicit, that is, both introduction points and exact polymorphic types are to be specified. However, the elimination of polymorphic types is semi-implicit: only elimination points are to be specified as polymorphic types themselves are inferred. This extension is particularly useful in Objective ML where polymorphism replaces subtyping.
[46] Didier Rémy and Jérôme Vouillon. The reality of virtual types for free! Unpublished note avaliable electronically, October 1998. [ bib | http | .ps.gz ]
We show, mostly through detailed examples, that programming patterns known to involve the notion of virtual types can be implemented in a real object-oriented language ---Ocaml--- in a direct way by taking advantage of parametric classes and a flexible treatment of object types via the use of row variables. We also attempt to explain the essence of virtual types. Our free solution to virtual types seems to be more general and often more flexible than ad hoc solutions that have been previously proposed.
[47] Didier Rémy. From Classes to Objects via Subtyping. A preliminary version appeared in LNCS 1381 (ESOP 98), June 1998. [ bib | PDF ]
We extend the Abadi-Cardelli calculus of primitive objects with object extension. We enrich object types with a more precise, uniform, and flexible type structure. This enables to type object extension under both width and depth subtyping. Objects may also have extend-only or virtual contra-variant methods and read-only co-variant methods. The resulting subtyping relation is richer, and types of objects can be weaken progressively from a class level to a more traditional object level along the subtype relationship.
[48] Didier Rémy. From Classes to Objects via Subtyping. In European Symposium On Programming, volume 1381 of Lecture Notes in Computer Science. Springer, March 1998. [ bib | .html ]
We extend the Abadi-Cardelli calculus of primitive objects with object extension. We enrich object types with a more precise, uniform, and flexible type structure. This enables to type object extension under both width and depth subtyping. Objects may also have extend-only or virtual contra-variant methods and read-only co-variant methods. The resulting subtyping relation is richer, and types of objects can be weaken progressively from a class level to a more traditional object level along the subtype relationship.
[49] Didier Rémy. Des enregistrements aux objets. Mémoire d'habilitation à diriger des recherches, Université de Paris 7, 1998. [ bib | PDF ]
Les enregistrements, produits à champ nommés, sont une structure simple et fondamentale en programmation, et sont présents depuis longtemps dans de nombreux langages. Toutefois, certaines opérations sur les enregistrements, comme l'ajout de champs, restent délicates dans un langage fortement typé. Les objets sont, au contraire, un concept très évolué, expressif, mais les difficultés à les typer ou à les coder dans un lambda-calcul typé semblent refléter une complexité intrinsèque.
Une technique simple et générale permet d'étendre le typage des enregistrements aux opérations les plus avancées, telles que l'accès polymorphe, l'extension, la possibilité d'avoir des valeurs par défaut et une forme de concaténation. En ajoutant à ces opérations des types existentiels, objets et classes deviennent directement programmables, sans sacrifice pour leur expressivité, mais au détriment de la lisibilité des types synthétisés.
Une extension de ML avec des objets primitifs, Objective ML, à la base de la couche objet du langage Ocaml, est alors proposée. L'utilisation de constructions primitives permet, en particulier, l'abréviation automatique des types qui rend l'interface avec l'utilisateur conviviale. Une extension harmonieuse du langage avec des méthodes polymorphes est également possible.
Tout en expliquant l'imbrication entre les enregistrements, les objets et classes, ces travaux montrent surtout que le polymorphisme de ML, un concept simple et fondamental suffit à rendre compte des opérations les plus complexes sur les objets. La simplicité et la robustesse d'Objective ML et de son mécanisme de typage, qui ne sacrifient en rien l'expressivité, contribuent à démystifier la programmation avec objets, et la rendent accessible en toute sécurité à l'utilisateur, même novice.
[50] Carl A. Gunter, Didier Rémy, and Jon G. Riecke. Return types for Functional Continuations. A preliminary version appeared as [58], 1998. [ bib | Software | See also | PDF ]
We add functional continuations and prompts to a language with an ML-style type system. The operators significantly extend and simplify the control operators in SML/NJ, and can be themselves used to implement (simple) exceptions. We prove that well-typed terms never produce run-time type errors and give a module for implementing them in the latest version of SML/NJ.
[51] Didier Rémy and Jérôme Vouillon. Objective ML: An effective object-oriented extension to ML. Theory And Practice of Object Systems, 4(1):27--50, 1998. A preliminary version appeared in the proceedings of the 24th ACM Conference on Principles of Programming Languages, 1997. [ bib | PDF ]
Objective ML is a small practical extension to ML with objects and top level classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods as well as parametric classes. This demonstrates that objects can be added to strongly typed languages based on ML polymorphism.
[52] Jacques Garrigue and Didier Rémy. Extending ML with Semi-Explicit Higher-Order Polymorphism. In International Symposium on Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 20--46. Springer, September 1997. [ bib | PDF ]
We propose a modest conservative extension to ML that allows semi-explicit higher-order polymorphism while preserving the essential properties of ML. In our proposal, the introduction of polymorphic types remains fully explicit, that is, both the introduction and the exact polymorphic type must be specified. However, the elimination of polymorphic types is now semi-implicit: only the elimination itself must be specified as the polymorphic type is inferred. This extension is particularly useful in Objective ML that privileges polymorphism to subtyping.
[53] Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Implicit typing à la ML for the join-calculus. In 8th International Conference on Concurrency Theory (CONCUR'97), volume 1243 of Lecture Notes in Computer Science, pages 196--212, Warsaw, Poland, 1997. Springer. [ bib | PDF ]
We adapt the Damas-Milner typing discipline to the join-calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join-definitions. We prove the correctness of our typing rules with regards to a chemical semantics. We also relate typed extensions of the core join-calculus to functional languages.
[54] Didier Rémy and Jérôme Vouillon. Objective ML: A simple object-oriented extension of ML. In Proceedings of the 24th ACM Conference on Principles of Programming Languages, pages 40--53, Paris, France, January 1997. [ bib | PDF ]
Objective ML is a small practical extension to ML with objects and toplevel classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods as well as parametric classes. This demonstrates that objects can be added to strongly typed languages based on ML polymorphism.
[55] Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, and Didier Rémy. A Calculus of Mobile Agents. In 7th International Conference on Concurrency Theory (CONCUR'96), volume 1119 of Lecture Notes in Computer Science, pages 406--421, Pisa, Italy, August 26-29 1996. Springer. [ bib | PDF ]
We introduce a calculus for mobile agents and give its chemical semantics, with a precise definition for migration, failure, and failure detection. Various examples written in our calculus illustrate how to express remote executions, dynamic loading of remote resources and protocols with mobile agents. We give the encoding of our distributed calculus into the join-calculus. (BibTeX reference.)
[56] Didier Rémy. Better subtypes and row variables for record types. Presented at the workshop on Advances in types for computer science at the Newton Institute, Cambridge, UK, August 1995. [ bib | .dvi.gz ]
In this note we compare row variables and subtypes for record types. We show that they are orthogonal to one another and that record types benefit from having both at the same time. We proposed a unifying framework of record types, and show that the several advantages of using an enriched latice of subtypes for record types, in particular this allows for extensible objects in the presence of subtyping.
[57] Didier Rémy. A case study of typechecking with constrained types: Typing record concatenation. Presented at the workshop on Advances in types for computer science at the Newton Institute, Cambridge, UK, August 1995. [ bib | .dvi.gz ]
We study static type-soundness of type systems with non-atomic-subtyping based on constrained types for first-order lambda-calculus (no Let) with one-field records given with a call-by-value reduction semantics. We then extend the language with general records with concatenation. This case study shows the flexibility of type inference with constrained types. We extend the constrained types with type operators in order to type-check record concatenation in the presence of subtyping. This method should provide wrappers to object-oriented languages based on the objects-as-records-of-methods paradigm. We do not address the practical issues of type inference here.
[58] Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A Generalization of Exceptions and Control in ML. In Proc. ACM Conf. on Functional Programming and Computer Architecture, June 1995. [ bib | PDF | http ]
We add functional continuations and prompts to a language with an ML-style type system. The operators significantly extend and simplify the control operators in SML/NJ, and can be themselves used to implement (simple) exceptions. We prove that well-typed terms never produce run-time type errors and give a module for implementing them in the latest version of SML/NJ.
[59] Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111--130, January 1995. Also appeared as SRC Research Report 120. Preliminary version appeared in the Proceedings of the ACM SigPlan Workshop on ML and its Applications, June 1992. [ bib | PDF ]
There are situations in programming where some dynamic typing is needed, even in the presence of advanced static type systems. We investigate the interplay of dynamic types with other advanced type constructions, discussing their integration into languages with explicit polymorphism (in the style of system F), implicit polymorphism (in the style of ML), abstract data types, and subtyping.
[60] Didier Rémy. Programming Objects with ML-ART: An extension to ML with Abstract and Record Types. In Masami Hagiya and John C. Mitchell, editors, International Symposium on Theoretical Aspects of Computer Software, number 789 in Lecture Notes in Computer Science, pages 321--346, Sendai, Japan, April 1994. Springer-Verlag. [ bib | PDF ]
Class-based objects can be programmed directly and efficiently in a simple extension to ML. The representation of objects, based on abstract and record types, allows all usual operations such as multiple inheritance, object returning capability, and message transmission to themselves as well as to their super classes. There is, however, no implicit coercion from objects to corresponding ones of super-classes. A simpler representation of objects without recursion on values is also described. The underlying language extends ML with recursive types, existential and universal types, and mutable extensible records. The language ML-ART is given with a call-by-value semantics for which type soundness is proved.
[61] Benjamin C. Pierce, Didier Rémy, and David N. Turner. A Typed Higher-Order Programming Language Based on the Pi-Calculus. A preliminary version was presented at the Workshop on Type Theory and its Application to Computer Systems, Kyoto University, July 1993. [ bib ]
[62] Didier Rémy. Syntactic Theories and the Algebra of Record Terms. Research Report 1869, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1993. [ bib | PDF ]
Many type systems for records have been proposed. For most of them, the types cannot be described as the terms of an algebra. In this case, type checking, or type inference in the case of first order type systems, cannot be derived from existing algorithms. We define record terms as the terms of an equational algebra. We prove decidability of the unification problem for records terms by showing that its equational theory is syntactic. We derive a complete algorithm and prove its termination. We define a notion of canonical terms and approximations of record terms by canonical terms, and show that approximations commute with unification. We also study generic record terms, which extend record terms to model a form of sharing between terms. We prove the syntacticness of the equational theory of generic record terms and the termination of the corresponding unification algorithm.
[63] Carl A. Gunter and Didier Rémy. A proof-theoretic assessment of runtime type errors. Research Report 11261-921230-43TM, AT&T Bell Laboratories, 600 Mountain Ave, Murray Hill, NJ 07974-2070, 1993. [ bib | PDF ]
We analyze the way in which a result concerning the absence of runtime type errors can be expressed when the semantics of a language is described using proof rules in what is sometimes called a natural semantics. We argue that the usual way of expressing such results has conceptual short-comings when compared with similar results for other methods of describing semantics. These short-comings are addressed through a form of operational semantics based on proof rules in what we call a partial proof semantics. A partial proof semantics represents steps of evaluation using proofs with logic variables and subgoals. Such a semantics allows a proof-theoretic expression of the absence of runtime type errors that addresses the problems with such results for natural semantics. We demonstrate that there is a close correspondence between partial proof semantics and a form of structural operational semantics that uses a grammar to describe evaluation contexts and rules for the evaluation of redexes that may appear in such contexts. Indeed, partial proof semantics can be seen as an intermediary between such a description and one using natural semantics. Our study is based on a case treatment for a language called RAVL for Records And Variants Language, which has a polymorphic type system that supports flexible programming with records and variants.
[64] Didier Rémy. Typing Record Concatenation for Free. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993. [ bib | PDF ]
We show that any functional language with record extension possesses record concatenation for free. We exhibit a translation from the latter into the former. We obtain a type system for a language with record concatenation by composing the translation with typechecking in a language with record extension. We apply this method to a version of ML with record extension and obtain an extension of ML with either asymmetric or symmetric concatenation. The latter extension is simple, flexible and has a very efficient type inference algorithm in practice. Concatenation together with removal of fields needs one more construct than extension of records. It can be added to the version of ML with record extension. However, many typed languages with record cannot type such a construct. The method still applies to them, producing type systems for record concatenation without removal of fields. Object systems also benefit of the encoding which shows that multiple inheritance does not actually require the concatenation of records but only their extension
[65] Didier Rémy. Type Inference for Records in a Natural Extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993. [ bib | PDF ]
We describe an extension of ML with records where inheritance is given by ML generic polymorphism. All common operations on records but concatenation are supported, in particular the free extension of records. Other operations such as renaming of fields are added. The solution relies on an extension of ML, where the language of types is sorted and considered modulo equations, and on a record extension of types. The solution is simple and modular and the type inference algorithm is efficient in practice.
[66] Didier Rémy. Efficient Representation of Extensible Records. In Proceedings of the 1992 workshop on ML and its Applications, page 12, San Francisco, USA, June 1992. [ bib | PDF ]
[67] Didier Rémy. Extending ML Type System with a Sorted Equational Theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992. [ bib | PDF ]
We extend the ML language by allowing a sorted regular equational theory on types for which unification is decidable and unitary. We prove that the extension keeps principal typings and subject reduction. A new set of typing rules is proposed so that type generalization is simpler and more efficient. We consider typing problems as general unification problems, which we solve with a formalism of unificands. Unificands naturally deal with sharing between types and lead to a more efficient type inference algorithm. The use of unificands also simplifies the proof of correctness of the algorithm by splitting it into more elementary steps.
[68] Didier Rémy. Typing Record Concatenation for Free. In Nineteenth Annual Symposium on Principles Of Programming Languages, pages 166--176, 1992. [ bib | PDF ]
[69] Didier Rémy. Projective ML. In 1992 ACM Conference on Lisp and Functional Programming, pages 66--75, New-York, 1992. ACM press. [ bib | PDF ]
In the last five years there have been many proposals for adding records in strongly typed functional languages. It is agreed that powerful operations should be provided. However the operations are numerous, and there is no agreement yet on which ones are really needed, and what they should do. Moreover, there is no basic calculus in which these operations can be described very easily. We propose a projective lambda calculus as the basis for operations on records. Projections operate on elevations, that is, records with defaults. This calculus extends lambda calculus while keeping its essential properties. We build projective ML from this calculus by adding the ML Let typing rule to the simply typed projective calculus. We show that projective ML possesses the subject reduction property, which means that well-typed programs can be reduced safely. Elevations are practical data structures that can be compiled efficiently. Moreover, standard records are definable in terms of projections.
[70] Didier Rémy. Type Inference for Records in a natural Extension of ML. Research Report 1431, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, May 1991. See also [65] and [72]. [ bib | PDF ]
[71] Didier Rémy. Algèbres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, 1990. [ bib | PDF ]
[72] Didier Rémy. Records and Variants as a natural Extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989. See also [65]. [ bib ]

This file was generated by bibtex2html 1.99.