Какое правильное определение `unfold` для немаркированного дерева?

Question

Я думал в том, как реализовать эквивалент unfold для следующего типа:

data Tree a = Node (Tree a) (Tree a) | Leaf a | Nil 

Это было не сразу очевидно, так как стандарт unfold для списков возвращает значение и следующее семя. Для этого типа данных это не имеет смысла, поскольку нет значения, пока вы не достигнете листового узла. Таким образом, действительно имеет смысл возвращать новые семена или останавливаться со значением. Я использую это определение:

data Drive s a = Stop | Unit a | Branch s s deriving Show 

unfold :: (t -> Drive t a) -> t -> Tree a 
unfold fn x = case fn x of 
    Branch a b -> Node (unfold fn a) (unfold fn b) 
    Unit a  -> Leaf a 
    Stop  -> Nil 

main = print $ unfold go 5 where 
    go 0 = Stop 
    go 1 = Unit 1 
    go n = Branch (n - 1) (n - 2) 

Хотя это, похоже, работает, я не уверен, что так оно и должно быть. Итак, вот в чем вопрос: какой правильный способ это сделать?

Answer 1

Если вы считаете, что тип данных является фиксированной точкой функтора, то вы можете видеть, что ваше определение является разумным обобщением списка.

module Unfold where 

Здесь мы начинаем по определению неподвижной опоры функтора f: это слой f затем еще немного фиксированной точкой:

newtype Fix f = InFix { outFix :: f (Fix f) } 

Чтобы сделать вещи немного яснее, вот определение функторов соответствующих спискам и деревьям. Они имеют в основном ту же форму, что и типы данных, за исключением того, что мы заменили рекурсивные вызовы дополнительным параметром. Другими словами, они описывают, что один слой из списка/дерева выглядит и является общим по возможным подструктурам r.

data ListF a r = LNil | LCons a r 
data TreeF a r = TNil | TLeaf a | TBranch r r 

Списки и деревья, то соответственно закрепление для предоставления ListF и TreeF:

type List a = Fix (ListF a) 
type Tree a = Fix (TreeF a) 

В любом случае, прыгая вы теперь лучше интуиция об этом Fixpoint бизнесе, мы можем видеть, что есть общий способ определения функции unfold.

Учитывая изначальное семя, а также функции, принимая семя и строительство один слой из f где рекурсивной структуры являются новые семена, мы можем построить всю структуру:

unfoldFix :: Functor f => (s -> f s) -> s -> Fix f 
unfoldFix node = go 
    where go = InFix . fmap go . node 

Это определение специализируется на обычный unfold в списке или ваше определение для деревьев. Другими словами: ваше определение действительно было правильным.