ICFP Workshops 2017
22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017)
Powered by
Conference Publishing Consulting

10th ACM SIGPLAN International Haskell Symposium (Haskell 2017), September 7-8, 2017, Oxford, UK

Haskell 2017 – Proceedings

Contents - Abstracts - Authors

10th ACM SIGPLAN International Haskell Symposium (Haskell 2017)

Frontmatter

Title Page


Message from the Chair
Welcome to the 10th International Symposium on Haskell! The main focus of the Symposium is to present original research on Haskell, discuss practical experience and future development of the language, and to promote other forms of denotative programming. The Symposium is on the 7–8 September 2017, in Oxford, United Kingdom, co-located with ICFP 2017.

Session 1

Ornaments: Exploiting Parametricity for Safer, More Automated Code Refactorization and Code Reuse (Invited Talk)
Didier Rémy
(Inria, France)
Inductive datatypes and parametric polymorphism are two key features introduced in the ML family of languages, which have already been widely exploited for structuring programs: Haskell and ML programs are often more elegant and more correct by construction. Still, we sometimes need code to be refactored or adapted to be reused in a slightly different context. While the type system is considerably helpful in these situations, by automatically locating type-inconsistent program points or incomplete pattern matchings, this process could be made safer and more automated by further exploiting parametricity. We propose a posteriori program abstraction as a principle for such code transformations.
We apply this principle to ornamentation which is a way to describe changes in datatype definitions reorganizing, adding, or dropping some pieces of data so that functions operating on the bare definition can be partially and sometimes totally lifted into functions operating on the ornamented structure.
We view ornamentation as an a posteriori abstraction of the bare code, called a generic lifting, which can then be instantiated into a concrete lifting, meta-reduced, and simplified. Both the source and target code live in core ML while the lifted code lives in a meta-language above ML equipped with a limited form of dependent types needed to capture some invariants of the generic lifting so that the concrete lifting can be simplified back into an ML program. Importantly, the lifted code can be closely related to the bare code, using logical relations thanks to the generic lifting detour.
Different, typical use cases of ornaments will be shown and the approach will be mainly illustrated on examples.

