After spending a decade focusing mostly on Haskell, I have spent the last three years looking deeply at OCaml. This talk will capture some lessons learned about my work in the two languages and their communities - how they are similar, how they differ, and how each might usefully grow to become more like the other. I will compare Haskell's purity against OCaml's support for mutation, type classes against modules as abstraction paradigms, laziness against strictness, along with some general thoughts about language philosophy. We'll also touch on the some of the challenges both languages face as open-source products, in need of both volunteers and funding. While some functional programming experience will definitely be helpful, I'll explain syntax as we go - no Haskell or OCaml knowledge required, as I want this talk to be accessible equally to the two communities.
In Haskell, type classes can act like functions from types to terms. However, unlike for functions, there is no way for the programmer to ask the compiler to verify that classes pattern-match exhaustively on their arguments, and their usage must always be marked by a constraint even when they are exhaustive. This paper introduces the notion of total type classes and, more generally, total constraints, which allow the programmer to describe a set of instances whose existence can be verified by inspecting the instance declarations of the class, instead of on a case-by-case basis when a specific instance is demanded. To achieve this functionality, our implementation records the missing constraints during typechecking and then modifies the typechecked program, rewriting it as though the programmer had included the constraints.
Automatic differentiation (AD) is a family of algorithms with many applications in scientific computing and machine learning. They compute numerical derivatives by interpreting or transforming the source code of numeric expressions. The correctness and efficiency of such AD algorithms has been the subject of much research, in particular that of reversemode AD which is particularly efficient for computing large gradients, but the code it generates is highly non-obvious. In this paper, we build on the earlier approach of van den Berg et al. [Science of Computer Programming, 231 (2024)], reverse-engineering their algorithm in terms of established program transformation techniques from abstract algebra and functional programming. We transform the existing interpreter-based approach into an efficient code generator by means of staging with Template Haskell, and leverage a fold fusion variant for staging and algebraic preservation maps to perform correct-by-construction binding time improvements. The resulting generated code achieves speedups of a factor of 110.
Eight years ago "Compiling without continuations" introduced the idea of so-called join points as a powerful optimisation tool in a functional language compiler. Since then join points have become more and more deeply entwined in GHC's optimisation passes; for example they are treated specially by the Simplifier and its Occurrence Analyser, and a dedicated pass called Exitification makes a join-point-specific transformation With the perspective of this experience, I am convinced that any serious functional compiler should use join points (or something equivalent): it's a powerful and re-usable idea. Yet beyond the initial paper, none of what we have learned has appeared in print. In this talk I will share the lessons of the last eight years of using join points in practice in GHC.
Persistent data structures are ubiquitous in functional programming languages and their designers frequently have to reason about amortized time complexity. But proving amortized bounds is difficult in a persistent setting, and penand-paper proofs give little assurance of correctness, while a full mechanization in a proof assistant can be too involved for the casual user. In this work, we define a strict domain specific language (DSL) for testing the amortized time complexity of persistent data structures using QuickCheck. Our DSL can give strong evidence of correctness, while imposing low overhead on the user. We have used our DSL to check the amortized time complexity of all lazy data structures in Okasaki's book. As a sign of our approach's effectiveness, we re-discovered a previously unreported gap in the analysis of persistent Finger Trees. We have released our work as the creditmonad package.
