Haskell 2016 – Proceedings

Message from the Chair
It is my great pleasure to welcome you to the 2016 ACM Haskell Symposium. This is the ninth Haskell Symposium and the fourth year in which the Symposium is organized as a two day event. This year the program committee continued the early submission track, which is meant to provide authors with an opportunity for early feedback. Three papers were submitted to the early track, of which one was accepted outright. 28 additional papers were submitted to the regular track, for a total of 31 submissions (not including demo submissions). All papers received a minimum of three reviews. After a one-week long online meeting, 18 papers were accepted in total. On behalf of the Program Committee, I would like to thank all the authors who submitted their work to the Haskell Symposium. I am grateful to the Program Committee members and external reviewers for their hard work under a tight schedule. Thanks also to the Haskell Symposium Steering Committee, ICFP organizers, and workshop co-chairs Andres Löh and Nicolas Wu.

Testing

FitSpec: Refining Property Sets for Functional Testing
Rudy Braquehais and Colin Runciman
(University of York, UK)
This paper presents FitSpec, a tool providing automated assistance in the task of refining sets of test properties for Haskell functions. FitSpec tests mutant variations of functions under test against a given property set, recording any surviving mutants that pass all tests. The number of surviving mutants and any smallest survivor are presented to the user. A surviving mutant indicates incompleteness of the property set, prompting the user to amend a property or to add a new one, making the property set stronger. Based on the same test results, FitSpec also provides conjectures in the form of equivalences and implications between property subsets. These conjectures help the user to identify minimal core subsets of properties and so to reduce the cost of future property-based testing.

QuickFuzz: An Automatic Random Fuzzer for Common File Formats
Gustavo Grieco, Martín Ceresa, and Pablo Buiras
(CIFASIS-CONICET, Argentina; Harvard University, USA)
Fuzzing is a technique that involves testing programs using invalid or erroneous inputs. Most fuzzers require a set of valid inputs as a starting point, in which mutations are then introduced. QuickFuzz is a fuzzer that leverages QuickCheck-style random test-case generationto automatically test programs that manipulate common file formats by fuzzing. We rely on existing Haskell implementations of file-format-handling libraries found on Hackage, the community-driven Haskell code repository. We have tried QuickFuzz in the wild and found that the approach is effective in discovering vulnerabilities in real-world implementations of browsers, image processing utilities and file compressors among others. In addition, we introduce a mechanism to automatically derive random generators for the types representing these formats. QuickFuzz handles most well-known image and media formats, and can be used to test programs and libraries written in any language.

Info

FRP

Causal Commutative Arrows Revisited
Jeremy Yallop and Hai Liu
(University of Cambridge, UK; Intel Labs, USA)
Causal commutative arrows (CCA) extend arrows with additional constructs and laws that make them suitable for modelling domains such as functional reactive programming, differential equations and synchronous dataflow.
Earlier work has revealed that a syntactic transformation of CCA computations into normal form can result in significant performance improvements, sometimes increasing the speed of programs by orders of magnitude.
In this work we reformulate the normalization as a type class instance and derive optimized observation functions via a specialization to stream transformers to demonstrate that the same dramatic improvements can be achieved without leaving the language.

Functional Reactive Programming, Refactored
Ivan Perez, Manuel Bärenz, and Henrik Nilsson
(University of Nottingham, UK; University of Bamberg, Germany)
Functional Reactive Programming (FRP) has come to mean many things. Yet, scratch the surface of the multitude of realisations, and there is great commonality between them. This paper investigates this commonality, turning it into a mathematically coherent and practical FRP realisation that allows us to express the functionality of many existing FRP systems and beyond by providing a minimal FRP core parameterised on a monad. We give proofs for our theoretical claims and we have verified the practical side by benchmarking a set of existing, non-trivial Yampa applications running on top of our new system with very good results.

Functors

