ICFP 2016 Workshops
21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)
Powered by
Conference Publishing Consulting

1st International Workshop on Type-Driven Development (TyDe 2016), September 18, 2016, Nara, Japan

TyDe 2016 – Proceedings

Contents - Abstracts - Authors

1st International Workshop on Type-Driven Development (TyDe 2016)

Title Page

Message from the Chairs
Welcome to the 1st ACM SIGPLAN Workshop on Type-Driven Development (TyDe ‘16), held in Nara, Japan on Sunday, 18th September, 2016, co-located with the International Conference on Functional Programming (ICFP 2016). The workshop aims to show how static type information may be used effectively in the development of computer programs.
Generic Lookup and Update for Infinitary Inductive-Recursive Types
Larry Diehl and Tim Sheard
(Portland State University, USA)
The class of Infinitary inductive-recursive (InfIR) types is commonly used to model type theory within itself. While it is common and convenient to provide examples of values within an InfIR model, writing functions that manipulate InfIR types is an underexplored area due to their inherent complexity. Our goal in this work is to push the boundaries of programming with InfIR types by introducing two functions operating over them. The first is a lookup function to extract sub-components from an InfIR type, and the second is an update function to replace sub-components within an InfIR type. We start by considering how to write such functions for concrete examples of InfIR types, and then show how to write generic versions of the functions for any datatype definable in the universe of InfIR types. We actually write two versions of the generic functions, one where the universe is open and another where the universe is closed.
Publisher's Version Article Search Info
APLicative Programming with Naperian Functors (Extended Abstract)
Jeremy Gibbons
(University of Oxford, UK)
A lot of the expressive power of array-oriented languages such as Iverson's APL and J comes from their implicit lifting of scalar operations to act on higher-ranked data, for example to add a value to each element of a vector, or to add two compatible matrices pointwise. But it is a shape error to attempt to combine arguments of incompatible shape, such as a 3-vector with a 4-vector. APL and J are dynamically typed, so such shape errors are caught only at run-time. Recent work by Slepak et al. develops a custom static type system for an array-oriented language. We show here that such a custom language design is unnecessary; the requisite compatibility checks can already be captured in modern expressive type systems, as found for example in Haskell, and moreover, generative type-driven programming can use that static type information constructively to automatically induce the appropriate liftings. We show also that the structure of multi-dimensional data is inherently a matter of Naperian applicative functors - lax monoidal functors, with strength, commutative up to isomorphism under composition.
Publisher's Version Article Search Info
Liberating Effects with Rows and Handlers
Daniel Hillerström and Sam Lindley
(University of Edinburgh, UK)
Algebraic effects and effect handlers provide a modular abstraction for effectful programming. They support user-defined effects, as in Haskell, in conjunction with direct-style effectful programming, as in ML. They also present a structured interface to programming with delimited continuations. In order to be modular, it is necessary for an effect type system to support extensible effects. Row polymorphism is a natural abstraction for modelling extensibility at the level of types. In this paper we argue that the abstraction required to implement extensible effects and their handlers is exactly row polymorphism. We use the Links functional web programming language as a platform to substantiate this claim. Links is a natural starting point as it uses row polymorphism for polymorphic variants, records, and its built-in effect types. It also has infrastructure for manipulating continuations. Through a small extension to Links we smoothly add support for effect handlers, making essential use of rows in the frontend and first-class continuations in the backend. We demonstrate the usability of our implementation by modelling the mathematical game of Nim as an abstract computation. We interpret this abstract computation in a variety of ways, illustrating how rows and handlers support modularity and smooth composition of effectful computations. We present a core calculus of row-polymorphic effects and handlers based on a variant of A-normal form used in the intermediate representation of Links. We give an operational semantics for the calculus and a novel generalisation of the CEK machine that implements the operational semantics, and prove that the two coincide.
Publisher's Version Article Search
Programming with Monadic CSP-Style Processes in Dependent Type Theory
Bashar Igried and Anton Setzer
(Swansea University, UK)

