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.


2 Answers 2


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

  • 4
    $\begingroup$ The answer from Da Man himself. Welcome Conor! $\endgroup$ Commented Mar 25, 2013 at 15:17
  • $\begingroup$ 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. $\endgroup$
    – efrey
    Commented Mar 26, 2013 at 1:56
  • $\begingroup$ Can this be related to the Taylor series of ln(1+x) somehow? $\endgroup$
    – yatima2975
    Commented Mar 26, 2013 at 15:22
  • 3
    $\begingroup$ 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) $\endgroup$
    – Rhymoid
    Commented Mar 29, 2013 at 12:50

I don't know of any work that pursues this line, but a few moments thought about it led me to this hypothesis: wouldn't the "root" of the exponential type just be the codomain, and the "logarithm" of the exponential just the domain?

  • $\begingroup$ Right, so I think your intuition is good but your conclusion is off. The root operation and the logarithm operation are what you get when you "invert" the codomain or the domain respectively, not the (co)domain's themselves. The question is, what do we mean by invert and what is the binary type operation it produces? $\endgroup$
    – efrey
    Commented Mar 24, 2013 at 22:11
  • $\begingroup$ 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. $\endgroup$ Commented Mar 24, 2013 at 22:35
  • $\begingroup$ Sorry, I have not been totally clear in my terminology. I do not mean to ask "what is the root, what is the result of applying the logarithm function". I am wondering what the operation of rooting is. What the operation of finding the logarithm is. If is expenentiation, what is a two types under the root operation. What is two types under the logarithm operation. What I mean by "invert the argument" is something there is not time to explain here. I will clarify my question, thanks. $\endgroup$
    – efrey
    Commented Mar 25, 2013 at 5:33
  • $\begingroup$ The paper I linked provides a semantics for the type a - b and the type a / b. I am not concerned with the result of reducing the operations logarithm and root, but in understanding their semantics as binary type operators. $\endgroup$
    – efrey
    Commented Mar 25, 2013 at 5:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.