← All papers
Understanding Haskell-style Overloading via Open Data and Open Functions
cs.PL
Jul 21, 2025 · v1
TL;DR
Mechanizes the metatheory of System F_D, a core language for Haskell-style overloading, in the Lean4 theorem prover.
Abstract
We present a new, uniform semantics for Haskell-style overloading. We realize our approach in a new core language, System F$_\mathrm{D}$, whose metatheory we mechanize in the Lean4 interactive theorem prover. System F$_\mathrm{D}$ is distinguished by its open data types and open functions, each given by a collection of instances rather than by a single definition. We show that System F$_\mathrm{D}$ can encode advanced features of Haskell's of type class systems, more expressively than current semantics of these features, and without assuming additional type equality axioms.
Problem
Existing semantics of Haskell-style overloading and type classes are non-uniform and often rely on extra type-equality axioms.
Approach
The authors present System F_D, a core language with open data types and open functions (each given by a collection of instances), giving a uniform semantics for overloading, and mechanize its metatheory in the Lean4 interactive theorem prover.
Results
System F_D encodes advanced Haskell type-class features more expressively than current semantics and without assuming additional type-equality axioms.