Hi Derek On 17 Jul 2007, at 17:42, Derek Elkins wrote:
On Tue, 2007-07-17 at 13:23 +0100, Conor McBride wrote:
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
As an inductive data type, isn't this empty?
Not in the manner which I intended. But it's a good question whether what I wrote unambiguously represented what I intended. In full-on nuspeak, I meant Mux = Nu mux. Mu muy. /\x y. Either (y, muy x y) (x, mux y x) with the inductive definition nested inside the coinductive one, so that we always eventually twist. Just once a summer, perhaps. I've basically written Stefan's version, exploiting fixpoints at kind * -> * -> * to deliver the symmetry by the twisted :~ constructor. As Apfelmus made rather more explicit, we have a coinductive sequence of (nonempty inductive sequences which end with a twist). I was hoping to signify this nesting by defining Mux to pack Muy, but I'm not sure that's a clear way to achieve the effect. With the Nu-Mu interpretation, the fair multiplexer is a coprogram: mux :: Stream x -> Stream y -> Mux x y mux (x :> xs) (y :> ys) = Mux (x :~ Mux (y :~ mux xs ys)) Nesting the other way around, we get this rather odd beast Xum = Mu muy. Nu mux. /\x y. Either (y, muy x y) (x, mux y x) which isn't empty either. Rather, it only allows finitely many uses of :- before it settles down to use :~ forever. That is, we eventually always twist. So this way round allows the fair multiplexer, but not the slightly biased one which produces two xs for every y. All of which goes to show that mixed co/programming is quite a sensitive business, and it's easy to be too casual with notation. All the best Conor