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
15:20 - 16:30
|Dependently Typed Haskell in Industry (Experience Report)|
|A Role for Dependent Types in Haskell|
|Higher-order Type-level Programming in Haskell|