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

GADTs were introduced in Haskell’s eco-system more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, functions with qualified types cannot perform induction over some GADTs, significantly undermining their use.

In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell’s type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical bi-implications, in contrast to their traditional unidirectional interpretation.

We present a fully-fledged design of bidirectional instances, covering the specification of typing and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proof-of-concept implementation of our algorithm, and revisit the meta-theory of type classes in the presence of our extension.

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 Calderon Galois, Inc.
10:30
30m
Research paper
Bidirectional Type Class Instances
Haskell
Koen Pauwels KU Leuven, Georgios Karachalias KU Leuven, Belgium, Michiel Derhaeg Guardsquare, Tom Schrijvers KU Leuven
11:00
30m
Research paper
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances
Haskell
Ryan Scott Indiana University at Bloomington, USA, Ryan R. Newton Indiana University
Pre-print File Attached
11:30
30m
Research paper
Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study
Haskell
Dominique Devriese Vrije Universiteit Brussel
File Attached