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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
