WGP 2015 – Proceedings

Foreword
It is our great pleasure to welcome you to the 11th ACM SIGPLAN Workshop on Generic Programming (WGP 2015), held in Vancouver 30th August 2015. The workshop is sponsored by ACM SIGPLAN and is affiliated with the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). Previous Workshops on Generic Programming have been held in Gothenburg, Boston, Copenhagen, Tokyo, Baltimore, Edinburgh, Victoria and Portland (all affiliated with ICFP), as informal workshops in Utrecht, Dagstuhl and Nottingham, and before that, as workshops affiliated with MPC in Ponte de Lima and Marstrand.

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
(Kitty Knows, UK; Zalora SEA, Singapore; Well-Typed, UK)
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
(University of Copenhagen, Denmark)
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.

Datatype Generic Programming in F#
Ernesto Rodriguez and Wouter Swierstra
(Utrecht University, Netherlands)
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
(Tallinn University of Technology, Estonia)
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.