Equational Theories and Monads from Polynomial Cayley Representations

Abstract

We generalise Cayley’s theorem for monoids by providing an explicit formula for a (multi-sorted) equational theory represented by the type, where is an arbitrary polynomial endofunctor with natural coefficients. From the computational perspective, examples of effects given by such theories include backtracking nondeterminism (obtained with the original Cayley representation, finite mutable state (obtained with, for a constant n), and their different combinations (via or). Moreover, we show that monads induced by such theories are implementable using the type formers available in programming languages based on a polymorphic -calculus, both as compositions of algebraic datatypes and as continuation-like monads. We give a set-theoretic model of the latter in terms of Barr-dinatural transformations. We also introduce CayMon, a tool that takes a polynomial as an input and generates the corresponding equational theory together with the two implementations of the induced monad in Haskell.