Haskell的一致性显式字典应用：形式化和一致性证明
Coherent Explicit Dictionary Application for Haskell: Formalisation and Coherence Proof
摘要：
类型类是Haskell最受欢迎的特性之一，并通过ad-hoc多态性扩展了其类型系统。由于他们的概念，有一些有用的功能，不能提供，因为希望提供两个正确的属性：一致性和全局唯一性的实例。一致性本质上保证了程序语义独立于类型检查器内部。库依赖于实例的全局唯一性来强制执行，例如，单个顺序关系用于有序二叉树的所有操作。无法提供的功能包括显式字典应用程序和本地实例，这在实践中非常有用。我们提出了一个新的设计，提供明确的字典应用程序，而不损害一致性和全球唯一性。我们引入了一个新的标准的基础上GHC的类型参数的角色，以决定当一个字典应用程序是安全的全局唯一性的实例。我们通过检测潜在的不一致性来源来保持一致性，并正式证明它。此外，我们的解决方案可以使用本地字典。除了正式开发我们的想法外，我们还在GHC中实现了一个工作原型。本报告包含完整的形式化和一致性证明。
英文摘要：
Type classes are one of Haskell's most popular features and extend its type system with ad-hoc polymorphism. Since their conception, there were useful features that could not be offered because of the desire to offer two correctness properties: coherence and global uniqueness of instances. Coherence essentially guarantees that program semantics are independent from type-checker internals. Global uniqueness of instances is relied upon by libraries for enforcing, for example, that a single order relation is used for all manipulations of an ordered binary tree. The features that could not be offered include explicit dictionary application and local instances, which would be highly useful in practice. We propose a new design for offering explicit dictionary application, without compromising coherence and global uniqueness. We introduce a novel criterion based on GHC's type argument roles to decide when a dictionary application is safe with respect to global uniqueness of instances. We preserve coherence by detecting potential sources of incoherence, and prove it formally. Moreover, our solution makes it possible to use local dictionaries. In addition to developing our ideas formally, we have implemented a working prototype in GHC. This report contains the full formalisation and coherence proof.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
