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

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.

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.

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.

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.

Keywords: ML ; Refactoring ; Logical Relations ; Dependent Types ; Functional programming ; Polymorphism ; Data types and structures ; Semantics ; Software maintenance tools ; Ornaments

Keywords: ML ; Polymorphism ; Refactoring ; Data types and structures ; Dependent Types ; Logical Relations ; Ornaments ; Semantics ; Software maintenance tools

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.)

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.