Workshop TyDe 2016 – Author Index 
Contents 
Abstracts 
Authors

Diehl, Larry 
TyDe '16: "Generic Lookup and Update ..."
Generic Lookup and Update for Infinitary InductiveRecursive Types
Larry Diehl and Tim Sheard (Portland State University, USA)
The class of Infinitary inductiverecursive (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 subcomponents from an
InfIR type, and the second is an update function to replace
subcomponents 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 InductiveRecursive Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {112},
doi = {10.1145/2976022.2976031},
year = {2016},
}
Publisher's Version
Article Search
Info


Foner, Kenneth 
TyDe '16: "choose Your Own Derivative ..."
choose Your Own Derivative (Extended Abstract)
Jennifer Paykin, Antal SpectorZabusky, 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. 

Gibbons, Jeremy 
TyDe '16: "APLicative Programming with ..."
APLicative Programming with Naperian Functors (Extended Abstract)
Jeremy Gibbons (University of Oxford, UK)
A lot of the expressive power of arrayoriented languages such as Iverson's APL and J comes from their implicit lifting of scalar operations to act on higherranked 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 3vector with a 4vector. APL and J are dynamically typed, so such shape errors are caught only at runtime. Recent work by Slepak et al. develops a custom static type system for an arrayoriented 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 typedriven programming can use that static type information constructively to automatically induce the appropriate liftings. We show also that the structure of multidimensional 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 = {1314},
doi = {10.1145/2976022.2976023},
year = {2016},
}
Publisher's Version
Article Search
Info


Hillerström, Daniel 
TyDe '16: "Liberating Effects with Rows ..."
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 userdefined effects, as in Haskell, in conjunction with
directstyle 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 builtin
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 firstclass
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 rowpolymorphic effects and handlers
based on a variant of Anormal 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 = {1527},
doi = {10.1145/2976022.2976033},
year = {2016},
}
Publisher's Version
Article Search


Igried, Bashar 
TyDe '16: "Programming with Monadic CSPStyle ..."
Programming with Monadic CSPStyle Processes in Dependent Type Theory
Bashar Igried and Anton Setzer (Swansea University, UK) We introduce a library called CSPAgda 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 nonwellfounded 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 inductiverecursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in objectoriented 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 Metaprogramming 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. 

Jansson, Patrik 
TyDe '16: "An Agda Formalisation of the ..."
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 (seminearrings, semirings and closed semirings) to matrices in order to verify algorithms that can be implemented using the closure operation in a semiring.
@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 = {6061},
doi = {10.1145/2976022.2976025},
year = {2016},
}
Publisher's Version
Article Search
Info


KaloperMeršinjak, David 
TyDe '16: "Generic PartiallyStatic Data ..."
Generic PartiallyStatic Data (Extended Abstract)
David KaloperMeršinjak and Jeremy Yallop (University of Cambridge, UK)
We describe a generic approach to defining partiallystatic data and corresponding operations.
@InProceedings{TyDe16p39,
author = {David KaloperMeršinjak and Jeremy Yallop},
title = {Generic PartiallyStatic Data (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {3940},
doi = {10.1145/2976022.2976028},
year = {2016},
}
Publisher's Version
Article Search


Kiselyov, Oleg 
TyDe '16: "Parameterized Extensible Effects ..."
Parameterized Extensible Effects and Session Types (Extended Abstract)
Oleg Kiselyov (Tohoku University, Japan)
Parameterized monad goes beyond monads in letting us represent
typestate. 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 typestate
effects. Parameterized monad is often used to implement session
types. We point out that extensible typestate 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 = {4142},
doi = {10.1145/2976022.2976034},
year = {2016},
}
Publisher's Version
Article Search
Info


Lindley, Sam 
TyDe '16: "Liberating Effects with Rows ..."
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 userdefined effects, as in Haskell, in conjunction with
directstyle 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 builtin
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 firstclass
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 rowpolymorphic effects and handlers
based on a variant of Anormal 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 = {1527},
doi = {10.1145/2976022.2976033},
year = {2016},
}
Publisher's Version
Article Search


O'Connor, Liam 
TyDe '16: "Applications of Applicative ..."
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
proofsearch and automation.
We describe a framework for describing proofsearch 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 propertybased 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 = {4355},
doi = {10.1145/2976022.2976030},
year = {2016},
}
Publisher's Version
Article Search


Osera, PeterMichael 
TyDe '16: "Programming Assistance for ..."
Programming Assistance for TypeDirected Programming (Extended Abstract)
PeterMichael Osera (Grinnell College, USA)
Typedirected 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 errorprone. We propose using typedirected program synthesis techniques to
build an interactive programming assistant for typedirected programming. This
tool bridges the gaps between simple autocompletion engines and program
synthesis, complementing the strengths of each.
@InProceedings{TyDe16p56,
author = {PeterMichael Osera},
title = {Programming Assistance for TypeDirected Programming (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {5657},
doi = {10.1145/2976022.2976027},
year = {2016},
}
Publisher's Version
Article Search


Paykin, Jennifer 
TyDe '16: "choose Your Own Derivative ..."
choose Your Own Derivative (Extended Abstract)
Jennifer Paykin, Antal SpectorZabusky, 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. 

Sandberg Eriksson, Adam 
TyDe '16: "An Agda Formalisation of the ..."
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 (seminearrings, semirings and closed semirings) to matrices in order to verify algorithms that can be implemented using the closure operation in a semiring.
@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 = {6061},
doi = {10.1145/2976022.2976025},
year = {2016},
}
Publisher's Version
Article Search
Info


Setzer, Anton 
TyDe '16: "Programming with Monadic CSPStyle ..."
Programming with Monadic CSPStyle Processes in Dependent Type Theory
Bashar Igried and Anton Setzer (Swansea University, UK) We introduce a library called CSPAgda 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 nonwellfounded 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 inductiverecursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in objectoriented 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 Metaprogramming 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. 

Sheard, Tim 
TyDe '16: "Generic Lookup and Update ..."
Generic Lookup and Update for Infinitary InductiveRecursive Types
Larry Diehl and Tim Sheard (Portland State University, USA)
The class of Infinitary inductiverecursive (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 subcomponents from an
InfIR type, and the second is an update function to replace
subcomponents 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 InductiveRecursive Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {112},
doi = {10.1145/2976022.2976031},
year = {2016},
}
Publisher's Version
Article Search
Info


SpectorZabusky, Antal 
TyDe '16: "choose Your Own Derivative ..."
choose Your Own Derivative (Extended Abstract)
Jennifer Paykin, Antal SpectorZabusky, 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. 

Vassena, Marco 
TyDe '16: "Generic Diff3 for Algebraic ..."
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 statebased, threeway, persistent, datatype 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. 

Yallop, Jeremy 
TyDe '16: "Generic PartiallyStatic Data ..."
Generic PartiallyStatic Data (Extended Abstract)
David KaloperMeršinjak and Jeremy Yallop (University of Cambridge, UK)
We describe a generic approach to defining partiallystatic data and corresponding operations.
@InProceedings{TyDe16p39,
author = {David KaloperMeršinjak and Jeremy Yallop},
title = {Generic PartiallyStatic Data (Extended Abstract)},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {3940},
doi = {10.1145/2976022.2976028},
year = {2016},
}
Publisher's Version
Article Search

18 authors
proc time: 1.28