Constrained type families
Constrained type families
复制标题
约束类型族
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
R. Eisenberg
中科院分区：
文献类型：
--
作者：
J. Garrett Morris;R. Eisenberg
我们提出了一种方法来支持在类型级计算，而不影响表现力或类型安全。现有的类型级计算框架要么需要整体性，要么隐含地假设它。例如，Haskell中的类型家族提供了一种强大的模块化方法来定义类型级计算。然而，它们目前的设计隐含地假设类型族是总体的，引入了无意义的类型，并使类型族及其扩展的元理论显着复杂化。我们提出了一种替代设计，使用限定类型来配对类型级计算与谓词，捕捉他们的域。我们的方法自然地捕捉到了类型族的直观性，简化了它们的元理论。作为证据，我们提出了第一个完整的证明的一致性的语言与封闭类型的家庭。
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.