Abstract:

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, the Scala programming language unifies concepts from object and module systems.

In particular, objects can contain type members, which can be selected as types, called path-dependent types. Focusing on path-dependent types, we develop a type-theoretic foundation for Scala: the calculus of Dependent Object Types (DOT). The DOT calculus finally grounds languages like Scala in firm theory. The DOT calculus helps in finding bugs in Scala, and in understanding feature interaction better as well as requirements. The DOT calculus serves as a good basis for future work which studies extensions or encodings on top of the core, bridging the gap from DOT to Scala, i.e. from an idealized formal model to a full programming language that's widely used in industry.

In the second part, we apply Scala’s type system reaping benefits beyond type safety. Using the Lightweight Modular Staging (LMS) framework, we review a principled approach, driven by types, to generative programming: writing expressive high-level programs that generate fast low-level code at runtime. We show how to extend the approach to verification by generating annotations that enable the low-level code to be independently validated for safety or functional correctness. We illustrate the LMS motto “abstraction without regret” with a small and fast SQL query engine, and a high-level, fast and safe HTTP parser.