Extensible types as unknown bialgebras

Andreas Nuyts


Date: Wed, May 07, 2025
Time: 12:00
Room: building 28, Turing


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 |
Next: |