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

[apfelmus]

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