<p>In general, for any type (or domain, or complete lattice) <span class="math-container">$X$</span> we can consider the least fixed-point operator <span class="math-container">$\mu_X : (X \to X) \to X$</span>. For recursive types we take <span class="math-container">$X = \mathsf{Type}$</span>, i.e., we apply <span class="math-container">$\mu$</span> at the universe of all types. Given a system of mutually recursive equations
<span class="math-container">\begin{align*}
A &amp;= F(A, B)\\
B &amp;= G(A, B)
\end{align*}</span>
where <span class="math-container">$F, G : X \times X \to X$</span>, rewrite this as a single equation
<span class="math-container">\begin{align*}
(A,B) = (F(A,B), G(A,B))
\end{align*}</span>
and then define <span class="math-container">$H : X \times X \to X \times X$</span> by <span class="math-container">$$H(A,B) = (F(A,B), G(A,B))$$</span> so that the original system becomes an ordinary fixed point equation
<span class="math-container">$$P = H(P)$$</span>
where <span class="math-container">$P = (A, B)$</span>. This shows that mutual recursion at <span class="math-container">$X$</span> is ordinary recursion at <span class="math-container">$X \times X$</span>. In terms of the <span class="math-container">$\mu$</span>-operator we may therefore solve the original system as
<span class="math-container">$$(A,B) = \mu_{X \times X} P . (F(P), G(P)).$$</span>
In the case of recursive types, just set <span class="math-container">$X = \mathsf{Type}$</span>.</p>

<p>We may further wonder whether we can replace <span class="math-container">$\mu_{X \times X}$</span> with two nested applications of <span class="math-container">$\mu_X$</span>, i.e., perhaps it is the case that
<span class="math-container">$$\mu_{X \times X} P . H(P) = \mu_X A . \mu_X B . H(A, B),$$</span>
or something like it. Indeed, <em>Bekić's Lemma</em> [1] explains how to compute the fixed point on <span class="math-container">$X \times X$</span> in terms of fixed points on <span class="math-container">$X$</span>, namely
<span class="math-container">$$\mu_{X \times X} (A,B) .(F(A,B), G(A,B)) = (A_0, B_0)$$</span>
where
<span class="math-container">\begin{align*}
A_0 &amp;= \mu_X A . F(A, \mu_X B . G(A,B)), \\
B_0 &amp;= \mu_X B . G(A_0,B).
\end{align*}</span>
Note however that the inner <span class="math-container">$\mu_X$</span> in <span class="math-container">$A_0$</span> computes a fixed point in the presence of a free parameter <span class="math-container">$A$</span>, which may be tricky depending on the exact situation.</p>

<p>In summary, you have a choice in solving systems of recursive type equations: either you generalize <span class="math-container">$\mu$</span> to pairs of types, or you allow <em>parameters</em> to appear when you apply <span class="math-container">$\mu$</span>.</p>

<p>[1]: Hans Bekić (1969) <a href="https://doi.org/10.1007/BFb0048939" rel="noreferrer">Definable operations in general algebras, and the theory of automata and flowcharts</a>. Published posthumously in: Jones C.B. (eds) <em>Programming Languages and Their Definition</em>. (1984) LNCS, vol 177.</p>

CC BY-SA 4.0
2019-04-09T09:07:00.310Z
2019-06-18T22:10:39.883Z
2019-06-18T22:10:39.883Z
Andrej Bauer
<p>I've been reading TAPL, and reached the section on recursive types. I understand the type operator <span class="math-container">$\mu$</span>. For example, the two type expressions are equivalent</p>

<pre><code>NatList = {nil: Unit, cons: (Nat, NatList)}
</code></pre>

<p>and 
<span class="math-container">$$ \mu X. 1 + \text{Nat} \times X $$</span></p>

<p>I'm confused how I would, using the <span class="math-container">$\mu$</span> operator, describe mutually recursive types such as</p>

