apfelmus apfelmus at quantentunnel.de
Thu Jul 19 06:51:14 EDT 2007

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