一句话：提出 choice polymorphism，使函数可复用于不同商类型，避免代码重复并接受更多合法定义。
商类型让类型包含等式性质，从而增强类型系统表达力，但现有实现存在两个问题：同一函数常需对每个商重复定义，且包含不尊重商的子项但整体合法的函数会被拒绝。本文提出一种商多态（quotient polymorphism），称为 choice polymorphism，允许函数跨商类型复用并提升表达力。作者给出实用示例，发展其底层理论，并在 Quotient Haskell 中实现。该工作缓解代码重复与过度拒绝问题，为商类型编程提供更灵活的多态机制。
Quotient types increase the power of type systems by allowing types to include equational properties. However, two key practical issues arise: code being duplicated, and valid code being rejected. Specifically, function definitions often need to be repeated for each quotient of a type, and valid functions may be rejected if they include subterms that do not respect the quotient. This article addresses these reusability and expressivity issues by introducing a notion of quotient polymorphism that we call choice polymorphism . We give practical examples of its use, develop the underlying theory, and implement it in Quotient Haskell.