Flexible and Reversible Conversion between Extensible Records and Overloading Constraints for ML

TL;DR

The paper addresses interoperability between explicit dictionary passing via records and compiler-driven overloading constraints in ML-like languages. It introduces inject and eject as first-class operators that reversibly transform between constrained functions and record-argument functions, enabling switching between dictionary-passing and constraint-resolution styles with minimal syntactic overhead. A formal type system, together with type inference and correctness sketches, is provided to support nested injections and ejections, restricted forms, and local resolution. The approach aims to improve code reuse across libraries that adopt different dispatch mechanisms, reducing wrapper boilerplate and enabling modular interoperation in a principled way. The work lays groundwork for further formalization, optimization, and potential extension to first-class operator design and overloaded-label extensible records.

Abstract

Most ML-like functional languages provide records and overloading as unrelated features. Records not only represent data structures, but are also used to implement dictionary passing, whereas overloading produces type constraints that are basically dictionaries subject to compiler-driven dispatching. In this paper we explore how records and overloading constraints can be converted one into the other, allowing the programmer to switch between the two at a very reasonable cost in terms of syntactic overhead. To achieve this we introduce two language constructs, namely inject and eject, performing a type-driven syntactic transformation. The former literally injects constraints into the type and produces a function adding an extra record argument. The latter does the opposite, ejecting a record argument from a function and turning fields into type constraints. The conversion is reversible and can be restricted to a subset of symbols, granting additional control to the programmer. Although what we call inject has already been proposed in literature, making it a language operator and coupling it with its reverse counterpart represent a novel design. The goal is to allow the programmer to switch from a dictionary-passing style to compiler-assisted constraint resolution, and vice versa, enabling reuse between libraries that otherwise would not interoperate.

Figures (5)

• Figure 1: Mixing manual dictionary-passing with constraint resolution can be problematic in Haskell. The snippet is hypothetical, as it shows a workaround that would require Haskell to support local instances and local resolution. Notably, even if such language extensions were fully supported, a considerable amount of wrapper code would still be required.
• Figure 2: The snippet shows how to make two libraries based on different programming practices interoperate through a combined use of injection and ejection. Despite some technical complications that arise in Haskell, mainly due to heavyweight records and monolithic type classes, the code gives an intuition of what the inject and eject operators are capable of.
• Figure 3: Example of injection and typing-time translation. Dictionary passing relies on extra arguments zero and add in the translated function sum on the right. Below, injection introduces a new record argument r and locally binds all overloaded names to the fields of r. This mimics the resolution of the constraints of sum by providing a local set of symbols to be passed as a dictionary.
• Figure 4: Example of ejection and translation performed by type rules. Ejection restores dictionary passing by adding lambda arguments zero and add, one for each field of the record parameter r of function sum. This is then erased by passing a record value, where all fields are bound to overloaded names.
• Figure 5: Explicit rebindings can be used for solving the constraints arising from the use of sum and eject multR. Local resolution grants the expected behaviour.

Theorems & Definitions (12)

• Definition 5.1.1: Instance Relation
• Definition 5.1.2: Hashing of Instance Suffixes
• Definition 5.1.3: Type Distance
• Definition 5.2.1: Best Fitting Instance
• Definition 5.2.2: Fitting Binding
• Definition 5.2.3: Constraints Compaction
• Definition 5.2.4: Unsolvable Constraint
• Definition 5.2.5: Constraint Solver
• Lemma 6.2.1: Correctness of Inject-R Translation
• Lemma 6.2.2: Correctness of Inject-All Translation