TyDe '19: "Generic Level Polymorphic ..."
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
Info
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)
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
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)
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
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)
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
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 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
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)
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
TyDe '19: "Deferring the Details and ..."
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
Info
TyDe '19: "Constraint-Based Type-Directed ..."
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
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)
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