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