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$ Jun 29 '14 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
    Jun 29 '14 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
    Jun 29 '14 at 12:19

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
    Jun 28 '14 at 20:03
  • 1
    $\begingroup$ Try using $1$ instead... $\endgroup$
    – cody
    Jun 29 '14 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$ Jun 29 '14 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
    Jun 29 '14 at 8:50
  • $\begingroup$ Ah, I see. You're right, it suffices to find one counter-examples for $A$'s. $\endgroup$ Jun 29 '14 at 9:33

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.