Search Results

We introduce the notion of Mendler dialgebra and provide a categorical semantics of recursion schemes of mixed variance in its terms. The Mendler-style approach - which employs second-order inference rules - to recursion schemes of mixed variance was championed by Uustalu and Vene in [Uustalu and Vene, 1999] using dinatural transformations, and we generalize their methods to include a variety of new recursion schemes including those presented by Ahn-Sheard in [Ahn and Sheard, 2011], and Stump et al. in [Aaron Stump et al., 2020]. We give sufficient criteria for reducibility of Mendler dialgebras to Lambek algebras [Joachim Lambek, 1968] which correspond to first-order inference rules. A similar reduction in elementary terms for the special case of the systems studied in [Uustalu and Vene, 1999] had been given by the authors, but our approach differs in that we use the language of two-sided fibrations [Street, 1974] to express the reduction for our generalization. This reveals that the "diagonal" of every two-sided fibration with a fibered initial object is isomorphic to a category of Lambek algebras; a dual version concerning reduction to Lambek coalgebras, as well as to bialgebras (inserters), [Joachim Lambek, 1970] is given. We also discuss various properties and examples of Mendler dialgebras, including higher-order abstract syntax which is paradigmatic for definitions of mixed variance. Generally, we regard the paper as a contribution to a more systematic understanding of the relation between higher-order and first-order inference rules.