[Haskell-cafe] Mux, was Re: Clearly, Haskell is ill-founded

[Conor McBride]

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