[Haskell-cafe] Re: Clearly, Haskell is ill-founded

[apfelmus]

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