ICFP Workshops 2017
22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017)

Title Page

Message from the Chairs
Welcome to the 2nd ACM SIGPLAN Workshop on Type-Driven Development (TyDe '17), held in Oxford, United Kingdom on Sunday, 3rd September, 2017, co-located with the International Conference on Functional Programming (ICFP 2017). The workshop aims to show how static type information may be used effectively in the development of computer programs.

Driving Types into PHP (Invited Talk)
Andrew Kennedy
(Facebook, UK)
Facebook’s main website, ads platform, and much of its internal tooling is implemented in PHP, a language not known for elegance or best practice in programming language design. Five years ago Facebook embarked on an ambitious project to migrate its code base to Hack, which takes the syntax of PHP, removes the worst features, and adds static typing and modern constructs for asynchronous programming. Its type system is an interesting mixture of ideas from Java, C#, Scala, and Caml, with flow-sensitive typing thrown in to capture typical PHP idioms. Type-driven development is now more than accepted: developers demand ever richer types, and evolution of the codebase goes hand-in-hand with evolution of the type system and programming language.

@InProceedings{TyDe17p1, author = {Andrew Kennedy}, title = {Driving Types into PHP (Invited Talk)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {1--1}, doi = {}, year = {2017}, }

Type-Directed Diffing of Structured Data
Victor Cacciari Miraldo, Pierre-Évariste Dagand, and Wouter Swierstra
(Utrecht University, Netherlands; UPMC, France)
The Unix diff utility that compares lines of text is used pervasively by version control systems. Yet certain changes to a program may be difficult to describe accurately in terms of modifications to individual lines of code. As a result, observing changes at such a fixed granularity may lead to unnecessary conflicts between different edits. This paper presents a generic representation for describing transformations between algebraic data types and a non-deterministic algorithm for computing such representations. These representations can be used to give a more accurate account of modifications made to algebraic data structures – and the abstract syntax trees of computer programs in particular – as opposed to only considering modifications between their textual representations.

@InProceedings{TyDe17p2, author = {Victor Cacciari Miraldo and Pierre-Évariste Dagand and Wouter Swierstra}, title = {Type-Directed Diffing of Structured Data}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {2--15}, doi = {}, year = {2017}, }

Structured Asynchrony with Algebraic Effects
Daan Leijen
(Microsoft Research, USA)
Algebraic effect handlers generalize many control-flow abstractions that are implemented specially in most languages, like exception handling, iterators, or backtracking. In this article, we show how we can implement full support for asynchronous programming as a library using just algebraic effect handlers. The consistent type driven approach also leads naturally to powerful abstractions like block-scoped interleaving, cancellation, and timeout's that are lacking in other major asynchronous frameworks. We also introduce the concept of ambient state to reason about state that is local to the current strand of asynchronous execution.

@InProceedings{TyDe17p16, author = {Daan Leijen}, title = {Structured Asynchrony with Algebraic Effects}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {16--29}, doi = {}, year = {2017}, }

Generic Packet Descriptions: Verified Parsing and Pretty Printing of Low-Level Data
Marcell van Geest and Wouter Swierstra
(Utrecht University, Netherlands)
Complex protocols describing the communication or storage of binary data are difficult to describe precisely. This paper presents a collection of data types for describing a binary data formats; the corresponding parser and pretty printer are generated automatically from a data description. By embedding these data types in a general purpose dependently typed programming language, we can verify once and for all that the parsers and pretty printers generated in this style are correct by construction. To validate our results, we show how to write a verified parser of the IPv4 network protocol.

@InProceedings{TyDe17p30, author = {Marcell van Geest and Wouter Swierstra}, title = {Generic Packet Descriptions: Verified Parsing and Pretty Printing of Low-Level Data}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {30--40}, doi = {}, year = {2017}, }