Modular Type Safety for Traits with Extensible Variants and Deep Pattern Matching
Abstract
Traits provide a powerful mechanism for code reuse by allowing the definition of shared behaviors that can be composed into classes. Scala traits in particular have been used extensively in both academia and industry to help define reusable components, especially in the context of domain-specific language (DSL) compilers. Pattern matching on the extensible data types representing a DSL’s constructs plays a key role in these applications. However, guaranteeing static type safety in this context is challenging: in Scala, a program using traits may successfully type check but then throw a runtime exception due to non-exhaustive pattern matching. This paper proposes a novel trait language which, for the first time, combines several important features: extensible data types with principled exhaustive pattern matching guarantees, separate type checking, method overriding, and deep pattern matching. The latter two, in particular, are crucial to supporting DSL analysis and optimization use cases, and the former two are important for reliable and scalable software development in the large. We formalize our approach in the framework of Boolean-algebraic subtyping, but its core ideas could be adapted to other type systems: our approach could be used to make languages with traits and extensible variants finally type safe, improving the experience of developers working with DSL compilation.
