一句话：用限定类型为类型族计算标注定义域，在保持表达力与类型安全的同时支持偏性，并给出闭类型族语言的一致性证明。
现有类型级计算框架通常要求或默认计算是全函数，例如 Haskell 类型族虽模块化且表达力强，却隐含假设其为全函数，从而引入无意义类型，并使类型族及其扩展的元理论复杂化。本文提出一种支持偏性的类型级计算设计：用限定类型（qualified types）将类型级计算与其定义域谓词配对，显式刻画类型族在哪些参数上有定义。该方法自然对应类型族的偏函数直觉，在不牺牲表达力与类型安全的前提下简化元理论。作为证据，作者给出首个含闭类型族的语言的完整一致性证明。
We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.