一句话：首次为基于 elaboration 的类型类解析在超类与灵活上下文等非确定性下建立连贯性的形式证明。
Haskell、Mercury、PureScript 等语言采用基于 elaboration 的类型类解析，它本质上是非确定性的：同一 wanted constraint 可由多个全局实例与局部约束共同满足。连贯性（coherence）是保证程序行为可预测的关键性质，但此前尚未在 superclasses、flexible contexts 等非确定性来源存在时得到形式证明。本文填补这一空白。受 full abstraction 启发，作者提出两步策略：先将源语言非确定地 elaboration 到一个保持 contextual equivalence 的中间语言，再从该中间语言确定地 elaboration 到目标语言。利用 logical relations，论文证明了第一步的 contextual equivalence，从而建立连贯性；第二步的确定性则直接保持该性质。
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.
@article{paperbot584,
title = {Coherence of type class resolution},
author = {Gert-Jan Bottu and Ningning Xie and Koar Marntirosian and Tom Schrijvers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341695}
}