Powered by
4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2019),
August 18, 2019,
Berlin, Germany
4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2019)
Frontmatter
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.
@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 = {1--13},
doi = {10.1145/3331554.3342603},
year = {2019},
}
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.
@InProceedings{TyDe19p14,
author = {Guillaume Allais},
title = {Generic Level Polymorphic N-ary Functions},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--26},
doi = {10.1145/3331554.3342604},
year = {2019},
}
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.
@InProceedings{TyDe19p27,
author = {Liam O'Connor},
title = {Deferring the Details and Deriving Programs},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {27--39},
doi = {10.1145/3331554.3342605},
year = {2019},
}
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.
@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 = {40--51},
doi = {10.1145/3331554.3342606},
year = {2019},
}
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.
@InProceedings{TyDe19p52,
author = {Stefan Monnier},
title = {Inductive Types Deconstructed: The Calculus of United Constructions},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {52--63},
doi = {10.1145/3331554.3342607},
year = {2019},
}
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.
@InProceedings{TyDe19p64,
author = {Peter-Michael Osera},
title = {Constraint-Based Type-Directed Program Synthesis},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {64--76},
doi = {10.1145/3331554.3342608},
year = {2019},
}
Publisher's Version
Article Search
proc time: 2.42