Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 11:00 - 11:30 at Aurora Borealis - Paper Session 1: Classes & Instances Chair(s): Jose Calderon

Dependently typed languages allow programmers to state and prove type class laws by simply encoding the laws as class methods. But writing implementations of these methods can frequently give way to large amounts of routine, boilerplate code, and depending on the law involved, the size of these proofs can grow superlinearly with the size of the data types involved.

We present a technique for automating away large swaths of this boilerplate by leveraging datatype-generic programming. We observe that any algebraic data type has an equivalent representation type that is composed of simpler, smaller types that are simpler to prove theorems over. By constructing an isomorphism between a data type and its representation type, we can derive proofs for the original data type by reusing the corresponding proof over the representation type. Our work is designed to be general-purpose and does not require advanced automation techniques such as tactic systems. As evidence for this claim, we implement these ideas in a Haskell library that defines generic, canonical implementations of the methods and proof obligations for classes in the standard base library.

Conference Day
Thu 22 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Paper Session 1: Classes & InstancesHaskell at Aurora Borealis
Chair(s): Jose CalderonGalois, Inc.
Research paper
Bidirectional Type Class Instances
Koen PauwelsKU Leuven, Georgios KarachaliasKU Leuven, Belgium, Michiel DerhaegGuardsquare, Tom SchrijversKU Leuven
Research paper
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances
Ryan ScottIndiana University at Bloomington, USA, Ryan R. NewtonIndiana University
Pre-print File Attached
Research paper
Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the ╬╝VeriFast verifier as a case study
Dominique DevrieseVrije Universiteit Brussel
File Attached