5 ms·
Analogies are lossy but one way to think of corecursion/recursion is that corecursion turns the seed into a maple tree and recursion eats the tree's branches an
by Dn_Ab 12y ago
Analogies are lossy but one way to think of corecursion/recursion is that corecursion turns the seed into a maple tree and recursion eats the tree's branches and spits out a table leg or something. Corecursion is generative and (structural) recursion aggregates/builds. You corecursively generate a possibly infinite stream while you recursively turn a finite list of numbers into their sum.
Other places you've probably already seen corecursiveness: Power Series in calculus, automatons in computer science and in the close cousin that is the so called map in MapReduce TM.
Programming with just (primitive but on higher order functions) recursion and corecursion is the basis of Total Functional Programming which, while not Turing complete is still very surprisingly powerful.
- oggy 12y agoWhat are the restrictions on combining primitive recursive and co-recursive functions in total functional programming? Clearly, "repeat" is primitively co-recursive, and "length" is primitively recursive, but "length . repeat" is non-terminating.
- tel 12y agolength . repeat won't type either. Briefly, recursion and corecursion have the following types cata : (f a -> a) -> mu f -> a ana : (a -> f a) -> a -> nu f where `mu` is the "least fixed point" of a base functor f and `nu` the "greatest fixed point". In non-terminal, non-strict languages `mu f == nu f`, but in total languages they don't. We call types of the form `mu f` data and types of the form `nu f` codata. Data is guaranteed to be finite while codata is not.
- oggy 12y agoThanks. Is there a way to type something like take 5 . repeat? Or more generally, how do you make use of codata in these languages?
- tel 12y agoYou think of it like a generator. Before I wrote something like ana : Step f seed -> seed -> Nu f but we might define `Nu f` using an existential to just be data Nu f = forall seed . (Step f seed, seed) and then you can write an eliminator for this type which just handles each step. So, `repeat` might look like data ListF a x = Nil | Cons a x repeat :: a -> Nu (ListF a) repeat a = Nu (\x -> Cons x x, a) and then `take` will be a parametric catamorphism on Nat which just repeatedly creates new layers and consumes them. Together these form a thing called a hylomorphism.
- dllthomas 12y agoMy understanding is that there's nothing wrong with using codata - the problem is with recursing on codata ("problem" in that you're stuck generating codata). Something like "take n" can produce data when reading codata because the recursion happens partly on data (in this case, n). I'm sure tel will let me know if I've made a misunderstood something.
- tel 12y agoThat's pretty much exactly it! The other thing to note is that the reduction semantics of codata are to... just sit there until it's consumed. If you use Haskell you get the idea that codata just expands and expands because of the behavior of the repl and laziness. Sometimes, a better intuition is that it's more like a Python generator which must be yielded explicitly (by a recursive algorithm recurring on some data).
- tel 12y agoAnother way to think about it is that only recursion "drives" computation. Corecursion sets up a potentially infinite number of computation steps each of which can be chosen to be churned through via recursion.