I have two types of trees in Haskell, defined as the least solution of the following equations:

$T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$

$T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$

In Haskell it would be something like

data T1 a = Leaf | Data a | Node (T1 a) (T1 a)

data T2 a = Leaf' | Data' a (T2 a) | Node' (T2 a) (T2 a)

How could I prove or disprove that $T_1$ and $T_2$ are isomorphic? I'd like to know which tools are used to prove the non-existence of isomorphisms.

  • $\begingroup$ Do you mean inductive types, or are infinite trees allowed (like in Haskell, which does not have inductive types)? Also, what do you mean by "isomorphic"? If you mean "isomorphic as sets of values" then the answer is obviously "yes, since they have the same cardinalitity". Do you mean something else? $\endgroup$ Commented Jun 29, 2014 at 8:33
  • $\begingroup$ Could it be possible to associate a size to your objects? You could then show that the counting sequence/generating functions associated with your objects are the same/different. $\endgroup$
    – john_leo
    Commented Jun 29, 2014 at 9:36
  • $\begingroup$ Inductive types are enough (I'll think about coinductive types later). I thought of them as functors, so the isomorphism should be parametric on $A$. $\endgroup$
    – resnick
    Commented Jun 29, 2014 at 12:19

3 Answers 3


Spoiler: the types are isomorphic.

First let me clarify what might be meant by "isomorphic". Say that two datatypes $S$ and $T$ are isomorphic if there are maps $f : S \to T$ and $g : T \to S$ such that $f(g(v)) = v$ for every value $v : T$ and $g(f(u)) = u$ for every value $u : U$.

Let us fix a type $A$. We can then write your equations without the parameter $A$ as $$T_1 = 1 + A + T_1 \times T_1$$ and $$T_2 = 1 + A \times T_2 + T_2 \times T_2.$$ (We really want to consider the types polymorphic in $A$, and we shall do so, but for the moment I'd like to get rid of $A$ as a parameter, so let us consider it temporarily fixed.) If we define "polynomial" type constructors $P_1(X) = 1 + A + X \times X$ and $P_2(X) = 1 + A \times X + X \times X$ then the above definitions become fixed-point equations $$T_1 = P_1(T_1)$$ and $$T_2 = P_2(T_2).$$ We can consider either the inductive solution (the initial algebra for the polynomial functor) or the coinductive solution (the final coalgebra). The former is what you get in ML-style language and the latter in Haskell. Let's do inductive, as that is algebra, while coinductive gets us into topology (which is cooler but a bit trickier).

Now, we would like to know whether the initial algebras for $P_1$ and $P_2$ are isomorphic parametrically in $A$, by which we mean that we want isomorphisms that are parametrically polymorphic in $A$. Beware, non-isomorphic functors may produce isomorphic initial algebras: lists of $A$'s are the initial algebra for both $X \mapsto 1 + A \times X$ and $X \mapsto 1 + A \times X + A \times A \times X$! So for instance it is not sufficient to find $Y$ such that $P_1(Y) \not\cong P_2(Y)$. But since we want isomorphisms that work for all $A$'s it is sufficient to find a single instance of $A$'s for which $T_1 \not\cong T_2$ (although that might be a bit hard to find...)

I am going to take it for granted that there are no isomorphisms between $A^n$ and $A^m$ for $n \neq m$ that are parametric in $A$. (Consider $A = \mathtt{bool}$.)

We can think of $T_1$ as an "infinite" nesting $P_1(P_1(P_1(\cdots)))$, so it makes sense to look at a finite approximation. Let us compute $P_1^n(X)$ for some $n$. The result is a polynomial in $A$ and $X$, which we express as $Q_n(A) + X \times R_n(A,X)$. For $n = 1$ we get (using Mathematica and expanding as a power series in $X$): $$(A+1)+O\left(X^2\right),$$ for $n = 2$ we get $$\left(A^2+3 A+2\right)+O\left(X^2\right)$$ for $n = 6$ we get $$\left(A^{32}+48 A^{31}+1112 A^{30}+16568 A^{29}+178484 A^{28}+1481816 A^{27}+9867676 A^{26}+54160004 A^{25}+249844422 A^{24}+982869432 A^{23}+3333905572 A^{22}+9834052604 A^{21}+25390949338 A^{20}+57672050948 A^{19}+115666688826 A^{18}+205373975070 A^{17}+323359748527 A^{16}+451792820168 A^{15}+560048078060 A^{14}+615271918604 A^{13}+597813614038 A^{12}+512098495020 A^{11}+385051162322 A^{10}+252634062394 A^9+143508813439 A^8+69855202828 A^7+28739884958 A^6+9808926186 A^5+2705141303 A^4+579784870 A^3+90704955 A^2+9224803 A+458330\right)+O\left(X^2\right)$$ So it seems that we get a whole lot of every power of $A$. A similar thing happens with $T_2$, for instance $P_2$ unfolded 6 times is $$ \left(256 A^{16}+6656 A^{15}+80768 A^{14}+607488 A^{13}+3171408 A^{12}+12191008 A^{11}+35710688 A^{10}+81347056 A^9+145690452 A^8+205905596 A^7+228957512 A^6+198261418 A^5+131104690 A^4+64020678 A^3+21778198 A^2+4612401 A+458330\right)+\left(3072 A^{17}+80128 A^{16}+975744 A^{15}+7366080 A^{14}+38598592 A^{13}+148916448 A^{12}+437720280 A^{11}+1000231448 A^{10}+1796273100 A^9+2544344160 A^8+2833851236 A^7+2456339273 A^6+1624706942 A^5+792912172 A^4+269323336 A^3+56895232 A^2+5632640 A\right) X+O\left(X^2\right)$$ In the "infinity" these coefficients on $A$'s will be infinite. We will get something that looks like $$T_1 = P_1^\infty(X) = \infty + \infty A + \infty A^2 + \infty A^3 + \cdots = \infty \times (1 +A + A^2 + A^3 + \cdots) = \infty \times \mathtt{List}(A)$$ and the same for $T_2$. So we form a hypothesis:

Theorem: Both $T_1$ and $T_2$ are isomorphic (parametrically in $A$) to the type $\mathtt{nat} \times \mathtt{List}(A)$.

Proof. The best proof would be actual implementations of the isomorphisms in question, but I do not have the time to do that. Perhaps a nice soul can volunteer to write these. Let me sketch an outline of the proof. Think of the elements of $T_1$ as trees which store some $A$'s in their leaves. To each value $v : T_1$ we assign a list $\ell_v = [a_1, \ldots, a_{n_v}]$ of the $A$'s stored in $v$, in left-to-right traversal order. There are infinitely many $v$'s which share the same $\ell_v$ because we can have arbitrarily many empty leaves. Order all $v$'s with the same $\ell_v$ in a canonical order of some sort, so that to each $v$ with a given $\ell_v$ we assign a number $n_v$ in this order. The mapping $v \mapsto (n_v, \ell_v)$ is the isomorphism from $T_1$ to $\mathtt{nat} \times \mathtt{List}(A)$. A similar construction works for $T_2$. QED.


A useful technique is to find a property $P$ that is preserved by isomorphism, that is if $X\cong Y$ then $P(X)=P(Y)$. Then if we can show that $P(X)\neq P(Y)$ then also $X\not\cong Y$.

In your case, let's pick $P(X)$ to be $X(\bot)$ is isomorphic to 1 where $\bot$ is the empty data type. Clearly, $P$ is preserved by isomorphisms. Now

$T_1(\bot) \cong 1 + \bot + T_1(\bot) \times T_1(\bot) \cong 1 + T_1(\bot) \times T_1(\bot)$

which has obviously more than one value, but

$T_2(\bot) \cong 1 + \bot \times T_2(\bot) \times T_2(\bot) \cong 1$.

Therefore $T_1$ and $T_2$ aren't isomorphic.

  • $\begingroup$ I had an error in the first equation (it didn't reflect the corresponding Haskell data-type). I modified it, but this solution now becomes unavailable, as now both types have more than one element (indeed, they are isomorphic when using $\bot$ as its parameter). $\endgroup$
    – resnick
    Commented Jun 28, 2014 at 20:03
  • 1
    $\begingroup$ Try using $1$ instead... $\endgroup$
    – cody
    Commented Jun 29, 2014 at 0:01
  • $\begingroup$ This reasoning is flawed, you're applying it to the type constructors instead of the fixed points of those type constructors. By your reasoning: let $T_1(X) = 1 + X$ and $T_2(X) = 1 + 1 + X$. Then $T_1(\mathtt{empty}) = 1 \not\cong 1 + 1 = T_2(\mathtt{empty})$, whereas the inductive types $N_1 = T_1(N_1)$ and $N_2 = T_2(N_2)$ are isomorphic because they are both the natural numbers. $\endgroup$ Commented Jun 29, 2014 at 8:38
  • $\begingroup$ @AndrejBauer This is something different. You're correct that it's not valid to compare just the type constructors, when we need to compare the fixed points. But that is not what I was doing. In the question, we're not working with $\mu A.T_1(A)$, as you seem to suggest. Instead, $A$ is a polymorphic type parameter. Therefore, it's valid to say that $T_1(A)$ and $T_2(A)$ aren't isomorphic, because they're not isomorphic for one particular choice of $A$. However after the OP updated the question, the original idea doesn't work any more (and cody's suggestion fails for the reasons you've given). $\endgroup$
    – Petr
    Commented Jun 29, 2014 at 8:50
  • $\begingroup$ Ah, I see. You're right, it suffices to find one counter-examples for $A$'s. $\endgroup$ Commented Jun 29, 2014 at 9:33

I don't think $T_1(A)$ and $T_2(A)$ are isomorphic in a meaningful way. That is, meaningful in the program where these data types are used. You can certainly convert one of them into another without loss of information, but the resulting isomorphism is not meaningful; it will not respect the structure of those types. Instead, the isomorphism will just stuff the data from one type into another in some random way.

An example of what I mean by "not meaningful" is the following isomorphism:

$$ P_1(A) = (1 + 1 + 1 +...) \times A $$ $$ P_2(A) = (1 + 1 + 1 +...) \times (A + A) $$

or even simpler:

$$ Q_1(A) = (1 + 1 + 1 +...) $$ $$ Q_2(A) = (1 + 1 + 1 +...) \times (1 + 1) $$

You can map $Q_1$ into $Q_2$ and back isomorphically; both are just "sets of natural numbers". But this isomorphism does not respect the structure of those types. For instance, a basic operation for a natural number is to increment it. But the increment operation is not preserved by this isomorphism.

Similarly, for the types $T_1(A)$ and $T_2(A)$, the structure of the types is that there is a tree-like recursion where a value of $T_1$ may branch into two values of $T_1$, and similarly for $T_2$. This structure cannot be preserved by an isomorphism between $T_1(A)$ and $T_2(A)$. Here is a formal way of proving that.

Let us introduce another type parameter $Z$ like this:

$$ T_1 = 1 + A + Z\times T_1×T_1 $$

$$ T_2 = 1 + A×T_2 + Z\times T_2×T_2$$

We recover the original definitions when $Z = 1$.

The types $T_1(A, Z)$ and $T_2(A,Z)$ can now be written as infinite polynomial series in the type parameters $A$ and $Z$. The initial terms of those series are:

$$ T_1(A, Z) = 1 + A + Z×(1 + A)×(1 + A) +... $$ $$ T_1(A, Z) = 1 + A×(1 + A + ...) + Z×(1 + A×(1 + A + ...))×(1 + A×(1 + A + ...)) +... $$

These time series contain an increasing sequence of powers of $Z$. Each time the tree branching happens, there is one more power of $Z$. This reflects the recursive structure of the types.

Looking at these times series as functions of $Z$ in terms of ordinary calculus, we can see that these are Taylor series expansions of the functions $T_1(A, Z)$ and $T_2(A,Z)$ for small values of $A$ and $Z$.

These functions are solutions of quadratic equations. We can write their solutions explicitly: $$T_1(A,Z) = \frac{1}{2\times Z}\left(1- \sqrt{1-4\times Z\times(1+A)}\, \right)$$ and $$T_2(A, Z) =\frac{1}{2\times Z}\left(1-A - \sqrt{(1-A)^2 -4\times Z}\, \right) $$

Of two possible roots of the quadratic equations, we need to choose the roots that become $1+ A + ...$ when $Z=0$. This fixes the signs in the formulas.

Now we can see that the functions $T_1(A, Z)$ and $T_2(A,Z)$ are different. Their series expansions are therefore also different. The series cannot be mapped onto each other without changing some of the powers of $Z$ or $A$.

This derivation is not particularly deep; it just shows that any isomorphism between the types $T_1(A, Z)$ and $T_2(A,Z)$ will necessarily break the hierarchy between tree branches. Most likely, that kind of isomorphism will not be meaningful in the context of the program code.

  • $\begingroup$ Andreij was careful to ask what was meant by isomorphism! E.g. $\mathbb{N}, \mathbb{Q}$, and the prime numbers are isomorphic set-theoretically, but the witnessing isomorphisms don't necessarily preserve other structural properties. Likewise from the POV of the Church-Turing thesis, machine-code, Prolog, and cellular automata are equivalent, but the witnessing compilers 'trash' structural properties of the respective programming paradigms. The upshot of this is that the very concept of isomorphism is (implicitly or explicitly) always assuming an ambient collection of valid 'transformations'. $\endgroup$ Commented Nov 2, 2022 at 12:47

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.