How to write a type that is isomorphic to Tree without nested lists?

Question

In Haskell, it is said that any ADT can be expressed as sum of products. I'm trying to find a flat type that is isomorphic to Tree, on Data.Tree.

Tree a = Node a [Tree a] -- has a nested type (List!)

I want to write a functionally identical definition for Tree without nested types:

Tree = ??? -- no nested types allowed

For that, I tried writing the recursive relation for the type algebras:

L a = 1 + a * L a
T a = a * L (T a)

Inlining L, I had:

T a = a * (1 + T a * L (T a))
T a = a * (1 * T a * (1 + T a * L (T a)))
T a = a * (1 + T a * (1 + T a * (1 + T a * L (T a))))

That wasn't going anywhere, so I stopped and did the multiplications, leaving me with:

T a = a + a * T a + a * T a * T a ...

Which is the same as:

T a = a * (T a) ^ 0 + a * (T a) ^ 1 + a * (T a) ^ 2 ...

That is a sum of products, but it is infinite. I can't write that in Haskell. By abusing the algebra:

(T a) - (T a) ^ 2 = a * T a
- (T a) ^ 2 - a * T a + (T a) = 0

Solving for T a, I found that:

T a = 1 - a

Which obviously doesn't make any sense. So, back to the original question: how do I flatten Tree from Data.Tree so I can write a type that is isomorphic to it without nested types?

This question isn't a duplicate of my previous question. The last one is about representing nested types with the Scott Encoding, for which the correct answer is "ignore the nesting". This one proceeds to ask how to flatten a nested type anyway (since it is needed for a particular use of the Scott Encoding, but not obligatory in general).

Answer 1

Once you got to

T a = a * (1 + T a * L (T a))

you could continue

    = a + a * T a * L (T a)   -- distribute
    = a + T a * (a * L (T a)) -- commute and reassociate
    = a + T a * T a           -- using your original definition of T backwards

so you arrive at

data Tree a = Leaf a | InsertLeftmostSubtree (Tree a) (Tree a)

I'm not sure to what extent this is an instance of a general procedure, however.

Answer 2

Before reading any of the answers, I thought this was a fun puzzle and worked out something equivalent to the accepted answer:

data Tree' a = Node a [Tree' a] deriving (Show, Eq, Ord)
data Tree a = Leaf a | Branch (Tree a) (Tree a) deriving (Show, Eq, Ord)

Beyond that, I wrote the conversion functions, in what seems like the only possible way:

convert :: Tree' a -> Tree a
convert (Node x [])     = (Leaf x)
convert (Node x (t:ts)) = Branch (convert t) $ convert (Node x ts)

convert' :: Tree a -> Tree' a
convert' (Leaf x)      = Node x []
convert' (Branch t ts) = Node x $ convert' t : subtrees
  where (Node x subtrees) = convert' ts

The implementations of these functions aren't a proof of correctness, but the fact that they typecheck, have no non-exhaustive pattern matches, and seem to work for simple inputs (ie convert . convert' == id), helps suggest that the data types are isomorphic to each other, which is encouraging.

As for the general structure of how to build such a thing, I came at it differently than the type algebra in the accepted answer, so maybe my thought process will be helpful in deriving a general method. The main thing was noticing that [x] can be converted, in the usual way, to data List a = Nil | Cons a (List a). So, we need to apply that transformation to the [Tree' a] field, while also preserving the extra a "above" the [Tree' a]. So, my Leaf a follows naturally as an equivalent to Nil but with an extra a; then the Branch constructor is analogous to Cons b (List b).

I think you can do something similar for any data constructor that contains a list: given Constructor a b [c], you convert this to two constructors in the new type:

data Converted a b c = Nil a b | Cons c (Converted a b c)

And if there are two lists in the old constructor, you can give each of them a constructor for just adding a single item to one of the lists:

data Old a b c = Old a [b] [c]

data New a b c = Done a
               | AddB b (New a b c)
               | AddC c (New a b c)