apfelmus apfelmus at quantentunnel.de
Mon Jul 16 11:54:08 EDT 2007

```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

```