Could you elaborate or provide links to examples of what you mean by solving this with codata?
I'm personally a big fan of existential types, but they usually don't need to be explicit. One place that shows up on Hackage that's worth studying is Edward Kmett's `folds` library. The type, Data.Fold.L.L is a codata type
data L = forall r . L (r -> b) (r -> a -> r) r
It uses existential typing for efficiency, but doesn't need to. Instead, it just helps to show the encapsulation going on here---you literally cannot examine `r` in any way besides applying some of the bundled functions (methods, destructors).The existential type highlights that L is acting as codata, but it's usually not recommended in practice as existential types are a little hard to manage. You could write L more simply and eliminate the `r` data
data L = L b (a -> L)
by just pre-applying the existentially typed data to each of its destructors and rebundling new L types where necessary.In any case, the point is that it's easy to build a variety of L variants, but hard to extend new operations on Ls.
sum :: Num a => L a a
sum = L id (+) 0
prod :: Num a => L a a
prod = L id (*) 1
list :: L a [a]
list = id (\r a -> a : r) []