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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
