Using ends to construct categorical fixed points

Question

Under advice from Toby Bartels, I am posting this question here; it falls under the general heading of constructing data types categorically as fixed points of functors.

The first question I have is a warm-up. There's a way to interpret a natural number n in any cartesian closed category $C$, as a dinatural transformation of the form

$$c^c \to c^c$$

which intuitively takes an element $f\colon c \to c$ to its $n$-th iterate $f^{(n)}\colon c \to c$. One may hope that if $C$ is "nice", then every such dinatural transformation will be of this form, or better still, that the end

$$\int_{c: C} (c^c)^{c^c}$$

(assuming it exists) behaves as a natural numbers object in $C$. So first, I am interested in what "nice" might mean here: what are some general conditions on $C$ that ensure we can construct a natural numbers object as an end in this way?

Second, this end can be rewritten as

$$\int_{c: C} c^{c^{1 + c}}$$

provided that $C$ has coproducts, and the assertion that this behaves as a natural numbers object is equivalent to saying it is an initial algebra for the endofunctor $F(c) = 1 + c$ (that's algebra for an endofunctor, not for a monad), making it a "fixed point" of $F$ by a famous old result of Lambek.

This suggests a second more general question: given an endofunctor $F: C \to C$ on cartesian closed $C$ with a strength (essentially, a structure of $C$-enrichment), I want to know what "nice" conditions on $C$ and/or $F$ guarantee that the end

$$e = \int_{c: C} c^{c^{F(c)}}$$

if it exists, is an initial $F$-algebra. It's not hard to write down an an $F$-algebra structure for this end $e$, and show that it is weakly initial, i.e., show that if $x$ is any $F$-algebra, then there at least exists an $F$-algebra map $e \to x$. The issue then is over the uniqueness of this map, or rather what nice conditions would guarantee that.

Discussion of specific cases like PER models would be alright, but I'd probably be a lot more excited if it led to consideration of more general abstract conditions on $C$ or $F$.

Answer 1

Hi Todd, I was hoping that someone more knowledgeable than me would answer this question, but since that hasn't happened yet I'll post a few comments.

As you probably already know, your observation that the end for the natural numbers object can be written as $\int_{c:C} ((1 + c) \to c) \to c$ exactly corresponds to the Church encoding of the natural numbers in System F, the second-order polymorphic lambda calculus. Gordon Plotkin and John Reynolds wrote a paper about 20 years ago on the expressible functors of system F, which they used to explain why there were no set-theoretic models of system F (in the sense that we cannot interpret the type $A \to B$ in system F as a function space from the meaning of $A$ to the meaning of $B$). "On Functors Expressible in the Polymorphic Typed Lambda Calculus" This does not exactly answer your question, since the expressible functors (the ones definable in the internal language of the category, basically) are only a subset of the ones you want to consider, but hopefully it's food for thought.

However, this Church encoding is not an NNO in any old model of System F; for this type to be a natural numbers object the model has to be a "parametric" model. What I mean by this is that it's not sufficient to have a model which validates only the $\beta$ and $\eta$ rules of the lambda calculus -- we actually need more equations than that. (If we have only these two rules, then we can only define a weak NNO.) A model is parametric when the universal quantifier preserves relations. That is, if we have a term $M$ of type $\forall \alpha. A(\alpha)$, and two types $\tau$ and $\sigma$ with a relation $R$ between them, then the relation $R$ should lift to a relation between $A(\tau)$ and $B(\sigma)$, and $(M\;\tau, M\;\sigma)$ should inhabit that relation. PER models by themselves are not parametric, but can be made parametric via the "parametric completion" process of Rosolini. Essentially, this is a way of cooking up a new model from an old one, where quantification is restricted to range over the relation-preserving ones, and we only consider elements that preserve that relation.

A related approach to finding fixed points of functors arises in work on denotational semantics. The basic idea is to work with enriched categories, so that homsets have CPO or metric space structure, and then you can use an appropriate fixed point theorem to show the existence of least fixed points of functors. For domains, this approach was first given a categorical explanation by Smyth and Plotkin in "The Category-Theoretic Solution of Recursive Domain Equations", and is explained in a nice survey article by Andy Pitts ("Relational Properties of Domains"). For metric-enriched categories, the best entry point I know is Kim Wagner's thesis, "Solving Recursive Domain Equations with Enriched Categories".

Answer 2

I asked Marcelo Fiore about this last week, and he instantly recognized the type of problem --- right down to the fact that one typically has existence of a map from the supposedly-initial algebra to an arbitrary given algebra, but not necessarily uniqueness. This answer consists of my best recollections of what Marcelo said.

The key phrase is "parametric polymorphism". In the general setting of polymorphism, one has the existence property just mentioned, but not necessarily uniqueness. In order to get uniqueness, one adds the extra ingredient of parametricity. If I understand correctly (and I'm not confident that I do), adding in parametricity is something like passing from a category of objects and maps to the resulting category of objects and relations.

One paper that Marcelo found was Categorical data types in parametric polymorphism by Ryu Hasegawa. I think it wasn't quite what he was looking for, in that it doesn't contain any ends. There are also relevant papers by both Freyd and Rosolini, apparently.

Sorry this is a bit garbled.