ICFP Workshops 2019
24th ACM SIGPLAN International Conference on Functional Programming (ICFP 2019)
Powered by
Conference Publishing Consulting

4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2019), August 18, 2019, Berlin, Germany

TyDe 2019 – Proceedings

Contents - Abstracts - Authors

4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2019)

Frontmatter

Title Page


Welcome from the Chairs
Welcome to the 4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe'19), held in Berlin, Germany on Sunday, August 18th, 2019, and co-located with the International Conference on Functional Programming (ICFP 2019). The workshop aims to show how static type information may be used effectively in the development of computer programs.

Papers

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)
Dependently-typed 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 non-intrusively (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 non-intrusive reasoning, our approach offers independence of the underlying monad and allows for readable proofs whose structure follows that of the code.

Publisher's Version Article Search
Generic Level Polymorphic N-ary Functions
Guillaume Allais
(University of Strathclyde, UK)
Agda's standard library struggles in various places with n-ary 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 unifier-friendly representation of n-ary functions. This allows us to write generic programs acting on n-ary functions which automatically reconstruct the representation of their inputs' types by unification. In particular, we can define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families, all requiring minimal user input.

Publisher's Version Article Search Info
Deferring the Details and Deriving Programs
Liam O'Connor
(UNSW, Australia)
A commonly-used technique in dependently-typed 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 Hoare-logic 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.

Publisher's Version Article Search Info
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)
Tic-Tac-Toe 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 Tic-Tac-Terrible implementations in the harsh world of virtually untyped |Strings|, through the safe haven of vectors that know their own length, and into a Tic-Tac-Titanium 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.

Publisher's Version Article Search
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 case-analysis 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 lower-level yet we show it can be translated to to a predicative version of the Calculus of Inductive Constructions in a type-preserving way. An additional benefit is that it can conveniently give a precise type to the default branch of "case" statements.

Publisher's Version Article Search
Constraint-Based Type-Directed Program Synthesis
Peter-Michael Osera
(Grinnell College, USA)
We explore an approach to type-directed program synthesis rooted in constraint-based 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, type-directed programming tool for the Haskell programming language and reflect on our initial experience with the tool.

Publisher's Version Article Search

proc time: 2.42