Định nghĩa chính xác của `mở ra` cho một cây không được gắn thẻ là gì?

Question

Tôi đã suy nghĩ về cách thức thực hiện tương đương với unfold cho các loại sau đây:

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

Hiện chưa rõ ràng kể từ khi chuẩn unfold cho các danh sách trả về giá trị và hạt giống tiếp theo. Đối với kiểu dữ liệu này, nó không có ý nghĩa, vì không có "giá trị" cho đến khi bạn đạt đến một nút lá. Bằng cách này, nó chỉ thực sự có ý nghĩa để trả lại hạt giống mới hoặc dừng lại với một giá trị. Tôi đang sử dụng định nghĩa này:

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) 

Trong khi điều này có vẻ hiệu quả, tôi không chắc đây là cách nó được cho là vậy. Vì vậy, đó là câu hỏi: cách chính xác để làm điều đó là gì?

Answer 1

Nếu bạn nghĩ về kiểu dữ liệu làm điểm sửa lỗi của hàm functor thì bạn có thể thấy định nghĩa của mình là khái quát hóa hợp lý của trường hợp danh sách.

module Unfold where 

Ở đây chúng ta bắt đầu bằng cách định nghĩa các fixpoint của một functor f: đó là một lớp f Tiếp theo một số fixpoint hơn:

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

Để làm cho mọi việc hơi rõ ràng hơn, sau đây là các định nghĩa của functors tương ứng với danh sách và cây cối. Về cơ bản chúng có hình dạng giống như các kiểu dữ liệu ngoại trừ việc chúng ta đã thay thế các cuộc gọi đệ quy bằng một tham số phụ. Nói cách khác, họ mô tả những gì một lớp của danh sách/cây trông giống như và là chung chung trên các cấu trúc con có thể r.

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

Lists và cây sau đó lần lượt là các fixpoints của ListF và TreeF:

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

Anyways, nhảy bây giờ bạn có một trực giác tốt hơn về kinh doanh fixpoint này, chúng ta có thể thấy rằng có một cách chung chung xác định hàm unfold cho các chức năng này.

Cho một hạt giống ban đầu cũng như một hàm lấy một hạt giống và xây dựng một lớp của f nơi cấu trúc đệ quy là hạt giống mới, chúng tôi có thể xây dựng một cấu trúc toàn bộ:

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

Định nghĩa này chuyên để bình thường unfold trong danh sách hoặc định nghĩa của bạn cho cây. Nói cách khác: định nghĩa của bạn thực sự là đúng.