Table of Contents

11th ACM SIGPLAN Workshop on Generic Programming (WGP 2015)

30th August 2015, Vancouver, British Columbia, Canada (co-located with ICFP 2015)

News

Program

09:00 - 10:00 Session 1 (chair: Sebastian Erdweg)
Invited Talk: Tillmann Rendel
Compositional and Linear Encoding (of Synthesized and Inherited Attributes as Object Algebras in Scala)
abstract video
10:00 - 10:30 Break
10:30 - 12:00 Session 2 (chair: Wouter Swierstra) Discussants
Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming
Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh
abstract paper video
Atze van der Ploeg
Session Types for Rust
Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen
abstract paper video
Aaron Turon
12:00 - 14:00 Lunch
14:00 - 15:00 Session 3 (chair: Patrick Bahr)
Invited Talk: Sam Lindley
Generic Programming with Effect Handlers
abstract video
15:00 - 16:00 Break
16:00 - 17:30 Session 4 (chair: Andres Löh) Discussants
Datatype Generic Programming in F#
Ernesto Rodriguez and Wouter Swierstra
abstract paper video
Tiark Rompf
Dependently Typed Programming with Finite Sets
Denis Firsov and Tarmo Uustalu
abstract paper video
Robert Atkey

Each paper presentation slot is 45 minutes: 30 minutes for the presentation + 5 minutes for the discussant + 10 minutes for general discussion.

Abstracts

Compositional and Linear Encoding (of Synthesized and Inherited Attributes as Object Algebras in Scala)

Tillmann Rendel

To maximally benefit from the modularity properties of the target language of an encoding, the encoding should be compositional and linear. We show our linear and compositional encoding of attribute grammars as object algebras in Scala. The encoding supports S-, I- and L-attributed grammars. Compositionality and linearity allow encoded programs to follow the structure of attribute grammars but also inherit the modularity of object algebras. While the core ideas of the encoding would work in many languages, we show how more Scala-specific tricks improve its usability and safety, but also which features we're missing. Finally, we reflect about which aspects of the OO and FP mix available in Scala are relevant for this kind of generic programming tasks.

Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming

Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh

We describe the design and motivation for Servant, an extensible, type-level DSL for describing Web APIs. Servant APIs are Haskell types. An API type can be interpreted in several different ways: as a server that processes requests, interprets them and dispatches them to appropriate handlers; as a client that can correctly query the endpoints of the API; as systematic documentation for the API; and more. Servant is fully extensible: the API language can be augmented with new constructs, and new interpretations can be defined. The key Haskell features making all this possible are data kinds, (open) type families and (open) type classes. The techniques we use are reminiscent of general-purpose generic programming. However, where most generic programming libraries are interested in automatically deriving programs for a large class of datatypes from many different domains, we are only interested in a small class of datatypes that is used in the DSL for describing APIs.

Session Types for Rust

Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen

We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties.

Generic programming with effect handlers

Sam Lindley

Plotkin and Power’s algebraic effects combined with Plotkin and Pretnar’s effect handlers provide a foundation for generic programming with effects.

I will present a practical introduction to effect handlers from the point of view of a functional programmer; I will demonstrate their use through a collection of example programs ranging from compositional pipelines, to the mathematical game of Nim, to aspect-oriented programming.

Time permitting, I will highlight different points in the design space with the help of two different prototype languages currently under development by my students; both languages provide special support for effect handlers. The first of these, implemented by Daniel Hillerström, is a mild extension to the Links web programming language (conceived by Philip Wadler and developed by his team at Edinburgh), taking advantage of the existing row type system of Links for effect typing and effect polymorphism. The second, implemented by Craig McLaughlin, is a prototype of the Frank language (conceived by Conor McBride and refined further by Conor and me), which takes the handler abstraction so seriously that it replaces all functions with handlers, and includes a novel form of effect polymorphism that never requires any effect variables to be revealed or to be mentioned by the programmer.

Datatype Generic Programming in F#

Ernesto Rodriguez and Wouter Swierstra

Datatype generic programming enables programmers to define functions by induction over the structure of types on which these functions operate. This paper presents a library for datatype generic programming in F#, built on top of the .NET reflection mechanism.The generic functions defined using this library can be called by any other language running on the .NET platform.

Dependently Typed Programming with Finite Sets

Denis Firsov and Tarmo Uustalu

Definitions of many mathematical structures used in computer science are parametrized by finite sets. To work with such structures in proof assistants, we need to be able to explain what a finite set is. In constructive mathematics, a widely used definition is listability: a set is considered to be finite, if its elements can be listed completely. In this paper, we formalize different variations of this definition in the Agda programming language. We develop a toolbox for boilerplate-free programming with finite sets that arise as subsets of some base set with decidable equality. Among other things we implement combinators for defining functions from finite sets and a prover for quantified formulas over decidable properties on finite sets.

Overview

Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic program are often quite rich in structure; for example they may be other programs, types or type constructors, class hierarchies, or even programming paradigms.

Generic programming techniques have always been of interest, both to practitioners and to theoreticians, and, for at least 20 years, generic programming techniques have been a specific focus of research in the functional and object-oriented programming communities. Generic programming has gradually spread to more and more mainstream languages, and today is widely used in industry. This workshop brings together leading researchers and practitioners in generic programming from around the world, and features papers capturing the state of the art in this important area.

We welcome contributions on all aspects, theoretical as well as practical, of

* generic programming,
* programming with (C++) concepts,
* meta-programming,
* programming with type classes,
* programming with modules,
* programming with dependent types,
* type systems for generic programming,
* polytypic programming,
* adaptive object-oriented programming,
* component-based programming,
* strategic programming,
* aspect-oriented programming,
* family polymorphism,
* object-oriented generic programming,
* implementation of generic programming languages,
* static and dynamic analyses of generic programs,
* and so on.

We plan to have formal proceedings, published by the ACM. Accepted papers will be included in the ACM Digital Library. Authors must grant ACM publication rights upon acceptance (http://authors.acm.org/main.html), but may retain copyright if they wish. Authors are encouraged to publish auxiliary material with their paper (source code, test data, and so forth). The proceedings will be freely available for download from the ACM Digital Library from one week before the start of the conference until two weeks after the conference.

Submission details

Submitted papers should fall into one of two categories:

Regular research papers are expected to present novel and interesting research results. Short papers need not present novel or fully polished results. Good candidates for short papers are those that report on interesting case studies of generic programming in open source or industry, present demos of generic programming tools or libraries, or discuss elegant and illustrative uses of generic programming ('pearls').

All submissions should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (two-column, 9pt). Regular research papers must not exceed 12 pages. Short papers must not exceed 6 pages. If applicable, papers should be marked with one of the labels 'case study, 'tool demo' or 'generic pearl' in the title at the time of submission.

Papers should be submitted via HotCRP at https://icfp-wgp15.hotcrp.com/.

Organizers

The call for papers is available as text file and pdf file.

Important Dates

Deadline for submission 22nd May 2015 (extended)
Notification of acceptance 26th June 2015
Final submission due 19th July 2015
Workshop 30th August 2015

Program Committee