Comodule Representations of Second-Order Functionals

TL;DR

This paper introduces a unified theory of second-order functional representations using comodule structures, encompassing classic and novel functional types with applications in constructive mathematics and computability theory.

Contribution

It develops a general framework for representing second-order functionals via comodules, unifying existing theories and introducing new representations with broad applicability.

Findings

Unified framework for second-order functional representations

Connections to constructive mathematics and Weihrauch reducibility

Examples include various types of continuous and effectful functionals

Abstract

We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally subsumes classic representations of continuous functionals with well-founded trees. We find other kinds of representations by varying the monad, the comodule, and in some cases the underlying category of containers. Examples include uniformly continuous or finitely supported functionals, functionals querying their arguments precisely once, or at most once, functionals interacting with an ambient environment through computational effects, as well as functionals trivially representing themselves. Many of these rely on our construction of a monad on containers from a monad on shapes and a weak Mendler-style monad algebra on the universe for positions. We show that comodule representability on the category of propositional containers, which have positions valued in a universe of propositions, is closely related to instance reducibility in constructive mathematics, and through it to Weihrauch reducibility in computability theory.