Conor McBride wrote: > Derek Elkins wrote: >> 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.
I too thought that the Mu fixed point should be empty since it's missing a base case. But that's not correct: Mu muy . /\ x y. Either (y, muy x y) (x, mux y x) ~ Mu muy . /\ y . Either (y, muy y) (Constant1, Constant2 y) ~ Mu muy . Either (Constant3 , muy) Constant4 The result is just a list of Constant3s that ends with a Constant4 instead of []. In other words, Constant4 = (x, mux y x) is the base case for the induction. Very cunning! > 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. Can the order of quantifiers be deduced from the declarations? codata Mux x y = Mux (Muy x y) data Muy x y = y :- Muy x y | x :~ Mux y x Probably, since Xum would be declared as data Yum x y = Yum (Xum x y) codata Xum x y = y :- Yum x y | x :~ Xum y x Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe