Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Tue 20 Aug 2019 16:06 - 16:30 at Aurora Borealis - Dependent Types in Haskell Chair(s): Joachim Breitner

Type family applications in Haskell must be fully saturated. This means that all type-level functions have to be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension to GHC that removes this restriction. We augment Haskell’s existing type arrow, ->, with an unmatchable arrow, ~>, that supports partial application of type families without compromising soundness. A soundness proof is provided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) in the type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.

Tue 20 Aug

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

15:20 - 16:30
Dependent Types in HaskellResearch Papers at Aurora Borealis
Chair(s): Joachim Breitner DFINITY Foundation
15:20
23m
Talk
Dependently Typed Haskell in Industry (Experience Report)
Research Papers
David Thrane Christiansen Galois, USA, Iavor Diatchki Galois, Inc., Robert Dockins Galois, Inc., Joe Hendrix Galois, Inc., Tristan Ravitch Galois, Inc.
15:43
23m
Talk
A Role for Dependent Types in Haskell
Research Papers
Stephanie Weirich University of Pennsylvania, USA, Pritam Choudhury University of Pennsylvania, Antoine Voizard University of Pennsylvannia, Richard A. Eisenberg Bryn Mawr College, USA
16:06
23m
Talk
Higher-order Type-level Programming in Haskell
Research Papers
Csongor Kiss Imperial College London, Tony Field Imperial College London, Susan Eisenbach Imperial College London, Simon Peyton Jones Microsoft, UK