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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:20 - 16:30
Dependent Types in HaskellResearch Papers at Aurora Borealis
Chair(s): Joachim BreitnerDFINITY Foundation
15:20
23m
Talk
Dependently Typed Haskell in Industry (Experience Report)
Research Papers
David Thrane ChristiansenGalois, USA, Iavor DiatchkiGalois, Inc., Robert DockinsGalois, Inc., Joe HendrixGalois, Inc., Tristan RavitchGalois, Inc.
15:43
23m
Talk
A Role for Dependent Types in Haskell
Research Papers
Stephanie WeirichUniversity of Pennsylvania, USA, Pritam ChoudhuryUniversity of Pennsylvania, Antoine VoizardUniversity of Pennsylvannia, Richard A. EisenbergBryn Mawr College, USA
16:06
23m
Talk
Higher-order Type-level Programming in Haskell
Research Papers
Csongor KissImperial College London, Tony FieldImperial College London, Susan EisenbachImperial College London, Simon Peyton JonesMicrosoft, UK