3 ms·
For codata vs data, this post worked for me: http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html Roughly, d
by noelwelsh 12y ago
For codata vs data, this post worked for me: http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html
Roughly, data is of finite size, and codata is of infinite size. Consider a (normal finite) list vs an infinite lazy list.
The standard pattern for working with data is to break it into smaller pieces, using pattern matching, till you hit a base case. In Scheme (hopefully close enough to CL you can read it; and not using pattern matching, but whateva) you write stuff like
(define (foldr f zero lst)
(cond lst
[(null? lst) zero]
[else (f (car lst) (foldr f zero (cdr lst)))]))
We break lst into smaller pieces till we hit the base case of the empty list. Classic stuff and everyone knows it.
Now what about codata? You can't break down infinite data till you hit a base case, because there is no base case. It's infinite! So you apply the Fundamental Theorem of Pretending You Understand Category Theory, and prepend co- to all technical terms in the description for data.
So if data is processed using pattern matching and recursion, then codata is processed using copattern matching and corecursion.
By a strange quirk of fate this actually makes sense. You can read more about corecursion (aka coinduction) on your local Internet, and I guess copatterns, as described in the post, are the next piece of the puzzle.
There is a slight analogy with setf but it doesn't go very far.
HTH.
- sqrt17 12y agodata and co-data are kind of like the -X and +X modalities in Prolog programs. Most of the time, it doesn't matter which one you use, but sometimes you need to write it backwards. Seeing the paper at http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf http://www.jucs.org/jucs_10_7/total_functional_programming/j... it's more related to proofs, and indeed Idris seems somewhat similar to Coq (a "programming" language for writing proofs). Or maybe I'm just totally lost.
- Ixiaus 12y agoIdris is dependently typed but I think it actually looks more like Agda and Haskell...
- klibertp 12y ago> In Scheme (hopefully close enough to CL Actually, I know Scheme much better than CL, so no problem here :) > So you apply the Fundamental Theorem of Pretending You Understand Category Theory, and prepend co- to all technical terms in the description for data. That, however, is a bit of a problem... > There is a slight analogy with setf but it doesn't go very far. Yup, that's what I had in mind; it really looks similar to setf on the surface. That it's something completely different inside should be obvious from it being Idris, category theory, dependent co-typing and co-everything else I don't understand at all :) Thanks for the link, I love the blog, will need to read this post.
- dllthomas 12y ago"So you apply the Fundamental Theorem of Pretending You Understand Category Theory, and prepend co- to all technical terms in the description for data." Very nice.