Abstractions for Type-Level Programming

Over the past decade, the Scala community has shown great interest in using type-level programming to obtain additional type safety. Unfortunately, the lack of support from the Scala compiler has been a barrier to the adoption of that technique, notably due to its negative impact on compilation times. In this thesis, we present three techniques for type-level programming in Scala. First, we explain the status quo, implicits, and show how we can divert them from their intended use to write ad hoc type-level programs. Second, we propose a generalization of Scala's singleton types, which adds the ability to manipulate term-level programs at the type level. Third, we introduce match types, a type-level equivalent of pattern matching, which we implemented in the Scala~3 compiler. Throughout this dissertation, we demonstrate the practicality of our newly introduced techniques, by the means of case studies and examples. Our performance evaluation shows that our new techniques outperform the status quo in terms of binary sizes and compilation times.