Modular Type Safety for Traits with Extensible Variants and Deep Pattern Matching
Abstract
Traits provide a powerful mechanism for code reuse, as they allow 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, deep pattern matching, method overriding, exhaustiveness guarantees, and separate type checking. The former three are crucial to supporting DSL analysis and optimization use cases, while the latter 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; thanks to it, languages like Scala that feature traits and extensible variants can finally become type safe, improving the experience of developers working with DSL compilation and related use cases.
