Data 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 sam

Data 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.