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

<p>In your case, let's pick $P(X)$ to be <em>$X(\bot)$ is isomorphic to 1</em> where $\bot$ is <a href="https://en.wikipedia.org/wiki/Bottom_type">the empty data type</a>. Clearly, $P$ is preserved by isomorphisms. Now</p>

<p>$T_1(\bot) \cong 1 + \bot + T_1(\bot) \times T_1(\bot) \cong 1 + T_1(\bot) \times T_1(\bot)$</p>

<p>which has obviously more than one value, but</p>

<p>$T_2(\bot) \cong 1 + \bot \times T_2(\bot) \times T_2(\bot) \cong 1$.</p>

<p>Therefore $T_1$ and $T_2$ aren't isomorphic.</p>

CC BY-SA 3.0
2014-06-28T20:03:46.237Z
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).
resnick
CC BY-SA 3.0
2014-06-29T00:01:05.183Z
Try using $1$ instead...
cody
CC BY-SA 3.0
2014-06-29T08:38:53.573Z
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.
Andrej Bauer
CC BY-SA 3.0
2014-06-29T08:50:06.510Z
@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).
Petr
CC BY-SA 3.0
2014-06-29T09:33:22.017Z
Ah, I see. You're right, it suffices to find one counter-examples for $A$'s.
Andrej Bauer
CC BY-SA 3.0
2014-06-28T16:16:02.850Z
2014-06-28T16:16:02.850Z
Petr
<p>I don't think <span class="math-container">$T_1(A)$</span> and <span class="math-container">$T_2(A)$</span> 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.</p>
<p>An example of what I mean by &quot;not meaningful&quot; is the following isomorphism:</p>
<p><span class="math-container">$$ P_1(A) = (1 + 1 + 1 +...) \times A $$</span>
<span class="math-container">$$ P_2(A) = (1 + 1 + 1 +...) \times (A + A) $$</span></p>
<p>or even simpler:</p>
<p><span class="math-container">$$ Q_1(A) = (1 + 1 + 1 +...)  $$</span>
<span class="math-container">$$ Q_2(A) = (1 + 1 + 1 +...) \times (1 + 1) $$</span></p>
<p>You can map <span class="math-container">$Q_1$</span> into <span class="math-container">$Q_2$</span> and back isomorphically; both are just &quot;sets of natural numbers&quot;. 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.</p>
<p>Similarly, for the types <span class="math-container">$T_1(A)$</span> and <span class="math-container">$T_2(A)$</span>, the structure of the types is that there is a tree-like recursion where a value of <span class="math-container">$T_1$</span> may branch into two values of <span class="math-container">$T_1$</span>, and similarly for <span class="math-container">$T_2$</span>. This structure cannot be preserved by an isomorphism between <span class="math-container">$T_1(A)$</span> and <span class="math-container">$T_2(A)$</span>. Here is a formal way of proving that.</p>
<p>Let us introduce another type parameter <span class="math-container">$Z$</span> like this:</p>
<p><span class="math-container">$$ T_1 = 1 + A + Z\times T_1×T_1 $$</span></p>
<p><span class="math-container">$$ T_2 = 1 + A×T_2 + Z\times T_2×T_2$$</span></p>
<p>We recover the original definitions when <span class="math-container">$Z = 1$</span>.</p>
<p>The types <span class="math-container">$T_1(A, Z)$</span> and <span class="math-container">$T_2(A,Z)$</span> can now be written as infinite polynomial series in the type parameters <span class="math-container">$A$</span> and <span class="math-container">$Z$</span>. The initial terms of those series are:</p>
<p><span class="math-container">$$   T_1(A, Z) = 1 + A + Z×(1 + A)×(1 + A) +...  $$</span>
<span class="math-container">$$   T_1(A, Z) = 1 + A×(1 + A + ...) + Z×(1 + A×(1 + A + ...))×(1 + A×(1 + A + ...)) +...  $$</span></p>
<p>These time series contain an increasing sequence of powers of <span class="math-container">$Z$</span>. Each time the tree branching happens, there is one more power of <span class="math-container">$Z$</span>. This reflects the recursive structure of the types.</p>
<p>Looking at these times series as functions of <span class="math-container">$Z$</span> in terms of ordinary calculus, we can see that these are Taylor series expansions of the functions <span class="math-container">$T_1(A, Z)$</span> and <span class="math-container">$T_2(A,Z)$</span> for small values of <span class="math-container">$A$</span> and <span class="math-container">$Z$</span>.</p>
<p>These functions are solutions of quadratic equations. We can write their solutions explicitly:
<span class="math-container">$$T_1(A,Z) = \frac{1}{2\times Z}\left(1- \sqrt{1-4\times Z\times(1+A)}\, \right)$$</span>
and
<span class="math-container">$$T_2(A, Z) =\frac{1}{2\times Z}\left(1-A - \sqrt{(1-A)^2 -4\times Z}\, \right) $$</span></p>
<p>Of two possible roots of the quadratic equations, we need to choose the roots that become <span class="math-container">$1+ A + ...$</span> when <span class="math-container">$Z=0$</span>. This fixes the signs in the formulas.</p>
<p>Now we can see that the functions <span class="math-container">$T_1(A, Z)$</span> and <span class="math-container">$T_2(A,Z)$</span> are different. Their series expansions are therefore also different. The series cannot be mapped onto each other without changing some of the powers of <span class="math-container">$Z$</span> or <span class="math-container">$A$</span>.</p>
<p>This derivation is not particularly deep; it just shows that any isomorphism between the types <span class="math-container">$T_1(A, Z)$</span> and <span class="math-container">$T_2(A,Z)$</span> 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.</p>