Free Delivery (Functional Pearl)
Jeremy Gibbons
(University of Oxford, UK)
Remote procedure calls are computationally expensive, because network round-trips take several orders of magnitude longer than local interactions. One common technique for amortizing this cost is to batch together multiple independent requests into one compound request. Batching requests amounts to serializing the abstract syntax tree of a small program, in order to transmit it and run it remotely. The standard representation for abstract syntax is to use free monads; we show that free applicative functors are actually a better choice of representation for this scenario.

Info

How to Twist Pointers without Breaking Them
Satvik Chauhan, Piyush P. Kurur, and Brent A. Yorgey
(Google, USA; IIT Kanpur, India; Hendrix College, USA)
Using the theory of monoids and monoid actions, we give a unified framework that handles three common pointer manipulation tasks, namely, data serialisation, deserialisation, and memory allocation. Our main theoretical contribution is the formulation of the notion of a twisted functor, a generalisation of the semi-direct product construction for monoids. We show that semi-direct products and twisted functors are particularly well suited as an abstraction for many pointer manipulation tasks.
We describe the implementation of these abstractions in the context of a cryptographic library for Haskell. Twisted functors allow us to abstract all pointer arithmetic and size calculations into a few lines of code, significantly reducing the opportunities for buffer overflows.

Web Technology

High-Performance Client-Side Web Applications through Haskell EDSLs
Anton Ekblad
(Chalmers University of Technology, Sweden)
We present Aplite, a domain-specific language embedded in Haskell for implementing performance-critical functions in client-side web applications. In Aplite, we apply partial evaluation, multi-stage programming and techniques adapted from machine code-targeting, high-performance EDSLs to the domain of web applications. We use Aplite to implement, among other benchmarks, procedural animation using Perlin noise, symmetrical encryption and K-means clustering, showing Aplite to be consistently faster than equivalent hand-written JavaScript -- up to an order of magnitude for some benchmarks. We also demonstrate how Aplite's multi-staged nature can be used to automatically tune programs to the environment in which they are running, as well as to inputs representative of the programs' intended workload.
High-performance computation in the web browser is an attractive goal for many reasons: interactive simulations and games, cryptographic applications and reducing web companies' electricity bills by outsourcing expensive computations to users' web browsers. Similarly, functional programming in the browser is attractive due to its promises of simpler, shorter, safer programs. In this paper, we propose a way to combine the two.

Experience Report: Developing High Performance HTTP/2 Server in Haskell
Kazuhiko Yamamoto
(IIJ, Japan)
While the speed of the Internet has been increasing, HTTP/1.1 has been plagued by head-of-line blocking, low concurrency and redundant headers. To solve these problems, HTTP/2 was standardized. This paper summarizes our experience implementing HTTP/2 in Haskell. We found several techniques to improve the performance of the header compression and identified a suitable data structure for HTTP/2 priority. Also, we showed that Haskell lightweight threads are useful for HTTP/2 where the common tactics of one lightweight thread per connection cannot be used. The HTTP/2 implementation of Warp, the popular HTTP server library in Haskell, ultimately provides better throughput than its HTTP/1.1 counterpart.

Language Features

Pattern Synonyms
Matthew Pickering, Gergő Érdi, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oxford, UK; Standard Chartered Bank, Singapore; Microsoft Research, UK; Bryn Mawr College, USA)
Pattern matching has proven to be a convenient, expressive way of inspecting data. Yet this language feature, in its traditional form, is limited: patterns must be data constructors of concrete data types. No computation or abstraction is allowed. The data type in question must be concrete, with no ability to enforce any invariants. Any change in this data type requires all clients to update their code.
This paper introduces pattern synonyms, which allow programmers to abstract over patterns, painting over all the shortcomings listed above. Pattern synonyms are assigned types, enabling a compiler to check the validity of a synonym independent of its definition. These types are intricate; detailing how to assign a type to a pattern synonym is a key contribution of this work. We have implemented pattern synonyms in the Glasgow Haskell Compiler, where they have enjoyed immediate popularity, but we believe this feature could easily be exported to other languages that support pattern matching.

