类型类分解的一致性
Coherence of Type Class Resolution
摘要：
在Haskell、Mercury和PureScript等语言中，基于细化的类型类解析通常是不确定的：可以有多种方法来满足全局实例和局部给定约束方面的所需约束。一致性是保持这种理智的关键属性;它保证了尽管存在非确定性，程序仍然可以预测地运行。尽管基于精细化的解析通常被认为是连贯的，但据我们所知，在存在非决定论的来源（如超类和灵活上下文）的情况下，还没有正式的证据证明这一属性。本文提供了一个形式化的证明来纠正这种情况。证明是不平凡的，因为语义阐述到目标语言的解析，其中不同的阐述可以通过没有源语言对应物的上下文来区分。受完全抽象概念的启发，我们提出了一个两步策略，首先非确定性地阐述到一个中间语言，保持上下文等价，然后确定性地阐述到目标语言。我们使用基于逻辑关系的方法来建立上下文对等，从而为第一步的阐述的连贯性，而第二步的决定论直截了当地保留这种连贯性属性。
英文摘要：
Elaboration-based type class resolution, as found in languages like Haskell, Mercury and PureScript, is generally nondeterministic: there can be multiple ways to satisfy a wanted constraint in terms of global instances and locally given constraints. Coherence is the key property that keeps this sane; it guarantees that, despite the nondeterminism, programs still behave predictably. Even though elaboration-based resolution is generally assumed coherent, as far as we know, there is no formal proof of this property in the presence of sources of nondeterminism, like superclasses and flexible contexts. This paper provides a formal proof to remedy the situation. The proof is non-trivial because the semantics elaborates resolution into a target language where different elaborations can be distinguished by contexts that do not have a source language counterpart. Inspired by the notion of full abstraction, we present a two-step strategy that first elaborates nondeterministically into an intermediate language that preserves contextual equivalence, and then deterministically elaborates from there into the target language. We use an approach based on logical relations to establish contextual equivalence and thus coherence for the first step of elaboration, while the second step's determinism straightforwardly preserves this coherence property.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