Algebraic Graphs with Class (Functional Pearl)
Andrey Mokhov
(Newcastle University, UK)
The paper presents a minimalistic and elegant approach to working with graphs in Haskell. It is built on a rigorous mathematical foundation --- an algebra of graphs --- that allows us to apply equational reasoning for proving the correctness of graph transformation algorithms. Algebraic graphs let us avoid partial functions typically caused by `malformed graphs' that contain an edge referring to a non-existent vertex. This helps to liberate APIs of existing graph libraries from partial functions.
The algebra of graphs can represent directed, undirected, reflexive and transitive graphs, as well as hypergraphs, by appropriately choosing the set of underlying axioms. The flexibility of the approach is demonstrated by developing a library for constructing and transforming polymorphic graphs.

Packrats Parse in Packs
Mario Blažević and Jacques Légaré
(Stilo International, Canada)
We present a novel but remarkably simple formulation of formal language grammars in Haskell as functions mapping a record of pro- duction parsers to itself. Thus formulated grammars are first-class objects, composable and reusable. We also provide a simple parser implementation for them, based on an improved packrat algorithm. In order to make the grammar manipulation code reusable, we introduce a set of type classes mirroring the existing type classes from Haskell base library, but whose methods have rank-2 types.

Info
Ode on a Random Urn (Functional Pearl)
Leonidas Lampropoulos, Antal Spector-Zabusky, and Kenneth Foner
(University of Pennsylvania, USA)
We present the urn, a simple tree-based data structure that supports sampling from and updating discrete probability distributions in logarithmic time. We avoid the usual complexity of traditional self-balancing binary search trees by not keeping values in a specific order. Instead, we keep the tree maximally balanced at all times using a single machine word of overhead: its size.
Urns provide an alternative interface for the frequency combinator from the QuickCheck library that allows for asymptotically more efficient sampling from dynamically-updated distributions. They also facilitate backtracking in property-based random testing, and can be applied to such complex examples from the literature as generating well-typed lambda terms or information flow machine states, demonstrating significant speedups.

Session 2

QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)
Maximilian Algehed, Koen Claessen, Moa Johansson, and Nick Smallbone
(Chalmers University of Technology, Sweden)
This document gives the outline of a system demonstration for the QuickSpec theory exploration tool.

Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results
Rudy Braquehais and Colin Runciman
(University of York, UK)
This paper presents Speculate, a tool that automatically conjectures laws involving conditional equations and inequalities about Haskell functions. Speculate enumerates expressions involving a given collection of Haskell functions, testing to separate those expressions into apparent equivalence classes. Expressions in the same equivalence class are used to conjecture equations. Representative expressions of different equivalence classes are used to conjecture conditional equations and inequalities. Speculate uses lightweight equational reasoning based on term rewriting to discard redundant laws and to avoid needless testing. Several applications demonstrate the effectiveness of Speculate.

Using Coq to Write Fast and Correct Haskell
John Wiegley and Benjamin Delaware
(BAE Systems, USA; Purdue University, USA)
Correctness and performance are often at odds in the field of systems engineering, either because correct programs are too costly to write or impractical to execute, or because well-performing code involves so many tricks of the trade that formal analysis is unable to isolate the main properties of the algorithm.
As a prime example of this tension, Coq is an established proof environment that allows writing correct, dependently-typed code, but it has been criticized for exorbitant development times, forcing the developer to choose between optimal code or tractable proofs. On the other side of the divide, Haskell has proven itself to be a capable, well-typed programming environment, yet easy-to-read, straightforward code must all too often be replaced by highly optimized variants that obscure the author's original intention.
This paper builds on the existing Fiat refinement framework to bridge this divide, demonstrating how to derive a correct-by-construction implementation that meets (or exceeds) the performance characteristics of highly optimized Haskell, starting from a high-level Coq specification. To achieve this goal, we extend Fiat with a stateful notion of refinement of abstract data types and add support for extracting stateful code via a free monad equipped with an algebra of heap-manipulating operations. As a case study, we reimplement a subset of the popular bytestring library, with little to no loss of performance, while retaining a high guarantee of program correctness.

A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow
(University of Maryland, USA; University of Pennsylvania, USA; Awake Networks, USA)
We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary theorem proving by verifying a parallel, monoidal string matching algorithm implemented in Haskell. We use refinement types to specify correctness properties, Haskell terms to express proofs of these properties, and Liquid Haskell to check the proofs. We evaluate Liquid Haskell as a theorem prover by replicating our 1428 LoC proof in a dependently-typed language (Coq - 1136 LoC). Finally, we compare both proofs, uncovering the relative advantages and disadvantages of the two provers.

Info
A Meta-EDSL for Distributed Web Applications
Anton Ekblad
(Chalmers University of Technology, Sweden)
We present a domain-specific language for constructing and configuring web applications distributed across any number of networked, heterogeneous systems. Our language is embedded in Haskell, provides a common framework for integrating components written in third-party EDSLs, and enables type-safe, access-controlled communication between nodes, as well as effortless sharing and movement of functionality between application components. We give an implementation of our language and demonstrate its applicability by using it to implement several important components of distributed web applications, including RDBMS integration, load balancing, and fine-grained sandboxing of untrusted third party code.
The rising popularity of cloud computing and heterogeneous computer architectures is putting a strain on conventional programming models, which commonly assume that one application executes on one machine, or at best on one out of several identical machines. With our language, we take the first step towards a programming model better suited for a computationally multicultural future.

Composable Network Stacks and Remote Monads
Justin Dawson, Mark Grebe, and Andy Gill
(University of Kansas, USA)
Monads and applicative functors are two ways that Haskell programmers bundle effectful primitives into effectful program fragments. In this paper, we investigate using monads and applicative functors to bundle remote effectful primitives, specifically aiming to amortize the cost of remote communications using bundling. We look at several ways of maximizing the bundling of primitives, drawing from the remote monad design pattern and Haxl system, and provide a taxonomy of mechanism for amortization, with examples. The result of this investigation is that monadic fragments can be efficiently bundled into packets, almost for free, when given a user-supplied packet transportation mechanism, and the primitives obey some simple pre- and post-conditions.

Session 3

Algorithmic Music in Haskell (Invited Talk)
Donya Quick
(Stevens Institute of Technology, USA)
Functional programming is becoming increasingly popular in artistic areas such as algorithmic music composition. Euterpea and Kulitta are two libraries for working with music in Haskell. Euterpea is a library for representing and manipulating basic musical structures, and is useful both in a pedagogical setting to teach functional programming through the arts and as a tool to create complex pieces of algorithmic music. Kulitta is a framework for automated composition that addresses music at a more abstract level than Euterpea, capturing aspects of musical style through geometric models and probabilistic grammars. Both of these libraries leverage Haskell’s pure functional nature and strong type system to achieve versatile, yet concise designs that allow the creation of diverse and interesting music. Features from these libraries have also been integral in the design of newer systems for natural language processing and artificial intelligence in the musical domain. This talk will explore challenges presented by creating these kinds of domain-specific embedded languages for working with music, and how taking functional approaches to them yields elegant solutions.

Well-Typed Music Does Not Sound Wrong (Experience Report)
Dmitrij Szamozvancev and Michael B. Gale
(University of Cambridge, UK)
Music description and generation are popular use cases for Haskell, ranging from live coding libraries to automatic harmonisation systems. Some approaches use probabilistic methods, others build on the theory of Western music composition, but there has been little work done on checking the correctness of musical pieces in terms of voice leading, harmony, and structure. Haskell's recent additions to the type-system now enable us to perform such analysis statically.
We present our experience of implementing a type-level model of classical music and an accompanying EDSL which enforce the rules of classical music at compile-time, turning composition mistakes into compiler errors. Along the way, we discuss the strengths and limitations of doing this in Haskell and demonstrate that the type system of the language is fully capable of expressing non-trivial and practical logic specific to a particular domain.

Back to the Future: Time Travel in FRP
Ivan Perez
(University of Nottingham, UK)
Functional Reactive Programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such as having a fixed time domain, time always flowing forward, and limiting the exploration of the past.
In this paper we show how these constraints can be overcome, giving local control over the time domain, the direction of time and the sampling step. We study the behaviour of FRP expressions when time flows backwards, and demonstrate how to synchronize subsystems running asynchronously and at different sampling rates. We have verified the practicality of our approach with two non-trivial games in which time control is central to the gameplay.

The Linearity Monad
Jennifer Paykin and Steve Zdancewic
(University of Pennsylvania, USA)
We introduce a technique for programming with domain-specific linear languages using the monad that arises from the theory of linear/non-linear logic. In this work we interpret the linear/non-linear model as a simple, effectful linear language embedded inside an existing non-linear host language. We implement a modular framework for defining these linear EDSLs in Haskell, allowing both shallow and deep embeddings. To demonstrate the effectiveness of the framework and the linearity monad, we implement languages for file handles, mutable arrays, session types, and quantum computing.

Info

Session 4

Elaboration on Functional Dependencies: Functional Dependencies Are Dead, Long Live Functional Dependencies!
Georgios Karachalias and Tom Schrijvers
(KU Leuven, Belgium)
Functional dependencies are a popular extension to Haskell's type-class system because they provide fine-grained control over type inference, resolve ambiguities and even enable type-level computations. Unfortunately, several aspects of Haskell's functional dependencies are ill-understood. In particular, the GHC compiler does not properly enforce the functional dependency property, and rejects well-typed programs because it does not know how to elaborate them into its core language, System FC. This paper presents a novel formalization of functional dependencies that addresses these issues: We explicitly capture the functional dependency property in the type system, in the form of explicit type equalities. We also provide a type inference algorithm and an accompanying elaboration strategy which allows all well-typed programs to be elaborated into System FC.

Quantified Class Constraints
Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler
(KU Leuven, Belgium; University of Hong Kong, China; University of Edinburgh, UK)
Quantified class constraints have been proposed many years ago to raise the expressive power of type classes from Horn clauses to the universal fragment of Hereditiary Harrop logic. Yet, while it has been much asked for over the years, the feature was never implemented or studied in depth. Instead, several workarounds have been proposed, all of which are ultimately stopgap measures.
This paper revisits the idea of quantified class constraints and elaborates it into a practical language design. We show the merit of quantified class constraints in terms of more expressive modeling and in terms of terminating type class resolution. In addition, we provide a declarative specification of the type system as well as a type inference algorithm that elaborates into System F. Moreover, we discuss termination conditions of our system and also provide a prototype implementation.

Hardware Software Co-design in Haskell
Markus Aronsson and Mary Sheeran
(Chalmers University of Technology, Sweden)
We present a library in Haskell for programming Field Programmable Gate Arrays (FPGAs), including hardware software co-design. Code for software (in C) and hardware (in VHDL) is generated from a single program, along with the code to support communication between hardware and software. We present type-based techniques for the simultaneous implementation of more than one embedded domain specific language (EDSL). We build upon a generic representation of imperative programs that is loosely coupled to instruction and expression types, allowing the individual parts to be developed and improved separately. Code generation is implemented as a series of translations between progressively smaller, typed EDSLs, safeguarding against errors that arise in untyped translations. Initial case studies show promising performance.

Streaming Irregular Arrays
Robert Clifton-Everest, Trevor L. McDonell, Manuel M. T. Chakravarty, and Gabriele Keller
(UNSW, Australia)
Previous work has demonstrated that it is possible to generate efficient and highly parallel code for multicore CPUs and GPUs from combinator-based array languages for a range of applications. That work, however, has been limited to operating on flat, rectangular structures without any facilities for irregularity or nesting.
In this paper, we show that even a limited form of nesting provides substantial benefits both in terms of the expressiveness of the language (increasing modularity and providing support for simple irregular structures) and the portability of the code (increasing portability across resource-constrained devices, such as GPUs). Specifically, we generalise Blelloch's flattening transformation along two lines: (1) we explicitly distinguish between definitely regular and potentially irregular computations; and (2) we handle multidimensional arrays. We demonstrate the utility of this generalisation by an extension of the embedded array language Accelerate to include irregular streams of multidimensional arrays. We discuss code generation, optimisation, and irregular stream scheduling as well as a range of benchmarks on both multicore CPUs and GPUs.

Improving STM Performance with Transactional Structs
Ryan Yates and Michael L. Scott
(University of Rochester, USA)
Software transactional memory (STM) has made it significantly easier to write correct concurrent programs in Haskell. Its performance, however, is limited by several inefficiencies. While safe concurrent computations are easy to express in Haskell’s STM, concurrent data structures suffer unfortunate bloat in the implementation due to an extra level of indirection for mutable references as well as the inability to express unboxed mutable transactional values. We address these deficiencies by introducing TStruct to the GHC run-time system, allowing strict unboxed transactional values as well as mutable references without an extra indirection. Using TStruct we implement several data structures, discuss their design, and provide benchmark results on a large multicore machine. Our benchmarks show that concurrent data structures built with TStruct out-scale and out-perform their TVar-based equivalents.

Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping
Chao-Hong Chen, Vikraman Choudhury, and Ryan R. Newton
(Indiana University, USA)
A key part of implementing high-level languages is providing built- in and default data structures. Yet selecting good defaults is hard. A mutable data structure’s workload is not known in advance, and it may shift over its lifetime—e.g., between read-heavy and write- heavy, or from heavy contention by multiple threads to single- threaded or low-frequency use. One idea is to switch implementa- tions adaptively, but it is nontrivial to switch the implementation of a concurrent data structure at runtime. Performing the transition requires a concurrent snapshot of data structure contents, which normally demands special engineering in the data structure’s de- sign. However, in this paper we identify and formalize an relevant property of lock-free algorithms. Namely, lock-freedom is su cient to guarantee that freezing memory locations in an arbitrary order will result in a valid snapshot. Several functional languages have data structures that freeze and thaw, transitioning between mutable and immutable, such as Haskell vectors and Clojure transients, but these enable only single-threaded writers. We generalize this approach to augment an arbitrary lock-free data structure with the ability to gradually freeze and optionally transition to a new representation. This aug- mentation doesn’t require changing the algorithm or code for the data structure, only replacing its datatype for mutable references with a freezable variant. In this paper, we present an algorithm for lifting plain to adaptive data and prove that the resulting hy- brid data structure is itself lock-free, linearizable, and simulates the original. We also perform an empirical case study in the context of heating up and cooling down concurrent maps.

proc time: 0.82