Isomorphism between algebraic data-types 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.
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.