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

[Conor McBride]

On 16 Jul 2007, at 19:53, Stefan Holdermans wrote:

> I wrote:
>
>> I came up with [...]
>
> apfelmus' solution is of course more elegant, but I guess it boils  
> down to the same basic idea.

Yep, you need inductive data to guarantee that you eventually stop
spitting out one sort of thing and flip over to the other. Here's my
version.

Mux...

 > data{-codata-} Mux x y = Mux (Muy x y)

...is defined by mutual induction with...

 > data Muy x y = y :- Muy x y | x :~ Mux y x

...which guarantees that we will get more x, despite the odd y
in the way. It's inductively defined, so we can't (y :-) forever;
we must eventually (x :~), then flip over. So,

 > demuxL :: Mux x y -> Stream x
 > demuxL (Mux muy) =
 >   let (x, mux) = skipper muy
 >   in  x :> demuxR mux

is productive, given this helper function

 > skipper :: Muy x y -> (x, Mux y x)
 > skipper (y :- muy) = skipper muy
 > skipper (x :~ mux) = (x, mux)

which is just plain structural recursion. Once we've got out x,
we carry on with a Mux y x, flipping round the obligation to
ensure that we don't stick with x forever. To carry on getting
xs out...

 > demuxR :: Mux y x -> Stream x
 > demuxR (Mux (x :- muy)) = x :> demuxR (Mux muy)
 > demuxR (Mux (y :~ mux)) = demuxL mux

...just pass them as they come, then flip back when the y arrives.

Apfelmus, thanks for

| 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 :>)

which is a very nice way to clean up my waffly spec.

I rather like this peculiar world of mixed coinductive and inductive
definitions. I haven't really got a feel for it yet, but I'm glad I've
been introduced to its rich sources of amusement and distraction, as
well as its potential utility. (My colleague, Peter Hancock, is the
culprit; also the man with the plan. For more, google

   Peter Hancock eating streams

and poke about.)

Cheers for now

Conor