## 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 +.

June 20th, 2005 at 12:38 pm

I don’t know if we ever exactly defined it. I think it should be this:

A Napierian container is a container whose set of shapes has exactly one element. Its logarithm is the corresponding set of positions.

If F 1 = 1, we may take log F = (dF) 1, ie log (1 |> P) = P (), exactly as you might hope.

We may readily observe that the Napierian containers are closed under identity, composition, product, K→ and ν.

They obey the laws you list, plus

log (F⋅G) = log F * log G

More generally, for n-ary containers, each kind of payload has a position set, given by the ‘partial logarithm’ log_i. The rule for variables is

log_i (λX_1 .. X_n. X_j) = δij

and the chain rule for logs is

log_i (F⋅[G_1...G_n]) = Σ_j. log_j F * log_i G_j

Using the chain rule, we get the ν rule. Taking

(νF) X_1 … X_n = F X_1 … X_n ((νF) X_1 … X-n)

log_i (νF) = μY. log_i F + log_(n+1) F * Y

Checks:

log (λX. νY. X * Y) = μY. 1 + Y

log (λX. νY. Y * X * Y) = μY. 1 + 2 * Y

These are all listy structures. If you want more exciting logarithms, you need to consider ν at higher kinds. Not quite sure what to do there, but it probably involves finding an old paper of Thorsten’s and a mirror.

June 20th, 2005 at 4:50 pm

In dependent container-land, predicate transformers which give no

choice to the Angel, and all choice to the Demon are called demonic.

They commute with conjunctions generally.

Vice-versa, an angelic one gives all choice to the angel, and commutes

with disjunctions generally.

Napier is demonic. He was in fact rumoured to have been in league with the devil, by those to whom he was feuar. He was, to put it mildly, a Protestant.

* Napier, John b. 1550, Merchiston Castle, near Edinburgh, Scot.

d. April 4, 1617, Merchiston Castle

From the preface to

“Plaine Discovery of the Whole Revelation of St. John” (1593).

dedicated to whoever was “your Majesty” in Scotland in 1593.

“Let it be your Majesty’s continuall study to reforme the

universall enormities of your country, and first to begin at your

Majesty’s owne house, familie and court, and purge the same of all

suspicion of Papists and Atheists and Newtrals, whereof this

Revelation forthtelleth that the number shall greatly increase in

these latter daies.”

See also the beautiful http://www-groups.dcs.st-and.ac.uk/~history/Bookpages/Napier10.jpeg:

June 21st, 2005 at 8:15 am

Naperian containers are datatypes in which there is exactly one constructor, like

Stream(A), any many coinductive things.

In a certain sense, all datatypes given by a finite set of constructors can be collapsed to one constructor, having two arguments that are respectively a finite index i and (dependently) the argument type of the i-th original constructor, defined by cases.

More precisely, you can encode everything with the new constructor. This uses dependent types in an essential way.