Extensible types as unknown bialgebras

Andreas Nuyts

Functional programming languages typically provide:

• inductive data types, whose elements are generated by their constructors, and processed by structural recursion,
• coinductive record types, whose elements are observed through their fields, and constructed by defining these fields corecursively.

The expression problem asks for a type former whose elements can be constructed through a known list of constructors, open to future extension, and observed through a known list of fields (a.k.a. methods) also open to future extension. I propose to understand such types as arbitrary bialgebras for a fixed pair of functors, whose reduction rules are specified by a distributive law or GSOS law between those functors, and am exploring ways to turn that into a functional programming technique. I would very much value insights from the TU Delft PL Group on these explorations.

---

Previous: Matteo Bertorotta | Pruning the Infinite, Example-Based Synthesis using Context-Sensitive E-Graph Saturation
Next: Maria Khakimova | Enhancing Agda's Error Messages with Hints