4 ms·
I've heard Haskell programmers talk about Data and Codata, and came away with the loose sense that Data might be like state and Codata might be like a stream.
by zachrose 6y ago
I've heard Haskell programmers talk about Data and Codata, and came away with the loose sense that Data might be like state and Codata might be like a stream.
That one would so confidently assert that "Codata is the categorical dual of Data" has me thinking there might be something here?
Anyone want to tell me how far off I am?
- Tarean 6y agoData and codata are dual, but that doesn't mean they are the inverse of each other. It means we can formalize them both in category theory and they have the same formalization with reversed arrows. More usefully, data is a finite data type and codata is an infinite data type. Some example: sum = foldr (+) 0 sum [0,1,2,3] > 6 sum [0..] ...loops forever... sum' = scanl (+) 0 sum' [0,1,2,3] > [0, 1, 3, 6] sum' [0..] > [0, 1, 3, 6, 10... Haskell doesn't actually distinguish between finite and infinite data. Some functions work fine on infinite data, some functions loop forever. Induction describes how to process data without diverging - process each input element in a finite time. Co-induction describes how to process codata without diverging - produce each output element in a finite time. This is useful if you want to prove things about infinite processes like operating systems.