Workshop TyDe 2019 – Author Index 
Contents 
Abstracts 
Authors

Allais, Guillaume 
TyDe '19: "Generic Level Polymorphic ..."
Generic Level Polymorphic Nary Functions
Guillaume Allais (University of Strathclyde, UK) Agda's standard library struggles in various places with nary functions and relations. It introduces congruence and substitution operators for functions of arities one and two, and provides users with convenient combinators for manipulating indexed families of arity exactly one. After a careful analysis of the kinds of problems the unifier can easily solve, we design a unifierfriendly representation of nary functions. This allows us to write generic programs acting on nary functions which automatically reconstruct the representation of their inputs' types by unification. In particular, we can define fully level polymorphic nary versions of congruence, substitution and the combinators for indexed families, all requiring minimal user input. @InProceedings{TyDe19p14, author = {Guillaume Allais}, title = {Generic Level Polymorphic Nary Functions}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {1426}, doi = {10.1145/3331554.3342604}, year = {2019}, } Publisher's Version Article Search Info 

Devriese, Dominique 
TyDe '19: "How to do Proofs: Practically ..."
How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)
Koen Jacobs, Andreas Nuyts, and Dominique Devriese (KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium) Dependentlytyped languages are great for stating and proving properties of pure functions. We can reason about them modularly (state and prove their properties independently of other functions) and nonintrusively (without modifying their implementation). But what if we are interested in properties about the results of effectful computations? Ideally, we could keep on stating and proving them just as nicely. This pearl shows we can. We formalise a way to lift a property about values to a property about effectful computations producing such values, and we demonstrate that we need not make any sacrifices when reasoning about them. In addition to this modular and nonintrusive reasoning, our approach offers independence of the underlying monad and allows for readable proofs whose structure follows that of the code. @InProceedings{TyDe19p1, author = {Koen Jacobs and Andreas Nuyts and Dominique Devriese}, title = {How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {113}, doi = {10.1145/3331554.3342603}, year = {2019}, } Publisher's Version Article Search 

Innes, Sean 
TyDe '19: "Tic Tac Types: A Gentle Introduction ..."
Tic Tac Types: A Gentle Introduction to Dependently Typed Programming (Functional Pearl)
Sean Innes and Nicolas Wu (University of Bristol, UK; Imperial College London, UK) TicTacToe is a simple, familiar, classic game enjoyed by many. This pearl is designed to give a flavour of the world of dependent types to the uninitiated functional programmer. We cover a journey from TicTacTerrible implementations in the harsh world of virtually untyped Strings, through the safe haven of vectors that know their own length, and into a TicTacTitanium version that is too strongly typed for its own good. Along the way we discover something we knew all along; types are great, but in moderation. This lesson is quickly put to use in a more complex recursive version. @InProceedings{TyDe19p40, author = {Sean Innes and Nicolas Wu}, title = {Tic Tac Types: A Gentle Introduction to Dependently Typed Programming (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {4051}, doi = {10.1145/3331554.3342606}, year = {2019}, } Publisher's Version Article Search 

Jacobs, Koen 
TyDe '19: "How to do Proofs: Practically ..."
How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)
Koen Jacobs, Andreas Nuyts, and Dominique Devriese (KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium) Dependentlytyped languages are great for stating and proving properties of pure functions. We can reason about them modularly (state and prove their properties independently of other functions) and nonintrusively (without modifying their implementation). But what if we are interested in properties about the results of effectful computations? Ideally, we could keep on stating and proving them just as nicely. This pearl shows we can. We formalise a way to lift a property about values to a property about effectful computations producing such values, and we demonstrate that we need not make any sacrifices when reasoning about them. In addition to this modular and nonintrusive reasoning, our approach offers independence of the underlying monad and allows for readable proofs whose structure follows that of the code. @InProceedings{TyDe19p1, author = {Koen Jacobs and Andreas Nuyts and Dominique Devriese}, title = {How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {113}, doi = {10.1145/3331554.3342603}, year = {2019}, } Publisher's Version Article Search 

Monnier, Stefan 
TyDe '19: "Inductive Types Deconstructed: ..."
Inductive Types Deconstructed: The Calculus of United Constructions
Stefan Monnier (Université de Montréal, Canada) Algebraic data types and inductive types like those of the Calculus of Inductive Constructions (CIC) are the bread and butter of statically typed functional programming languages. They conveniently combine in a single package product types, sum types, recursive types, and indexed types. But this also makes them somewhat heavyweight: for example, tuples have to be defined as "degenerate" single constructor inductive types, and extraction of a single field becomes a laborious full caseanalysis on the object. We consider this to be unsatisfactory. In this article, we develop an alternative presentation of CIC's inductive types where the various elements are provided separately, such that inductive types are built on top of tuples and sums rather than the other way around. The resulting language is lowerlevel yet we show it can be translated to to a predicative version of the Calculus of Inductive Constructions in a typepreserving way. An additional benefit is that it can conveniently give a precise type to the default branch of "case" statements. @InProceedings{TyDe19p52, author = {Stefan Monnier}, title = {Inductive Types Deconstructed: The Calculus of United Constructions}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {5263}, doi = {10.1145/3331554.3342607}, year = {2019}, } Publisher's Version Article Search 

Nuyts, Andreas 
TyDe '19: "How to do Proofs: Practically ..."
How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)
Koen Jacobs, Andreas Nuyts, and Dominique Devriese (KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium) Dependentlytyped languages are great for stating and proving properties of pure functions. We can reason about them modularly (state and prove their properties independently of other functions) and nonintrusively (without modifying their implementation). But what if we are interested in properties about the results of effectful computations? Ideally, we could keep on stating and proving them just as nicely. This pearl shows we can. We formalise a way to lift a property about values to a property about effectful computations producing such values, and we demonstrate that we need not make any sacrifices when reasoning about them. In addition to this modular and nonintrusive reasoning, our approach offers independence of the underlying monad and allows for readable proofs whose structure follows that of the code. @InProceedings{TyDe19p1, author = {Koen Jacobs and Andreas Nuyts and Dominique Devriese}, title = {How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {113}, doi = {10.1145/3331554.3342603}, year = {2019}, } Publisher's Version Article Search 

O'Connor, Liam 
TyDe '19: "Deferring the Details and ..."
Deferring the Details and Deriving Programs
Liam O'Connor (UNSW, Australia) A commonlyused technique in dependentlytyped programming is to encode invariants about a data structure into its type, thus ensuring that the data structure is correct by construction. Unfortunately, this often necessitates the embedding of explicit proof terms within the data structure, which are not part of the structure conceptually, but merely supplied to ensure that the data invariants are maintained. As the complexity of the specifications in the types increases, these additional terms tend to clutter definitions, reducing readability. We introduce a technique where these proof terms can be supplied later, by constructing the data structure within a proof delay applicative functor. We apply this technique to Trip, our new language for Hoarelogic verification of imperative programs embedded in Agda, where our applicative functor is used as the basis for a verification condition generator, turning the typed holes of Agda into a method for stepwise derivation of a program from its specification in the form of a Hoare triple. @InProceedings{TyDe19p27, author = {Liam O'Connor}, title = {Deferring the Details and Deriving Programs}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {2739}, doi = {10.1145/3331554.3342605}, year = {2019}, } Publisher's Version Article Search Info 

Osera, PeterMichael 
TyDe '19: "ConstraintBased TypeDirected ..."
ConstraintBased TypeDirected Program Synthesis
PeterMichael Osera (Grinnell College, USA) We explore an approach to typedirected program synthesis rooted in constraintbased type inference techniques. By doing this, we aim to more efficiently synthesize polymorphic code while also tackling advanced typing features such as GADTs that build upon polymorphism. Along the way, we also present an implementation of these techniques in Scythe, a prototype live, typedirected programming tool for the Haskell programming language and reflect on our initial experience with the tool. @InProceedings{TyDe19p64, author = {PeterMichael Osera}, title = {ConstraintBased TypeDirected Program Synthesis}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {6476}, doi = {10.1145/3331554.3342608}, year = {2019}, } Publisher's Version Article Search 

Wu, Nicolas 
TyDe '19: "Tic Tac Types: A Gentle Introduction ..."
Tic Tac Types: A Gentle Introduction to Dependently Typed Programming (Functional Pearl)
Sean Innes and Nicolas Wu (University of Bristol, UK; Imperial College London, UK) TicTacToe is a simple, familiar, classic game enjoyed by many. This pearl is designed to give a flavour of the world of dependent types to the uninitiated functional programmer. We cover a journey from TicTacTerrible implementations in the harsh world of virtually untyped Strings, through the safe haven of vectors that know their own length, and into a TicTacTitanium version that is too strongly typed for its own good. Along the way we discover something we knew all along; types are great, but in moderation. This lesson is quickly put to use in a more complex recursive version. @InProceedings{TyDe19p40, author = {Sean Innes and Nicolas Wu}, title = {Tic Tac Types: A Gentle Introduction to Dependently Typed Programming (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {4051}, doi = {10.1145/3331554.3342606}, year = {2019}, } Publisher's Version Article Search 
9 authors
proc time: 0.55