一句话：提出一种从代数视角高层次构造双射之差的方法，避免逐点推理和分别构造正反方向，且不牺牲性能。
双射的“加法”是直接练习：在左和右两个和类型分支上分别运行两个双射，即可得到两个和类型之间的双射。但如何从一个双射中“减去”另一个却远不直观。组合数学中已有若干构造两个双射之“差”的计算原理。本文从计算与代数视角重新审视该问题，展示如何在高层次上构造此类双射，避免逐点推理，也无需被迫分别构造正向与反向映射，同时不牺牲性能。文章以 functional pearl 的形式呈现，强调代数结构在函数式编程中的表达力与实用性。
It is a straightforward exercise to write a program to "add" two bijections---resulting in a bijection between two sum types, which runs the first bijection on elements from the left summand and the second bijection on the right. It is much less obvious how to "subtract" one bijection from another. This problem has been studied in the context of combinatorics, with several computational principles known for producing the "difference" of two bijections. We consider the problem from a computational and algebraic perspective, showing how to construct such bijections at a high level, avoiding pointwise reasoning or being forced to construct the forward and backward directions separately---without sacrificing performance.
@article{paperbot284,
title = {What’s the difference? a functional pearl on subtracting bijections},
author = {Brent A. Yorgey and Kenneth Foner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236796}
}