一句话：利用幺半群的经典表示，使 vector reverse 等依赖类型函数无需额外等式证明即可通过类型检查。
向量（长度索引列表）是依赖类型的经典例子，但多数教程会避开那些定义时需要自然数之间非平凡等式才能通过类型检查的函数。本文展示如何编写 vector reverse 这类依赖幺半群等式的函数，而无需编写额外证明。核心方法基于幺半群的一种众所周知表示，用它组织带累积参数的函数定义，使所需的结合律、单位元等性质在类型检查时自动成立。该技术可推广到许多以幺半群索引类型上的累积参数函数，甚至可“免费”判定任意幺半群等式。文章以 vector reverse 为例说明这一编程模式。
Abstract Vectors—or length-indexed lists—are classic example of a dependent type. Yet, most tutorials stay clear of any function on vectors whose definition requires non-trivial equalities between natural numbers to type check. This pearl shows how to write functions, such as vector reverse, that rely on monoidal equalities to be type correct without having to write any additional proofs. These techniques can be applied to many other functions over types indexed by a monoid, written using an accumulating parameter, and even be used to decide arbitrary equalities over monoids ‘for free.’
@article{paperbot1622,
title = {A well-known representation of monoids and its application to the function ‘vector reverse’},
author = {WOUTER SWIERSTRA},
journal = {Journal of Functional Programming},
volume = {32},
year = {2022},
doi = {10.1017/s0956796822000065}
}