{"ID":2892482,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2507.16086","arxiv_id":"2507.16086","title":"Understanding Haskell-style Overloading via Open Data and Open Functions","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.","short_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...","url_abs":"https://arxiv.org/abs/2507.16086","url_pdf":"https://arxiv.org/pdf/2507.16086v1","authors":"[\"Andrew Marmaduke\",\"Apoorv Ingle\",\"J. Garrett Morris\"]","published":"2025-07-21T21:46:30Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}