Comodule Representations of Second-Order Functionals
Danel Ahman
University of Tartu
Abstract:
In information-theoretic terms, a map is continuous when a finite amount of
information about the input suffices for computing a finite amount of
information about the output. Already Brouwer observed that this allows one to
represent a continuous functional from sequences to numbers with a certain
well-founded question-answer tree. The idea has been extended to other kinds of
second-order functionals, such as stream transformers, continuous functionals on
final coalgebras, sequentially realisable functionals, and others.
In type theory, a second-order functional is a (dependently typed) map
F : (∏(a : A) . P a) → (∏(b : B) . Q b).
Its continuity is once again witnessed by a well-founded tree whose nodes are
“questions” a : A, the branches are indexed by “answers” P a, and the leaves are
“results” Q b. In this work, we observe that such tree representations can be
expressed in purely category-theoretic terms, using the notion of right
T-comodules for the monad T of well-founded trees on the category of containers.
A tree representation for F is then just a Kleisli container map for the monad T.
Doing so exposes a rich underlying structure, and immediately suggests
generalisations: any right T-comodule for any monad T on containers gives rise
to a representation theorem for second-order functionals. We give several
examples of these, ranging from finitely supported functionals, to functionals
that can query their input just once (or sometimes not at all), to functionals
that can additionally interact with their environment, to partial functionals,
to observing that any functional can be trivially represented by itself.
This is joint work with Andrej Bauer from the University of Ljubljana.