pith. sign in

arxiv: 1907.00844 · v2 · pith:PSPGPIKOnew · submitted 2019-07-01 · 💻 cs.PL

Coherence of Type Class Resolution

Gert-Jan Bottu , Ningning Xie , Koar Marntirosian , Tom Schrijvers This is my paper

Pith reviewed 2026-05-25 11:25 UTC · model grok-4.3

classification 💻 cs.PL
keywords type class resolutioncoherenceelaborationcontextual equivalencelogical relationsnondeterminismsuperclassesHaskell
0
0 comments X

The pith

Elaboration-based type class resolution remains coherent despite nondeterminism from superclasses and flexible contexts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that type class resolution in languages like Haskell stays coherent even when multiple resolutions are possible for a constraint. Coherence means that programs produce the same observable behavior no matter which valid resolution path is chosen during elaboration. The challenge is that the target language after elaboration can distinguish different resolutions using contexts that have no counterpart in the source language. To handle this, the proof splits elaboration into two steps: a nondeterministic step into an intermediate language that preserves contextual equivalence, followed by a deterministic step into the target. Logical relations establish the equivalence for the first step, and determinism takes care of the second.

Core claim

The central claim is that elaboration-based type class resolution is coherent in the presence of nondeterminism such as superclasses and flexible contexts. The proof proceeds by nondeterministically elaborating source programs into an intermediate language that preserves contextual equivalence, shown via logical relations, and then deterministically elaborating the intermediate language into the target language, which preserves the equivalence property by construction.

What carries the argument

Two-step elaboration: nondeterministic step into an intermediate language that preserves contextual equivalence (via logical relations), followed by deterministic step into the target language.

If this is right

  • Different resolution choices during compilation never change the observable behavior of the resulting program.
  • Superclasses and flexible contexts can be added without breaking the guarantee that all valid resolutions are equivalent.
  • Compilers are free to pick any resolution strategy as long as it produces a valid elaboration.
  • The same coherence property holds for languages that use similar elaboration-based resolution such as Mercury and PureScript.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The two-step method could be reused to prove coherence in other elaboration systems that lose direct source-target correspondence.
  • It suggests a general pattern for proving properties when direct full abstraction fails but an intermediate language can restore it.
  • The approach may extend to features like overlapping instances if they can be modeled in the intermediate language.

Load-bearing premise

The assumption that contextual equivalence between different elaborations in the intermediate language corresponds exactly to equivalence observable from the source language.

What would settle it

A source-language program and context where two different valid resolutions produce target programs that can be distinguished by an observation possible in the source language.

Figures

Figures reproduced from arXiv: 1907.00844 by Gert-Jan Bottu, Koar Marntirosian, Ningning Xie, Tom Schrijvers.

