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

9
votes

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).

2
haskellfunctional-programmingalgebraic-data-types
although I think that I know what you want (and probably Reid already solved it) can you please add what you understand under a flat data-structure? (Because you don't seem to mind the recursion which I find surprising) – Random Dev
Specifically, I want it to be expressible as a sum of products with, yes, possibly, recursion on the bound variable. Ex: data Rec a = A a (Rec a) | B a a a a | C a (Rec a) a | D a, is perfectly valid. But recursion on another recursive procedure (such as the [Tree a] here) isn't OK. I want that specifically because I'm encoding Haskell datatypes on the Lambda Calculus using the Scott Encoding, which doesn't account for nested types, so I have to somehow do it without nesting. – MaiaVictor
@Viclib Tree doesn't seem problematic to me, for Scott encoding. Shouldn't this work? – András Kovács
András, not when you are trying to fold over them with normalizing terms, as you proved in another thread. For that, I had to extend the encoding with recursive calls, such that cons becomes (head tail cons nil → cons cons nil head tail) instead of (head tail cons nil → cons head tail). Using that, I'm able to derive a normalizing fold for any datatype generically by representing them as Scott :: [[Field]], where (Field :: Bool) == true if the field is recursive. That way, List is represented as [[false true] []], for example. Not sure it is the only way. Any idea? – MaiaVictor
possible duplicate of How do you represent nested types using the Scott Encoding? – amalloy

2 Answers

12
votes

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.

2
votes

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)