Conor's exercise:
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.
I came up with: data Stream a = ConsS a (Stream a) -- CODATA data Mux a b = Mux (L a b) (R a b) (Mux a b) -- CODATA data L a b = LL a | LR b (L a b) data R a b = RL a (R a b) | RR b lastL :: L a b -> a lastL (LL x) = x lastL (LR y l) = lastL l initL :: L a b -> Stream b -> Stream b initL (LL x) = id initL (LR y l) = ConsS y . initL l lastR :: R a b -> b lastR (RL x r) = lastR r lastR (RR y) = y initR :: R a b -> Stream a -> Stream a initR (RL x r) = ConsS x . initR r initR (RR y) = id demuxL :: Mux a b -> Stream a demuxL (Mux l r m) = ConsS (lastL l) (initR r (demuxL m)) demuxR :: Mux a b -> Stream b demuxR (Mux l r m) = initL l (ConsS (lastR r) (demuxR m)) Cheers, Stefan