Figure 1
Figure 1. Figure 1: The different calculi with elaborations The coherence proof consists of two main parts: Coherent Elaboration from λTC to F D. Our elaboration from λTC into F D is nondeterministic, but type preserving. Furthermore, we show that any two F D elaborations of the same λTC term are logically related, and prove that this logical relation implies contextual equivalence. This establishes that the elaboration from … view at source ↗
Figure 2
Figure 2. Figure 2: λTC syntax 3 SOURCE LANGUAGE λTC This section presents our source language λTC, a basic calculus which isolates nondeterministic resolution. The calculus only supports features that are essential for type class resolution and its coherence. Consequently, the language is strongly normalizing, and thus does not support recursive let expressions, mutual recursion or recursive methods. This is a sensible choic… view at source ↗
Figure 3
Figure 3. Figure 3: 1 shows selected typing rules. The full set of rules can be found in Section B.2 of the appendix. We ignore the red (elaboration-related) parts for now and explain them in detail in Section 4.1. The judgments P; ΓC; Γ ⊢tm e ⇒ τ and P; ΓC; Γ ⊢tm e ⇐ τ denote inferring a monotype τ for expression e and checking e to have a monotype τ respectively, in environments P, ΓC and Γ. Note that the constraint and typ… view at source ↗
Figure 4
Figure 4. Figure 4: Closure and unambiguity relations P; ΓC; Γ ⊨ Q⇝ e (Constraint Entailment) (δ : Q) ∈ Γ ⊢ct x P; ΓC; Γ ⇝ Γ P; ΓC; Γ ⊨ Q⇝ δ sEntailT-local P = P1, (D : ∀aj .Q ′ i ⇒ Q ′ ).m 7→ Γ ′ : e, P2 Γ ′ = •, aj , δi : Q ′ i ,bk, δ h : Qh Q = [τ j/aj]Q ′ P1; ΓC; Γ ′ ⊢tm e ⇒ τ⇝ e ⊢ct x P; ΓC; Γ ⇝ Γ (ΓC; Γ ⊢ty τ j ⇝ σj , ∀j) (ΓC; •, aj ⊢Q Q ′ i ⇝ σ ′ i , ∀i) (ΓC; •, aj ,bk ⊢Q Qh ⇝ σ ′′ h , ∀h) (P; ΓC; Γ ⊨ [τ j/aj]Q ′ i⇝ ei… view at source ↗
Figure 5
Figure 5. Figure 5: λTC constraint entailment P; ΓC ⊢inst inst : P ′ (Instance Decl Typing) (m : Q ′ i ⇒ TC a : ∀aj .Q ′ h ⇒ τ 1) ∈ ΓC bk = fv(τ ) ΓC; •,bk ⊢ty τ ⇝ σ closure(ΓC;Qp ) = Qq unambig(∀bk .Qq ⇒ TC τ ) (ΓC; •,bk ⊢Q Qq ⇝ σq , ∀q) D fresh δ q fresh δ ′ h fresh (P; ΓC; •,bk, δ q : Qq ⊨ [τ /a]Q ′ i⇝ ei , ∀i) Γ ′ = •,bk, δ q : Qq , aj , δ ′ h : [τ /a]Q ′ h P; ΓC; Γ ′ ⊢tm e ⇐ [τ /a]τ 1⇝ e (D ′ : ∀b ′ m.Q ′ n ⇒ TC τ 2).m ′… view at source ↗
Figure 6
Figure 6. Figure 6: λTC instance declaration typing Through a let binding (rule sTm-infT-let), the programmer provides a type scheme for a variable, thus potentially introducing local constraints. As explained above, the unambiguity check from [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Target language syntax Type Class Resolution. The type class resolution rules can be found in [PITH_FULL_IMAGE:figures/full_fig_p009_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: FD, selected syntax Σ; ΓC; Γ ⊢tm e : σ ⇝ e (FD Term Typing) Σ; ΓC; Γ ⊢d d : TC σ ⇝ e (m : TC a : σ ′ ) ∈ ΓC Σ; ΓC; Γ ⊢tm d.m : [σ/a]σ ′ ⇝ e.m iTm-method Σ; ΓC; Γ ⊢tm e : Q ⇒ σ ⇝ e1 Σ; ΓC; Γ ⊢d d : Q ⇝ e2 Σ; ΓC; Γ ⊢tm e d : σ ⇝ e1 e2 iTm-constrE Σ; ΓC; Γ, δ : Q ⊢tm e : σ ⇝ e ΓC; Γ ⊢Q Q ⇝ σ e ′ = λδ : σ .e Σ; ΓC; Γ ⊢tm λδ : Q.e : Q ⇒ σ ⇝ e ′ iTm-constrI ΓC; Γ ⊢Q Q ⇝ σ (Constr. Well-Formedness) ΓC; Γ ⊢ty σ ⇝ … view at source ↗
Figure 9
Figure 9. Figure 9: FD typing and operational semantics, selected rules ⊢ct x Σ; ΓC; Γ (FD Environment Well-Formedness) unambig(∀aj .Qi ⇒ TC σ) ΓC; • ⊢C ∀aj .Qi ⇒ TC σ (m : TC a : σ ′ ) ∈ ΓC Σ; ΓC; • ⊢tm e : ∀aj .Qi ⇒ [σ/a]σ ′ ⇝ e D < dom(Σ) (D ′ : ∀a ′ m.Q ′ n ⇒ TC σ ′ ).m ′ 7→ e ′ < Σ where[σj/aj]σ = [σ ′ m/a ′ m]σ ′ ⊢ct x Σ; ΓC; Γ ⊢ct x Σ, (D : ∀aj .Qi ⇒ TC σ).m 7→ e; ΓC; Γ iCtx-MEnv [PITH_FULL_IMAGE:figures/full_fig_p012… view at source ↗
Figure 10
Figure 10. Figure 10: FD environment well-formedness, selected rules Typing [PITH_FULL_IMAGE:figures/full_fig_p012_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: FD dictionary typing Non-Overlapping Instances. The main requirement for achieving coherence of type class resolution, is that type class instances do not overlap. This requirement is common in Haskell and is for example enforced in GHC (though strongly discouraged, the OverlappingInstances pragma disables it). By storing all method implementations (with their corresponding instances) in a single environm… view at source ↗
Figure 12
Figure 12. Figure 12: λTC typing with elaboration to FD, selected rules P; ΓC; Γ ⊨ M Q⇝ d (Constraint Entailment) (δ : Q) ∈ Γ ⊢ M ct x P; ΓC; Γ ⇝ Σ; ΓC; Γ P; ΓC; Γ ⊨ M Q⇝ δ sEntail-local P = P1, (D : ∀aj .Qi ⇒ Q ′ ).m 7→ Γ ′ : e, P2 Γ ′ = •, aj , δi : Qi ,bk, δ h : Qh Q = [τ j/aj]Q ′ (ΓC; Γ ⊢ M ty τ j ⇝ σj , ∀j) ⊢M ct x P; ΓC; Γ ⇝ Σ; ΓC; Γ (P; ΓC; Γ ⊨ M [τ j/aj]Qi⇝ di , ∀i) P; ΓC; Γ ⊨ M Q⇝ D σj di sEntail-inst [PITH_FULL_IMAG… view at source ↗
Figure 13
Figure 13. Figure 13: λTC constraint entailment with elaboration to FD Metatheory. We discuss the coherence of the elaboration from λTC to F D in detail in Section 7, and mention here that it is type preserving: Theorem 6 (Typing Preservation - Expressions). If P; ΓC; Γ ⊢ M tm e ⇒ τ⇝ e, and ⊢ M ct x P; ΓC; Γ ⇝ Σ; ΓC; Γ, and ΓC; Γ ⊢ M ty τ ⇝ σ, then Σ; ΓC; Γ ⊢tm e : σ. The same theorem holds for check mode, but is omitted for s… view at source ↗
Figure 14
Figure 14. Figure 14: Dependency graph for Theorems 1, 6 and 7 Proof. This theorem is mutually proven with Theorems 6 and 7. This mutual dependency is illustrated in [PITH_FULL_IMAGE:figures/full_fig_p047_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Dependency graph for Theorems 13, 15 and 16 Proof. By induction on the environment well-formedness relation. This theorem is mutually proven with Theorems 15 and 16 ( [PITH_FULL_IMAGE:figures/full_fig_p075_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Dependency graph for Theorems 25, 27 and 28 Proof. By structural induction on P and mutually proven with Theorems 27 and 28 (see [PITH_FULL_IMAGE:figures/full_fig_p113_16.png] view at source ↗
read the original 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 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper claims to deliver the first formal proof of coherence for elaboration-based type class resolution in the presence of nondeterminism arising from superclasses and flexible contexts. The proof proceeds in two steps: nondeterministic elaboration into an intermediate language (IL) whose contextual equivalence is established via logical relations, followed by deterministic elaboration from the IL into the target language, which preserves the equivalence.

Significance. If the proof is correct, the result is significant: it supplies a machine-checked or at least rigorously formalized argument for a property long assumed in Haskell, Mercury and PureScript but previously lacking a published proof under realistic sources of nondeterminism. The two-step strategy directly tackles the full-abstraction-style problem that target-language contexts can distinguish elaborations invisible at the source level.

minor comments (3)
  1. §3, definition of the IL: the typing rules for dictionary construction are presented only informally; a compact inference-rule figure would make the subsequent logical-relation definition easier to follow.
  2. §4.2, Lemma 4.3 (fundamental lemma): the statement mentions 'closed terms' but the accompanying proof sketch quantifies over open terms with a closing substitution; clarifying the exact statement would remove a minor source of confusion.
  3. Figure 5 (example derivation): the source and target terms are aligned vertically but the intermediate-language term is omitted; adding the IL term would illustrate the two-step path more clearly.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the paper, recognition of its significance, and recommendation for minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's central result is a formal proof of coherence via a two-step elaboration strategy: nondeterministic elaboration into an intermediate language whose contextual equivalence is established using standard logical relations, followed by a deterministic step that preserves the property. This technique is externally motivated by full-abstraction arguments and does not reduce to any self-definition, fitted parameter renamed as prediction, or load-bearing self-citation chain. The derivation is self-contained against the stated semantics and does not invoke uniqueness theorems or ansatzes from prior author work as the sole justification.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof relies on the standard assumption in PL theory that logical relations can establish contextual equivalence.

axioms (1)
  • domain assumption Contextual equivalence is preserved by the first elaboration step
    Central to the two-step strategy described in the abstract.

pith-pipeline@v0.9.0 · 5740 in / 942 out tokens · 40692 ms · 2026-05-25T11:25:59.491737+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages

  1. [1]

    λδ: Q.e is a value

    By iEval-app: e ′ = e ′ 1 e2 iTm-constrI Σ; ΓC ; Γ,δ: Q ⊢tm e :σ ΓC ; Γ ⊢Q Q Σ; ΓC ; Γ ⊢tm λδ: Q.e : Q ⇒σ iTm-constrI with ΓC = •, Γ = •. λδ: Q.e is a value. iTm-constrE Σ; ΓC ; Γ ⊢tm e : Q ⇒σ Σ; ΓC ; Γ ⊢d d : Q Σ; ΓC ; Γ ⊢tm e d :σ iTm-constrE with ΓC = •, Γ = •. From the 1st rule premise: Σ; ΓC ; Γ ⊢tm e : Q ⇒σ (110) By applying the induction hypothesis...

    work page 2019

  2. [2]

    ∈ ϕand for every mappingδ7→ (dv ′ 1, dv ′

    work page

  3. [3]

    Therefore, we obtainγi(ϕi(R(Λa.ei))) = Λa.γi(ϕi(R(ei))), for i ∈ { 1, 2}

    ∈ γ, we have a < fv(e ′ i ) and a < fv(dv ′ i ), where i ∈ { 1, 2}. Therefore, we obtainγi(ϕi(R(Λa.ei))) = Λa.γi(ϕi(R(ei))), for i ∈ { 1, 2}. With these equations, the goal above reduces to (Σ1 : Λa.γ1(ϕ1(R(e1))), Σ2 : Λa.γ2(ϕ2(R(e2)))) ∈ E ⟦∀a.σ⟧ΓC R By applying the definition of the E relation, taking into account that expressions of the form Λa.e are v...

    work page 2019

  4. [4]

    ⇝ M ′ 2 (662) P; ΓC ; Γ′ ⊢M tm e ′ 1 ⇒τ1 →τ2 ⇝ e11 (663) P; ΓC ; Γ′ ⊢M tm e ′ 1 ⇒τ′ 1 →τ2 ⇝ e12 (664) By Lemma 7, we know thatτ′ 1 =τ1. By applying Part 2 of this theorem to Equations 661 and 662, we get: Σ1 : M ′ 1 ≃l oдΣ2 : M ′ 2 : (ΓC ; Γ ⇒σ) 7→ ( ΓC ; Γ′ ⇒σ1) By unfolding the definition of logical equivalence in the above and applying it on Equation 6...

    work page 2019

  5. [5]

    Consequently, since F D context elaboration is deterministic (Theorem 38), we get that M 1 = M ′ 1 and M 2 = M ′

    work page

  6. [6]

    □ M.3 Partial Coherence Theorems Theorem 27 (Coherence - Dictionaries - Part A)

    Goal 745 follows from Equations 746, 748, 750 and 751. □ M.3 Partial Coherence Theorems Theorem 27 (Coherence - Dictionaries - Part A). If P; ΓC ; Γ ⊨M Q ⇝ d 1 and P; ΓC ; Γ ⊨M Q ⇝ d 2 and ⊢M ct x P; ΓC ; Γ ⇝ Σ1; ΓC ; Γ and ⊢M ct x P; ΓC ; Γ ⇝ Σ2; ΓC ; Γ then ΓC ; Γ ⊢ Σ1 : d 1 ≃l oдΣ2 : d 2 : Q where ΓC ; Γ ⊢M Q Q ⇝ Q. Proc. ACM Program. Lang., Vol. 3, No...

    work page 2019

  7. [7]

    ∈ γwhere (Σ1 : dv ′ 1, Σ2 : dv ′

    work page

  8. [8]

    From Theorem 25, we get that ΓC ⊢ Σ1 ≃l oдΣ2

    ∈ V ⟦Q⟧ΓC R (784) We thus know that: γ1(ϕ1(R(δ))) = dv1 γ2(ϕ2(R(δ′))) = dv ′ 2 From the definition of the V relation in Equations 783 and 784 it follows that: Σ1; ΓC ; • ⊢d dv1 : R(Q) (785) Σ2; ΓC ; • ⊢d dv ′ 2 : R(Q) (786) Applying preservation Theorem 7 to our hypothesis that ⊢M ct x P; ΓC ; Γ ⇝ Σ1; ΓC ; Γ and ⊢M ct x P; ΓC ; Γ ⇝ Σ2; ΓC ; Γ gives us ⊢ct...

    work page

  9. [9]

    □ Theorem 28 (Coherence - Expressions - Part A)

    ∈ V ⟦R(Q)⟧ΓC • (787) Goal 782 follows from Equation 787 by Lemma 35. □ Theorem 28 (Coherence - Expressions - Part A). • If P; ΓC ; Γ ⊢M tm e ⇒τ⇝ e1 and P; ΓC ; Γ ⊢M tm e ⇒τ⇝ e2 and ⊢M ct x P; ΓC ; Γ ⇝ Σ1; ΓC ; Γ and ⊢M ct x P; ΓC ; Γ ⇝ Σ2; ΓC ; Γ then ΓC ; Γ ⊢ Σ1 : e1 ≃l oдΣ2 : e2 :σwhere ΓC ; Γ ⊢M ty τ⇝σ. • If P; ΓC ; Γ ⊢M tm e ⇐τ⇝ e1 and P; ΓC ; Γ ⊢M tm...

    work page 2019

  10. [10]

    From Theorem 3, in combination with Equations 854 and 855, we know that: ⊢ct x P; ΓC , ΓC ′ 1; • ⇝ • ⊢ct x P; ΓC , ΓC ′ 2; • ⇝ • The goal follows from the induction hypothesis. pдm = inst ; pдm′ By case analysis on the program typing derivations (sPgmT-inst): P; ΓC ⊢inst inst : P 11 (856) P; ΓC ⊢inst inst : P 21 (857) P, P 11; ΓC ⊢pдm pдm′ :τ; P 12; ΓC 1 ...

    work page 2019

  11. [11]

    We do this by showing that e0 − →∗ e ′ 0

    We need to show that there exists aneh such that e0 − →∗ eh and e ′ 0 − →∗ eh. We do this by showing that e0 − →∗ e ′ 0. By inversion, the last part of Derivation 1007 must be an instance of iTm-arrI directly followed by iTm-arrE, as shown below. Σ; ΓC ; •, x :σ⊢tm e1 :σ′ ⇝ e1 ΓC ; • ⊢ty σ⇝σ Σ; ΓC ; • ⊢tm λx :σ.e1 :σ→σ′ ⇝λx :σ.e1 iTm-arrI Σ; ΓC ; • ⊢tm e2...

    work page 2019

  12. [12]

    We do this by showing that e0 − →∗ e ′ 0

    We need to show that there exists aneh such that e0 − →∗ eh and e ′ 0 − →∗ eh. We do this by showing that e0 − →∗ e ′ 0. By inversion, the last part of Derivation 1011 must be an instance of iTm-forallI directly followed by iTm-forallE, as shown below. Σ; ΓC ; •, a ⊢tm e :σ′ ⇝ e Σ; ΓC ; • ⊢tm Λa.e : ∀a.σ′ ⇝ Λa.e iTm-forallI ΓC ; • ⊢ty σ⇝σ Σ; ΓC ; • ⊢tm (Λ...

    work page 2019

  13. [13]

    We do this by showing that e0 − →∗ e ′ 0

    We need to show that there exists aneh such that e0 − →∗ eh and e ′ 0 − →∗ eh. We do this by showing that e0 − →∗ e ′ 0. By inversion, the last part of Derivation 1015 must be an instance of iTm-constrI directly followed by iTm-constrE, as shown below. Σ; ΓC ; •,δ: Q ⊢tm e :σ⇝ e1 ΓC ; • ⊢ty σ⇝σ Σ; ΓC ; • ⊢tm λδ: Q.e : Q ⇒σ⇝λδ:σ.e1 iTm-constrI Σ; ΓC ; • ⊢d...

    work page

  14. [14]

    We need to show that there is a eh such that e0 − →∗ eh and e ′ 0 − →∗ eh. Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 91. Publication date: August 2019. 91:142 Gert-Jan Bottu, Ningning Xie, Koar Marntirosian, and Tom Schrijvers By inversion on Equation 1017, we have e0 = ((Λaj.λδi :σ′ i i .{m = em})σj ei).m andσ0 = [[σj/aj]σq/a]σm, for someσm, em...

    work page 2019

  15. [15]

    We do this by showing that e0 − →∗ e ′ 0

    We need to show that there exists aneh such that e0 − →∗ eh and e ′ 0 − →∗ eh. We do this by showing that e0 − →∗ e ′ 0. By inversion, the last rule used for Derivation 1020 must be an instance of iTm-let. Σ; ΓC ; • ⊢tm e1 :σ⇝ e1 Σ; ΓC ; •, x :σ⊢tm e2 :σ′ ⇝ e2 ΓC ; • ⊢ty σ⇝σ Σ; ΓC ; • ⊢tm let x :σ= e1 in e :σ′ ⇝ let x :σ= e1 in e2 iTm-constrI where e0 = l...

    work page 2019