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