Abstract Named and optional arguments are prevalent features in many mainstream programming languages, enhancing code readability and flexibility. Despite widespread use, their formalization has not been extensively studied. This paper bridges this gap by presenting a type-safe foundation for named and optional arguments using intersection and union types. We begin by identifying a critical type-safety issue in popular static type checkers for Python and Ruby, particularly in handling first-class named arguments in the presence of subtyping. Our solution involves rewriting call sites to ensure type safety, which we formalize through a translation into a core calculus called $$\lambda _\textsf{iu}$$ λ iu . The type safety of the translation is proven using the Coq proof assistant. The practical implementation of our approach in the CP language validates our theoretical contributions. Furthermore, we informally discuss how our approach could be adapted to encode named and optional arguments in other existing languages.

Inheritance is a key concept in many programming languages. Dynamically typed languages, such as JavaScript, often support powerful forms of dynamic inheritance. However, dynamic inheritance poses significant challenges for static typing. Most statically typed languages only provide static inheritance to achieve type safety at the cost of flexibility. This article presents a compiler for the CP language, which is a statically typed language that supports dynamic inheritance via a merge operator and also has an expressive form of parametric polymorphism. The merge operator enables a form of multiple inheritance and first-class classes, as well as virtual classes and family polymorphism. With these features, CP allows the development of highly modular and loosely coupled components. However, the efficient compilation of CP code is non-trivial, especially if separate compilation is desired. In particular, subtyping in CP is coercive for type safety, which poses significant challenges in obtaining an efficient compilation scheme. We show how CP is compilable to languages supporting extensible records or similar data structures, where record labels are generated from types for efficient lookup on merges. The main ideas of the compilation scheme are formalized in Coq and proven to be type-safe. The concrete implementation of the CP compiler targets JavaScript, where records are modeled as JavaScript objects. We conduct an empirical evaluation with various benchmarks and evaluate the impact of several CP-specific optimizations. With our optimizations, CP can be orders of magnitude faster than with a naive compilation scheme for merges, obtaining performance on par with class-based JavaScript programs.

Compositional programming is a programming paradigm that emphasizes modularity and is implemented in the CP programming language. The foundations for compositional programming are based on a purely functional variant of System F with intersection types, called F i + , which includes distributivity rules for subtyping. This paper shows how to extend compositional programming and CP with mutable references, enabling a modular, imperative compositional programming style. A technical obstacle solved in our work is the interaction between distributive intersection subtyping and mutable references. Davies and Pfenning [2000] studied this problem in standard formulations of intersection type systems and argued that, when combined with references, distributive subtyping rules lead to type unsoundness. To recover type soundness, they proposed dropping distributivity rules in subtyping. CP cannot adopt this solution, since it fundamentally relies on distributivity for modularity. Therefore, we revisit the problem and show that, by adopting bidirectional typing , a more lightweight and type sound restriction is possible: we can simply restrict the typing rule for references. This solution retains distributivity and an unrestricted intersection introduction rule. We present a first calculus, based on Davies and Pfenning ’s work, which illustrates the generality of our solution. Then we present an extension of F i + with references, which adopts our restriction and enables imperative compositional programming. We implement an extension of CP with references and show how to model a modular live-variable analysis in CP. Both calculi and their proofs are formalized in the Coq proof assistant.

The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called Fi+. The semantics of Fi+ employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of Fi+ does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them. This paper presents a new formulation of Fi+ based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full Fi+ calculus. Unlike the elaboration semantics, which gives the semantics to Fi+ indirectly via a target language, the TDOS approach gives a semantics to Fi+ directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the Fi+ calculus and all its proofs in the Coq proof assistant.

A common approach to defining domain-specific languages (DSLs) is via a direct embedding into a host language. There are several well-known techniques to do such embeddings, including shallow and deep embeddings. However, such embeddings come with various trade-offs in existing programming languages. Owing to such trade-offs, many embedded DSLs end up using a mix of approaches in practice, requiring a substantial amount of code, as well as some advanced coding techniques. In this paper, we show that the recently proposed Compositional Programming paradigm and the CP language provide improved support for embedded DSLs. In CP we obtain a new form of embedding, which we call a compositional embedding, that has most of the advantages of both shallow and deep embeddings. On the one hand, compositional embeddings enable various forms of linguistic reuse that are characteristic of shallow embeddings, including the ability to reuse host-language optimizations in the DSL and add new DSL constructs easily. On the other hand, similarly to deep embeddings, compositional embeddings support definitions by pattern matching or dynamic dispatching (including dependent interpretations, transformations, and optimizations) over the abstract syntax of the DSL and have the ability to add new interpretations. We illustrate an instance of compositional embeddings with a DSL for document authoring called ExT. The DSL is highly flexible and extensible, allowing users to create various non-trivial extensions easily. For instance, ExT supports various extensions that enable the production of wiki-like documents, LaTeX documents, vector graphics or charts. The viability of compositional embeddings for ExT is evaluated with three applications.

Modularity is a key concern in programming. However, programming languages remain limited in terms of modularity and extensibility. Small canonical problems, such as the Expression Problem (EP), illustrate some of the basic issues: the dilemma between choosing one kind of extensibility over another one in most programming languages. Other problems, such as how to express dependencies in a modular way, add up to the basic issues and remain a significant challenge. This article presents a new statically typed modular programming style called Compositional Programming . In Compositional Programming, there is no EP: It is easy to get extensibility in multiple dimensions (i.e., it is easy to add new variants as well as new operations). Compositional Programming offers an alternative way to model data structures that differs from both algebraic datatypes in functional programming and conventional OOP class hierarchies. We introduce four key concepts for Compositional Programming: compositional interfaces , compositional traits , method patterns , and nested trait composition . Altogether, these concepts allow us to naturally solve challenges such as the Expression Problem, model attribute-grammar-like programs, and generally deal with modular programs with complex dependencies . We present a language design, called CP , which is proved to be type-safe, together with several examples and three case studies.