一句话：将角色机制融入依赖类型系统并在 Coq 中证明其可靠性，为 GHC 引入依赖类型奠定基础。
现代 Haskell 支持零成本强制转换（coercion），允许运行时表示相同的类型之间自由转换，这一特性依靠角色（role）机制来禁止不安全的转换。然而，如何将角色机制融入依赖类型系统尚不明确。本文展示了如何把角色引入依赖类型系统，并使用 Coq 证明助手对所得系统的可靠性（soundness）进行了机器化验证。该工作被设计为在 Glasgow Haskell Compiler（GHC）中添加依赖类型的基础，同时也可供其他希望采纳 Haskell 安全强制转换特性的依赖类型语言设计者参考。关键结果是给出了一个经过形式化验证的、支持角色的依赖类型系统。
Modern Haskell supports zero-cost coercions, a mechanism where types that share the same run-time representation may be freely converted between. To make sure such conversions are safe and desirable, this feature relies on a mechanism of roles to prohibit invalid coercions. In this work, we show how to incorporate roles into dependent types systems and prove, using the Coq proof assistant, that the resulting system is sound. We have designed this work as a foundation for the addition of dependent types to the Glasgow Haskell Compiler, but we also expect that it will be of use to designers of other dependently-typed languages who might want to adopt Haskell’s safe coercions feature.
@article{paperbot593,
title = {A role for dependent types in Haskell},
author = {Stephanie Weirich and Pritam Choudhury and Antoine Voizard and Richard A. Eisenberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341705}
}