Implicit Code Generation for Polymorphism

As software keeps growing in size and complexity, more sophisticated programming languages are needed to keep software development manageable. One important aspect in a capable programming language is its type system. A sufficiently powerful static type system can not only reduce bugs, but also implicitly generate common boilerplate code. This thesis improves upon on two forms of this implicit type-directed code generation, both in the context of polymorphism: parametric polymorphism and type classes. The goal of this work is to improve the current state of the art in polymorphism, and we tackle this in three complementary ways: Firstly, we investigate parametric polymorphism in Haskell by evaluating two design decisions related to type instantiation. For this, we introduce the concept of stability as a way of making these decisions. Stability is a measure of whether the meaning of a program alters under small, seemingly innocuous changes in the code (e.g., inlining). We define a type system family, which can be materialised to four different approaches of type instantiation. After defining 11 different stability related properties, and formally verifying them against every variant of the type system family, we conclude that the most stable approach is lazy (instantiate a polytype only when absolutely necessary) and shallow (instantiate only top-level type variables, not variables that appear after explicit arguments). Secondly, we increase confidence in the type class resolution mechanism, the implicit type-directed code generation used by Haskell for function overloading. While type class resolution is generally nondeterministic (both in Haskell and other languages like Mercury and PureScript), we prove that it still behaves predictably. Indeed, multiple ways can exist to satisfy a wanted constraint in terms of global instances and locally given constraints. However, the property of coherence guarantees that every possible outcome of this nondeterministic resolution process behaves indistinguishably from the others in practice. Even though coherence is generally assumed to hold for type class resolution, as far as we know, this work is the first to provide a formal proof of this property in the presence of sources of nondeterminism, like superclasses and flexible contexts. The proof is non-trivial because the semantics elaborates resolution into a target language where different elaborations can be distinguished by contexts that do not have a source language counterpart. Inspired by the notion of full abstraction we present a two-step strategy that first elaborates nondeterministically into an intermediate language that preserves contextual equivalence, and then deterministically elaborates from there into the target language. We use an approach based on logical relations to establish contextual equivalence and thus coherence for the first step of elaboration, while the second step's determinism straightforwardly preserves this coherence property. Thirdly, we increase expressivity of type classes from Horn clauses to the universal fragment of Hereditary Harrop logic. In fact, quantified class constraints have been proposed many years ago for exactly this purpose. Yet, despite being widely asked for over the years, besides a number of stopgap workarounds, quantified constraints had never been formally studied or implemented. We elaborate the idea into a practical language design, and provide a declarative specification of the type system. Furthermore, we design a type inference algorithm that elaborates into System F. While not a direct mapping, this work has provided the necessary kick-start for a GHC implementation of quantified constraints. Finally, we extend the aforementioned coherence proof with quantified class constraints, a non-trivial extension, to show the adaptability of the proof. In conclusion, we have improved the state of the art of polymorphism, and its type-directed code generation aspects in particular. We have increased (1) the stability of parametric polymorphism, (2) faith in the correctness of type class resolution by formally proving it coherent, and (3) the expressivity of type classes by adopting quantified class constraints. This clears the way for more wide-spread adoption of these features.

Publication year:2022

Accessibility:Open