Come scrivere un tipo che è isomorfo su Tree senza liste annidate?

Question

In Haskell, si dice che qualsiasi ADT può essere espresso come somma di prodotti. Sto cercando di trovare un tipo piatto isomorfo a Tree, su Data.Tree.

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

Voglio scrivere una definizione funzionalmente identico per albero senza tipi nidificati:

Tree = ??? -- no nested types allowed 

Per questo, ho provato a scrivere la relazione ricorsiva per il tipo algebre:

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

inlining L, ho avuto:

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

.210

Che non stava andando da nessuna parte, così mi sono fermato e ha fatto le moltiplicazioni, lasciandomi con:

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

Quale è la stessa:

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

Quella è una somma di prodotti, ma è infinito. Non posso scriverlo in Haskell. Abusando l'algebra:

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

Risolvendo per T a, ho scoperto che:

T a = 1 - a 

che ovviamente non ha alcun senso. Quindi, tornando alla domanda iniziale: come appiattisco Tree da Data.Tree così posso scrivere un tipo che è isomorfo senza tipi annidati?

Questa domanda non è una replica di my previous question. L'ultimo riguarda la rappresentazione di tipi annidati con la codifica di Scott, per la quale la risposta corretta è "ignorare il nidificazione". Questo procede chiedendo comunque come appiattire un tipo annidato (poiché è necessario per un uso particolare di Scott Encoding, ma non obbligatorio in generale).

Answer 1

Una volta avuto modo di

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

si potrebbe continuare

= 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 

così si arriva al

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

Non sono sicuro fino a che punto questo è un esempio di un procedura generale, tuttavia.

Answer 2

Prima di leggere una qualsiasi delle risposte, ho pensato che questo fosse un puzzle divertente e lavorato fuori qualcosa di equivalente alla risposta accettata:

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) 

di là di questo, ho scritto le funzioni di conversione, in quello che sembra l'unico possibile modo:

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 

le implementazioni di queste funzioni non sono una prova di correttezza, ma il fatto che essi TYPECHECK, hanno nessun modello non esaustivo corrisponde, e sembra funzionare per ingressi semplici (cioè convert . convert' == id), aiuta a suggerire che i dati t le forme sono isomorfe l'una con l'altra, il che è incoraggiante.

Per quanto riguarda la struttura generale di come costruire una cosa del genere, mi è venuto in modo diverso rispetto all'algebra di tipo nella risposta accettata, quindi forse il mio processo di pensiero sarà utile nel derivare un metodo generale. La cosa principale era notare che [x] può essere convertito, nel solito modo, a data List a = Nil | Cons a (List a). Pertanto, è necessario applicare tale trasformazione al campo [Tree' a], preservando anche l'ulteriore a "sopra" dello [Tree' a]. Quindi, il mio Leaf a segue naturalmente come equivalente a Nil ma con un extra a; quindi il costruttore Branch è analogo a Cons b (List b).

Penso che si possa fare qualcosa di simile per qualsiasi costruttore di dati che contiene un elenco: data Constructor a b [c], si converte questo per due costruttori nel nuovo tipo:

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

e se ci sono due liste nel vecchio costruttore, si può dare a ciascuno di loro un costruttore per solo l'aggiunta di un singolo elemento per una delle liste:

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)