Abstract

Functional programming languages encourage expressing large parts of a program as declarative data flow pipelines, free of side-effects such as shared mutable state. Such pipelines traverse recursive data by pattern matching, and share the repetitive code of these traversals by defining higher-order functions. Writing programs in functional style eliminates large classes of programmer errors, hence higher-order functions and pattern matching have been adopted by most general purpose programming languages today.

However, pattern matching introduces new modes of failure as well: It is easy to forget a case, and input data that is not covered leads to a crash at runtime. Thus, a compiler should integrate a static program analysis to warn about such uncovered pattern-matches before the program is run.

A compiler should also generate fast code for programs involving higher-order functions. More than 30 years of practical research have evolved the Glasgow Haskell Compiler (GHC) into an industrial strength tool. This evolution brought forth a number of useful and efficient compiler optimisations that are informed by static higher-order analyses. However, the more proficient a higher-order analysis becomes, the harder it gets to explain its implementation to maintainers, let alone convince interested bystanders of its correctness.

In this thesis, I present two results of my work to improve GHC: the first is a static analysis for pattern-match coverage checking that is both more efficient and more precise than the state of the art; the second is a design pattern for deriving static higher-order analyses and dynamic semantics alike from a generic denotational interpreter, in order to share intuition and correctness proofs. This design pattern generalises Cousot’s seminal work on trace-based abstract interpretation to higher-order analyses such as GHC’s Demand Analysis.

I’m posting Sebastian’s thesis here because I worked particuarly closely with him while he was a PhD student, although I was not his advisor. It is great work!