|
|
|
|
|
|
by tel
4422 days ago
|
|
|
Those are just at different levels of meaning. I don't think there's a direct relationship between stack/tail recursion and recursion/corecursion. To get a brief feel for the difference consider the "type function": T x = 1 + x
where 1 is the type with only one value and the type (X + Y) is the tagged union of types X and Y. We might decide to talk about the type "iterated T" as the type IT = T (T (T (T (T (T ...))))))
= 1 + (1 + (1 + (1 + (1 + ...))))))
If we tag "left" values with Inl and "right" values with Inr and take * to be the only value of type 1, then values of IT look like Inl *
Inr (Inl *)
Inr (Inr (Inr (Inr (Inl *))))
which looks a lot like the Peano Naturals. Now, a recursive definition on IT looks like cata : forall x . (T x -> x) -> IT -> x
and a corecursive definition looks like ana : forall x . (x -> T x) -> x -> IT
In other words, recursion occurs by constantly pulling "layers" of type T off of values of IT while corecursion occurs by adding "layers" of type T on to seed values to build an IT.We can convert IT to natural numbers by using cata cata (\tx -> case tx of { Inr * -> 0; Inl n -> 1 + n })
and we can invert that conversion with ana ana (\x -> case (x > 0) of { True -> Inl x; False -> Inr * })
and we can build the "infinite" structure omega with ana omega = ana (\x -> Inl x)
|
|
|