# What is the logarithm or root operation in type-space?

I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types a - b and a/b.

Unlike addition and multiplication, there are not one but two inverses of exponentiation, logarithms and rooting. If function types (a → b) are type-theoretic exponentiation, given the type a → b (or b^a) what does it mean to have the type logb(c) or the type a√c?

Does it make sense to extend logarithms and roots to types at all?

If so, has there been any work in this area, and what are some good directions on how to comprehend the repercussions?

I tried looking up information on this via logic, hoping the Curry-Howard correspondence could help me, but to no avail.

-

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$.

It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{log}\!_X(F\:X)$. Note that if $F\:X\cong \mathop{log}F\to X$, then we certainly have $F\:1\cong 1$, so the container tells us nothing interesting other than its elements: containers with a choice of shapes do not have logarithms.

Familiar laws of logarithms make sense when you think in terms of position sets

$$\begin{array}{rcl@{\qquad}l} \mathop{log} (\mathop{K}1) &=& 0 & \mbox{no positions in empty container}\\ \mathop{log} I &=& 1 & \mbox{container for one, one position}\\ \mathop{log} (F\times G) &=& \mathop{log}F+\mathop{log}G & \mbox{pair of containers, choice of positions} \\ \mathop{log} (F\cdot G) &=& \mathop{log}F\times\mathop{log}G & \mbox{container of containers, pair of positions} \end{array}$$

We also gain $\mathop{log}\!_X(\nu Y. T) = \mu Z. \mathop{log}\!_X T$ where $Z=\mathop{log}\!_XY$ under the binder. That is, the path to each element in some codata is defined inductively by iterating the logarithm. E.g.,

$$\mathop{log}\mathop{Stream} = \mathop{log}\!_X(\nu Y. X\times Y) = \mu Z. 1 + Z = \mathop{Nat}$$

Given that the derivative tells us the type in one-hole contexts and the logarithm tells us positions, we should expect a connection, and indeed

$$F\:1\cong 1 \;\Rightarrow\; \mathop{log}F\cong \partial F\:1$$

Where there is no choice of shape, a position is just the same as a one-hole context with the elements rubbed out. More generally, $\partial F\:1$ always represents the choice of an $F$ shape together with an element position within that shape.

I'm afraid I have less to say about roots, but one could start from a similar definition and follow one's nose. For more uses of logarithms of types, check Ralf Hinze's "Memo functions, polytypically!". Gotta run...

-
The answer from Da Man himself. Welcome Conor! –  Andrej Bauer Mar 25 '13 at 15:17
Hmm, I am interested to see what root types are, as they would require types having imaginary numbers of inhabitants. Unless I am wrong. I will accept your answer, but if you have the time to elaborate on roots that would be much appreciated. –  efrey Mar 26 '13 at 1:56
Can this be related to the Taylor series of ln(1+x) somehow? –  yatima2975 Mar 26 '13 at 15:22
With logarithms and exponentials, I wonder... what do we need to construct a Napier object? (e.g. the supposedly unique object e such that ∂e = e) –  Rhymoid Mar 29 '13 at 12:50
Not sure that's right. If I have $x^y$, the $y$th root is $x$ and the base $x$ logarithm is $y$. The inversion is of the operation, not the components. –  Marc Hamann Mar 24 '13 at 22:35