<p>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?</p>

CC BY-SA 3.0
2013-03-24T22:11:25.057Z
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?
efrey
CC BY-SA 3.0
2013-03-24T22:35:28.567Z
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
CC BY-SA 3.0
2013-03-25T05:33:18.720Z
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.
efrey
CC BY-SA 3.0
2013-03-25T05:50:56.307Z
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.
efrey
CC BY-SA 3.0
2013-03-24T21:35:23.673Z
2013-03-24T21:35:23.673Z
Marc Hamann
<p>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$.</p>

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

<p>Familiar laws of logarithms make sense when you think in terms of position sets</p>

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

<p>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 <em>path</em> to each element in some codata is defined inductively by iterating the logarithm. E.g.,</p>

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

<p>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</p>

<p>$$F\:1\cong 1 \;\Rightarrow\; \mathop{log}F\cong \partial F\:1$$</p>

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

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

CC BY-SA 3.0
2013-03-25T15:17:26.690Z
The answer from Da Man himself. Welcome Conor!
Andrej Bauer
CC BY-SA 3.0
2013-03-26T01:56:35.673Z
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
CC BY-SA 3.0
2013-03-26T15:22:06.983Z
Can this be related to the Taylor series of ln(1+x) somehow?
yatima2975
CC BY-SA 3.0
2013-03-29T12:50:07.027Z
With logarithms and exponentials, I wonder... what do we need to construct a [Napier object](http://en.wikipedia.org/wiki/E_%28mathematical_constant%29)? (e.g. the supposedly unique object `e` such that `∂e = e`)
Rhymoid
CC BY-SA 3.0
2013-03-25T10:28:57.220Z
2013-03-25T10:45:49.867Z
2013-03-25T10:45:49.867Z
pigworker
<p>I was recently reading <a href="http://www.cs.indiana.edu/~sabry/papers/rational.pdf">The Two Dualities of Computation: Negative and Fractional Types</a>.  The paper expands on sum-types and product-types, giving semantics to the types <code>a - b</code> and <code>a/b</code>.</p>

<p>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 <code>a → b</code> (or <code>b^a</code>) what does it mean to have
the type <code>logb(c)</code> or the type <code>a√c</code>?</p>

<p>Does it make sense to extend logarithms and roots to types at all?</p>

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

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

CC BY-SA 4.0
2024-09-29T05:29:10.427Z
The root operation appears in tiny objects, i.e. objects such that `a ->` has a further right adjoint. It's related to parametricity.
Trebor
<lo.logic><pl.programming-languages><type-theory><algebra>
What is the logarithm or root operation in type-space?
efrey
# What is the logarithm or root operation in type-space?

(Asked by: username_0 on 2013-03-24)

I was recently reading [The Two Dualities of Computation: Negative and Fractional Types](http://www.cs.indiana.edu/~sabry/papers/rational.pdf). 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.

**Tags:** lo.logic, pl.programming-languages, type-theory, algebra

> **Comments:**
> **username_1**: The root operation appears in tiny objects, i.e. objects such that `a ->` has a further right adjoint. It's related to parametricity.  

---

## 2 answers

### Answer by username_3 on 2013-03-25. Score: 40 | Accepted answer

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

> **Comments:**
> **username_4**: The answer from Da Man himself. Welcome Conor!  
> **username_0**: 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.  
> **username_5**: Can this be related to the Taylor series of ln(1+x) somehow?  
> **username_6**: With logarithms and exponentials, I wonder... what do we need to construct a [Napier object](http://en.wikipedia.org/wiki/E_%28mathematical_constant%29)? (e.g. the supposedly unique object `e` such that `∂e = e`)  

---

### Answer by username_2 on 2013-03-24. Score: 1

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?

> **Comments:**
> **username_0**: 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?  
> **username_2**: 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.  
> **username_0**: 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.  
> **username_0**: 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.  

---

