pith. sign in

arxiv: 1906.12242 · v2 · pith:QKHJEMPOnew · submitted 2019-06-28 · 💻 cs.PL

Bidirectional Type Class Instances (Extended Version)

Koen Pauwels , Georgios Karachalias , Michiel Derhaeg , Tom Schrijvers This is my paper

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

classification 💻 cs.PL
keywords type classesGADTsHaskellbidirectional instancesSystem FCtype inferenceconservative extension
0
0 comments X

The pith

Haskell type class instances can be interpreted as logical bi-implications rather than unidirectional implications.

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

The paper identifies that some GADTs are hard to equip with even basic type class instances under the standard unidirectional reading. It introduces bidirectional type class instances as a conservative extension in which each instance stands for a logical bi-implication. The design supplies new typing rules, an elaboration translation into System FC, and a type-inference algorithm that produces the elaborated code. The authors show that the extension preserves the meta-theoretic properties of the existing type-class system, including soundness and coherence, and supply a proof-of-concept implementation.

Core claim

Under the bidirectional interpretation, class instances correspond to logical bi-implications. This reading yields a fully specified set of typing rules and an elaboration into System FC together with a type-inference algorithm. The resulting system is a conservative extension: every program that was well-typed before remains well-typed, and the meta-theoretic properties of the original type-class mechanism (soundness, coherence) continue to hold.

What carries the argument

Bidirectional type class instances, which are interpreted as logical bi-implications and equipped with typing rules and an elaboration to System FC.

If this is right

  • Instances for GADTs that were previously impossible become expressible.
  • All existing well-typed Haskell programs remain well-typed without modification.
  • Type inference and elaboration continue to be decidable and produce System FC terms.
  • The coherence and soundness guarantees of the original type-class system are retained.

Where Pith is reading between the lines

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

  • The same bi-implication view might simplify other interactions between GADTs and functional dependencies or type families.
  • Programmers could deliberately write symmetric instance declarations to document reversible relationships.
  • Similar bidirectional extensions could be explored for other unidirectional constructs such as functional dependencies.

Load-bearing premise

The bidirectional reading can be realized as a conservative extension whose typing rules and elaboration preserve soundness, coherence and the other meta-theoretic properties of existing type classes.

What would settle it

A concrete program that is accepted by the bidirectional rules, elaborates to a well-typed System FC term, yet produces an incoherent or unsound result at runtime, or a simple GADT for which no instance can still be written even after the extension.

Figures

Figures reproduced from arXiv: 1906.12242 by Georgios Karachalias, Koen Pauwels, Michiel Derhaeg, Tom Schrijvers.

