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 $X \mapsto X^K$.
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:

\[
    \begin{array}[t]{l}
      log_x(a^k) = log_x(a) * k, \\
      log_x(a*b) = log_x(a) + log_x(b), \;\;\; \mbox{Note: non-linear}\\
      log_x 1 = 0, \;\;\;\;\;\; \mbox{Note: non-affine}\\
      log_x(x) = 1, \\
      x^{log_x a} = a.
  \end{array}
\]
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 +.

3 Responses to “What is a Naperian container?”

  1. Conor Says:

    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.

  2. Hank Says:

    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:

  3. Hank Says:

    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.

Leave a Reply

You must be logged in to post a comment.