| 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.
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.
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.
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.
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.
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.
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.
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
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.
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 . ## 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 |
Patrick Bahr (co-chair), University of Copenhagen
Sebastian Erdweg (co-chair), Technical University of Darmstadt
Edwin Brady, University of St Andrews
Edsko de Vries, Well-Typed LLP
Mauro Jaskelioff, National University of Rosario
Johan Jeuring, Utrecht University
Pieter Koopman, Radboud University Nijmegen
Bruno C. d. S. Oliveira, University of Hong Kong
Nicolas Pouillard, IT University of Copenhagen
Sukyoung Ryu, Korea Advanced Institute of Science and Technology
Sibylle Schupp, Hamburg University of Technology
Sam Tobin-Hochstadt, Indiana University