Figure 1
Figure 1. Figure 1: Source and Target Syntax 5.2 Target Syntax The syntax of System FC programs is presented in Figure 1b. In contrast to prior specifications of type classes that use System F as the target language for elaboration, our elabo￾ration targets System FC. Though for plain type classes this is not required (System F is a strict subset of System FC), it is essential for bidirectional instances, as we explained in S… view at source ↗
Figure 2
Figure 2. Figure 2: Basic System: Declaration Typing and Elaboration into System FC TTC, the superclass axioms d n , and the method f . We use proji TC(d) to denote the extraction of the i-th field of a class dictionary d of type TTC a: proji TC(d) ≡ case d of { KTC x → xi } Instance Declarations Judgment P; Γ ⊢INS ins : Pi ⇝ decl handles instance declarations and is also given by a single rule. Rule Ins is for the most part … view at source ↗
Figure 3
Figure 3. Figure 3: Basic System: Additional Judgments A.2 Type Inference and Elaboration Algorithm We now present and briefly discuss the judgments we omit￾ted in Section 5.5. A.2.1 Constraint Generation Constraint generation with elaboration for terms takes the form Γ ⊢TM e : τ ⇝ t | C; E and is presented in [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: System FC Typing term instantiation becomes explicit via type application. Sim￾ilarly, the source-level elimination of constraints Q amounts to term-level application in System FC. Arguments d cap￾ture the yet-unknown dictionaries, evidence for the wanted constraints Q. Rule Let handles (possibly recursive) monomorphic let￾bindings. After assigning a fresh unification variable a to the term variable x, we … view at source ↗
Figure 5
Figure 5. Figure 5: Term Elaboration and Constraint Generation choose not to perform let-generalization,17 so Rule Let does not make a distinction between constraints generated by e1 or e2; they are both part of the result. Finally, we record that the (monomorphic) type of x is equal to the type of the term it is bound to: a ∼ τ1. Rule TmAbs is straightforward: we generate a fresh type variable for the argument x, and collect… view at source ↗
read the original abstract

GADTs were introduced in Haskell's eco-system more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes. In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell's type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical bi-implications, in contrast to their traditional unidirectional interpretation. We present a fully-fledged design of bidirectional instances, covering the specification of typing and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proof-of-concept implementation of our algorithm, and revisit the meta-theory of type classes in the presence of our extension.

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

1 major / 0 minor

Summary. The paper proposes bidirectional type class instances as a conservative extension to Haskell's type classes for better interaction with GADTs. Under this interpretation, class instances correspond to logical bi-implications rather than the traditional unidirectional implications. It presents a full design including typing rules and elaboration to System FC, a type inference and elaboration algorithm, a proof-of-concept implementation, and a revisit of the meta-theory of type classes in the presence of the extension.

Significance. If the claims hold, the extension would address a practical difficulty in providing instances for some GADTs, which has persisted since their introduction over a decade ago. The abstract highlights a proof-of-concept implementation and meta-theoretic revisit as part of the contribution.

major comments (1)
  1. The abstract asserts that bidirectional instances can be realized as a conservative extension whose typing rules and elaboration to System FC preserve meta-theoretic properties such as soundness and coherence, but the submission provides only the abstract with no typing rules, elaboration details, or proof sketches visible, making it impossible to assess whether the central claim is supported by the development.

Simulated Author's Rebuttal

1 responses · 1 unresolved

We thank the referee for their comments. We respond to the major comment below.

read point-by-point responses

  1. Referee: The abstract asserts that bidirectional instances can be realized as a conservative extension whose typing rules and elaboration to System FC preserve meta-theoretic properties such as soundness and coherence, but the submission provides only the abstract with no typing rules, elaboration details, or proof sketches visible, making it impossible to assess whether the central claim is supported by the development.

    Authors: The provided manuscript consists only of the abstract, which summarizes the contributions but does not include the typing rules, System FC elaboration, inference algorithm, implementation, or meta-theoretic proofs. The full extended paper on arXiv:1906.12242 contains these elements as described in the abstract. Since the details are not visible in the given text, we cannot exhibit them here. revision: no

standing simulated objections not resolved
  • The referee's observation that only the abstract is visible, preventing assessment of the typing rules, elaboration, and meta-theoretic claims.

Circularity Check

0 steps flagged

No circularity detectable from abstract alone

full rationale

Only the abstract is available for analysis. It asserts a conservative extension with bidirectional instances interpreted as bi-implications, along with typing rules, elaboration to System FC, an inference algorithm, and meta-theoretic preservation, but presents no equations, derivations, fitted parameters, or self-citations that could be inspected for reduction to inputs by construction. No load-bearing steps of any enumerated kind are quotable, so the derivation chain cannot be walked and no circularity is identified. This matches the expectation that papers without visible self-referential reductions receive score 0.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no concrete free parameters, axioms, or invented entities; ledger left empty.

pith-pipeline@v0.9.0 · 5656 in / 1030 out tokens · 20797 ms · 2026-05-25T13:08:35.560778+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

13 extracted references · 13 canonical work pages

  1. [1]

    Coherence of Type Class Resolution. Proc. ACM Program. Lang. (2019). Accepted. Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. 2005a. Associated Type Synonyms. SIGPLAN Not. 40, 9 (2005), 241–253. Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and Simon Marlow. 2005b. Associated Types with Class. In POPL ’05. ACM, 1–13. L...

    work page 2019

  2. [2]

    SIGPLAN Not

    Concepts: Linguistic Support for Generic Programming in C++. SIGPLAN Not. 41, 10 (2006), 291–310. Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler

    work page 2006

  3. [3]

    TOPLAS 18, 2 (March 1996)

    Type Classes in Haskell. TOPLAS 18, 2 (March 1996). Thomas Hallgren

    work page 1996

  4. [4]

    ACM Trans

    Type Inference with Polymorphic Recursion. ACM Trans. Program. Lang. Syst. 15, 2 (April 1993), 253–289. R. Hindley

    work page 1993

  5. [5]

    The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc. 146 (1969), 29–60. Bidirectional Type Class Instances (Extended Version) Haskell ’19, August 22–23, 2019, Berlin, Germany Patricia Johann and Neil Ghani

    work page 1969

  6. [6]

    SIGPLAN Not

    Foundations for Structured Program- ming with GADTs. SIGPLAN Not. 43, 1 (Jan. 2008), 297–308. Mark P. Jones

    work page 2008

  7. [7]

    52, 10 (Sept

    Elaboration on Functional Dependencies: Functional Dependencies Are Dead, Long Live Functional Dependencies! SIGPLAN Not. 52, 10 (Sept. 2017), 133–147. Robert Kowalski

    work page 2017

  8. [8]

    SIG- PLAN Not

    A Simple Semantics for Haskell Overloading. SIG- PLAN Not. 49, 12 (2014), 107–118. J. Garrett Morris and Richard A. Eisenberg

    work page 2014

  9. [9]

    SIGPLAN Not

    Simple Unification-based Type Inference for GADTs. SIGPLAN Not. 41, 9 (2006), 50–61. Norman Ramsey, João Dias, and Simon Peyton Jones

    work page 2006

  10. [10]

    SIGPLAN Not

    Hoopl: A Modular, Reusable Library for Dataflow Analysis and Transformation. SIGPLAN Not. 45, 11 (Sept. 2010), 121–134. John C. Reynolds

    work page 2010

  11. [11]

    In Program- ming Symposium, Proceedings Colloque Sur La Programmation

    Towards a Theory of Type Structure. In Program- ming Symposium, Proceedings Colloque Sur La Programmation . 408–423. John C. Reynolds. 1983a. Types, Abstraction, and Parametric Polymorphism. In Information Processing 83, R.E.A. Mason (Ed.). 513–523. John C. Reynolds. 1983b. Types, abstraction and parametric polymorphism. (1983). Tom Schrijvers, Simon Peyt...

    work page 1983

  12. [12]

    In ICFP ’08

    Type Checking with Open Type Functions. In ICFP ’08. ACM, 51–62. M. Sulzmann, M. M. T. Chakravarty, S. Peyton Jones, and K. Donnelly. 2007a. System F with Type Equality Coercions. In TLDI ’07. ACM. Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, and Peter J. Stuckey. 2007b. Understanding Functional Dependencies via Constraint Handling Rules. J. Func...

    work page 2007

  13. [13]

    Outsidein(x) Modular Type Inference with Local Assump- tions. J. Funct. Program. 21, 4-5 (Sept. 2011), 333–412. P. Wadler and S. Blott

    work page 2011