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. @InProceedings{TyDe16p58, author = {Jennifer Paykin and Antal SpectorZabusky and Kenneth Foner}, title = {choose Your Own Derivative (Extended Abstract)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {5859}, doi = {10.1145/2976022.2976024}, year = {2016}, } Publisher's Version Article Search 

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. @InProceedings{TyDe16p28, author = {Bashar Igried and Anton Setzer}, title = {Programming with Monadic CSPStyle Processes in Dependent Type Theory}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {2838}, doi = {10.1145/2976022.2976032}, year = {2016}, } Publisher's Version Article Search Info 

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. @InProceedings{TyDe16p58, author = {Jennifer Paykin and Antal SpectorZabusky and Kenneth Foner}, title = {choose Your Own Derivative (Extended Abstract)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {5859}, doi = {10.1145/2976022.2976024}, year = {2016}, } Publisher's Version Article Search 

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. @InProceedings{TyDe16p28, author = {Bashar Igried and Anton Setzer}, title = {Programming with Monadic CSPStyle Processes in Dependent Type Theory}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {2838}, doi = {10.1145/2976022.2976032}, year = {2016}, } Publisher's Version Article Search Info 

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. @InProceedings{TyDe16p58, author = {Jennifer Paykin and Antal SpectorZabusky and Kenneth Foner}, title = {choose Your Own Derivative (Extended Abstract)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {5859}, doi = {10.1145/2976022.2976024}, year = {2016}, } Publisher's Version Article Search 

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. @InProceedings{TyDe16p62, author = {Marco Vassena}, title = {Generic Diff3 for Algebraic Datatypes}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {6271}, doi = {10.1145/2976022.2976026}, year = {2016}, } Publisher's Version Article Search 

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: 2.45