Compositional programming in action

Abstract

Compositionality is an important principle in software engineering, meaning that a complex system can be built by composing simpler parts. However, achieving compositionality in practice remains challenging, as exemplified by the expression problem -- a well-known dilemma that highlights the tension between modularity and extensibility. CP, a new statically typed programming language, naturally solves such challenges through language-level support for compositional programming.

This thesis mainly studies the practical aspects of CP. We start with a crash course in CP and showcase why compositional programming matters with two applications. First, regarding object-oriented programming, CP innovates with a trait-based model with merging that prevents implicit overriding in inheritance. By comparing with type-unsafe code in TypeScript, we show that CP achieves dynamic multiple inheritance and family polymorphism without sacrificing type safety. Second, regarding domain-specific languages, CP enables a novel embedding technique that combines the advantages of shallow and deep embeddings and surpasses other techniques like tagless-final embeddings by supporting modular dependencies.

Next, we detail the design and implementation of the CP compiler. With novel language features for compositionality, the efficient compilation of CP code is non-trivial, especially when separate compilation is desired. Our key innovation is to compile merges to type-indexed records, which outperforms prior theoretic work based on nested pairs. To maintain type safety in trait inheritance, CP's type system employs coercive subtyping, which incurs a performance penalty in compiled code. We mitigate the issue with several optimizations, including eliminating coercions for equivalent types. We evaluate the impact of these optimizations using benchmarks and show that the optimized compiler targeting JavaScript can be orders of magnitude faster than a naive compilation scheme, obtaining performance on par with class-based JavaScript programs.

Finally, we extend CP with union types, complementing ubiquitous intersection types, in order to provide a solid foundation for named and optional arguments. Our approach resolves a critical type-safety issue found in popular static type checkers for Python and Ruby, particularly in handling first-class named arguments in the presence of subtyping. A detailed comparative analysis of named and optional arguments in existing languages shows that CP's design achieves a good balance of simplicity and effectiveness.

Both the compilation scheme for CP and the encoding of named and optional arguments are formalized in Coq and proven to be type-safe.