Håkon Gylterud: Higer-kinded containers

Abstract: Containers provide a convenient mathematical model of data structures and have a close connection to Joyal's combinatorial species. In functional programming, containers and their morphisms represent polynomial functors on sets. In Haskell terms, we say they have kind \(* \to *\). However, in modern functional programming higher-kinded operations occur frequently. These higher-kinded operations represent operations on functors themselves. For instance, a monad transformer is an operation of kind \((* \to *) \to (* \to *)\).

In joint work with Thorsten Altenkirch and Zhili Tian, I am working on extending the notion of container to arbitrary kinds. In this talk I will motivate and report on our progress. In particular, we will discuss a specific proposal for a notion of higher-kinded container which supports substitutions and fixed points.