一句话：提出证明义务可由 SMT 判定的商类型，并实现为 Liquid Haskell 扩展 Quotient Haskell。
子类型与商类型是对偶的类型抽象，但子类型已被广泛显式或隐式使用，商类型除证明助手外鲜有实际应用。其推广困难的关键在于使用商类型会产生大量证明义务。本文引入一类商类型，使其证明义务可由 SMT 求解器判定，从而显著降低使用负担。作者以 Liquid Haskell 扩展的形式实现 Quotient Haskell，支持商类型，并通过该实现表明这一轻量级方案在实践中可行。
Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell , an extension of Liquid Haskell with support for quotient types.