Higher-order type-level programming in Haskell
File(s)cameraready.pdf (765.78 KB)
Published version
Author(s)
Kiss, Csongor
Field, Anthony
Eisenbach, Susa
Peyton Jones, Simon
Type
Conference Paper
Abstract
Type family applications in Haskell must be fully saturated. This means that all type-level functions haveto be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension toGHC that removes this restriction. We augment Haskell’s existing type arrow,→, with anunmatchablearrow,↠, that supports partial application of type families without compromising soundness. A soundness proof isprovided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) inthe type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.
Date Issued
2019-08-01
Date Acceptance
2019-06-14
Citation
Proceedings of the ACM on Programming Languages, 2019, 3, pp.1-17
ISSN
2475-1421
Publisher
ACM
Start Page
1
End Page
17
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
3
Copyright Statement
© 2019 Association for Computing Machinery.
Source
International Conference on Functional Programming
Publication Status
Published
Start Date
2019-08-18
Finish Date
2019-08-23
Coverage Spatial
Berlin, Germany
Date Publish Online
2019-07-26