How the rose tree unfolds (from origami programming)
I read the article Origami Programming by Jeremy Gibbons and I am having a hard time understanding how the functions unfoldR
and unfoldF
for Rose Trees
.
In the document, the type Rose Tree
is defined as:
data Rose α = Node α (Forest α)
type Forest α = List (Rose α)
The functions unfoldR
and unfoldF
are mutually recursive and are defined as:
unfoldR :: (β → α) → (β → List β) → β → Rose α
unfoldR f g x = Node (f x) (unfoldF f g x)
unfoldF :: (β → α) → (β → List β) → β → Forest α
unfoldF f g x = mapL (unfoldR f g) (g x)
It looks like, barring a few small edge cases, these functions will return endlessly. How do these two mutually recursive functions end up?
source to share
They don't necessarily end!
The definitions unfoldR
and unfoldF
form a co-inductive function of types Rose
and, Forest
respectively. Co-induction is a double structural induction. Coinductive functions are designed to create infinite data structures that will later be consumed through a recursive function.
Because of Haskell's lazy evaluation, we can define and create an infinite mutually recursive data structure Rose
and Forest
by applying the function f :: (β → α)
and g :: (β → List β)
and an initial "seed" x :: β
for any unfoldR
and unfoldF
.
Then we would use an infinite data structure with another recursive function h :: Rose -> γ
Matching example undefined:
f :: (β → α) f = undefined g :: (β → List β) g = undefined x :: β x = undefined h :: Rose -> γ h = undefined result :: γ result = h $ unfoldR f g x
This result
will evaluate the computation over an infinite structure. But if it's an infinite data structure, how h
does it end ? How can you result
estimate?
While this unfoldR f g x
will lead to an infinite structure, h
only a finite subset of the search space will be searched and therefore result
can be estimated.
Note. We can also define f
, g
and x
to create a finite structure, it does not have to be infinite
source to share