Desugaring Haskell's do-Notation into Applicative Operations
Simon Marlow, Simon Peyton Jones, Edward Kmett, and Andrey Mokhov
(Facebook, UK; Microsoft Research, UK; S&P Global, USA; Newcastle University, UK)
Monads have taken the world by storm, and are supported by do-notation (at least in Haskell). Programmers are increasingly waking up to the usefulness and ubiquity of Applicatives, but they have so far been hampered by the absence of supporting notation. In this paper we show how to re-use the very same do-notation to work for Applicatives as well, providing efficiency benefits for some types that are both Monad and Applicative, and syntactic convenience for those that are merely Applicative. The result is fully implemented as an optional extension in GHC, and is in use at Facebook to make it easy to write highly-parallel queries in a distributed system.

Strictness and STM

Revisiting Software Transactional Memory in Haskell
Matthew Le, Ryan Yates, and Matthew Fluet
(Rochester Institute of Technology, USA; University of Rochester, USA)
Software Transactional Memory (STM) has become very popular in Haskell. Currently, there are nearly 500 packages on Haskell’s package archive that directly use STM. Despite the widespread use in real world applications, Haskell’s STM implementation has seen very few updates since its introduction in 2005.
In this work, we describe our efforts to redesign the STM implementation in the Glasgow Haskell Compiler (GHC), based on a TL2-like implementation that is able to support both orElse and retry without the use of traditional nested transactions. We argue that our implementation is simpler than the current GHC implementation while supporting opacity. We also demonstrate that our implementation performs better than the current GHC implementation on a number of benchmarks by multiple orders of magnitude for long-running transactions.
In an effort to measure the performance of orElse and retry, we present an STM-based work stealing scheduler. With orElse and retry, we are able to elegantly implement the scheduler in just a few lines of code. We have modified the Par Monad, a real-world Haskell package that provides deterministic parallelism, to use our STM-based work stealing scheduler and show that it is not only simpler but is able to perform as well as the current scheduler.

Autobahn: Using Genetic Algorithms to Infer Strictness Annotations
Yisu Remy Wang, Diogenes Nunez, and Kathleen Fisher
(Tufts University, USA)
Although laziness enables beautiful code, it comes with non-trivial performance costs. The ghc compiler for Haskell has optimizations to reduce those costs, but the optimizations are not sufficient. As a result, Haskell also provides a variety of strictness annotations so that users can indicate program points where an expression should be evaluated eagerly. Skillful use of those annotations is a black art, known only to expert Haskell programmers. In this paper, we introduce AUTOBAHN, a tool that uses genetic algorithms to automatically infer strictness annotations that improve program performance on representative inputs. Users examine the suggested annotations for soundness and can instruct AUTOBAHN to automatically produce modified sources. Experiments on 60 programs from the NoFib benchmark suite show that AUTOBAHN can infer annotation sets that improve runtime performance by a geometric mean of 8.5%. Case studies show AUTOBAHN can reduce the live size of a GC simulator by 99% and infer application-specific annotations for Aeson library code. A 10-fold cross-validation study shows the AUTOBAHN -optimized GC simulator generally outperforms a version optimized by an expert.

Types

Experience Report: Types for a Relational Algebra Library
Lennart Augustsson and Mårten Ågren
(Standard Chartered Bank, UK; Standard Chartered Bank, Singapore)
As part of our software toolkit at a major financial institution we have a library for relational algebra. This library is written in C++ and the type checking of the operations on the relations is very dynamic; all relations have the same static type. Of course, relational algebra operations have stringent type constraints, and since we believe in static typing, we would prefer these to be checked at compile time.
We have managed to get full static type checking of the relational code, using some modern extensions to the Haskell type system, such as closed type families, type level strings, user-defined kinds, and custom type errors. The static type checking incurs no runtime overhead compared to the dynamically checked library.
Some effort has gone into making the use of the typed library similar to the dynamically typed version. We have also tried to produce good error messages when something is wrong.