CC BY-SA 4.0
2022-11-02T12:47:52.437Z
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'.
Martin Berger
CC BY-SA 4.0
2022-11-02T11:38:15.507Z
2022-11-02T11:38:15.507Z
winitzki
<p>Spoiler: the types are isomorphic.</p>

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

<p>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 <em>inductive</em> solution (the initial algebra for the polynomial functor) or the <em>coinductive</em> 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).</p>

<p>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 <em>not</em> 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 <em>is</em> 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...)</p>

<p>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}$.)</p>

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

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

<p><em>Proof.</em> 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 <em>infinitely</em> 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.</p>

CC BY-SA 3.0
2014-06-29T09:32:29.763Z
2014-06-29T09:50:37.073Z
2014-06-29T09:50:37.073Z
Andrej Bauer
<p>I have two types of trees in Haskell, defined as the least solution of the following equations:</p>

<p>$T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$</p>

<p>$T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$</p>

<p>In Haskell it would be something like</p>

<pre><code>data T1 a = Leaf | Data a | Node (T1 a) (T1 a)

data T2 a = Leaf' | Data' a (T2 a) | Node' (T2 a) (T2 a)
</code></pre>

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

CC BY-SA 3.0
2014-06-29T08:33:25.223Z
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?
Andrej Bauer
CC BY-SA 3.0
2014-06-29T09:36:48.880Z
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.
john_leo
CC BY-SA 3.0
2014-06-29T12:19:26.677Z
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$.
resnick
<ds.data-structures><functional-programming><ct.category-theory><type-systems><haskell>
Isomorphism between algebraic data-types
resnick
# Isomorphism between algebraic data-types

(Asked by: username_0 on 2014-06-28)

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.

**Tags:** ds.data-structures, functional-programming, ct.category-theory, type-systems, haskell

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

---

## 3 answers

### Answer by username_1 on 2014-06-29. Score: 8 | Accepted answer

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.


---

### Answer by username_3 on 2014-06-28. Score: 5

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](https://en.wikipedia.org/wiki/Bottom_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.

> **Comments:**
> **username_0**: 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).  
> **username_4**: Try using $1$ instead...  
> **username_1**: 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.  
> **username_3**: @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 username_4's suggestion fails for the reasons you've given).  
> **username_1**: Ah, I see. You're right, it suffices to find one counter-examples for $A$'s.  

---

### Answer by username_5 on 2022-11-02. Score: 1

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.

> **Comments:**
> **username_6**: 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'.  

---

