What is a Naperian container?
Conor and I once talked about `Naperian’ containers, that so to speak work well with logarithms.
He reminds me that A Naperian container has one shape, and a set of positions.
So it represents an endofunctor .
The logarithm of this container is K.
Every container is a sum of Naperian containers.
To be Naperian is to be a multiplicative, unsummy kind of thing,
all products and exponentials, with no Sigma. Sheer testosterone. [The dependent counterpart is a monotone predicate transformer that commutes with all intersections. ]
Conor’s comment to this note dances the McBride with/out-of the subject,
and relates it to derivatives.
There is a connection between lambda abstraction
and some basic laws of logarithms, namely that in some respects
lambda-abstraction behaves like a logarithm, in that it satisfies
laws such as:
Linear lambda-abstraction corresponds to the case where the logarithm is Naperian.
To handle log_x(k^x) you need a special constant (^) reflecting ^ in the sense that
b^a^(^) = a ^ b. Then log_x(k^x) is (k^) = k^(^).
As Conor pointed out, Naperian functors are closed under composition
(which when taking logarithms translates into ×). In some sense they are closed under
nu expressions, and he shows how to take the logarithm of these.
The weird similarity between lambda abstraction and logarithms was (according to a manuscript by Felice Cardone and Roger Hindley on the history of the lambda-calculus ) known to Böhm in the 1970’s. It really has to do with the combinatorial completeness for the untyped lambda calculus of 4 arithmetical combinators, with exponentiation
A^F reflecting application F(A). Lambda abstraction is the undoing of application in the same way as taking the logarithm is the undoing of exponentiation. You get combinatorial completeness for the linear lambda calculus by dropping
0 and +, and for affine lambda calculus by dropping only +.