Powered by
10th ACM SIGPLAN International Haskell Symposium (Haskell 2017),
September 7-8, 2017,
Oxford, UK
10th ACM SIGPLAN International Haskell Symposium (Haskell 2017)
Frontmatter
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.
@InProceedings{Haskell17p1,
author = {Didier Rémy},
title = {Ornaments: Exploiting Parametricity for Safer, More Automated Code Refactorization and Code Reuse (Invited Talk)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {1--1},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p2,
author = {Andrey Mokhov},
title = {Algebraic Graphs with Class (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {2--13},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p14,
author = {Mario Blažević and Jacques Légaré},
title = {Packrats Parse in Packs},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {14--25},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p26,
author = {Leonidas Lampropoulos and Antal Spector-Zabusky and Kenneth Foner},
title = {Ode on a Random Urn (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {26--37},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p38,
author = {Maximilian Algehed and Koen Claessen and Moa Johansson and Nick Smallbone},
title = {QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {38--39},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p40,
author = {Rudy Braquehais and Colin Runciman},
title = {Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {40--51},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p52,
author = {John Wiegley and Benjamin Delaware},
title = {Using Coq to Write Fast and Correct Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {52--62},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p63,
author = {Niki Vazou and Leonidas Lampropoulos and Jeff Polakow},
title = {A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {63--74},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p75,
author = {Anton Ekblad},
title = {A Meta-EDSL for Distributed Web Applications},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {75--85},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p86,
author = {Justin Dawson and Mark Grebe and Andy Gill},
title = {Composable Network Stacks and Remote Monads},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {86--97},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p98,
author = {Donya Quick},
title = {Algorithmic Music in Haskell (Invited Talk)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {98--98},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p99,
author = {Dmitrij Szamozvancev and Michael B. Gale},
title = {Well-Typed Music Does Not Sound Wrong (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {99--104},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p105,
author = {Ivan Perez},
title = {Back to the Future: Time Travel in FRP},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {105--116},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p117,
author = {Jennifer Paykin and Steve Zdancewic},
title = {The Linearity Monad},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {117--132},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p133,
author = {Georgios Karachalias and Tom Schrijvers},
title = {Elaboration on Functional Dependencies: Functional Dependencies Are Dead, Long Live Functional Dependencies!},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {133--147},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p148,
author = {Gert-Jan Bottu and Georgios Karachalias and Tom Schrijvers and Bruno C. d. S. Oliveira and Philip Wadler},
title = {Quantified Class Constraints},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {148--161},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p162,
author = {Markus Aronsson and Mary Sheeran},
title = {Hardware Software Co-design in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {162--173},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p174,
author = {Robert Clifton-Everest and Trevor L. McDonell and Manuel M. T. Chakravarty and Gabriele Keller},
title = {Streaming Irregular Arrays},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {174--185},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p186,
author = {Ryan Yates and Michael L. Scott},
title = {Improving STM Performance with Transactional Structs},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {186--196},
doi = {},
year = {2017},
}
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.
@InProceedings{Haskell17p197,
author = {Chao-Hong Chen and Vikraman Choudhury and Ryan R. Newton},
title = {Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {197--211},
doi = {},
year = {2017},
}
proc time: 0.82