The purpose of the Haskell Symposium is to discuss experiences with
Haskell and future developments for the language.
Topics of interest include, but are not limited to:
Papers in the latter three categories need not necessarily report
original research results; they may instead, for example, report
practical experience that will be useful to others, reusable
programming idioms, or elegant new ways of approaching a
problem.
The key criterion for such a paper is that it makes a
contribution from which other Haskellers can benefit. It is not
enough simply to describe a program!
Regular papers should explain their research contributions in both
general and technical terms, identifying what has been accomplished,
explaining why it is significant, and relating it to previous work (also
for other languages where appropriate).
In addition, we solicit proposals for system demonstrations, based on
running (perhaps prototype) software rather than necessarily on novel
research results. Such short demo proposals should explain why a
demonstration would be of interest to the Haskell community.
Accepted demo proposals, assessed for relevance by the PC, will be
published on the symposium web page, but not formally published in the
proceedings.
Submitted papers should be in portable document format (PDF),
formatted using the ACM SIGPLAN style guidelines
(http://www.acm.org/sigs/sigplan/authorInformation.htm).
The text
should be in a 9pt font in two columns; the length is restricted to
12 pages, except for Experience Report
papers, which are restricted to 6 pages. Each paper submission must
adhere to SIGPLAN's republication policy.
Demo proposals are limited to 2-page abstracts,
in the same ACM format as papers.
"Functional Pearls", "Experience Reports", and "Demo Proposals" should
be marked as such with those words in the title at time of submission.
The paper submission deadline and length limitations are firm. There
will be no extensions, and papers violating the length limitations will
be summarily rejected.
Session 1
chair: Colin Runciman
09:00–09:25
The HERMIT in the Machine: A Plugin for the Interactive Transformation of GHC Core Language Programs
(@YouTube)
Abstract:
The importance of reasoning about and refactoring programs is a
central tenet of functional programming. Yet our compilers and development
toolchains only provide rudimentary support for these
tasks. This paper introduces a programmatic and compiler-centric
interface that facilitates refactoring and equational reasoning. To
develop our ideas, we have implemented HERMIT, a toolkit enabling
informal but systematic transformation of Haskell programs
from inside the Glasgow Haskell Compiler's optimization pipeline.
With HERMIT, users can experiment with optimizations and equational
reasoning, while the tedious heavy lifting of performing the
actual transformations is done for them.
HERMIT provides a transformation API that can be used to
build higher-level rewrite tools. One use-case is prototyping new
optimizations as clients of this API before being committed to
the GHC toolchain. We describe a HERMIT application—a read-eval-print
shell for performing transformations using HERMIT. We
also demonstrate using this shell to prototype an optimization on a
specific example, and report our initial experiences and remaining
challenges.
Abstract:
Though Haskell is predominantly type-safe, implementations contain
a few loopholes through which code can bypass typing and
module encapsulation. This paper presents Safe Haskell, a language
extension that closes these loopholes. Safe Haskell makes it possible
to confine and safely execute untrusted, possibly malicious
code. By strictly enforcing types, Safe Haskell allows a variety of
different policies from API sandboxing to information-flow control
to be implemented easily as monads. Safe Haskell is aimed to
be as unobtrusive as possible. It enforces properties that programmers
tend to meet already by convention. We describe the design
of Safe Haskell and an implementation (currently shipping with
GHC) that infers safety for code that lies in a safe subset of the
language. We use Safe Haskell to implement an online Haskell interpreter
that can securely execute arbitrary untrusted code with no
overhead. The use of Safe Haskell greatly simplifies this task and
allows the use of a large body of existing code and tools.
Session 2
chair: Iavor Diatchki
10:10–10:35
Guiding Parallel Array Fusion with Indexed Types
(@YouTube)
Abstract:
We present a refined approach to parallel array fusion that uses
indexed types to specify the internal representation of each array.
Our approach aids the client programmer in reasoning about the
performance of their program in terms of the source code. It also
makes the intermediate code easier to transform at compile-time,
resulting in faster compilation and more reliable runtimes. We
demonstrate how our new approach improves both the clarity and
performance of several end-user written programs, including a fluid
flow solver and an interpolator for volumetric data.
Abstract:
Flattening nested parallelism is a vectorising code transform that
converts irregular nested parallelism into flat data parallelism. Although
the result has good asymptotic performance, flattening thoroughly
restructures the code. Many intermediate data structures and
traversals are introduced, which may or may not be eliminated by
subsequent optimisation. We present a novel program analysis to
identify parts of the program where flattening would only introduce
overhead, without appropriate gain. We present empirical evidence
that avoiding vectorisation in these cases leads to more efficient
programs than if we had applied vectorisation and then relied on
array fusion to eliminate intermediates from the resulting code.
Session 3
chair: Brent A. Yorgey
Abstract:
The specification of a class in Haskell often starts with stating, in
comments, the laws that should be satisfied by methods defined
in instances of the class, followed by the type of the methods of
the class. This paper develops a framework that supports testing
such class laws using QuickCheck. Our framework is a light-weight
class law testing framework, which requires a limited amount of
work per class law, and per datatype for which the class law is
tested. We also show how to test class laws with partially-defined
values. Using partially-defined values, we show that the standard
lazy and strict implementations of the state monad do not satisfy
the expected laws.
11:35–12:00
Feat: Functional Enumeration of Algebraic Types
(@YouTube)
Abstract:
In mathematics, an enumeration of a set S is a bijective function
from (an initial segment of) the natural numbers to S. We define
"functional enumerations" as efficiently computable such bijections.
This paper describes a theory of functional enumeration and
provides an algebra of enumerations closed under sums, products,
guarded recursion and bijections. We partition each enumerated set
into numbered, finite subsets.
We provide a generic enumeration such that the number of each
part corresponds to the size of its values (measured in the number
of constructors). We implement our ideas in a Haskell library
called testing-feat, and make the source code freely available.
Feat provides efficient "random access" to enumerated values. The
primary application is property-based testing, where it is used to
define both random sampling (for example QuickCheck generators)
and exhaustive enumeration (in the style of SmallCheck). We
claim that functional enumeration is the best option for automatically
generating test cases from large groups of mutually recursive
syntax tree types. As a case study we use Feat to test the pretty-printer
of the Template Haskell library (uncovering several bugs).
12:00–12:25
Shrinking and Showing Functions
(Functional Pearl) (@YouTube)
Koen Claessen
Abstract:
Although quantification over functions in QuickCheck properties
has been supported from the beginning, displaying and shrinking
them as counter examples has not. The reason is that in general,
functions are infinite objects, which means that there is no sensible
show function for them, and shrinking an infinite object within
a finite number of steps seems impossible. This paper presents a
general technique with which functions as counter examples can
be shrunk to finite objects, which can then be displayed to the user.
The approach turns out to be practically usable, which is shown by
a number of examples. The two main limitations are that higher-order
functions cannot be dealt with, and it is hard to deal with
terms that contain functions as subterms.
Session 4
chair: Simon Peyton Jones
13:45–14:10
Surveyor: A DSEL for Representing and Analyzing Strongly Typed Surveys
(@YouTube)
Abstract:
Polls and surveys are increasingly employed to gather information
about attitudes and experiences of all kinds of populations and user
groups. The ultimate purpose of a survey is to identify trends and
relationships that can inform decision makers. To this end, the data
gathered by a survey must be appropriately analyzed.
Most of the currently existing tools focus on the user interface
aspect of the data collection task, but pay little attention to the structure
and type of the collected data, which are usually represented
as potentially tag-annotated, but otherwise unstructured, plain text.
This makes the task of writing data analysis programs often difficult
and error-prone, whereas a typed data representation could
support the writing of type-directed data analysis tools that would
enjoy the many benefits of static typing.
In this paper we present Surveyor, a DSEL that allows the compositional
construction of typed surveys, where the types describe
the structure of the data to be collected. A survey can be run to
gather typed data, which can then be subjected to analysis tools that
are built using Surveyor's typed combinators. Altogether the Surveyor
DSEL realizes a strongly typed and type-directed approach
to data gathering and analysis.
The implementation of our DSEL is based on GADTs to allow
a flexible, yet strongly typed representation of surveys. Moreover,
the implementation employs the Scrap-Your-Boilerplate library to
facilitate the type-dependent traversal, extraction, and combination
of data gathered from surveys.
14:10–14:35
Daniel Winograd-Cort and
Paul Hudak
Abstract:
Functional reactive programming (FRP) is a useful model for programming
real-time and reactive systems in which one defines a
signal function to process a stream of input values into a stream of
output values. However, performing side effects (e.g. memory mutation
or input/output) in this model is tricky and typically unsafe.
In previous work, Winograd-Cort et al. [2012] introduced resource types
and wormholes to address this problem.
This paper better motivates, expands upon, and formalizes the
notion of a wormhole to fully unlock its potential. We show, for example,
that wormholes can be used to define the concept of causality.
This in turn allows us to provide behaviors such as looping, a
core component of most languages, without building it directly into
the language. We also improve upon our previous design by making
wormholes less verbose and easier to use.
To formalize the notion of a wormhole, we define an extension
to the simply typed lambda calculus, complete with typing rules
and operational semantics. In addition, we present a new form of
semantic transition that we call a temporal transition to specify
how an FRP program behaves over time and to allow us to better
reason about causality. As our model is designed for a Haskell
implementation, the semantics are lazy. Finally, with the language
defined, we prove that our wormholes indeed allow side effects to
be performed safely in an FRP framework.
14:35–15:00
Monoids: Theme and Variations
(Functional Pearl) (@YouTube)
Abstract:
The monoid is a humble algebraic structure, at first glance even
downright boring. However, there's much more to monoids than
meets the eye. Using examples taken from the diagrams vector
graphics framework as a case study, I demonstrate the power and
beauty of monoids for library design. The paper begins with an
extremely simple model of diagrams and proceeds through a series
of incremental variations, all related somehow to the central theme
of monoids. Along the way, I illustrate the power of compositional
semantics; why you should also pay attention to the monoid's
even humbler cousin, the semigroup; monoid homomorphisms; and
monoid actions.
Session 5
chair: Nils Anders Danielsson
15:25–15:50
Dependently Typed Programming with Singletons
(@YouTube)
Abstract:
Haskell programmers have been experimenting with dependent
types for at least a decade, using clever encodings that push the
limits of the Haskell type system. However, the cleverness of these
encodings is also their main drawback. Although the ideas are inspired
by dependently typed programs, the code looks significantly
different. As a result, GHC implementors have responded with extensions
to Haskell's type system, such as GADTs, type families,
and datatype promotion. However, there remains a significant difference
between programming in Haskell and in full-spectrum dependently
typed languages. Haskell enforces a phase separation between
runtime values and compile-time types. Therefore, singleton
types are necessary to express the dependency between values and
types. These singleton types introduce overhead and redundancy
for the programmer.
This paper presents the singletons library, which generates the
boilerplate code necessary for dependently typed programming
using GHC. To compare with full-spectrum languages, we present
an extended example based on an Agda interface for safe database
access. The paper concludes with a detailed discussion on the
current capabilities of GHC for dependently typed programming
and suggestions for future extensions to better support this style of
programming.
15:50–16:05
xmonad in Coq
(Experience Report): Programming a Window Manager with a Proof Assistant
(@YouTube)
Wouter Swierstra
Abstract:
This report documents the insights gained from implementing the
core functionality of xmonad, a popular window manager written
in Haskell, in the Coq proof assistant. Rather than focus on verification,
this report outlines the technical challenges involved with
incorporating Coq code in a Haskell project.
16:05–16:30
Template Your Boilerplate: Using Template Haskell for Efficient Generic Programming
(@YouTube)
Michael D. Adams and
Thomas M. DuBuisson
Abstract:
Generic programming allows the concise expression of algorithms
that would otherwise require large amounts of handwritten code. A
number of such systems have been developed over the years, but a
common drawback of these systems is poor runtime performance
relative to handwritten, non-generic code. Generic-programming
systems vary significantly in this regard, but few consistently match
the performance of handwritten code. This poses a dilemma for developers.
Generic-programming systems offer concision but cost
performance. Handwritten code offers performance but costs concision.
This paper explores the use of Template Haskell to achieve
the best of both worlds. It presents a generic-programming system
for Haskell that provides both the concision of other generic-programming
systems and the efficiency of handwritten code. Our
system gives the programmer a high-level, generic-programming
interface, but uses Template Haskell to generate efficient, non-generic
code that outperforms existing generic-programming systems
for Haskell.
This paper presents the results of benchmarking our system
against both handwritten code and several other generic-programming
systems. In these benchmarks, our system matches
the performance of handwritten code while other systems average
anywhere from two to twenty times slower.
Session 6
chair: Zhenjiang Hu
16:40–17:05
Layout-sensitive Language Extensibility with SugarHaskell
(@YouTube)
Abstract:
Programmers need convenient syntax to write elegant and concise
programs. Consequently, the Haskell standard provides syntactic
sugar for some scenarios (e.g., do notation for monadic code), authors
of Haskell compilers provide syntactic sugar for more scenarios
(e.g., arrow notation in GHC), and some Haskell programmers
implement preprocessors for their individual needs (e.g., idiom
brackets in SHE). But manually written preprocessors cannot
scale: They are expensive, error-prone, and not composable. Most
researchers and programmers therefore refrain from using the syntactic
notations they need in actual Haskell programs, but only use
them in documentation or papers. We present a syntactically extensible
version of Haskell, SugarHaskell, that empowers ordinary
programmers to implement and use custom syntactic sugar.
Building on our previous work on syntactic extensibility for
Java, SugarHaskell integrates syntactic extensions as sugar libraries
into Haskell's module system. Syntax extensions in SugarHaskell
can declare arbitrary context-free and layout-sensitive syntax. SugarHaskell
modules are compiled into Haskell modules and further
processed by a Haskell compiler. We provide an Eclipse-based IDE
for SugarHaskell that is extensible, too, and automatically provides
syntax coloring for all syntax extensions imported into a module.
We have validated SugarHaskell with several case studies, including
arrow notation (as implemented in GHC) and EBNF as a
concise syntax for the declaration of algebraic data types with associated
concrete syntax. EBNF declarations also show how to extend
the extension mechanism itself: They introduce syntactic sugar for
using the declared concrete syntax in other SugarHaskell modules.