We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad structure facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinductively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock’s notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new elements of the data type of processes from existing ones.

The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of finitary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in template Meta-programming in C++; and the use of interactive programs in dependent type theory.

We introduce a simulator as an interactive program in Agda. The simulator allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes.


Publisher's Version Article Search Info
Generic Partially-Static Data (Extended Abstract)
David Kaloper-Meršinjak and Jeremy Yallop
(University of Cambridge, UK)
We describe a generic approach to defining partially-static data and corresponding operations.
Publisher's Version Article Search
Parameterized Extensible Effects and Session Types (Extended Abstract)
Oleg Kiselyov
(Tohoku University, Japan)
Parameterized monad goes beyond monads in letting us represent type-state. An effect executed by a computation may change the set of effects it may be allowed to do afterwards. We describe how to easily `add' and `subtract' such type-state effects. Parameterized monad is often used to implement session types. We point out that extensible type-state effects are themselves a form of session types.
Publisher's Version Article Search Info
Applications of Applicative Proof Search
Liam O'Connor
(UNSW, Australia; Data61, Australia)
In this paper, we develop a library of typed proof search procedures, and demonstrate their remarkable utility as a mechanism for proof-search and automation. We describe a framework for describing proof-search procedures in Agda, with a library of tactical combinators based on applicative functors. This framework is very general, so we demonstrate the approach with two common applications from the field of software verification: a library for property-based testing in the style of SmallCheck, and the embedding of a basic model checker inside our framework, which we use to verify the correctness of common concurrency algorithms.
Publisher's Version Article Search
Programming Assistance for Type-Directed Programming (Extended Abstract)
Peter-Michael Osera
(Grinnell College, USA)
Type-directed programming is a powerful programming paradigm where rich types dictate the structure of the program, making design largely automatic. While mechanical, this paradigm still requires manual reasoning that is both tedious and error-prone. We propose using type-directed program synthesis techniques to build an interactive programming assistant for type-directed programming. This tool bridges the gaps between simple auto-completion engines and program synthesis, complementing the strengths of each.
Publisher's Version Article Search
choose Your Own Derivative (Extended Abstract)
Jennifer Paykin, Antal Spector-Zabusky, and Kenneth Foner
(University of Pennsylvania, USA)

We discuss a generalization of the synchronization mechanism selective choice. We argue that selective choice can be extended to synchronize arbitrary data structures of events, based on a typing paradigm introduced by McBride: the derivatives of recursive data types. We discuss our work in progress implementing generalized selective choice as a Haskell library based on generic programming.


Publisher's Version Article Search
An Agda Formalisation of the Transitive Closure of Block Matrices (Extended Abstract)
Adam Sandberg Eriksson and Patrik Jansson
(Chalmers University of Technology, Sweden)
We define a block based matrix representation in Agda and lift various algebraic structures (semi-near-rings, semi-rings and closed semi-rings) to matrices in order to verify algorithms that can be implemented using the closure operation in a semi-ring.
Publisher's Version Article Search Info
Generic Diff3 for Algebraic Datatypes
Marco Vassena
(Chalmers University of Technology, Sweden)

Many version control systems, including Git and Mercurial, rely on diff3 to merge different revisions of the same file. More precisely diff3 automatically merges two text files, given a common base version, comparing them line by line and raising conflicts when the changes made are irreconcilable. The program ignores the actual structure of the data stored in the files, hence it might generate spurious conflicts, which must be manually resolved by the user. In this paper, we present a state-based, three-way, persistent, data-type generic diff3 algorithm whose increased precision in detecting changes reduces the number of false conflicts raised and improves its merging capabilities. We have implemented the algorithm in Agda, a proof assistant with dependent types, and developed a model to reason about “diffing” and merging. We have formalized sanity properties and specifications of diff3 and proved that our algorithm meets them. Furthermore, we have identified the minimal conditions under which the merging algorithm raises a conflict and established a structural invariant preserved.


Publisher's Version Article Search

proc time: 1.45