一句话：为 GHC 引入不可匹配箭头，支持类型族部分应用，并证明其可靠性。
Haskell 中类型族的应用必须完全饱和，因此类型级函数只能是一阶的，导致代码冗长且难读。本文为 GHC 增加一种扩展：在现有类型箭头之外引入不可匹配箭头，以支持类型族的部分应用，同时保持类型系统的可靠性，并给出可靠性证明。作者在常用类型级库上评估该技术，发现类型级逻辑的代码量可减少约 80%，同时提升代码质量与可读性。
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.
@article{paperbot606,
title = {Higher-order type-level programming in Haskell},
author = {Csongor Kiss and Tony Field and Susan Eisenbach and Simon Peyton Jones},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341706}
}