Imperial College London
Alternate

Emeritus ProfessorSusanEisenbach

Faculty of Engineering, Department of Computing

Emeritus Professor of Computing
 
 
 
//

Contact

 

s.eisenbach Website

 
 
//

Location

 

Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Kiss:2019:10.1145/3341706,
author = {Kiss, C and Field, A and Eisenbach, S and Peyton, Jones S},
doi = {10.1145/3341706},
pages = {1--17},
publisher = {ACM},
title = {Higher-order type-level programming in Haskell},
url = {http://dx.doi.org/10.1145/3341706},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Kiss,C
AU  - Field,A
AU  - Eisenbach,S
AU  - Peyton,Jones S
DO  - 10.1145/3341706
EP  - 17
PB  - ACM
PY  - 2019///
SN  - 2475-1421
SP  - 1
TI  - Higher-order type-level programming in Haskell
UR  - http://dx.doi.org/10.1145/3341706
UR  - http://hdl.handle.net/10044/1/72117
ER  -
Download