3 ms·

Thanks. 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 ago
  You 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 ago
  My 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 ago
    That'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 ago
    Another 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.