## The universal property of logarithms

This is Neil’s scribe here.

We have made some progress with taking logarithms of functors, and seem to have a nice categorical analysis. This includes a universal property of the logarithm of a functor, a complete characterisation of those functors which have logarithms, a formula for calculating the logarithm of a functor (when it exists), and a simple derivation of the properties of the logarithm. Don’t get too excited though for reasons which become clear later.

We start by defining a functor by . So Y(A) is a covariant hom functor and Y(A) is exactly what Conor and Hank have been calling `Naperian containers’. In general Y doesn’t have a right adjoint, but we call a functor F **logarithmic** iff there is an object and a bijection between maps in and maps in , or equivalently maps in C.

Thm. Every Naperian container is logarithmic, and the log is calculated by thye McBridean formula .

Prf. If F is Naperian, it is of the form Y(B), so by Yoneda the maps are in bijective correspondence with maps . The result then follows by showing that equals B. []

(We cheat by using Yoneda. Some hygeine is required that we will sort out later.)

Thm. Every logarithmic functor F is a Naperian container.

Prf. By assumption, the maps in are in bijection with the maps in .

By Yoneda, the latter maps are in bijection with elements of F(A). So F(A) equals . So , and hence is Naperian. []

This is a nice result. It shows that the logarithmic functors are precisely the extensions of Naperian containers.

The properties we will derive are these:

- , where `1′ stands for the constant 1-valued functor, and likewise `0′ for the constant 0-valued functor. (These are terminal and initial objects in the functor category.)
- , where K is an object in our category.
- (Conor’s law) .

Prf. For the first property, simply calculate . For the rest, note that F and G must be of the form Y(A) and Y(B). Now just use the first result.

Conclusion. This all looked very nice at one point. But these last results are actually pretty darn trivial. Maybe there is more substance to them if we avoid the use of Yoneda. For example the last three laws can be proved using the universal property.

April 21st, 2008 at 3:14 am

Confusingly, this just showed up in my RSS feed today, but is dated three years ago. Since the only mention I’ve seen of Naperian types is in a preprint by Gibbons, I suspect there is clock skew and this really is newish. Hopefully someone gets pinged by my comment.

When I wrote a type as an exponential, a labmate in a different discipline immediately asked what a logarithm would be, so I have been thinking along these same lines recently, playing with the recursive equations for Stream, List, Nat, and whatnot. Is this perhaps useful for flattening a type for parallel computation? What about non-Naperian types that are related to Naperian types? Take lists as finite prefixes of infinite streams; the “McBridean formula” gives the same result for both, even though the latter is non-Naperian.

I’m hoping that you do find something non-trivial, as I want to read about it from someone who knows what they are talking about

April 21st, 2008 at 3:14 am

Should read “the former is non-Naperian”…