5
$\begingroup$

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>
Tree = (Value, Forest)

Obviously the type above can be reduced to a single type

Tree = (Value, List<Tree>)

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.

$\endgroup$
8
$\begingroup$

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)).$$ This is indeed so in many cases and goes under the name Bekič's Lemma. Note however that the inner $\mu_X$ 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$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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