Powered by
1st International Workshop on Type-Driven Development (TyDe 2016),
September 18, 2016,
Nara, Japan
1st International Workshop on Type-Driven Development (TyDe 2016)
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.
@InProceedings{TyDe16p1,
author = {Larry Diehl and Tim Sheard},
title = {Generic Lookup and Update for Infinitary Inductive-Recursive Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--12},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p13,
author = {Jeremy Gibbons},
title = {APLicative Programming with Naperian Functors (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {13--14},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p15,
author = {Daniel Hillerström and Sam Lindley},
title = {Liberating Effects with Rows and Handlers},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {15--27},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p28,
author = {Bashar Igried and Anton Setzer},
title = {Programming with Monadic CSP-Style Processes in Dependent Type Theory},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {28--38},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p39,
author = {David Kaloper-Meršinjak and Jeremy Yallop},
title = {Generic Partially-Static Data (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {39--40},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p41,
author = {Oleg Kiselyov},
title = {Parameterized Extensible Effects and Session Types (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {41--42},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p43,
author = {Liam O'Connor},
title = {Applications of Applicative Proof Search},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {43--55},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p56,
author = {Peter-Michael Osera},
title = {Programming Assistance for Type-Directed Programming (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {56--57},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p58,
author = {Jennifer Paykin and Antal Spector-Zabusky and Kenneth Foner},
title = {choose Your Own Derivative (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {58--59},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p60,
author = {Adam Sandberg Eriksson and Patrik Jansson},
title = {An Agda Formalisation of the Transitive Closure of Block Matrices (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {60--61},
doi = {},
year = {2016},
}
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.
@InProceedings{TyDe16p62,
author = {Marco Vassena},
title = {Generic Diff3 for Algebraic Datatypes},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {62--71},
doi = {},
year = {2016},
}
proc time: 1.03