<pre><code>Forest = List&lt;Tree&gt;
Tree = (Value, Forest)
</code></pre>

<p>Obviously the type above can be reduced to a single type</p>

<pre><code>Tree = (Value, List&lt;Tree&gt;)
</code></pre>

<p>But is there any way to write this using type-theoretic notation? Specifically I am wondering how the isorecursive operations <code>fold</code> and <code>unfold</code> operate on mutually recursive types, since I feel like <code>unfold</code> would have to expand both the definition of <code>Tree</code> and of <code>Forest</code>.</p>

<type-theory><type-inference>
Can Isorecursive types capture mutually recursive data types?
Enrico Borba
# Can Isorecursive types capture mutually recursive data types?

(Asked by: username_0 on 2019-04-08)

I've been reading TAPL, and reached the section on recursive types. I understand the type operator $\mu$. For example, the two type expressions are equivalent
NatList = {nil: Unit, cons: (Nat, NatList)}

and 
$$ \mu X. 1 + \text{Nat} \times X $$
I'm confused how I would, using the $\mu$ operator, describe mutually recursive types such as
Forest = List
Tree = (Value, Forest)

Obviously the type above can be reduced to a single type
Tree = (Value, List)

But is there any way to write this using type-theoretic notation? Specifically I am wondering how the isorecursive operations fold and unfold operate on mutually recursive types, since I feel like unfold would have to expand both the definition of Tree and of Forest.

**Tags:** type-theory, type-inference


---

## 1 answers

### Answer by username_1 on 2019-04-09. Score: 14 | Accepted answer

In general, for any type (or domain, or complete lattice) $X$ we can consider the least fixed-point operator $\mu\_X : (X \to X) \to X$. For recursive types we take $X = \mathsf{Type}$, i.e., we apply $\mu$ at the universe of all types. Given a system of mutually recursive equations
\begin{align\*}
A &= F(A, B)\\
B &= G(A, B)
\end{align\*}
where $F, G : X \times X \to X$, rewrite this as a single equation
\begin{align\*}
(A,B) = (F(A,B), G(A,B))
\end{align\*}
and then define $H : X \times X \to X \times X$ by $$H(A,B) = (F(A,B), G(A,B))$$ so that the original system becomes an ordinary fixed point equation
$$P = H(P)$$
where $P = (A, B)$. This shows that mutual recursion at $X$ is ordinary recursion at $X \times X$. In terms of the $\mu$-operator we may therefore solve the original system as
$$(A,B) = \mu\_{X \times X} P . (F(P), G(P)).$$
In the case of recursive types, just set $X = \mathsf{Type}$.

We may further wonder whether we can replace $\mu\_{X \times X}$ with two nested applications of $\mu\_X$, i.e., perhaps it is the case that
$$\mu\_{X \times X} P . H(P) = \mu\_X A . \mu\_X B . H(A, B),$$
or something like it. Indeed, *Bekić's Lemma* [1] explains how to compute the fixed point on $X \times X$ in terms of fixed points on $X$, namely
$$\mu\_{X \times X} (A,B) .(F(A,B), G(A,B)) = (A\_0, B\_0)$$
where
\begin{align\*}
A\_0 &= \mu\_X A . F(A, \mu\_X B . G(A,B)), \\
B\_0 &= \mu\_X B . G(A\_0,B).
\end{align\*}
Note however that the inner $\mu\_X$ in $A\_0$ computes a fixed point in the presence of a free parameter $A$, which may be tricky depending on the exact situation.

In summary, you have a choice in solving systems of recursive type equations: either you generalize $\mu$ to pairs of types, or you allow *parameters* to appear when you apply $\mu$.

[1]: Hans Bekić (1969) [Definable operations in general algebras, and the theory of automata and flowcharts](https://doi.org/10.1007/BFb0048939). Published posthumously in: Jones C.B. (eds) *Programming Languages and Their Definition*. (1984) LNCS, vol 177.


---

