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 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
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 23mTalk | 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 23mTalk | 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 23mTalk | 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 |