Embedding Session Types in Haskell
Sam Lindley and J. Garrett Morris
(University of Edinburgh, UK)
We present a novel embedding of session-typed concurrency in Haskell. We extend an existing HOAS embedding of linear λ-calculus with a set of core session-typed primitives, using indexed type families to express the constraints of the session typing discipline. We give two interpretations of our embedding, one in terms of GHC’s built-in concurrency and another in terms of purely functional continuations. Our safety guarantees, including deadlock freedom, are assured statically and introduce no additional runtime overhead.

Monads

The Key Monad: Type-Safe Unconstrained Dynamic Typing
Atze van der Ploeg, Koen Claessen, and Pablo Buiras
(Chalmers University of Technology, Sweden; Harvard University, USA)
We present a small extension to Haskell called the Key monad. With the Key monad, unique keys of different types can be created and can be tested for equality. When two keys are equal, we also obtain a concrete proof that their types are equal. This gives us a form of dynamic typing, without the need for Typeable constraints. We show that our extension allows us to safely do things we could not otherwise do: it allows us to implement the ST monad (inefficiently), to implement an embedded form of arrow notation, and to translate parametric HOAS to typed de Bruijn indices, among others. Although strongly related to the ST monad, the Key monad is simpler and might be easier to prove safe. We do not provide such a proof of the safety of the Key monad, but we note that, surprisingly, a full proof of the safety of the ST monad also remains elusive to this day. Hence, another reason for studying the Key monad is that a safety proof for it might be a stepping stone towards a safety proof of the ST monad.

Supermonads: One Notion to Bind Them All
Jan Bracker and Henrik Nilsson
(University of Nottingham, UK)
Several popular generalizations of monads have been implemented in Haskell. Unfortunately, because the shape of the associated type constructors do not match the standard Haskell monad interface, each such implementation provides its own type class and versions of associated library functions. Furthermore, simultaneous use of different monadic notions can be cumbersome as it in general is necessary to be explicit about which notion is used where. In this paper we introduce supermonads: an encoding of monadic notions that captures several different generalizations along with a version of the standard library of monadic functions that work uniformly with all of them. As standard Haskell type inference does not work for supermonads due to their generality, our supermonad implementation is accompanied with a language extension, in the form of a plugin for the Glasgow Haskell Compiler (GHC), that allows type inference for supermonads, obviating the need for manual annotations.

Abstractions that Scale

Non-recursive Make Considered Harmful: Build Systems at Scale
Andrey Mokhov, Neil Mitchell, Simon Peyton Jones, and Simon Marlow
(Newcastle University, UK; Standard Chartered Bank, UK; Microsoft Research, UK; Facebook, UK)
Most build systems start small and simple, but over time grow into hairy monsters that few dare to touch. As we demonstrate in this paper, there are a few issues that cause build systems major scalability challenges, and many pervasively used build systems (e.g. Make) do not scale well.
This paper presents a solution to the challenges we identify. We use functional programming to design abstractions for build systems, and implement them on top of the Shake library, which allows us to describe build rules and dependencies. To substantiate our claims, we engineer a new build system for the Glasgow Haskell Compiler. The result is more scalable, faster, and spectacularly more maintainable than its Make-based predecessor.

Lazy Graph Processing in Haskell
Philip Dexter, Yu David Liu, and Kenneth Chiu
(SUNY Binghamton, USA)
This paper presents a Haskell library for graph processing: DeltaGraph. One unique feature of this system is that intentions to perform graph updates can be memoized in-graph in a decentralized fashion, and the propagation of these intentions within the graph can be decoupled from the realization of the updates. As a result, DeltaGraph can respond to updates in constant time and work elegantly with parallelism support. We build a Twitter-like application on top of DeltaGraph to demonstrate its effectiveness and explore parallelism and opportunistic computing optimizations.