We had a great time at both ICFP (plus co-located events) and MSFP this year. Many thanks to the organisers for managing to create compelling online versions of these events in challenging cicumstances. We’ve seen many great talks, and had lots of interesting discussions.
Ben was the program chair of the Haskell Implementors’ Workshop (HIW) this year, and several others of us had contributions at these conferences which we are summarising below. We include links to slides and videos (as far as they are available yet). We will add the missing video links once they become available.
Using STM for modular concurrency
Duncan Coutts, invited talk at Haskell Symposium
Software Transactional Memory (STM) has been available within Haskell for around fifteen years, yet it remains a somewhat under-appreciated feature. This talk aims to redress that by sharing the experiences from a recent successful industrial project that relies extensively and fundamentally on STM. There are good articles, book chapters and blogs on STM at the micro level: looking at the details of the primitives and how to use them to build bigger abstractions. This talk will try to focus on STM at the macro level: larger scale design patterns, how it fits into a system as a whole, and testing techniques.
The focus of this experience report is the application of STM in the context of highly concurrent systems with many modular concurrent components, and the use of STM to help structure the communication and interaction of these components. This contrasts for example with a database pattern where many threads executing transitions on one bundle of shared state.
Staged Sums of Products
Andres Löh with Matthew Pickering and Nicolas Wu, paper presentation at Haskell Symposium
Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.
A Low-Latency Garbage Collector for GHC (Demo)
Ben Gamari with Laura Dietz, demo at Haskell Symposium
GHC 8.10.1 offers a new latency-oriented garbage collector to complement the existing throughput-oriented copying collector. This demonstration discusses the pros and cons of the latency-optimized GC design, briefly discusses the technical trade-offs made by the design, and describes the sorts of application for which the collector is suitable. We include a brief quantitative evaluation on a typical large-heap server workload.
Liquid Haskell as a GHC Plugin
Alfredo Di Napoli with Ranjit Jhala, Andres Löh, Niki Vazou, talk at HIW
Liquid Haskell is a system that extends GHC with refinement types. Constraints arising from the refinement types are sent to an external automatic theorem prover such as z3. By employing such additional checks, one can express more interesting properties about Haskell programs statically.
Up until now, Liquid Haskell has been a separate executable that uses the GHC API, but would run on Haskell files individually and just say “SAFE” or “UNSAFE”. If “SAFE”, one could then proceed to compile a program normally.
In the recent months, we have rewritten Liquid Haskell to now be a GHC plugin. The main advantages of this approach are: First, there is just a single invocation necessary per Haskell source file, so the workflow becomes easier. Second, we can integrate with GHC and Cabal to support libraries and packages properly. When checking source files, Liquid Haskell requires information about the constraints already established for dependent libraries. Previously, these had to be hand-distributed for selected modules with Liquid Haskell itself. Now, they become part of normal GHC interface files and can be distributed for arbitrary user packages via Hackage.
In this talk, we present the Liquid Haskell plugin workflow and why we think it is superior to the old approach. We also discuss the implementation of the plugin: it is interesting because it does not neatly fit into the plugin categories currently provided. Morally, Liquid Haskell typechecks the code, but in order to generate constraints to feed to the prover, it must access (unoptimised!) core code. We explain the final design, and some of the iterations we needed to get there.
GHC Devops Update
Ben Gamari, HIW
As a part of the general GHC status update by Simon Peyton Jones, Ben ended up giving an update on GHC Devops.
Adding Backtraces to Exceptions
David Eichmann, lightning talk at HIW
David Eichmann spoke about an on-going effort to introduce backtrace information into GHC’s exception mechanism, fixing a long-standing pain-point for production users. In his remarks he briefly motivated the problem, described GHC’s existing backtrace collection mechanisms, and described the proposed approach for introducing backtraces into the GHC’s exception types.
Interested readers are invited to comment on the the associated GHC Proposal.
A Vision of Compartmentalized Concurrency in Haskell
Ben Gamari, lightning talk at HIW
Ben described a hypothetical design for improving the scalability of Glasgow Haskell by introducing a notion of multiple distinct heaps (known as domains) in a single Haskell process. This mechanism would enable improved locality on NUMA large machines (by keeping domains on particular NUMA nodes) while improving garbage collector performance (due to reduced synchronization) and exploiting the low communication-cost of a shared-memory environment. Ben explains some of the implementation challenges of this design and encourages contributors interested in undertaking implementation of this idea to get in touch.
Shattered Lens
Oleg Grenrus, extended abstract presentation at MSFP
Video — Slides — Extended abstract
A very well-behaved lens from a structure type to a value type is usually specified using two functions, a getter and a setter . These functions are required to satisfy three laws involving equalities.
This formulation is problematic if we want to talk about the equality of lenses, for example to prove the associativity of lens composition. When the theory we work in doesn’t have unique identity proofs (UIP), we run into coherence problems, trying to show that equality proofs are equal.
I found a good formulation of prisms, which we say to be “decidable embeddings”. Yet, I failed to find as good a description of lenses, where good means merely propositional, uniquely determining description. However there are some ideas on how to think about lenses, and on what to look at next.
More about Well-Typed
If you want to find more about what we offer at Well-Typed, please check out our Services page, or just send us an email.