Understanding Haskell-style Overloading via Open Data and Open Functions

Andrew Marmaduke, Apoorv Ingle, J. Garrett Morris

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…