Coherence of Type Class Resolution
Gert-Jan Bottu, Ningning Xie, Koar Marntirosian, Tom Schrijvers

TL;DR
This paper provides a formal proof that elaboration-based type class resolution in languages like Haskell and PureScript is coherent, even with nondeterministic sources like superclasses, ensuring predictable program behavior.
Contribution
It introduces a formal proof of coherence for elaboration-based type class resolution in the presence of nondeterminism, using a two-step elaboration strategy and logical relations.
Findings
Proof of coherence for elaboration-based resolution
Two-step elaboration preserves contextual equivalence
Deterministic elaboration maintains coherence
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
