Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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)


Wow, thank you so much for your answer. it definitely helped me understand better!




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: