Conor McBride wrote:
To that end, an exercise. Implement a codata type
data{-codata-} Mux x y = ...
which intersperses x's and y's in such a way that
(1) an initial segment of a Mux does not determine whether the next element is an x or a y (ie, no forced *pattern* of alternation)
(2) there are productive coprograms
demuxL :: Mux x y -> Stream x demuxR :: Mux x y -> Stream y
(ie, alternation is none the less forced)
You may need to introduce some (inductive) data to achieve this. If you always think "always", then you need codata, but if you eventually think "eventually", you need data.
------------- Spoiler warning: significant λs follow ------------- A very interesting exercise! Here's a solution: -- lists with at least one element data List1 x = One x | Cons x (List1 x) append :: List1 x -> Stream x -> Stream x append (One x) ys = x :> ys append (Cons x xs) ys = x :> prepend xs ys -- stream of alternating runs of xs and ys codata Mix x y = Stream (List1 x, List1 y) demixL ((xs,ys) :> xys) = xs `append` demixL xys demixR ((xs,ys) :> xys) = ys `append` demixR xys -- remove x-bias codata Mux x y = Either (Mix x y) (Mix y x) demuxL (Left xys) = demixL xys demuxL (Right yxs) = demixR yxs demuxR (Left xys) = demixR xys demuxR (Right yxs) = demixL yxs A non-solution would simply be the pair (Stream x, Stream y), but this doesn't capture the order in which xs and ys interleave. I think this can be formalized with the obvious operations consL :: x -> Mux x y -> Mux x y consR :: y -> Mux x y -> Mux x y by requiring that they don't commute consL x . consR y ≠ consR y . consL x Or rather, one should require that the observation observe :: Mux x y -> Stream (Either x y) respects consL and consR: observe . consL x = (Left x :>) observe . consR y = (Right y :>) Regards, apfelmus